Add Lattice.Lift2Conf

goblint · Dec 14, 2023 · 1ecca1d · 1ecca1d
1 parent 38942f9
commit 1ecca1d
Show file tree

Hide file tree

Showing 6 changed files with 21 additions and 11 deletions.
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -54,7 +54,7 @@ struct
 
   module G =
   struct
-    include Lattice.Lift2 (Priv.G) (VD) (Printable.DefaultNames)
+    include Lattice.Lift2Conf (struct let expand1 = false let expand2 = false end) (Priv.G) (VD) (Printable.DefaultNames)
 
     let priv = function
       | `Bot -> Priv.G.bot ()

diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
@@ -198,7 +198,7 @@ struct
 
   module G =
   struct
-    include Lattice.Lift2 (GMutex) (GThread) (Printable.DefaultNames)
+    include Lattice.Lift2Conf (struct let expand1 = false let expand2 = false end) (GMutex) (GThread) (Printable.DefaultNames)
 
     let mutex = function
       | `Bot -> GMutex.bot ()

diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
@@ -132,7 +132,7 @@ struct
 
     module G =
     struct
-      include Lattice.Lift2 (GProtecting) (GProtected) (Printable.DefaultNames)
+      include Lattice.Lift2Conf (struct let expand1 = false let expand2 = false end) (GProtecting) (GProtected) (Printable.DefaultNames)
 
       let protecting = function
         | `Bot -> GProtecting.bot ()

diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml
@@ -194,7 +194,7 @@ struct
 
   module G =
   struct
-    include Lattice.Lift2 (OffsetTrie) (MemoSet) (Printable.DefaultNames)
+    include Lattice.Lift2Conf (struct let expand1 = false let expand2 = false end) (OffsetTrie) (MemoSet) (Printable.DefaultNames)
 
     let access = function
       | `Bot -> OffsetTrie.bot ()

diff --git a/src/common/domains/printable.ml b/src/common/domains/printable.ml
@@ -370,21 +370,23 @@ struct
   let relift = Option.map Base.relift
 end
 
-module Lift2 (Base1: S) (Base2: S) (N: LiftingNames) =
+module Lift2Conf (Conf: EitherConf) (Base1: S) (Base2: S) (N: LiftingNames) =
 struct
   type t = [`Bot | `Lifted1 of Base1.t | `Lifted2 of Base2.t | `Top] [@@deriving eq, ord, hash]
   include Std
   include N
 
   let pretty () (state:t) =
     match state with
+    (* TODO: expand *)
     | `Lifted1 n ->  Base1.pretty () n
     | `Lifted2 n ->  Base2.pretty () n
     | `Bot -> text bot_name
     | `Top -> text top_name
 
   let show state =
     match state with
+    (* TODO: expand *)
     | `Lifted1 n ->  Base1.show n
     | `Lifted2 n ->  Base2.show n
     | `Bot -> bot_name
@@ -399,16 +401,22 @@ struct
   let printXml f = function
     | `Bot       -> BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" N.bot_name
     | `Top       -> BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" N.top_name
-    | `Lifted1 x -> BatPrintf.fprintf f "<value>\n<map>\n<key>\nLifted1\n</key>\n%a</map>\n</value>\n" Base1.printXml x
-    | `Lifted2 x -> BatPrintf.fprintf f "<value>\n<map>\n<key>\nLifted2\n</key>\n%a</map>\n</value>\n" Base2.printXml x
+    | `Lifted1 x when Conf.expand1 -> BatPrintf.fprintf f "<value>\n<map>\n<key>\nLifted1\n</key>\n%a</map>\n</value>\n" Base1.printXml x
+    | `Lifted1 x -> Base1.printXml f x
+    | `Lifted2 x when Conf.expand2 -> BatPrintf.fprintf f "<value>\n<map>\n<key>\nLifted2\n</key>\n%a</map>\n</value>\n" Base2.printXml x
+    | `Lifted2 x -> Base2.printXml f x
 
   let to_yojson = function
     | `Bot -> `String N.bot_name
     | `Top -> `String N.top_name
-    | `Lifted1 x -> `Assoc [ Base1.name (), Base1.to_yojson x ]
-    | `Lifted2 x -> `Assoc [ Base2.name (), Base2.to_yojson x ]
+    | `Lifted1 x when Conf.expand1 -> `Assoc [ Base1.name (), Base1.to_yojson x ]
+    | `Lifted1 x -> Base1.to_yojson x
+    | `Lifted2 x when Conf.expand2 -> `Assoc [ Base2.name (), Base2.to_yojson x ]
+    | `Lifted2 x -> Base2.to_yojson x
 end
 
+module Lift2 = Lift2Conf (struct let expand1 = true let expand2 = true end)
+
 module type ProdConfiguration =
 sig
   val expand_fst: bool

diff --git a/src/domain/lattice.ml b/src/domain/lattice.ml
@@ -336,9 +336,9 @@ struct
     | _ -> x
 end
 
-module Lift2 (Base1: S) (Base2: S) (N: Printable.LiftingNames) =
+module Lift2Conf (Conf: Printable.EitherConf) (Base1: S) (Base2: S) (N: Printable.LiftingNames) =
 struct
-  include Printable.Lift2 (Base1) (Base2) (N)
+  include Printable.Lift2Conf (Conf) (Base1) (Base2) (N)
 
   let bot () = `Bot
   let is_bot x = x = `Bot
@@ -408,6 +408,8 @@ struct
 
 end
 
+module Lift2 = Lift2Conf (struct let expand1 = true let expand2 = true end)
+
 module ProdConf (C: Printable.ProdConfiguration) (Base1: S) (Base2: S) =
 struct
   include Printable.ProdConf (C) (Base1) (Base2)