Improve printing of global constraint variable names

goblint · Feb 2, 2023 · d697cec · d697cec
1 parent 361a349
commit d697cec
Show file tree

Hide file tree

Showing 6 changed files with 13 additions and 9 deletions.
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -45,7 +45,7 @@ struct
 
   module V =
   struct
-    include Printable.Either (Priv.V) (ThreadIdDomain.Thread)
+    include Printable.Either (struct include Priv.V let name () = "priv" end) (struct include ThreadIdDomain.Thread let name () = "threadreturn" end)
     let priv x = `Left x
     let thread x = `Right x
     include StdV

diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
@@ -85,6 +85,7 @@ struct
   struct
     (* TODO: Either3? *)
     include Printable.Either (Printable.Either (VMutex) (VMutexInits)) (VGlobal)
+    let name () = "MutexGlobals"
     let mutex x: t = `Left (`Left x)
     let mutex_inits: t = `Left (`Right ())
     let global x: t = `Right x

diff --git a/src/analyses/mCPRegistry.ml b/src/analyses/mCPRegistry.ml
@@ -197,7 +197,8 @@ struct
     f n (assoc_dom n) d
 
   let pretty () = unop_map (fun n (module S: Printable.S) x ->
-      Pretty.dprintf "%s:%a" (S.name ()) S.pretty (obj x)
+      let analysis_name = find_spec_name n in
+      Pretty.dprintf "%s:%a" analysis_name S.pretty (obj x)
     )
 
   let show = unop_map (fun n (module S: Printable.S) x ->
@@ -257,6 +258,7 @@ struct
   open Obj
 
   include DomVariantPrintable (PrintableOfSysVarSpec (DLSpec))
+  let name () = "MCP.V"
 
   let unop_map f ((n, d):t) =
     f n (assoc_dom n) d

diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
@@ -25,7 +25,7 @@ struct
 
     module V =
     struct
-      include Printable.Either (CilType.Varinfo) (ValueDomain.Addr)
+      include Printable.Either (struct include CilType.Varinfo let name () = "protecting" end) (struct include ValueDomain.Addr let name () = "protected" end)
       let name () = "mutex"
       let protecting x = `Left x
       let protected x = `Right x

diff --git a/src/domains/printable.ml b/src/domains/printable.ml
@@ -255,13 +255,13 @@ struct
 
   let pretty () (state:t) =
     match state with
-    | `Left n ->  Base1.pretty () n
-    | `Right n ->  Base2.pretty () n
+    | `Left n -> Pretty.dprintf "%s:%a" (Base1.name ()) Base1.pretty n
+    | `Right n -> Pretty.dprintf "%s:%a" (Base2.name ()) Base2.pretty n
 
   let show state =
     match state with
-    | `Left n ->  Base1.show n
-    | `Right n ->  Base2.show n
+    | `Left n -> (Base1.name ()) ^ ":" ^ Base1.show n
+    | `Right n -> (Base2.name ()) ^ ":" ^ Base2.show n
 
   let name () = "either " ^ Base1.name () ^ " or " ^ Base2.name ()
   let printXml f = function

diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
@@ -450,8 +450,8 @@ struct
     | `G x -> `G (GV.relift x)
 
   let pretty_trace () = function
-    | `L a -> LV.pretty_trace () a
-    | `G a -> GV.pretty_trace () a
+    | `L a -> Pretty.dprintf "L:%a" LV.pretty_trace a
+    | `G a -> Pretty.dprintf "G:%a" GV.pretty_trace a
 
   let printXml f = function
     | `L a -> LV.printXml f a
@@ -1213,6 +1213,7 @@ struct
   module V =
   struct
     include Printable.Either (S.V) (Node)
+    let name () = "DeadBranch"
     let s x = `Left x
     let node x = `Right x
     let is_write_only = function