Simplify default Lattice.Flat usage

sim642 · sim642 · commit ea029bc5b13f · 2023-12-14T16:29:23.000+02:00
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 (Printable.DefaultConf) (CilType.Stmt)
+module Statements = Lattice.Flat (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 (Printable.DefaultConf) (DomVariantLattice0 (DLSpec))
+  include Lattice.Lift (DomVariantLattice0 (DLSpec))
   let name () = "MCP.G"
 end
 
diff --git a/src/analyses/threadId.ml b/src/analyses/threadId.ml
@@ -31,7 +31,7 @@ struct
 
   module N =
   struct
-    include Lattice.Flat (struct include Printable.DefaultConf let bot_name = "unknown node" let top_name = "unknown node" end) (VNI)
+    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
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 (Printable.DefaultConf) (Signs)
+  include Lattice.Flat (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,7 @@ 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 (struct
+module NodeFlatLattice = Lattice.FlatConf (struct
     include Printable.DefaultConf
     let top_name = "Unknown node"
     let bot_name = "Unreachable node"
diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml
@@ -1713,7 +1713,7 @@ 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 (struct
+  include Lattice.FlatConf (struct
       include Printable.DefaultConf
       let top_name = "Unknown int"
       let bot_name = "Error int"
diff --git a/src/cdomains/mutexAttrDomain.ml b/src/cdomains/mutexAttrDomain.ml
@@ -18,7 +18,7 @@ struct
     end)
 end
 
-include Lattice.Flat (struct include Printable.DefaultConf let bot_name = "Uninitialized" let top_name = "Top" end) (MutexKind)
+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 (
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 (struct include Printable.DefaultConf let top_name = "Unknown" let bot_name = "Error" end) (RegMap)
+module RegionDom = Lattice.LiftConf (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 (struct include Printable.DefaultConf let top_name="top" let bot_name="⊥" end) (VarLat)
+  module Var = Lattice.LiftConf (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
@@ -202,7 +202,7 @@ module ThreadLiftNames = struct
 end
 module Lift (Thread: S) =
 struct
-  include Lattice.Flat (ThreadLiftNames) (Thread)
+  include Lattice.FlatConf (ThreadLiftNames) (Thread)
   let name () = "Thread"
 end
 
diff --git a/src/cdomains/unionDomain.ml b/src/cdomains/unionDomain.ml
@@ -16,7 +16,7 @@ sig
 end
 
 module Field = struct
-  include Lattice.Flat (struct
+  include Lattice.FlatConf (struct
       include Printable.DefaultConf
       let top_name = "Unknown field"
       let bot_name = "If you see this, you are special!"
diff --git a/src/common/domains/printable.ml b/src/common/domains/printable.ml
@@ -197,6 +197,7 @@ struct
   let top_name = "top"
   let expand1 = true
   let expand2 = true
+  let expand3 = true
 end
 
 module LiftConf (Conf: LiftConf) (Base: S) =
@@ -291,7 +292,7 @@ struct
     | `Right x -> `Right (Base2.relift x)
 end
 
-module Either = EitherConf (struct let expand1 = true let expand2 = true end)
+module Either = EitherConf (DefaultConf)
 
 module type Either3Conf =
 sig
@@ -345,7 +346,7 @@ struct
     | `Right x -> `Right (Base3.relift x)
 end
 
-module Either3 = Either3Conf (struct let expand1 = true let expand2 = true let expand3 = true end)
+module Either3 = Either3Conf (DefaultConf)
 
 module Option (Base: S) (N: Name) =
 struct
@@ -425,8 +426,6 @@ struct
     | `Lifted2 x -> Base2.to_yojson x
 end
 
-module Lift2 = Lift2Conf (DefaultConf)
-
 module type ProdConfiguration =
 sig
   val expand_fst: bool
diff --git a/src/domain/boolDomain.ml b/src/domain/boolDomain.ml
@@ -41,7 +41,7 @@ struct
 end
 
 module FlatBool: Lattice.S with type t = [`Bot | `Lifted of bool | `Top] =
-  Lattice.Flat (struct
+  Lattice.FlatConf (struct
     include Printable.DefaultConf
     let top_name = "?"
     let bot_name = "-"
diff --git a/src/domain/lattice.ml b/src/domain/lattice.ml
@@ -183,7 +183,7 @@ struct
   let pretty_diff () ((x:t),(y:t)): Pretty.doc = M.pretty_diff () (unlift x, unlift y)
 end
 
-module Flat (Conf: Printable.LiftConf) (Base: Printable.S) =
+module FlatConf (Conf: Printable.LiftConf) (Base: Printable.S) =
 struct
   include Printable.LiftConf (Conf) (Base)
   let bot () = `Bot
@@ -227,8 +227,10 @@ struct
 
 end
 
+module Flat = FlatConf (Printable.DefaultConf)
 
-module Lift (Conf: Printable.LiftConf) (Base: S) =
+
+module LiftConf (Conf: Printable.LiftConf) (Base: S) =
 struct
   include Printable.LiftConf (Conf) (Base)
 
@@ -278,6 +280,8 @@ struct
     | _ -> x
 end
 
+module Lift = LiftConf (Printable.DefaultConf)
+
 module LiftPO (Conf: Printable.LiftConf) (Base: PO) =
 struct
   include Printable.LiftConf (Conf) (Base)
diff --git a/src/domains/invariant.ml b/src/domains/invariant.ml
@@ -33,7 +33,7 @@ struct
   let top_name = "true"
 end
 
-include Lattice.Lift (N) (ExpLat)
+include Lattice.LiftConf (N) (ExpLat)
 
 let none = top ()
 let of_exp = lift
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
@@ -17,29 +17,17 @@ module TC = WrapperFunctionAnalysis0.ThreadCreateUniqueCount
 module ThreadNodeLattice = Lattice.Prod (NFL) (TC)
 module ML = LibraryDesc.MathLifted
 
-module VI = Lattice.Flat (struct
-    include Printable.DefaultConf
-    let top_name = "Unknown line"
-    let bot_name = "Unreachable line"
-  end) (Basetype.Variables)
+module VI = Lattice.Flat (Basetype.Variables)
 
 type iterprevvar = int -> (MyCFG.node * Obj.t * int) -> MyARG.inline_edge -> unit
 type itervar = int -> unit
 let compare_itervar _ _ = 0
 let compare_iterprevvar _ _ = 0
 
-module FlatYojson = Lattice.Flat (struct
-    include Printable.DefaultConf
-    let top_name = "top yojson"
-    let bot_name = "bot yojson"
-  end) (Printable.Yojson)
+module FlatYojson = Lattice.Flat (Printable.Yojson)
 
 module SD: Lattice.S with type t = [`Bot | `Lifted of string | `Top] =
-  Lattice.Flat (struct
-    include Printable.DefaultConf
-    let top_name = "?"
-    let bot_name = "-"
-  end) (Basetype.RawStrings)
+  Lattice.Flat (Basetype.RawStrings)
 module VD = ValueDomain.Compound
 module AD = ValueDomain.AD
 
diff --git a/src/domains/valueDomainQueries.ml b/src/domains/valueDomainQueries.ml
@@ -9,7 +9,7 @@ module AD = PreValueDomain.AD
 module ID =
 struct
   module I = IntDomain.IntDomTuple
-  include Lattice.Lift (Printable.DefaultConf) (I)
+  include Lattice.Lift (I)
 
   let lift op x = `Lifted (op x)
   let unlift op x = match x with
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
@@ -142,7 +142,7 @@ exception Deadcode
 (** [Dom (D)] produces D lifted where bottom means dead-code *)
 module Dom (LD: Lattice.S) =
 struct
-  include Lattice.Lift (struct
+  include Lattice.LiftConf (struct
       include Printable.DefaultConf
       let bot_name = "Dead code"
       let top_name = "Totally unknown and messed up"
diff --git a/src/util/library/libraryDesc.ml b/src/util/library/libraryDesc.ml
@@ -184,7 +184,7 @@ module MathPrintable = struct
     )
 end
 
-module MathLifted = Lattice.Flat (struct
+module MathLifted = Lattice.FlatConf (struct
     include Printable.DefaultConf
     let top_name = "Unknown or no math desc"
     let bot_name = "Nonexistent math desc"
diff --git a/src/witness/observerAnalysis.ml b/src/witness/observerAnalysis.ml
@@ -29,7 +29,7 @@ struct
     let n () = -1
     let names x = "state " ^ string_of_int x
   end
-  module D = Lattice.Flat (Printable.DefaultConf) (Printable.Chain (ChainParams))
+  module D = Lattice.Flat (Printable.Chain (ChainParams))
   module C = D
   module P = IdentityP (D) (* fully path-sensitive *)
 
