Merge pull request #1312 from goblint/issue-1192

Small output readability improvements
goblint · Feb 26, 2024 · c5b3a4f · c5b3a4f
2 parents f2f5cc1 + f4d5a45
commit c5b3a4f
Show file tree

Hide file tree

Showing 31 changed files with 560 additions and 106 deletions.
diff --git a/src/analyses/mHPAnalysis.ml b/src/analyses/mHPAnalysis.ml
@@ -12,7 +12,10 @@ struct
     include MHP
     let name () = "mhp"
     let may_race = MHP.may_happen_in_parallel
-    let should_print _ = true
+    let should_print {tid; created; must_joined} =
+      GobConfig.get_bool "dbg.full-output" ||
+      (not (ConcDomain.ThreadSet.is_empty created) ||
+       not (ConcDomain.ThreadSet.is_empty must_joined))
   end
 
   let access ctx _: MHP.t = MHP.current (Analyses.ask_of_ctx ctx)

diff --git a/src/analyses/wrapperFunctionAnalysis.ml b/src/analyses/wrapperFunctionAnalysis.ml
@@ -131,8 +131,19 @@ module MallocWrapper : MCPSpec = struct
       CilType.Location.show loc
 
     let name_varinfo (t, node, c) =
-      Format.asprintf "(alloc@sid:%s@tid:%s(#%s))" (Node.show_id node) (ThreadLifted.show t) (UniqueCount.show c)
-
+        let uniq_count =
+          if not (GobConfig.get_bool "dbg.full-output") && UniqueCount.is_top c then
+            Format.dprintf ""
+          else
+            Format.dprintf "(#%s)" (UniqueCount.show c)
+        in
+        let tid =
+          if not (GobConfig.get_bool "dbg.full-output") && ThreadLifted.is_top t then
+            Format.dprintf ""
+          else
+            Format.dprintf "@tid:%s%t" (ThreadLifted.show t) uniq_count
+        in
+        Format.asprintf "(alloc@sid:%s%t)" (Node.show_id node) tid
   end
 
   module NodeVarinfoMap = RichVarinfo.BiVarinfoMap.Make(ThreadNode)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
@@ -313,10 +313,22 @@ struct
   let widen = lift2 I.widen
   let narrow = lift2 I.narrow
 
-  let show x = I.show x.v  (* TODO add ikind to output *)
-  let pretty () x = I.pretty () x.v (* TODO add ikind to output *)
+  let show x =
+    if not (GobConfig.get_bool "dbg.full-output") && I.is_top_of x.ikind x.v then
+      "⊤"
+    else
+      I.show x.v  (* TODO add ikind to output *)
+  let pretty () x =
+    if not (GobConfig.get_bool "dbg.full-output") && I.is_top_of x.ikind x.v then
+      Pretty.text "⊤"
+    else
+      I.pretty () x.v (* TODO add ikind to output *)
   let pretty_diff () (x, y) = I.pretty_diff () (x.v, y.v) (* TODO check ikinds, add them to output *)
-  let printXml o x = I.printXml o x.v (* TODO add ikind to output *)
+  let printXml o x =
+    if not (GobConfig.get_bool "dbg.full-output") && I.is_top_of x.ikind x.v then
+      BatPrintf.fprintf o "<value>\n<data>\n⊤\n</data>\n</value>\n"
+    else
+      I.printXml o x.v (* TODO add ikind to output *)
   (* This is for debugging *)
   let name () = "IntDomLifter(" ^ (I.name ()) ^ ")"
   let to_yojson x = I.to_yojson x.v
@@ -3477,9 +3489,27 @@ module IntDomTupleImpl = struct
     in
     mapp2 { fp2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.to_incl_list } x |> flat merge
 
+  let same show x = let xs = to_list_some x in let us = List.unique xs in let n = List.length us in
+    if n = 1 then Some (List.hd xs)
+    else (
+      if n>1 then Messages.info ~category:Unsound "Inconsistent state! %a" (Pretty.docList ~sep:(Pretty.text ",") (Pretty.text % show)) us; (* do not want to abort *)
+      None
+    )
+  let to_int = same Z.to_string % mapp2 { fp2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.to_int }
 
-  let pretty () = (fun xs -> text "(" ++ (try List.reduce (fun a b -> a ++ text "," ++ b) xs with Invalid_argument _ -> nil) ++ text ")") % to_list % mapp { fp = fun (type a) (module I:SOverflow with type t = a) -> (* assert sf==I.short; *) I.pretty () } (* NOTE: the version above does something else. also, we ignore the sf-argument here. *)
-
+  let pretty () x =
+    match to_int x with
+    | Some v when not (GobConfig.get_bool "dbg.full-output") -> Pretty.text (Z.to_string v)
+    | _ ->
+      mapp { fp = fun (type a) (module I:SOverflow with type t = a) -> (* assert sf==I.short; *) I.pretty () } x
+      |> to_list
+      |> (fun xs ->
+          text "(" ++ (
+            try
+              List.reduce (fun a b -> a ++ text "," ++ b) xs
+            with Invalid_argument _ ->
+              nil)
+          ++ text ")") (* NOTE: the version above does something else. also, we ignore the sf-argument here. *)
 
   let refine_functions ik : (t -> t) list =
     let maybe reffun ik domtup dom =
@@ -3575,20 +3605,17 @@ module IntDomTupleImpl = struct
     if List.mem `Eq xs then `Eq else
     if List.mem `Neq xs then `Neq else
       `Top
-  let same show x =
-    let us = List.unique (to_list_some x) in
-    match us with
-    | [x] -> Some x
-    | [] -> None
-    | _ ->
-      Messages.info ~category:Unsound "Inconsistent state! %a" (Pretty.docList ~sep:(Pretty.text ",") (Pretty.text % show)) us; (* do not want to abort *)
-      None
-  let to_int = same Z.to_string % mapp2 { fp2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.to_int }
+
   let to_bool = same string_of_bool % mapp { fp = fun (type a) (module I:SOverflow with type t = a) -> I.to_bool }
   let minimal = flat (List.max ~cmp:Z.compare) % mapp2 { fp2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.minimal }
   let maximal = flat (List.min ~cmp:Z.compare) % mapp2 { fp2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.maximal }
   (* others *)
-  let show = String.concat "; " % to_list % mapp { fp = fun (type a) (module I:SOverflow with type t = a) x -> I.name () ^ ":" ^ (I.show x) }
+  let show x =
+    match to_int x with
+    | Some v  when not (GobConfig.get_bool "dbg.full-output") -> Z.to_string v
+    | _ -> mapp { fp = fun (type a) (module I:SOverflow with type t = a) x -> I.name () ^ ":" ^ (I.show x) } x
+              |> to_list
+              |> String.concat "; "
   let to_yojson = [%to_yojson: Yojson.Safe.t list] % to_list % mapp { fp = fun (type a) (module I:SOverflow with type t = a) x -> I.to_yojson x }
   let hash = List.fold_left (lxor) 0 % to_list % mapp { fp = fun (type a) (module I:SOverflow with type t = a) -> I.hash }
 
@@ -3698,7 +3725,10 @@ module IntDomTupleImpl = struct
 
   (* printing boilerplate *)
   let pretty_diff () (x,y) = dprintf "%a instead of %a" pretty x pretty y
-  let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (show x)
+  let printXml f x =
+    match to_int x with
+    | Some v when not (GobConfig.get_bool "dbg.full-output") -> BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (Z.to_string v)
+    | _ -> BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (show x)
 
   let invariant_ikind e ik x =
     match to_int x with

diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml
@@ -55,19 +55,23 @@ struct
             (struct let name = "no index" end)))
         (struct let name = "no node" end))
 
-  let show = function
-    | (f, Some (n, i)) ->
-      f.vname
-      ^ "@" ^ (CilType.Location.show (UpdateCil.getLoc n))
-      ^ "#" ^ Option.fold ~none:"top" ~some:string_of_int i
-    | (f, None) -> f.vname
+  let show (f, ni_opt) = 
+    let vname = f.vname in
+    match ni_opt with
+    | None -> vname
+    | Some (n, i_opt) ->
+      let vname_loc = vname ^ "@" ^ CilType.Location.show (UpdateCil.getLoc n) in
+      match i_opt with
+      | Some i -> vname_loc ^ "#" ^ string_of_int i
+      | None when GobConfig.get_bool "dbg.full-output" -> vname_loc ^ "#⊤"
+      | None -> vname_loc
 
   include Printable.SimpleShow (
     struct
       type nonrec t = t
       let show = show
     end
-  )
+    )
 
   let threadinit v ~multiple: t = (v, None)
 
@@ -128,9 +132,9 @@ struct
       include S
       let name () = "created (once)"
     end) (struct
-    include S
-    let name () = "created (multiple times)"
-  end)
+      include S
+      let name () = "created (multiple times)"
+    end)
 
 
   let is_unique (_, s) =

diff --git a/src/cdomains/mHP.ml b/src/cdomains/mHP.ml
@@ -24,7 +24,12 @@ let current (ask:Queries.ask) =
   }
 
 let pretty () {tid; created; must_joined} =
-  let tid_doc = Some (Pretty.dprintf "tid=%a" ThreadIdDomain.ThreadLifted.pretty tid) in
+  let tid_doc = 
+    if GobConfig.get_bool "dbg.full-output" then
+      Some (Pretty.dprintf "tid=%a" ThreadIdDomain.ThreadLifted.pretty tid)
+    else
+      None
+  in
   (* avoid useless empty sets in race output *)
   let created_doc =
     if ConcDomain.ThreadSet.is_empty created then

diff --git a/src/config/options.schema.json b/src/config/options.schema.json
@@ -2038,6 +2038,12 @@
             "Should the analysis call Check.checkFile after creating the CFG (helpful to verify that transformations respect CIL's invariants.",
           "type": "boolean",
           "default": false
+        },
+        "full-output": {
+          "title": "dbg.full-output",
+          "description": "Output abstract values, etc. with full internal details, without readability-oriented simplifications.",
+          "type": "boolean",
+          "default": false
         }
       },
       "additionalProperties": false

diff --git a/tests/regression/02-base/87-casts-dep-on-param.t b/tests/regression/02-base/87-casts-dep-on-param.t
@@ -0,0 +1,24 @@
+  $ goblint --set ana.activated "['base', 'mallocWrapper']" --set ana.ctx_insens[+] 'base' --set ana.ctx_insens[+] 'mallocWrapper' --set ana.base.privatization none --enable warn.debug 87-casts-dep-on-param.c 2>&1 | sed -r 's/sid:[0-9]+/sid:$SID/' | tee default-output.txt
+  [Warning] Without thread escape analysis, every local variable whose address is taken is considered escaped, i.e., global!
+  [Info][Unsound] Unknown address in {&i} has escaped. (87-casts-dep-on-param.c:11:3-11:11)
+  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (87-casts-dep-on-param.c:11:3-11:11)
+  [Debug][Analyzer] Base EvalInt i query answering bot instead of {?, NULL, &(alloc@sid:$SID)} (87-casts-dep-on-param.c:13:7-13:15)
+  [Debug][Analyzer] Base EvalInt i query answering bot instead of {?, NULL, &(alloc@sid:$SID)} (87-casts-dep-on-param.c:14:3-14:11)
+  [Info][Unsound] Unknown address in {&p} has escaped. (87-casts-dep-on-param.c:17:7-17:19)
+  [Info][Unsound] Unknown address in {&i} has escaped. (87-casts-dep-on-param.c:17:7-17:19)
+  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (87-casts-dep-on-param.c:17:7-17:19)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 15
+    dead: 0
+    total lines: 15
+
+  $ goblint --set ana.activated "['base', 'mallocWrapper']" --set ana.ctx_insens[+] 'base' --set ana.ctx_insens[+] 'mallocWrapper' --set ana.base.privatization none --enable warn.debug --enable dbg.full-output 87-casts-dep-on-param.c 2>&1 | sed -r 's/sid:[0-9]+/sid:$SID/' > full-output.txt
+
+  $ diff default-output.txt full-output.txt
+  4,5c4,5
+  < [Debug][Analyzer] Base EvalInt i query answering bot instead of {?, NULL, &(alloc@sid:$SID)} (87-casts-dep-on-param.c:13:7-13:15)
+  < [Debug][Analyzer] Base EvalInt i query answering bot instead of {?, NULL, &(alloc@sid:$SID)} (87-casts-dep-on-param.c:14:3-14:11)
+  ---
+  > [Debug][Analyzer] Base EvalInt i query answering bot instead of {?, NULL, &(alloc@sid:$SID@tid:Top Threads(#top))} (87-casts-dep-on-param.c:13:7-13:15)
+  > [Debug][Analyzer] Base EvalInt i query answering bot instead of {?, NULL, &(alloc@sid:$SID@tid:Top Threads(#top))} (87-casts-dep-on-param.c:14:3-14:11)
+  [1]
diff --git a/tests/regression/02-base/dune b/tests/regression/02-base/dune
@@ -0,0 +1,2 @@
+(cram
+ (deps (glob_files *.c)))
diff --git a/tests/regression/04-mutex/01-simple_rc.t b/tests/regression/04-mutex/01-simple_rc.t
@@ -1,9 +1,9 @@
-  $ goblint --enable warn.deterministic 01-simple_rc.c
+  $ goblint --enable warn.deterministic 01-simple_rc.c 2>&1 | tee default-output.txt
   [Warning][Race] Memory location myglobal (race with conf. 110): (01-simple_rc.c:4:5-4:13)
-    write with [mhp:{tid=[main, t_fun@01-simple_rc.c:17:3-17:40#top]}, lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40#top]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
-    write with [mhp:{tid=[main]; created={[main, t_fun@01-simple_rc.c:17:3-17:40#top]}}, lock:{mutex2}, thread:[main]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
-    read with [mhp:{tid=[main, t_fun@01-simple_rc.c:17:3-17:40#top]}, lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40#top]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
-    read with [mhp:{tid=[main]; created={[main, t_fun@01-simple_rc.c:17:3-17:40#top]}}, lock:{mutex2}, thread:[main]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
+    write with [lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
+    write with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, thread:[main]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
+    read with [lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
+    read with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, thread:[main]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
   [Info][Race] Memory locations race summary:
     safe: 0
     vulnerable: 0
@@ -13,3 +13,18 @@
     live: 12
     dead: 0
     total lines: 12
+
+  $ goblint --enable warn.deterministic --enable dbg.full-output 01-simple_rc.c > full-output.txt 2>&1
+
+  $ diff default-output.txt full-output.txt
+  2,5c2,5
+  <   write with [lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
+  <   write with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, thread:[main]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
+  <   read with [lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
+  <   read with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, thread:[main]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
+  ---
+  >   write with [mhp:{tid=[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]}, lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
+  >   write with [mhp:{tid=[main]; created={[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]}}, lock:{mutex2}, thread:[main]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
+  >   read with [mhp:{tid=[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]}, lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
+  >   read with [mhp:{tid=[main]; created={[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]}}, lock:{mutex2}, thread:[main]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
+  [1]