Merge pull request #1294 from goblint/printable-expand

Improve readability of global invariants

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

src/analyses/wrapperFunctionAnalysis0.ml

@@ -36,7 +36,8 @@ module ThreadCreateUniqueCount =
   MakeUniqueCount (val unique_count_args_from_config "ana.thread.unique_thread_id_count")
 
 (* since the query also references NodeFlatLattice, it also needs to reside here *)
-module NodeFlatLattice = Lattice.Flat (Node) (struct
+module NodeFlatLattice = Lattice.FlatConf (struct
+    include Printable.DefaultConf
     let top_name = "Unknown node"
     let bot_name = "Unreachable node"
-  end)
+  end) (Node)

src/cdomains/intDomain.ml

@@ -1713,10 +1713,11 @@ end
 module Flat (Base: IkindUnawareS) = (* identical to Lift, but goes to `Top/`Bot if Base raises Unknown/Error *)
 struct
   type int_t = Base.int_t
-  include Lattice.Flat (Base) (struct
+  include Lattice.FlatConf (struct
+      include Printable.DefaultConf
       let top_name = "Unknown int"
       let bot_name = "Error int"
-    end)
+    end) (Base)
 
   let top_of ik = top ()
   let bot_of ik = bot ()
@@ -1792,10 +1793,11 @@ end
 
 module Lift (Base: IkindUnawareS) = (* identical to Flat, but does not go to `Top/Bot` if Base raises Unknown/Error *)
 struct
-  include Lattice.LiftPO (Base) (struct
+  include Lattice.LiftPO (struct
+      include Printable.DefaultConf
       let top_name = "MaxInt"
       let bot_name = "MinInt"
-    end)
+    end) (Base)
   type int_t = Base.int_t
   let top_of ik = top ()
   let bot_of ik = bot ()

src/cdomains/mutexAttrDomain.ml

@@ -18,7 +18,7 @@ struct
     end)
 end
 
-include Lattice.Flat(MutexKind) (struct let bot_name = "Uninitialized" let top_name = "Top" end)
+include Lattice.FlatConf (struct include Printable.DefaultConf let bot_name = "Uninitialized" let top_name = "Top" end) (MutexKind)
 
 (* Needed because OS X is weird and assigns different constants than normal systems... :( *)
 let recursive_int = lazy (

src/cdomains/regionDomain.ml

@@ -8,23 +8,9 @@ module B = Printable.UnitConf (struct let name = "•" end)
 
 module VFB =
 struct
-  include Printable.Either (VF) (B)
+  include Printable.EitherConf (struct include Printable.DefaultConf let expand1 = false let expand2 = false end) (VF) (B)
   let name () = "region"
 
-  let pretty () = function
-    | `Right () -> Pretty.text "•"
-    | `Left x -> VF.pretty () x
-
-  let show = function
-    | `Right () -> "•"
-    | `Left x -> VF.show x
-
-  let printXml f = function
-    | `Right () ->
-      BatPrintf.fprintf f "<value>\n<data>\n•\n</data>\n</value>\n"
-    | `Left x ->
-      BatPrintf.fprintf f "<value>\n<data>\n%a\n</data>\n</value>\n" VF.printXml x
-
   let collapse (x:t) (y:t): bool =
     match x,y with
     | `Right (), `Right () -> true
@@ -252,4 +238,4 @@ struct
 end
 
 (* TODO: remove Lift *)
-module RegionDom = Lattice.Lift (RegMap) (struct let top_name = "Unknown" let bot_name = "Error" end)
+module RegionDom = Lattice.LiftConf (struct include Printable.DefaultConf let top_name = "Unknown" let bot_name = "Error" end) (RegMap)

src/cdomains/stackDomain.ml

@@ -30,7 +30,7 @@ struct
 
   module VarLat = Lattice.Fake (Basetype.Variables)
 
-  module Var = Lattice.Lift (VarLat) (struct let top_name="top" let bot_name="⊥" end)
+  module Var = Lattice.LiftConf (struct include Printable.DefaultConf let top_name="top" let bot_name="⊥" end) (VarLat)
   include Lattice.Liszt (Var)
 
   let top () : t = []

src/cdomains/symbLocksDomain.ml

@@ -306,6 +306,7 @@ struct
   end
 
   include AddressDomain.AddressPrintable (Mval.MakePrintable (Offset.MakePrintable (Idx)))
+  let name () = "i-lock"
 
   let rec conv_const_offset x =
     match x with

src/cdomains/threadIdDomain.ml

@@ -196,12 +196,14 @@ struct
 end
 
 module ThreadLiftNames = struct
+  include Printable.DefaultConf
   let bot_name = "Bot Threads"
   let top_name = "Top Threads"
+  let expand1 = false
 end
 module Lift (Thread: S) =
 struct
-  include Lattice.Flat (Thread) (ThreadLiftNames)
+  include Lattice.FlatConf (ThreadLiftNames) (Thread)
   let name () = "Thread"
 end
 
@@ -217,7 +219,7 @@ struct
       let name = "FlagConfiguredTID"
     end)
 
-  module D = Lattice.Lift2(H.D)(P.D)(struct let bot_name = "bot" let top_name = "top" end)
+  module D = Lattice.Lift2 (H.D) (P.D)
 
   let history_enabled () =
     match GobConfig.get_string "ana.thread.domain" with

src/cdomains/unionDomain.ml

@@ -16,10 +16,11 @@ sig
 end
 
 module Field = struct
-  include Lattice.Flat (CilType.Fieldinfo) (struct
+  include Lattice.FlatConf (struct
+      include Printable.DefaultConf
       let top_name = "Unknown field"
       let bot_name = "If you see this, you are special!"
-    end)
+    end) (CilType.Fieldinfo)
 
   let meet f g =
     if equal f g then