diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 46a54af2ba..912d1f3bff 100644
--- 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 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
index 0126449413..10deaa4d16 100644
--- a/src/analyses/basePriv.ml
+++ b/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 ()
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index 73a2e75de1..90e5b28f82 100644
--- a/src/analyses/commonPriv.ml
+++ b/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 ()
diff --git a/src/analyses/loopTermination.ml b/src/analyses/loopTermination.ml
index 10e0f5c5f4..857b6189d0 100644
--- 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 (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
index 5d0174d44c..3961bc4d60 100644
--- 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.LiftConf (struct include Printable.DefaultConf let expand1 = false end) (DomVariantLattice0 (DLSpec))
let name () = "MCP.G"
end
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index ee050f55ca..a13c8d6bfd 100644
--- 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 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
index 9c2272fabb..f35e6756a1 100644
--- 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 include Printable.DefaultConf let expand1 = false let expand2 = false end) (OffsetTrie) (MemoSet)
let access = function
| `Bot -> OffsetTrie.bot ()
diff --git a/src/analyses/symbLocks.ml b/src/analyses/symbLocks.ml
index f6fdd96c2e..c237967a7a 100644
--- a/src/analyses/symbLocks.ml
+++ b/src/analyses/symbLocks.ml
@@ -106,13 +106,12 @@ 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
@@ -120,6 +119,7 @@ struct
end
)
end
+ module E = Printable.Either (PLock) (ILock)
include SetDomain.Make (E)
let name () = "symblock"
diff --git a/src/analyses/threadId.ml b/src/analyses/threadId.ml
index da2c688ad1..86e7f770a8 100644
--- 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.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
index 31168df86a..2c26ad33b6 100644
--- 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 (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
index 9ea9c0c9aa..cd5940011e 100644
--- 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.FlatConf (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
index 5d5174744f..376dab71c2 100644
--- 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.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 ()
diff --git a/src/cdomains/mutexAttrDomain.ml b/src/cdomains/mutexAttrDomain.ml
index 748ede0ff5..ea9696d26f 100644
--- 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.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
index 681eb79007..cd9141876c 100644
--- a/src/cdomains/regionDomain.ml
+++ b/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 "\n\n•\n\n\n"
- | `Left x ->
- BatPrintf.fprintf f "\n\n%a\n\n\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)
diff --git a/src/cdomains/stackDomain.ml b/src/cdomains/stackDomain.ml
index 3a83c78503..50864d6294 100644
--- 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.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/symbLocksDomain.ml b/src/cdomains/symbLocksDomain.ml
index 4a44911a53..85578d5fad 100644
--- a/src/cdomains/symbLocksDomain.ml
+++ b/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
diff --git a/src/cdomains/threadIdDomain.ml b/src/cdomains/threadIdDomain.ml
index d0c3f7b61b..85f9a0297b 100644
--- a/src/cdomains/threadIdDomain.ml
+++ b/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
diff --git a/src/cdomains/unionDomain.ml b/src/cdomains/unionDomain.ml
index ac25450c6a..ad5c531061 100644
--- 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.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
diff --git a/src/common/domains/printable.ml b/src/common/domains/printable.ml
index cc01718ee8..0b1769e99c 100644
--- 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,67 @@ struct
let tag = lift_f M.tag
end
-module Lift (Base: S) (N: LiftingNames) =
+
+module type PrefixNameConf =
+sig
+ val expand: bool
+end
+
+module PrefixName (Conf: PrefixNameConf) (Base: S): S with type t = Base.t =
+struct
+ include Base
+
+ let pretty () x =
+ if Conf.expand then
+ Pretty.dprintf "%s:%a" (Base.name ()) Base.pretty x
+ else
+ Base.pretty () x
+
+ let show x =
+ if Conf.expand then
+ Base.name () ^ ":" ^ Base.show x
+ else
+ Base.show x
+
+ let printXml f x =
+ if Conf.expand then
+ BatPrintf.fprintf f "\n\n" (Base.name ()) Base.printXml x
+ else
+ Base.printXml f x
+
+ let to_yojson x =
+ if Conf.expand then
+ `Assoc [(Base.name (), Base.to_yojson x)]
+ else
+ Base.to_yojson x
+end
+
+
+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
+ let expand3 = true
+end
+
+module LiftConf (Conf: LiftConf) (Base: S) =
+struct
+ open struct
+ module Base = PrefixName (struct let expand = Conf.expand1 end) (Base)
+ end
+
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 +261,13 @@ struct
let name () = "lifted " ^ Base.name ()
let printXml f = function
- | `Bot -> BatPrintf.fprintf f "\n\n%s\n\n\n" (XmlUtil.escape N.bot_name)
- | `Top -> BatPrintf.fprintf f "\n\n%s\n\n\n" (XmlUtil.escape N.top_name)
+ | `Bot -> BatPrintf.fprintf f "\n\n%s\n\n\n" (XmlUtil.escape bot_name)
+ | `Top -> BatPrintf.fprintf f "\n\n%s\n\n\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
@@ -244,62 +288,87 @@ struct
] (* S TODO: decide frequencies *)
end
-module Either (Base1: S) (Base2: S) =
+module type EitherConf =
+sig
+ val expand1: bool
+ val expand2: bool
+end
+
+module EitherConf (Conf: EitherConf) (Base1: S) (Base2: S) =
struct
+ open struct
+ module Base1 = PrefixName (struct let expand = Conf.expand1 end) (Base1)
+ module Base2 = PrefixName (struct let expand = Conf.expand2 end) (Base2)
+ end
+
type t = [`Left of Base1.t | `Right of Base2.t] [@@deriving eq, ord, hash]
include Std
let pretty () (state:t) =
match state with
- | `Left n -> Pretty.dprintf "%s:%a" (Base1.name ()) Base1.pretty n
- | `Right n -> Pretty.dprintf "%s:%a" (Base2.name ()) Base2.pretty n
+ | `Left n -> Base1.pretty () n
+ | `Right n -> Base2.pretty () n
let show state =
match state with
- | `Left n -> (Base1.name ()) ^ ":" ^ Base1.show n
- | `Right n -> (Base2.name ()) ^ ":" ^ Base2.show n
+ | `Left n -> Base1.show n
+ | `Right n -> Base2.show n
let name () = "either " ^ Base1.name () ^ " or " ^ Base2.name ()
let printXml f = function
- | `Left x -> BatPrintf.fprintf f "\n\n" Base1.printXml x
- | `Right x -> BatPrintf.fprintf f "\n\n" Base2.printXml x
+ | `Left x -> Base1.printXml f x
+ | `Right x -> Base2.printXml f x
let to_yojson = function
- | `Left x -> `Assoc [ Base1.name (), Base1.to_yojson x ]
- | `Right x -> `Assoc [ Base2.name (), Base2.to_yojson x ]
+ | `Left x -> Base1.to_yojson x
+ | `Right x -> Base2.to_yojson x
let relift = function
| `Left x -> `Left (Base1.relift x)
| `Right x -> `Right (Base2.relift x)
end
-module Either3 (Base1: S) (Base2: S) (Base3: S) =
+module Either = EitherConf (DefaultConf)
+
+module type Either3Conf =
+sig
+ include EitherConf
+ val expand3: bool
+end
+
+module Either3Conf (Conf: Either3Conf) (Base1: S) (Base2: S) (Base3: S) =
struct
+ open struct
+ module Base1 = PrefixName (struct let expand = Conf.expand1 end) (Base1)
+ module Base2 = PrefixName (struct let expand = Conf.expand2 end) (Base2)
+ module Base3 = PrefixName (struct let expand = Conf.expand3 end) (Base3)
+ end
+
type t = [`Left of Base1.t | `Middle of Base2.t | `Right of Base3.t] [@@deriving eq, ord, hash]
include Std
let pretty () (state:t) =
match state with
- | `Left n -> Pretty.dprintf "%s:%a" (Base1.name ()) Base1.pretty n
- | `Middle n -> Pretty.dprintf "%s:%a" (Base2.name ()) Base2.pretty n
- | `Right n -> Pretty.dprintf "%s:%a" (Base3.name ()) Base3.pretty n
+ | `Left n -> Base1.pretty () n
+ | `Middle n -> Base2.pretty () n
+ | `Right n -> Base3.pretty () n
let show state =
match state with
- | `Left n -> (Base1.name ()) ^ ":" ^ Base1.show n
- | `Middle n -> (Base2.name ()) ^ ":" ^ Base2.show n
- | `Right n -> (Base3.name ()) ^ ":" ^ Base3.show n
+ | `Left n -> Base1.show n
+ | `Middle n -> Base2.show n
+ | `Right n -> Base3.show n
let name () = "either " ^ Base1.name () ^ " or " ^ Base2.name () ^ " or " ^ Base3.name ()
let printXml f = function
- | `Left x -> BatPrintf.fprintf f "\n\n" Base1.printXml x
- | `Middle x -> BatPrintf.fprintf f "\n\n" Base2.printXml x
- | `Right x -> BatPrintf.fprintf f "\n\n" Base3.printXml x
+ | `Left x -> Base1.printXml f x
+ | `Middle x -> Base2.printXml f x
+ | `Right x -> Base3.printXml f x
let to_yojson = function
- | `Left x -> `Assoc [ Base1.name (), Base1.to_yojson x ]
- | `Middle x -> `Assoc [ Base2.name (), Base2.to_yojson x ]
- | `Right x -> `Assoc [ Base3.name (), Base3.to_yojson x ]
+ | `Left x -> Base1.to_yojson x
+ | `Middle x -> Base2.to_yojson x
+ | `Right x -> Base3.to_yojson x
let relift = function
| `Left x -> `Left (Base1.relift x)
@@ -307,6 +376,8 @@ struct
| `Right x -> `Right (Base3.relift x)
end
+module Either3 = Either3Conf (DefaultConf)
+
module Option (Base: S) (N: Name) =
struct
type t = Base.t option [@@deriving eq, ord, hash]
@@ -334,11 +405,22 @@ struct
let relift = Option.map Base.relift
end
-module Lift2 (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
+ open struct
+ module Base1 = PrefixName (struct let expand = Conf.expand1 end) (Base1)
+ module Base2 = PrefixName (struct let expand = Conf.expand2 end) (Base2)
+ end
+
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
@@ -361,16 +443,16 @@ struct
let name () = "lifted " ^ Base1.name () ^ " and " ^ Base2.name ()
let printXml f = function
- | `Bot -> BatPrintf.fprintf f "\n\n%s\n\n\n" N.bot_name
- | `Top -> BatPrintf.fprintf f "\n\n%s\n\n\n" N.top_name
- | `Lifted1 x -> BatPrintf.fprintf f "\n\n\n" Base1.printXml x
- | `Lifted2 x -> BatPrintf.fprintf f "\n\n\n" Base2.printXml x
+ | `Bot -> BatPrintf.fprintf f "\n\n%s\n\n\n" bot_name
+ | `Top -> BatPrintf.fprintf f "\n\n%s\n\n\n" top_name
+ | `Lifted1 x -> Base1.printXml f 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 ]
+ | `Bot -> `String bot_name
+ | `Top -> `String top_name
+ | `Lifted1 x -> Base1.to_yojson x
+ | `Lifted2 x -> Base2.to_yojson x
end
module type ProdConfiguration =
diff --git a/src/domain/boolDomain.ml b/src/domain/boolDomain.ml
index 08be66a602..d92d716d7a 100644
--- 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.FlatConf (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
index 9ea3f74635..99322c09d8 100644
--- 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 FlatConf (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
@@ -227,10 +227,12 @@ struct
end
+module Flat = FlatConf (Printable.DefaultConf)
-module Lift (Base: S) (N: Printable.LiftingNames) =
+
+module LiftConf (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 +280,11 @@ struct
| _ -> x
end
-module LiftPO (Base: PO) (N: Printable.LiftingNames) =
+module Lift = LiftConf (Printable.DefaultConf)
+
+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 +340,9 @@ struct
| _ -> x
end
-module Lift2 (Base1: S) (Base2: S) (N: Printable.LiftingNames) =
+module Lift2Conf (Conf: Printable.Lift2Conf) (Base1: S) (Base2: S) =
struct
- include Printable.Lift2 (Base1) (Base2) (N)
+ include Printable.Lift2Conf (Conf) (Base1) (Base2)
let bot () = `Bot
let is_bot x = x = `Bot
@@ -408,6 +412,8 @@ struct
end
+module Lift2 = Lift2Conf (Printable.DefaultConf)
+
module ProdConf (C: Printable.ProdConfiguration) (Base1: S) (Base2: S) =
struct
include Printable.ProdConf (C) (Base1) (Base2)
diff --git a/src/domains/invariant.ml b/src/domains/invariant.ml
index 1a0c3c033c..b281e8f7b3 100644
--- 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.LiftConf (N) (ExpLat)
let none = top ()
let of_exp = lift
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index 228320bef3..24e5d45593 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -17,26 +17,17 @@ module TC = WrapperFunctionAnalysis0.ThreadCreateUniqueCount
module ThreadNodeLattice = Lattice.Prod (NFL) (TC)
module ML = LibraryDesc.MathLifted
-module VI = Lattice.Flat (Basetype.Variables) (struct
- let top_name = "Unknown line"
- let bot_name = "Unreachable line"
- end)
+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 (Printable.Yojson) (struct
- let top_name = "top yojson"
- let bot_name = "bot yojson"
- end)
+module FlatYojson = Lattice.Flat (Printable.Yojson)
module SD: Lattice.S with type t = [`Bot | `Lifted of string | `Top] =
- Lattice.Flat (Basetype.RawStrings) (struct
- let top_name = "?"
- let bot_name = "-"
- end)
+ Lattice.Flat (Basetype.RawStrings)
module VD = ValueDomain.Compound
module AD = ValueDomain.AD
diff --git a/src/domains/valueDomainQueries.ml b/src/domains/valueDomainQueries.ml
index 8266582ac2..bafec3f8bd 100644
--- 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 (I) (Printable.DefaultNames)
+ 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
index a37a3043c2..405df5b6a6 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -74,7 +74,7 @@ end
module GVarF (V: SpecSysVar) =
struct
- include Printable.Either (V) (CilType.Fundec)
+ include Printable.EitherConf (struct let expand1 = false let expand2 = true end) (V) (CilType.Fundec)
let name () = "FromSpec"
let spec x = `Left x
let contexts x = `Right x
@@ -90,7 +90,7 @@ end
module GVarFC (V:SpecSysVar) (C:Printable.S) =
struct
- include Printable.Either (V) (Printable.Prod (CilType.Fundec) (C))
+ include Printable.EitherConf (struct let expand1 = false let expand2 = true end) (V) (Printable.Prod (CilType.Fundec) (C))
let name () = "FromSpec"
let spec x = `Left x
let call (x, c) = `Right (x, c)
@@ -117,7 +117,7 @@ struct
let name () = "contexts"
end
- include Lattice.Lift2 (G) (CSet) (Printable.DefaultNames)
+ include Lattice.Lift2 (G) (CSet)
let spec = function
| `Bot -> G.bot ()
@@ -142,10 +142,11 @@ exception Deadcode
(** [Dom (D)] produces D lifted where bottom means dead-code *)
module Dom (LD: Lattice.S) =
struct
- include Lattice.Lift (LD) (struct
+ include Lattice.LiftConf (struct
+ include Printable.DefaultConf
let bot_name = "Dead code"
let top_name = "Totally unknown and messed up"
- end)
+ end) (LD)
let lift (x:LD.t) : t = `Lifted x
@@ -155,7 +156,7 @@ struct
| _ -> raise Deadcode
let printXml f = function
- | `Top -> BatPrintf.fprintf f "%s" (XmlUtil.escape top_name)
+ | `Top -> BatPrintf.fprintf f "%s" (XmlUtil.escape Printable.DefaultConf.top_name)
| `Bot -> ()
| `Lifted x -> LD.printXml f x
end
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 77d3a38186..8039a867d8 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -1075,15 +1075,15 @@ module EqIncrSolverFromEqSolver (Sol: GenericEqSolver): GenericEqIncrSolver =
(** Translate a [GlobConstrSys] into a [EqConstrSys] *)
module EqConstrSysFromGlobConstrSys (S:GlobConstrSys)
: EqConstrSys with type v = Var2(S.LVar)(S.GVar).t
- and type d = Lattice.Lift2(S.G)(S.D)(Printable.DefaultNames).t
+ and type d = Lattice.Lift2(S.G)(S.D).t
and module Var = Var2(S.LVar)(S.GVar)
- and module Dom = Lattice.Lift2(S.G)(S.D)(Printable.DefaultNames)
+ and module Dom = Lattice.Lift2(S.G)(S.D)
=
struct
module Var = Var2(S.LVar)(S.GVar)
module Dom =
struct
- include Lattice.Lift2(S.G)(S.D)(Printable.DefaultNames)
+ 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
@@ -1338,7 +1338,7 @@ struct
module V =
struct
- include Printable.Either (S.V) (Node)
+ include Printable.EitherConf (struct let expand1 = false let expand2 = true end) (S.V) (Node)
let name () = "DeadBranch"
let s x = `Left x
let node x = `Right x
@@ -1355,7 +1355,7 @@ struct
module G =
struct
- include Lattice.Lift2 (S.G) (EM) (Printable.DefaultNames)
+ include Lattice.Lift2 (S.G) (EM)
let name () = "deadbranch"
let s = function
@@ -1472,7 +1472,7 @@ struct
module V =
struct
- include Printable.Either3 (S.V) (Printable.Prod (Node) (C)) (Printable.Prod (CilType.Fundec) (C))
+ 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))
let name () = "longjmp"
let s x = `Left x
let longjmpto x = `Middle x
@@ -1484,7 +1484,7 @@ struct
module G =
struct
- include Lattice.Lift2 (S.G) (S.D) (Printable.DefaultNames)
+ include Lattice.Lift2 (S.G) (S.D)
let s = function
| `Bot -> S.G.bot ()
@@ -1737,7 +1737,7 @@ struct
module G =
struct
- include Lattice.Lift2 (G) (CallerSet) (Printable.DefaultNames)
+ include Lattice.Lift2 (G) (CallerSet)
let spec = function
| `Bot -> G.bot ()
diff --git a/src/util/library/libraryDesc.ml b/src/util/library/libraryDesc.ml
index 4997b306a9..78a72b1741 100644
--- a/src/util/library/libraryDesc.ml
+++ b/src/util/library/libraryDesc.ml
@@ -184,7 +184,8 @@ module MathPrintable = struct
)
end
-module MathLifted = Lattice.Flat (MathPrintable) (struct
+module MathLifted = Lattice.FlatConf (struct
+ include Printable.DefaultConf
let top_name = "Unknown or no math desc"
let bot_name = "Nonexistent math desc"
- end)
+ end) (MathPrintable)
diff --git a/src/witness/observerAnalysis.ml b/src/witness/observerAnalysis.ml
index e8daf56155..58b5b31fe4 100644
--- 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.Chain (ChainParams)) (Printable.DefaultNames)
+ module D = Lattice.Flat (Printable.Chain (ChainParams))
module C = D
module P = IdentityP (D) (* fully path-sensitive *)