Merge pull request #1294 from goblint/printable-expand

Improve readability of global invariants

Author: sim642

src/analyses/base.ml

@@ -54,7 +54,7 @@ struct
 
   module G =
   struct
-    include Lattice.Lift2 (Priv.G) (VD) (Printable.DefaultNames)
+    include Lattice.Lift2Conf (struct include Printable.DefaultConf let expand1 = false let expand2 = false end) (Priv.G) (VD)
 
     let priv = function
       | `Bot -> Priv.G.bot ()

src/analyses/basePriv.ml

@@ -544,7 +544,7 @@ struct
       )
     )
     else (
-      if ConcDomain.ThreadSet.is_top tids then 
+      if ConcDomain.ThreadSet.is_top tids then
         st
       else
         match ConcDomain.ThreadSet.elements tids with
@@ -660,21 +660,11 @@ struct
   struct
     include VarinfoV (* [g]' *)
     let name () = "unprotected"
-    let show x = show x ^ ":unprotected" (* distinguishable variant names for html *)
-    include Printable.SimpleShow (struct
-        type nonrec t = t
-        let show = show
-      end)
   end
   module VProt =
   struct
     include VarinfoV (* [g] *)
     let name () = "protected"
-    let show x = show x ^ ":protected" (* distinguishable variant names for html *)
-    include Printable.SimpleShow (struct
-        type nonrec t = t
-        let show = show
-      end)
   end
   module V =
   struct
@@ -809,7 +799,7 @@ struct
   struct
     (* weak: G -> (2^M -> WeakRange) *)
     (* sync: M -> (2^M -> SyncRange) *)
-    include Lattice.Lift2 (GWeak) (GSync) (Printable.DefaultNames)
+    include Lattice.Lift2Conf (struct include Printable.DefaultConf let expand1 = false let expand2 = false end) (GWeak) (GSync)
 
     let weak = function
       | `Bot -> GWeak.bot ()

src/analyses/commonPriv.ml

@@ -74,18 +74,16 @@ struct
   struct
     include LockDomain.Addr
     let name () = "mutex"
-    let show x = show x ^ ":mutex" (* distinguishable variant names for html *)
   end
   module VMutexInits = Printable.UnitConf (struct let name = "MUTEX_INITS" end)
   module VGlobal =
   struct
     include VarinfoV
     let name () = "global"
-    let show x = show x ^ ":global" (* distinguishable variant names for html *)
   end
   module V =
   struct
-    include Printable.Either3 (VMutex) (VMutexInits) (VGlobal)
+    include Printable.Either3Conf (struct include Printable.DefaultConf let expand2 = false end) (VMutex) (VMutexInits) (VGlobal)
     let name () = "MutexGlobals"
     let mutex x: t = `Left x
     let mutex_inits: t = `Middle ()
@@ -173,7 +171,7 @@ struct
 
   module V =
   struct
-    include Printable.Either (MutexGlobals.V) (TID)
+    include Printable.EitherConf (struct let expand1 = false let expand2 = true end) (MutexGlobals.V) (TID)
     let mutex x = `Left (MutexGlobals.V.mutex x)
     let mutex_inits = `Left MutexGlobals.V.mutex_inits
     let global x = `Left (MutexGlobals.V.global x)
@@ -200,7 +198,7 @@ struct
 
   module G =
   struct
-    include Lattice.Lift2 (GMutex) (GThread) (Printable.DefaultNames)
+    include Lattice.Lift2Conf (struct include Printable.DefaultConf let expand1 = false let expand2 = false end) (GMutex) (GThread)
 
     let mutex = function
       | `Bot -> GMutex.bot ()

src/analyses/loopTermination.ml

@@ -19,7 +19,7 @@ let check_bounded ctx varinfo =
 (** We want to record termination information of loops and use the loop
  * statements for that. We use this lifting because we need to have a
  * lattice. *)
-module Statements = Lattice.Flat (CilType.Stmt) (Printable.DefaultNames)
+module Statements = Lattice.Flat (CilType.Stmt)
 
 (** The termination analysis considering loops and gotos *)
 module Spec : Analyses.MCPSpec =

src/analyses/mCPRegistry.ml

@@ -426,7 +426,7 @@ end
 
 module DomVariantLattice (DLSpec : DomainListLatticeSpec) =
 struct
-  include Lattice.Lift (DomVariantLattice0 (DLSpec)) (Printable.DefaultNames)
+  include Lattice.LiftConf (struct include Printable.DefaultConf let expand1 = false end) (DomVariantLattice0 (DLSpec))
   let name () = "MCP.G"
 end
 

src/analyses/mutexAnalysis.ml

@@ -132,7 +132,7 @@ struct
 
     module G =
     struct
-      include Lattice.Lift2 (GProtecting) (GProtected) (Printable.DefaultNames)
+      include Lattice.Lift2Conf (struct include Printable.DefaultConf let expand1 = false let expand2 = false end) (GProtecting) (GProtected)
 
       let protecting = function
         | `Bot -> GProtecting.bot ()

src/analyses/raceAnalysis.ml

@@ -194,7 +194,7 @@ struct
 
   module G =
   struct
-    include Lattice.Lift2 (OffsetTrie) (MemoSet) (Printable.DefaultNames)
+    include Lattice.Lift2Conf (struct include Printable.DefaultConf let expand1 = false let expand2 = false end) (OffsetTrie) (MemoSet)
 
     let access = function
       | `Bot -> OffsetTrie.bot ()

src/analyses/symbLocks.ml

@@ -106,20 +106,20 @@ struct
 
   module A =
   struct
-    module E = struct
-      include Printable.Either (CilType.Offset) (ILock)
-
-      let pretty () = function
-        | `Left o -> Pretty.dprintf "p-lock:%a" (d_offset (text "*")) o
-        | `Right addr -> Pretty.dprintf "i-lock:%a" ILock.pretty addr
+    module PLock =
+    struct
+      include CilType.Offset
+      let name () = "p-lock"
 
+      let pretty = d_offset (text "*")
       include Printable.SimplePretty (
         struct
           type nonrec t = t
           let pretty = pretty
         end
         )
     end
+    module E = Printable.Either (PLock) (ILock)
     include SetDomain.Make (E)
 
     let name () = "symblock"

src/analyses/threadId.ml

@@ -31,7 +31,7 @@ struct
 
   module N =
   struct
-    include Lattice.Flat (VNI) (struct let bot_name = "unknown node" let top_name = "unknown node" end)
+    include Lattice.FlatConf (struct include Printable.DefaultConf let bot_name = "unknown node" let top_name = "unknown node" end) (VNI)
     let name () = "wrapper call"
   end
   module TD = Thread.D

src/analyses/tutorials/signs.ml

@@ -36,7 +36,7 @@ end
  * We then lift the above operations to the lattice. *)
 module SL =
 struct
-  include Lattice.Flat (Signs) (Printable.DefaultNames)
+  include Lattice.Flat (Signs)
   let of_int i = `Lifted (Signs.of_int i)
 
   let lt x y = match x, y with