From f4d6197ee0ea2520b71036557e56e8f90cb635d5 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 14 Dec 2023 15:12:09 +0200 Subject: [PATCH 01/12] Add Printable.EitherConf --- src/analyses/commonPriv.ml | 2 +- src/common/domains/printable.ml | 34 ++++++++++++++++++++++++--------- src/framework/analyses.ml | 4 ++-- src/framework/constraints.ml | 2 +- 4 files changed, 29 insertions(+), 13 deletions(-) diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml index 73a2e75de1..87490a814a 100644 --- a/src/analyses/commonPriv.ml +++ b/src/analyses/commonPriv.ml @@ -173,7 +173,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) diff --git a/src/common/domains/printable.ml b/src/common/domains/printable.ml index cc01718ee8..a1f33efdad 100644 --- a/src/common/domains/printable.ml +++ b/src/common/domains/printable.ml @@ -244,35 +244,51 @@ 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 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 when Conf.expand1 -> Pretty.dprintf "%s:%a" (Base1.name ()) Base1.pretty n + | `Left n -> Base1.pretty () n + | `Right n when Conf.expand2 -> Pretty.dprintf "%s:%a" (Base2.name ()) Base2.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 when Conf.expand1 -> (Base1.name ()) ^ ":" ^ Base1.show n + | `Left n -> Base1.show n + | `Right n when Conf.expand2 -> (Base2.name ()) ^ ":" ^ Base2.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\nLeft\n\n%a\n\n" Base1.printXml x - | `Right x -> BatPrintf.fprintf f "\n\nRight\n\n%a\n\n" Base2.printXml x + | `Left x when Conf.expand1 -> BatPrintf.fprintf f "\n\nLeft\n\n%a\n\n" Base1.printXml x + | `Left x -> Base1.printXml f x + | `Right x when Conf.expand2 -> BatPrintf.fprintf f "\n\nRight\n\n%a\n\n" Base2.printXml 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 when Conf.expand1 -> `Assoc [ Base1.name (), Base1.to_yojson x ] + | `Left x -> Base1.to_yojson x + | `Right x when Conf.expand2 -> `Assoc [ Base2.name (), Base2.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 Either = EitherConf (struct let expand1 = true let expand2 = true end) + module Either3 (Base1: S) (Base2: S) (Base3: S) = struct type t = [`Left of Base1.t | `Middle of Base2.t | `Right of Base3.t] [@@deriving eq, ord, hash] diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index a37a3043c2..44f1f1894e 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) diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 77d3a38186..25b2060e0c 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -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 From 2509d22f2b4254ca69e19dcd0f6cca9a026985aa Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 14 Dec 2023 15:29:53 +0200 Subject: [PATCH 02/12] Add Printable.Either3Conf --- src/common/domains/printable.ml | 46 +++++++++++++++++++++++---------- src/framework/constraints.ml | 2 +- 2 files changed, 34 insertions(+), 14 deletions(-) diff --git a/src/common/domains/printable.ml b/src/common/domains/printable.ml index a1f33efdad..8311dd2ef0 100644 --- a/src/common/domains/printable.ml +++ b/src/common/domains/printable.ml @@ -289,33 +289,51 @@ end module Either = EitherConf (struct let expand1 = true let expand2 = true end) -module Either3 (Base1: S) (Base2: S) (Base3: S) = +module type Either3Conf = +sig + include EitherConf + val expand3: bool +end + +module Either3Conf (Conf: Either3Conf) (Base1: S) (Base2: S) (Base3: S) = struct 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 when Conf.expand1 -> Pretty.dprintf "%s:%a" (Base1.name ()) Base1.pretty n + | `Left n -> Base1.pretty () n + | `Middle n when Conf.expand2 -> Pretty.dprintf "%s:%a" (Base2.name ()) Base2.pretty n + | `Middle n -> Base2.pretty () n + | `Right n when Conf.expand3 -> Pretty.dprintf "%s:%a" (Base3.name ()) Base3.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 when Conf.expand1 -> (Base1.name ()) ^ ":" ^ Base1.show n + | `Left n -> Base1.show n + | `Middle n when Conf.expand2 -> (Base2.name ()) ^ ":" ^ Base2.show n + | `Middle n -> Base2.show n + | `Right n when Conf.expand3 -> (Base3.name ()) ^ ":" ^ Base3.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\nLeft\n\n%a\n\n" Base1.printXml x - | `Middle x -> BatPrintf.fprintf f "\n\nMiddle\n\n%a\n\n" Base2.printXml x - | `Right x -> BatPrintf.fprintf f "\n\nRight\n\n%a\n\n" Base3.printXml x + | `Left x when Conf.expand1 -> BatPrintf.fprintf f "\n\nLeft\n\n%a\n\n" Base1.printXml x + | `Left x -> Base1.printXml f x + | `Middle x when Conf.expand2 -> BatPrintf.fprintf f "\n\nMiddle\n\n%a\n\n" Base2.printXml x + | `Middle x -> Base2.printXml f x + | `Right x when Conf.expand3 -> BatPrintf.fprintf f "\n\nRight\n\n%a\n\n" Base3.printXml 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 when Conf.expand1 -> `Assoc [ Base1.name (), Base1.to_yojson x ] + | `Left x -> Base1.to_yojson x + | `Middle x when Conf.expand2 -> `Assoc [ Base2.name (), Base2.to_yojson x ] + | `Middle x -> Base2.to_yojson x + | `Right x when Conf.expand3 -> `Assoc [ Base3.name (), Base3.to_yojson x ] + | `Right x -> Base3.to_yojson x let relift = function | `Left x -> `Left (Base1.relift x) @@ -323,6 +341,8 @@ struct | `Right x -> `Right (Base3.relift x) end +module Either3 = Either3Conf (struct let expand1 = true let expand2 = true let expand3 = true end) + module Option (Base: S) (N: Name) = struct type t = Base.t option [@@deriving eq, ord, hash] diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 25b2060e0c..ee1ea00a01 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -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 From 38942f96edb2cca3143ff66d19d2ba12ecc0b2fa Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 14 Dec 2023 15:32:20 +0200 Subject: [PATCH 03/12] Remove variant name duplication in privatizations --- src/analyses/basePriv.ml | 12 +----------- src/analyses/commonPriv.ml | 2 -- 2 files changed, 1 insertion(+), 13 deletions(-) diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 0126449413..72854d474d 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 diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml index 87490a814a..0453862bc0 100644 --- a/src/analyses/commonPriv.ml +++ b/src/analyses/commonPriv.ml @@ -74,14 +74,12 @@ 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 From 3d5c65db7de3912c889193132208846d2c990ff9 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 14 Dec 2023 15:48:07 +0200 Subject: [PATCH 04/12] Add Lattice.Lift2Conf --- src/analyses/base.ml | 2 +- src/analyses/basePriv.ml | 2 +- src/analyses/commonPriv.ml | 2 +- src/analyses/mutexAnalysis.ml | 2 +- src/analyses/raceAnalysis.ml | 2 +- src/common/domains/printable.ml | 18 +++++++++++++----- src/domain/lattice.ml | 6 ++++-- 7 files changed, 22 insertions(+), 12 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 7cc937b201..8c4bb67b0b 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 let expand1 = false let expand2 = false end) (Priv.G) (VD) (Printable.DefaultNames) let priv = function | `Bot -> Priv.G.bot () diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 72854d474d..b486dfd552 100644 --- 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.Lift2 (GWeak) (GSync) (Printable.DefaultNames) + include Lattice.Lift2Conf (struct let expand1 = false let expand2 = false end) (GWeak) (GSync) (Printable.DefaultNames) let weak = function | `Bot -> GWeak.bot () diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml index 0453862bc0..1bf03581c2 100644 --- 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 index ee050f55ca..1b52f5dd40 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 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 index 9c2272fabb..241bcb14f8 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 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 index 8311dd2ef0..882cb30bf5 100644 --- a/src/common/domains/printable.ml +++ b/src/common/domains/printable.ml @@ -370,7 +370,7 @@ 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 @@ -378,6 +378,7 @@ struct let pretty () (state:t) = match state with + (* TODO: expand *) | `Lifted1 n -> Base1.pretty () n | `Lifted2 n -> Base2.pretty () n | `Bot -> text bot_name @@ -385,6 +386,7 @@ struct 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 "\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\nLifted1\n\n%a\n\n" Base1.printXml x - | `Lifted2 x -> BatPrintf.fprintf f "\n\n\nLifted2\n\n%a\n\n" Base2.printXml x + | `Lifted1 x when Conf.expand1 -> BatPrintf.fprintf f "\n\n\nLifted1\n\n%a\n\n" Base1.printXml x + | `Lifted1 x -> Base1.printXml f x + | `Lifted2 x when Conf.expand2 -> BatPrintf.fprintf f "\n\n\nLifted2\n\n%a\n\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 index 9ea3f74635..448f801ec1 100644 --- 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) From b71518c7d51ab0bf9444d062ff305895ede10e73 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 14 Dec 2023 16:18:03 +0200 Subject: [PATCH 05/12] Refactor Printable.LiftingNames --- src/analyses/base.ml | 2 +- src/analyses/basePriv.ml | 2 +- src/analyses/commonPriv.ml | 2 +- src/analyses/loopTermination.ml | 2 +- src/analyses/mCPRegistry.ml | 2 +- src/analyses/mutexAnalysis.ml | 2 +- src/analyses/raceAnalysis.ml | 2 +- src/analyses/threadId.ml | 2 +- src/analyses/tutorials/signs.ml | 2 +- src/analyses/wrapperFunctionAnalysis0.ml | 5 +- src/cdomains/intDomain.ml | 10 ++-- src/cdomains/mutexAttrDomain.ml | 2 +- src/cdomains/regionDomain.ml | 2 +- src/cdomains/stackDomain.ml | 2 +- src/cdomains/threadIdDomain.ml | 5 +- src/cdomains/unionDomain.ml | 5 +- src/common/domains/printable.ml | 60 ++++++++++++++---------- src/domain/boolDomain.ml | 5 +- src/domain/lattice.ml | 18 +++---- src/domains/invariant.ml | 3 +- src/domains/queries.ml | 15 +++--- src/domains/valueDomainQueries.ml | 2 +- src/framework/analyses.ml | 9 ++-- src/framework/constraints.ml | 12 ++--- src/util/library/libraryDesc.ml | 5 +- src/witness/observerAnalysis.ml | 2 +- 26 files changed, 101 insertions(+), 79 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 8c4bb67b0b..92ddf3f12b 100644 --- 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 index b486dfd552..10deaa4d16 100644 --- 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 index 1bf03581c2..35b801e32b 100644 --- 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 index 10e0f5c5f4..66cbd5772f 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 (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 index 5d0174d44c..a685b31798 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.Lift (Printable.DefaultConf) (DomVariantLattice0 (DLSpec)) let name () = "MCP.G" end diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 1b52f5dd40..a13c8d6bfd 100644 --- 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 index 241bcb14f8..f35e6756a1 100644 --- 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 index da2c688ad1..f954077836 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.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 index 31168df86a..6ba720d0ea 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 (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 index 9ea9c0c9aa..ba04c7ed7f 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.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 index 5d5174744f..23f4d88e25 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.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 index 748ede0ff5..b7c18a3cae 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.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 index 681eb79007..b0f8d5d57e 100644 --- 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 index 3a83c78503..bd77a7d82f 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.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 index d0c3f7b61b..ed9ad2c854 100644 --- 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 index ac25450c6a..9871b95e1b 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.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 index 882cb30bf5..d52f6a4d2a 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,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 "\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 @@ -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 "\n\n%s\n\n\n" N.bot_name - | `Top -> BatPrintf.fprintf f "\n\n%s\n\n\n" N.top_name + | `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 when Conf.expand1 -> BatPrintf.fprintf f "\n\n\nLifted1\n\n%a\n\n" Base1.printXml x | `Lifted1 x -> Base1.printXml f x | `Lifted2 x when Conf.expand2 -> BatPrintf.fprintf f "\n\n\nLifted2\n\n%a\n\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 index 08be66a602..a4bd45c052 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.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 index 448f801ec1..0d21a1a320 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 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 index 1a0c3c033c..d719f8b9c1 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.Lift (N) (ExpLat) let none = top () let of_exp = lift diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 228320bef3..526e82cb5e 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -17,26 +17,29 @@ module TC = WrapperFunctionAnalysis0.ThreadCreateUniqueCount module ThreadNodeLattice = Lattice.Prod (NFL) (TC) module ML = LibraryDesc.MathLifted -module VI = Lattice.Flat (Basetype.Variables) (struct +module VI = Lattice.Flat (struct + include Printable.DefaultConf let top_name = "Unknown line" let bot_name = "Unreachable line" - end) + end) (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 +module FlatYojson = Lattice.Flat (struct + include Printable.DefaultConf let top_name = "top yojson" let bot_name = "bot yojson" - end) + end) (Printable.Yojson) module SD: Lattice.S with type t = [`Bot | `Lifted of string | `Top] = - Lattice.Flat (Basetype.RawStrings) (struct + Lattice.Flat (struct + include Printable.DefaultConf let top_name = "?" let bot_name = "-" - end) + end) (Basetype.RawStrings) module VD = ValueDomain.Compound module AD = ValueDomain.AD diff --git a/src/domains/valueDomainQueries.ml b/src/domains/valueDomainQueries.ml index 8266582ac2..b7644a32ed 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 (Printable.DefaultConf) (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 44f1f1894e..6734b67121 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -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.Lift (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 ee1ea00a01..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 @@ -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 @@ -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..a07c0ee27f 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.Flat (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..d4af989ebc 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.DefaultConf) (Printable.Chain (ChainParams)) module C = D module P = IdentityP (D) (* fully path-sensitive *) From ea029bc5b13f1a50772c7d053ad0aec0e2cec8cc Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 14 Dec 2023 16:29:23 +0200 Subject: [PATCH 06/12] Simplify default Lattice.Flat usage --- src/analyses/loopTermination.ml | 2 +- src/analyses/mCPRegistry.ml | 2 +- src/analyses/threadId.ml | 2 +- src/analyses/tutorials/signs.ml | 2 +- src/analyses/wrapperFunctionAnalysis0.ml | 2 +- src/cdomains/intDomain.ml | 2 +- src/cdomains/mutexAttrDomain.ml | 2 +- src/cdomains/regionDomain.ml | 2 +- src/cdomains/stackDomain.ml | 2 +- src/cdomains/threadIdDomain.ml | 2 +- src/cdomains/unionDomain.ml | 2 +- src/common/domains/printable.ml | 7 +++---- src/domain/boolDomain.ml | 2 +- src/domain/lattice.ml | 8 ++++++-- src/domains/invariant.ml | 2 +- src/domains/queries.ml | 18 +++--------------- src/domains/valueDomainQueries.ml | 2 +- src/framework/analyses.ml | 2 +- src/util/library/libraryDesc.ml | 2 +- src/witness/observerAnalysis.ml | 2 +- 20 files changed, 29 insertions(+), 38 deletions(-) diff --git a/src/analyses/loopTermination.ml b/src/analyses/loopTermination.ml index 66cbd5772f..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 (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 index a685b31798..663a1d8862 100644 --- 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 index f954077836..86e7f770a8 100644 --- 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 index 6ba720d0ea..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 (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 index ba04c7ed7f..cd5940011e 100644 --- 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 index 23f4d88e25..376dab71c2 100644 --- 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 index b7c18a3cae..ea9696d26f 100644 --- 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 index b0f8d5d57e..26a89f1013 100644 --- 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 index bd77a7d82f..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 (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 index ed9ad2c854..c21bb40628 100644 --- 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 index 9871b95e1b..ad5c531061 100644 --- 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 index d52f6a4d2a..37dd88f9ac 100644 --- 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 index a4bd45c052..d92d716d7a 100644 --- 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 index 0d21a1a320..99322c09d8 100644 --- 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 index d719f8b9c1..b281e8f7b3 100644 --- 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 index 526e82cb5e..24e5d45593 100644 --- 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 index b7644a32ed..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 (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 index 6734b67121..405df5b6a6 100644 --- 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 index a07c0ee27f..78a72b1741 100644 --- 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 index d4af989ebc..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.DefaultConf) (Printable.Chain (ChainParams)) + module D = Lattice.Flat (Printable.Chain (ChainParams)) module C = D module P = IdentityP (D) (* fully path-sensitive *) From dceb4bea539b167647066346679cab4a0e168987 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 15 Dec 2023 10:56:20 +0200 Subject: [PATCH 07/12] Extract Printable.PrefixName functor to deduplicate expand code --- src/common/domains/printable.ml | 77 ++++++++++++++++++++++----------- 1 file changed, 51 insertions(+), 26 deletions(-) diff --git a/src/common/domains/printable.ml b/src/common/domains/printable.ml index 37dd88f9ac..7e08157898 100644 --- a/src/common/domains/printable.ml +++ b/src/common/domains/printable.ml @@ -184,6 +184,41 @@ struct end +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%s\n\n%a\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 @@ -257,34 +292,31 @@ 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 when Conf.expand1 -> Pretty.dprintf "%s:%a" (Base1.name ()) Base1.pretty n | `Left n -> Base1.pretty () n - | `Right n when Conf.expand2 -> Pretty.dprintf "%s:%a" (Base2.name ()) Base2.pretty n | `Right n -> Base2.pretty () n let show state = match state with - | `Left n when Conf.expand1 -> (Base1.name ()) ^ ":" ^ Base1.show n | `Left n -> Base1.show n - | `Right n when Conf.expand2 -> (Base2.name ()) ^ ":" ^ Base2.show n | `Right n -> Base2.show n let name () = "either " ^ Base1.name () ^ " or " ^ Base2.name () let printXml f = function - | `Left x when Conf.expand1 -> BatPrintf.fprintf f "\n\nLeft\n\n%a\n\n" Base1.printXml x | `Left x -> Base1.printXml f x - | `Right x when Conf.expand2 -> BatPrintf.fprintf f "\n\nRight\n\n%a\n\n" Base2.printXml x | `Right x -> Base2.printXml f x let to_yojson = function - | `Left x when Conf.expand1 -> `Assoc [ Base1.name (), Base1.to_yojson x ] | `Left x -> Base1.to_yojson x - | `Right x when Conf.expand2 -> `Assoc [ Base2.name (), Base2.to_yojson x ] | `Right x -> Base2.to_yojson x let relift = function @@ -302,42 +334,36 @@ 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 when Conf.expand1 -> Pretty.dprintf "%s:%a" (Base1.name ()) Base1.pretty n | `Left n -> Base1.pretty () n - | `Middle n when Conf.expand2 -> Pretty.dprintf "%s:%a" (Base2.name ()) Base2.pretty n | `Middle n -> Base2.pretty () n - | `Right n when Conf.expand3 -> Pretty.dprintf "%s:%a" (Base3.name ()) Base3.pretty n | `Right n -> Base3.pretty () n let show state = match state with - | `Left n when Conf.expand1 -> (Base1.name ()) ^ ":" ^ Base1.show n | `Left n -> Base1.show n - | `Middle n when Conf.expand2 -> (Base2.name ()) ^ ":" ^ Base2.show n | `Middle n -> Base2.show n - | `Right n when Conf.expand3 -> (Base3.name ()) ^ ":" ^ Base3.show n | `Right n -> Base3.show n let name () = "either " ^ Base1.name () ^ " or " ^ Base2.name () ^ " or " ^ Base3.name () let printXml f = function - | `Left x when Conf.expand1 -> BatPrintf.fprintf f "\n\nLeft\n\n%a\n\n" Base1.printXml x | `Left x -> Base1.printXml f x - | `Middle x when Conf.expand2 -> BatPrintf.fprintf f "\n\nMiddle\n\n%a\n\n" Base2.printXml x | `Middle x -> Base2.printXml f x - | `Right x when Conf.expand3 -> BatPrintf.fprintf f "\n\nRight\n\n%a\n\n" Base3.printXml x | `Right x -> Base3.printXml f x let to_yojson = function - | `Left x when Conf.expand1 -> `Assoc [ Base1.name (), Base1.to_yojson x ] | `Left x -> Base1.to_yojson x - | `Middle x when Conf.expand2 -> `Assoc [ Base2.name (), Base2.to_yojson x ] | `Middle x -> Base2.to_yojson x - | `Right x when Conf.expand3 -> `Assoc [ Base3.name (), Base3.to_yojson x ] | `Right x -> Base3.to_yojson x let relift = function @@ -383,13 +409,17 @@ 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 open Conf let pretty () (state:t) = match state with - (* TODO: expand *) | `Lifted1 n -> Base1.pretty () n | `Lifted2 n -> Base2.pretty () n | `Bot -> text bot_name @@ -397,7 +427,6 @@ struct let show state = match state with - (* TODO: expand *) | `Lifted1 n -> Base1.show n | `Lifted2 n -> Base2.show n | `Bot -> bot_name @@ -412,17 +441,13 @@ struct let printXml f = function | `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 when Conf.expand1 -> BatPrintf.fprintf f "\n\n\nLifted1\n\n%a\n\n" Base1.printXml x | `Lifted1 x -> Base1.printXml f x - | `Lifted2 x when Conf.expand2 -> BatPrintf.fprintf f "\n\n\nLifted2\n\n%a\n\n" Base2.printXml x | `Lifted2 x -> Base2.printXml f x let to_yojson = function | `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 From cc39ddd112604c30aeffef657ae1c8e6b63064d5 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 15 Dec 2023 11:05:30 +0200 Subject: [PATCH 08/12] Use Conf in Printable.LiftConf --- src/analyses/mCPRegistry.ml | 2 +- src/common/domains/printable.ml | 4 ++++ 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/src/analyses/mCPRegistry.ml b/src/analyses/mCPRegistry.ml index 663a1d8862..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)) + include Lattice.LiftConf (struct include Printable.DefaultConf let expand1 = false end) (DomVariantLattice0 (DLSpec)) let name () = "MCP.G" end diff --git a/src/common/domains/printable.ml b/src/common/domains/printable.ml index 7e08157898..0b1769e99c 100644 --- a/src/common/domains/printable.ml +++ b/src/common/domains/printable.ml @@ -237,6 +237,10 @@ 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 open Conf From 318f2c2d787d2f41f58528f6f95329396907bf8a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 15 Dec 2023 11:19:06 +0200 Subject: [PATCH 09/12] Do not expand MUTEX_INITS unknown --- src/analyses/commonPriv.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml index 35b801e32b..90e5b28f82 100644 --- a/src/analyses/commonPriv.ml +++ b/src/analyses/commonPriv.ml @@ -83,7 +83,7 @@ struct 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 () From c1e1632a2641def5717602bf553c5086f70d4c90 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 15 Dec 2023 11:19:21 +0200 Subject: [PATCH 10/12] Simplify RegionDomain.VFB printing --- src/cdomains/regionDomain.ml | 16 +--------------- 1 file changed, 1 insertion(+), 15 deletions(-) diff --git a/src/cdomains/regionDomain.ml b/src/cdomains/regionDomain.ml index 26a89f1013..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 From bbe86ae4fc521aa510a7fe7952f64f9295a60086 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 15 Dec 2023 11:27:46 +0200 Subject: [PATCH 11/12] Simplify SymbLocks.A.E printing --- src/analyses/symbLocks.ml | 12 ++++++------ src/cdomains/symbLocksDomain.ml | 1 + 2 files changed, 7 insertions(+), 6 deletions(-) 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/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 From 152b54baa51e85b54452b82011e17178f7ce00ce Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 15 Dec 2023 11:34:18 +0200 Subject: [PATCH 12/12] Do not expand lifted thread ID --- src/cdomains/threadIdDomain.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/cdomains/threadIdDomain.ml b/src/cdomains/threadIdDomain.ml index c21bb40628..85f9a0297b 100644 --- a/src/cdomains/threadIdDomain.ml +++ b/src/cdomains/threadIdDomain.ml @@ -199,6 +199,7 @@ 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