Improve readability of Spec lifted domains

src/constraint/translators.ml

@@ -35,14 +35,7 @@ module EqConstrSysFromGlobConstrSys (S:DemandGlobConstrSys)
 =
 struct
   module Var = Var2(S.LVar)(S.GVar)
-  module Dom =
-  struct
-    include Lattice.Lift2 (S.G) (S.D)
-    let printXml f = function
-      | `Lifted1 a -> S.G.printXml f a
-      | `Lifted2 a -> S.D.printXml f a
-      | (`Bot | `Top) as x -> printXml f x
-  end
+  module Dom = Lattice.Lift2Conf (struct include Printable.DefaultConf let expand1 = false let expand2 = false end) (S.G) (S.D)
   type v = Var.t
   type d = Dom.t
 

src/framework/analyses.ml

@@ -97,7 +97,7 @@ struct
     let name () = "contexts"
   end
 
-  include Lattice.Lift2 (G) (CSet)
+  include Lattice.Lift2Conf (struct include Printable.DefaultConf let expand1 = false let expand2 = false end) (G) (CSet)
 
   let spec = function
     | `Bot -> G.bot ()
@@ -123,9 +123,9 @@ exception Deadcode
 module Dom (LD: Lattice.S) =
 struct
   include Lattice.LiftConf (struct
-      include Printable.DefaultConf
       let bot_name = "Dead code"
       let top_name = "Totally unknown and messed up"
+      let expand1 = false
     end) (LD)
 
   let unlift x =

src/lifters/contextGasLifter.ml

@@ -28,7 +28,12 @@ struct
 
   module Context_Gas_Prod (Base1: Lattice.S) (Base2: Lattice.S) =
   struct
-    include Lattice.Prod (Base1) (Base2)
+    module Base2 =
+    struct
+      include Base2
+      let name () = "context gas"
+    end
+    include Lattice.Prod (Base1) (Base2) (* TODO: suppress S.D name? *)
     let printXml f (x,y) =
       BatPrintf.fprintf f "\n%a<analysis name=\"context gas value\">\n%a\n</analysis>" Base1.printXml x Base2.printXml y
   end

src/lifters/longjmpLifter.ml

@@ -11,7 +11,17 @@ struct
 
   module V =
   struct
-    include Printable.Either3Conf (struct let expand1 = false let expand2 = true let expand3 = true end) (S.V) (Printable.Prod (Node) (C)) (Printable.Prod (CilType.Fundec) (C))
+    module Longjmpto =
+    struct
+      include Printable.Prod (Node) (C)
+      let name () = "longjmpto"
+    end
+    module Longjmpret =
+    struct
+      include Printable.Prod (CilType.Fundec) (C)
+      let name () = "longjmpret"
+    end
+    include Printable.Either3Conf (struct let expand1 = false let expand2 = true let expand3 = true end) (S.V) (Longjmpto) (Longjmpret)
     let name () = "longjmp"
     let s x = `Left x
     let longjmpto x = `Middle x
@@ -23,7 +33,7 @@ struct
 
   module G =
   struct
-    include Lattice.Lift2 (S.G) (S.D)
+    include Lattice.Lift2Conf (struct include Printable.DefaultConf let expand1 = false let expand2 = false end) (S.G) (S.D)
 
     let s = function
       | `Bot -> S.G.bot ()

src/lifters/recursionTermLifter.ml

@@ -31,7 +31,7 @@ struct
 
   module G =
   struct
-    include Lattice.Lift2 (G) (CallerSet)
+    include Lattice.Lift2Conf (struct include Printable.DefaultConf let expand1 = false let expand2 = false end) (G) (CallerSet)
 
     let spec = function
       | `Bot -> G.bot ()

src/lifters/specLifters.ml

@@ -321,14 +321,20 @@ module OptEqual (S: Spec) = struct
   include (S : Spec with module D := D and module G := G and module C := C)
 end
 
+module LevelSliceDomain =
+struct
+  include Lattice.Reverse (IntDomain.Lifted)
+  let name () = "level"
+end
+
 (** If dbg.slice.on, stops entering functions after dbg.slice.n levels. *)
 module LevelSliceLifter (S:Spec)
-  : Spec with module D = Lattice.Prod (S.D) (Lattice.Reverse (IntDomain.Lifted))
+  : Spec with module D = Lattice.Prod (S.D) (LevelSliceDomain)
           and module G = S.G
           and module C = S.C
 =
 struct
-  module D = Lattice.Prod (S.D) (Lattice.Reverse (IntDomain.Lifted))
+  module D = Lattice.Prod (S.D) (LevelSliceDomain) (* TODO: suppress Base name? *)
   module G = S.G
   module C = S.C
   module V = S.V
@@ -454,10 +460,14 @@ struct
     include S.D
     let printXml f d = BatPrintf.fprintf f "<value>%a</value>" printXml d
   end
-  module M = MapDomain.PatriciaMapBot (Basetype.Variables) (DD) (* should be CilFun -> S.C, but CilFun is not Groupable, and S.C is no Lattice *)
+  module M =
+  struct
+    include MapDomain.PatriciaMapBot (Basetype.Variables) (DD) (* should be CilFun -> S.C, but CilFun is not Groupable, and S.C is no Lattice *)
+    let name () = "widen-context"
+  end
 
   module D = struct
-    include Lattice.Prod (S.D) (M)
+    include Lattice.Prod (S.D) (M) (* TODO: suppress S.D name? *)
     let printXml f (d,m) = BatPrintf.fprintf f "\n%a<analysis name=\"widen-context\">\n%a\n</analysis>" S.D.printXml d M.printXml m
   end
   module G = S.G
@@ -763,6 +773,11 @@ struct
 
   module V =
   struct
+    module Node =
+    struct
+      include Node
+      let name () = "deadbranch"
+    end
     include Printable.EitherConf (struct let expand1 = false let expand2 = true end) (S.V) (Node)
     let name () = "DeadBranch"
     let s x = `Left x
@@ -780,7 +795,7 @@ struct
 
   module G =
   struct
-    include Lattice.Lift2 (S.G) (EM)
+    include Lattice.Lift2Conf (struct include Printable.DefaultConf let expand1 = false let expand2 = false end) (S.G) (EM)
     let name () = "deadbranch"
 
     let s = function

src/lifters/wideningDelay.ml

@@ -21,8 +21,12 @@ end
 
 module Dom (Base: S) (ChainParams: Printable.ChainParams) =
 struct
-  module Chain = Printable.Chain (ChainParams)
-  include Printable.Prod (Base) (Chain)
+  module Chain =
+  struct
+    include Printable.Chain (ChainParams)
+    let name () = "widen-delay"
+  end
+  include Printable.Prod (Base) (Chain) (* TODO: suppress Base name? *)
 
   let lift d = (d, 0)
   let unlift (d, _) = d

src/lifters/wideningToken.ml

@@ -14,3 +14,5 @@ end
 
 (* Change to variant type if need other tokens than witness UUIDs. *)
 include Printable.Prod (Uuid) (Index)
+
+let name () = "widen-token"

src/lifters/wideningTokenLifter.ml

@@ -9,7 +9,11 @@
 module Token = WideningToken
 
 (** Widening token set. *)
-module TS = SetDomain.ToppedSet (Token) (struct let topname = "Top" end)
+module TS =
+struct
+  include SetDomain.ToppedSet (Token) (struct let topname = "Top" end)
+  let name () = "widen-tokens"
+end
 
 (** Reference to current {!add} implementation. Maintained by {!Lifter}. *)
 let add_ref: (Token.t -> unit) Domain.DLS.key = Domain.DLS.new_key (fun () _ ->
@@ -58,7 +62,7 @@ open Analyses
     except widening tokens are used to delay widenings. *)
 module Dom (D: Lattice.S) =
 struct
-  include Lattice.Prod (D) (TS)
+  include Lattice.Prod (D) (TS) (* TODO: suppress Base name? *)
   let unlift (d, _) = d
   let lift d = (d, TS.bot ())