Refactor Printable.LiftingNames

sim642 · sim642 · commit b71518c7d51a · 2023-12-14T16:18:03.000+02:00
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -54,7 +54,7 @@ struct
 
   module G =
   struct
-    include Lattice.Lift2Conf (struct let expand1 = false let expand2 = false end) (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 ()
diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
@@ -799,7 +799,7 @@ struct
   struct
     (* weak: G -> (2^M -> WeakRange) *)
     (* sync: M -> (2^M -> SyncRange) *)
-    include Lattice.Lift2Conf (struct let expand1 = false let expand2 = false end) (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 ()
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
@@ -198,7 +198,7 @@ struct
 
   module G =
   struct
-    include Lattice.Lift2Conf (struct let expand1 = false let expand2 = false end) (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 ()
diff --git a/src/analyses/loopTermination.ml b/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 (Printable.DefaultConf) (CilType.Stmt)
 
 (** The termination analysis considering loops and gotos *)
 module Spec : Analyses.MCPSpec =
diff --git a/src/analyses/mCPRegistry.ml b/src/analyses/mCPRegistry.ml
@@ -426,7 +426,7 @@ end
 
 module DomVariantLattice (DLSpec : DomainListLatticeSpec) =
 struct
-  include Lattice.Lift (DomVariantLattice0 (DLSpec)) (Printable.DefaultNames)
+  include Lattice.Lift (Printable.DefaultConf) (DomVariantLattice0 (DLSpec))
   let name () = "MCP.G"
 end
 
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
@@ -132,7 +132,7 @@ struct
 
     module G =
     struct
-      include Lattice.Lift2Conf (struct let expand1 = false let expand2 = false end) (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 ()
diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml
@@ -194,7 +194,7 @@ struct
 
   module G =
   struct
-    include Lattice.Lift2Conf (struct let expand1 = false let expand2 = false end) (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 ()
diff --git a/src/analyses/threadId.ml b/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.Flat (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
diff --git a/src/analyses/tutorials/signs.ml b/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 (Printable.DefaultConf) (Signs)
   let of_int i = `Lifted (Signs.of_int i)
 
   let lt x y = match x, y with
diff --git a/src/analyses/wrapperFunctionAnalysis0.ml b/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.Flat (struct
+    include Printable.DefaultConf
     let top_name = "Unknown node"
     let bot_name = "Unreachable node"
-  end)
+  end) (Node)
diff --git a/src/cdomains/intDomain.ml b/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.Flat (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 ()
diff --git a/src/cdomains/mutexAttrDomain.ml b/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.Flat (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 (
diff --git a/src/cdomains/regionDomain.ml b/src/cdomains/regionDomain.ml
@@ -252,4 +252,4 @@ struct
 end
 
 (* TODO: remove Lift *)
-module RegionDom = Lattice.Lift (RegMap) (struct let top_name = "Unknown" let bot_name = "Error" end)
+module RegionDom = Lattice.Lift (struct include Printable.DefaultConf let top_name = "Unknown" let bot_name = "Error" end) (RegMap)
diff --git a/src/cdomains/stackDomain.ml b/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.Lift (struct include Printable.DefaultConf let top_name="top" let bot_name="⊥" end) (VarLat)
   include Lattice.Liszt (Var)
 
   let top () : t = []
diff --git a/src/cdomains/threadIdDomain.ml b/src/cdomains/threadIdDomain.ml
@@ -196,12 +196,13 @@ struct
 end
 
 module ThreadLiftNames = struct
+  include Printable.DefaultConf
   let bot_name = "Bot Threads"
   let top_name = "Top Threads"
 end
 module Lift (Thread: S) =
 struct
-  include Lattice.Flat (Thread) (ThreadLiftNames)
+  include Lattice.Flat (ThreadLiftNames) (Thread)
   let name () = "Thread"
 end
 
@@ -217,7 +218,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
diff --git a/src/cdomains/unionDomain.ml b/src/cdomains/unionDomain.ml
@@ -16,10 +16,11 @@ sig
 end
 
 module Field = struct
-  include Lattice.Flat (CilType.Fieldinfo) (struct
+  include Lattice.Flat (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
diff --git a/src/common/domains/printable.ml b/src/common/domains/printable.ml
@@ -103,18 +103,6 @@ struct
 end
 module Unit = UnitConf (struct let name = "()" end)
 
-module type LiftingNames =
-sig
-  val bot_name: string
-  val top_name: string
-end
-
-module DefaultNames =
-struct
-  let bot_name = "bot"
-  let top_name = "top"
-end
-
 (* HAS SIDE-EFFECTS ---- PLEASE INSTANCIATE ONLY ONCE!!! *)
 module HConsed (Base:S) =
 struct
@@ -195,11 +183,27 @@ struct
   let tag = lift_f M.tag
 end
 
-module Lift (Base: S) (N: LiftingNames) =
+
+module type LiftConf =
+sig
+  val bot_name: string
+  val top_name: string
+  val expand1: bool
+end
+
+module DefaultConf =
+struct
+  let bot_name = "bot"
+  let top_name = "top"
+  let expand1 = true
+  let expand2 = true
+end
+
+module LiftConf (Conf: LiftConf) (Base: S) =
 struct
   type t = [`Bot | `Lifted of Base.t | `Top] [@@deriving eq, ord, hash]
   include Std
-  include N
+  open Conf
 
   let lift x = `Lifted x
 
@@ -217,13 +221,13 @@ struct
 
   let name () = "lifted " ^ Base.name ()
   let printXml f = function
-    | `Bot      -> BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (XmlUtil.escape N.bot_name)
-    | `Top      -> BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (XmlUtil.escape N.top_name)
+    | `Bot      -> BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (XmlUtil.escape bot_name)
+    | `Top      -> BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (XmlUtil.escape top_name)
     | `Lifted x -> Base.printXml f x
 
   let to_yojson = function
-    | `Bot -> `String N.bot_name
-    | `Top -> `String N.top_name
+    | `Bot -> `String bot_name
+    | `Top -> `String top_name
     | `Lifted x -> Base.to_yojson x
 
   let relift x = match x with
@@ -370,11 +374,17 @@ struct
   let relift = Option.map Base.relift
 end
 
-module Lift2Conf (Conf: EitherConf) (Base1: S) (Base2: S) (N: LiftingNames) =
+module type Lift2Conf =
+sig
+  include LiftConf
+  val expand2: bool
+end
+
+module Lift2Conf (Conf: Lift2Conf) (Base1: S) (Base2: S) =
 struct
   type t = [`Bot | `Lifted1 of Base1.t | `Lifted2 of Base2.t | `Top] [@@deriving eq, ord, hash]
   include Std
-  include N
+  open Conf
 
   let pretty () (state:t) =
     match state with
@@ -399,23 +409,23 @@ struct
 
   let name () = "lifted " ^ Base1.name () ^ " and " ^ Base2.name ()
   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
+    | `Bot       -> BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" bot_name
+    | `Top       -> BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" top_name
     | `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
+    | `Bot -> `String bot_name
+    | `Top -> `String top_name
     | `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 Lift2 = Lift2Conf (DefaultConf)
 
 module type ProdConfiguration =
 sig
diff --git a/src/domain/boolDomain.ml b/src/domain/boolDomain.ml
@@ -41,7 +41,8 @@ struct
 end
 
 module FlatBool: Lattice.S with type t = [`Bot | `Lifted of bool | `Top] =
-  Lattice.Flat (Bool) (struct
+  Lattice.Flat (struct
+    include Printable.DefaultConf
     let top_name = "?"
     let bot_name = "-"
-  end)
+  end) (Bool)
diff --git a/src/domain/lattice.ml b/src/domain/lattice.ml
@@ -183,9 +183,9 @@ struct
   let pretty_diff () ((x:t),(y:t)): Pretty.doc = M.pretty_diff () (unlift x, unlift y)
 end
 
-module Flat (Base: Printable.S) (N: Printable.LiftingNames) =
+module Flat (Conf: Printable.LiftConf) (Base: Printable.S) =
 struct
-  include Printable.Lift (Base) (N)
+  include Printable.LiftConf (Conf) (Base)
   let bot () = `Bot
   let is_bot x = x = `Bot
   let top () = `Top
@@ -228,9 +228,9 @@ struct
 end
 
 
-module Lift (Base: S) (N: Printable.LiftingNames) =
+module Lift (Conf: Printable.LiftConf) (Base: S) =
 struct
-  include Printable.Lift (Base) (N)
+  include Printable.LiftConf (Conf) (Base)
 
   let bot () = `Bot
   let is_bot x = x = `Bot
@@ -278,9 +278,9 @@ struct
     | _ -> x
 end
 
-module LiftPO (Base: PO) (N: Printable.LiftingNames) =
+module LiftPO (Conf: Printable.LiftConf) (Base: PO) =
 struct
-  include Printable.Lift (Base) (N)
+  include Printable.LiftConf (Conf) (Base)
 
   let bot () = `Bot
   let is_bot x = x = `Bot
@@ -336,9 +336,9 @@ struct
     | _ -> x
 end
 
-module Lift2Conf (Conf: Printable.EitherConf) (Base1: S) (Base2: S) (N: Printable.LiftingNames) =
+module Lift2Conf (Conf: Printable.Lift2Conf) (Base1: S) (Base2: S) =
 struct
-  include Printable.Lift2Conf (Conf) (Base1) (Base2) (N)
+  include Printable.Lift2Conf (Conf) (Base1) (Base2)
 
   let bot () = `Bot
   let is_bot x = x = `Bot
@@ -408,7 +408,7 @@ struct
 
 end
 
-module Lift2 = Lift2Conf (struct let expand1 = true let expand2 = true end)
+module Lift2 = Lift2Conf (Printable.DefaultConf)
 
 module ProdConf (C: Printable.ProdConfiguration) (Base1: S) (Base2: S) =
 struct
diff --git a/src/domains/invariant.ml b/src/domains/invariant.ml
@@ -28,11 +28,12 @@ end
 
 module N =
 struct
+  include Printable.DefaultConf
   let bot_name = "false"
   let top_name = "true"
 end
 
-include Lattice.Lift (ExpLat) (N)
+include Lattice.Lift (N) (ExpLat)
 
 let none = top ()
 let of_exp = lift
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
diff --git a/src/domains/valueDomainQueries.ml b/src/domains/valueDomainQueries.ml
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
diff --git a/src/util/library/libraryDesc.ml b/src/util/library/libraryDesc.ml
diff --git a/src/witness/observerAnalysis.ml b/src/witness/observerAnalysis.ml
