From 8b35075f3f386e78111a18dc7cbbb7ca23858df9 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 2 Oct 2024 16:51:56 +0300 Subject: [PATCH 1/3] Remove IntDomain.Booleans --- src/analyses/threadReturn.ml | 2 +- src/cdomain/value/cdomains/intDomain.ml | 6 ------ src/cdomain/value/cdomains/intDomain.mli | 4 ---- src/cdomains/lockDomain.ml | 2 +- .../00-sanity/33-hoare-over-paths.t | 20 +++++++++---------- tests/unit/maindomaintest.ml | 3 --- 6 files changed, 12 insertions(+), 25 deletions(-) diff --git a/src/analyses/threadReturn.ml b/src/analyses/threadReturn.ml index f3b9622b00..d72e2586e8 100644 --- a/src/analyses/threadReturn.ml +++ b/src/analyses/threadReturn.ml @@ -12,7 +12,7 @@ struct include Analyses.IdentitySpec let name () = "threadreturn" - module D = IntDomain.Booleans + module D = BoolDomain.MayBool include Analyses.ValueContexts(D) (* transfer functions *) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index a0e9a38f37..1e84e8365d 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -2436,12 +2436,6 @@ struct let invariant _ _ = Invariant.none (* TODO *) end -module Booleans = MakeBooleans ( - struct - let truename = "True" - let falsename = "False" - end) - (* Inclusion/Exclusion sets. Go to top on arithmetic operations (except for some easy cases, e.g. multiplication with 0). Joins on widen, i.e. precise integers as long as not derived from arithmetic expressions. *) module Enums : S with type int_t = Z.t = struct module R = Interval32 (* range for exclusion *) diff --git a/src/cdomain/value/cdomains/intDomain.mli b/src/cdomain/value/cdomains/intDomain.mli index ca64692290..74588b94d8 100644 --- a/src/cdomain/value/cdomains/intDomain.mli +++ b/src/cdomain/value/cdomains/intDomain.mli @@ -452,10 +452,6 @@ end module MakeBooleans (Names: BooleansNames): IkindUnawareS with type t = bool (** Creates an abstract domain for integers represented by boolean values. *) -module Booleans: IkindUnawareS with type t = bool -(** Boolean abstract domain, where true is output "True" and false is output - * "False" *) - (* module None: S with type t = unit (** Domain with nothing in it. *) diff --git a/src/cdomains/lockDomain.ml b/src/cdomains/lockDomain.ml index 08353f4795..b71573d6f6 100644 --- a/src/cdomains/lockDomain.ml +++ b/src/cdomains/lockDomain.ml @@ -42,7 +42,7 @@ struct end (* true means exclusive lock and false represents reader lock*) -module RW = IntDomain.Booleans +module RW = BoolDomain.MayBool (* TODO: name booleans? *) (* pair Addr and RW; also change pretty printing*) module MakeRW (P: Printable.S) = diff --git a/tests/regression/00-sanity/33-hoare-over-paths.t b/tests/regression/00-sanity/33-hoare-over-paths.t index 5148f5e1f2..9f88f836b0 100644 --- a/tests/regression/00-sanity/33-hoare-over-paths.t +++ b/tests/regression/00-sanity/33-hoare-over-paths.t @@ -21,7 +21,7 @@ }, {}, {}, {}), threadid:(wrapper call:unknown node, Thread:[main], created:(current function:bot, callees:bot)), threadflag:Singlethreaded, - threadreturn:True, + threadreturn:true, escape:{}, mutexEvents:(), access:(), @@ -44,7 +44,7 @@ }, {}, {}, {}), threadid:(wrapper call:unknown node, Thread:[main], created:(current function:bot, callees:bot)), threadflag:Singlethreaded, - threadreturn:True, + threadreturn:true, escape:{}, mutexEvents:(), access:(), @@ -66,7 +66,7 @@ }, {}, {}, {}), threadid:(wrapper call:unknown node, Thread:[main], created:(current function:bot, callees:bot)), threadflag:Singlethreaded, - threadreturn:True, + threadreturn:true, escape:{}, mutexEvents:(), access:(), @@ -88,7 +88,7 @@ }, {}, {}, {}), threadid:(wrapper call:unknown node, Thread:[main], created:(current function:bot, callees:bot)), threadflag:Singlethreaded, - threadreturn:True, + threadreturn:true, escape:{}, mutexEvents:(), access:(), @@ -110,7 +110,7 @@ }, {}, {}, {}), threadid:(wrapper call:unknown node, Thread:[main], created:(current function:bot, callees:bot)), threadflag:Singlethreaded, - threadreturn:True, + threadreturn:true, escape:{}, mutexEvents:(), access:(), @@ -132,7 +132,7 @@ }, {}, {}, {}), threadid:(wrapper call:unknown node, Thread:[main], created:(current function:bot, callees:bot)), threadflag:Singlethreaded, - threadreturn:True, + threadreturn:true, escape:{}, mutexEvents:(), access:(), @@ -153,7 +153,7 @@ }, {}, {}, {}), threadid:(wrapper call:unknown node, Thread:[main], created:(current function:bot, callees:bot)), threadflag:Singlethreaded, - threadreturn:True, + threadreturn:true, escape:{}, mutexEvents:(), access:(), @@ -172,7 +172,7 @@ }, {}, {}, {}), threadid:(wrapper call:unknown node, Thread:[main], created:(current function:bot, callees:bot)), threadflag:Singlethreaded, - threadreturn:True, + threadreturn:true, escape:{}, mutexEvents:(), access:(), @@ -194,7 +194,7 @@ }, {}, {}, {}), threadid:(wrapper call:unknown node, Thread:[main], created:(current function:bot, callees:bot)), threadflag:Singlethreaded, - threadreturn:True, + threadreturn:true, escape:{}, mutexEvents:(), access:(), @@ -215,7 +215,7 @@ }, {}, {}, {}), threadid:(wrapper call:unknown node, Thread:[main], created:(current function:bot, callees:bot)), threadflag:Singlethreaded, - threadreturn:True, + threadreturn:true, escape:{}, mutexEvents:(), access:(), diff --git a/tests/unit/maindomaintest.ml b/tests/unit/maindomaintest.ml index 8e1db76b83..4b379a252f 100644 --- a/tests/unit/maindomaintest.ml +++ b/tests/unit/maindomaintest.ml @@ -28,9 +28,6 @@ let domains: (module Lattice.S) list = [ (* (module IntDomainProperties.IntegerSet); (* TODO: top properties error *) *) (module IntDomain.Lifted); (* not abstraction of IntegerSet *) - (* TODO: move to intDomains if passing *) - (module IntDomain.Booleans); - (* TODO: fix *) (* (module IntDomain.Enums); *) (* (module IntDomain.IntDomTuple); *) From f4cc7503d47ae45e2076832150454289a8c28e1b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 2 Oct 2024 17:04:09 +0300 Subject: [PATCH 2/3] Remove Basetype.RawBools --- src/cdomain/value/cdomains/valueDomain.ml | 2 +- src/common/cdomains/basetype.ml | 11 ----------- src/domain/boolDomain.ml | 19 +++++++++++++------ 3 files changed, 14 insertions(+), 18 deletions(-) diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml index 0fbfb50955..f9f4b06ffb 100644 --- a/src/cdomain/value/cdomains/valueDomain.ml +++ b/src/cdomain/value/cdomains/valueDomain.ml @@ -69,7 +69,7 @@ end (* ZeroInit is false if malloc was used to allocate memory and true if calloc was used *) module ZeroInit : ZeroInit = struct - include Lattice.Fake(Basetype.RawBools) + include Lattice.Fake (BoolDomain.Bool) let name () = "zeroinit" let is_malloc x = not x diff --git a/src/common/cdomains/basetype.ml b/src/common/cdomains/basetype.ml index 1b846309aa..bf832b1c3c 100644 --- a/src/common/cdomains/basetype.ml +++ b/src/common/cdomains/basetype.ml @@ -33,17 +33,6 @@ struct let printXml f x = BatPrintf.fprintf f "\n\n%s\n\n\n" (XmlUtil.escape (show x)) end -module RawBools: Printable.S with type t = bool = -struct - include Printable.StdLeaf - open Pretty - type t = bool [@@deriving eq, ord, hash, to_yojson] - let show (x:t) = if x then "true" else "false" - let pretty () x = text (show x) - let name () = "raw bools" - let printXml f x = BatPrintf.fprintf f "\n\n%s\n\n\n" (show x) -end - module CilExp = struct include CilType.Exp diff --git a/src/domain/boolDomain.ml b/src/domain/boolDomain.ml index d92d716d7a..90337f1879 100644 --- a/src/domain/boolDomain.ml +++ b/src/domain/boolDomain.ml @@ -2,13 +2,20 @@ module Bool = struct - include Basetype.RawBools - (* type t = bool - let equal = Bool.equal - let compare = Bool.compare - let relift x = x - let arbitrary () = QCheck.bool *) + include Printable.StdLeaf + type t = bool [@@deriving eq, ord, hash] + let name () = "bool" + let show x = if x then "true" else "false" + include Printable.SimpleShow (struct + type nonrec t = t + let show = show + end) + let to_yojson = [%to_yojson: bool] (* override to_yojson from SimpleShow *) + + let arbitrary () = QCheck.bool + + (* For Lattice.S *) let pretty_diff () (x,y) = GoblintCil.Pretty.dprintf "%s: %a not leq %a" (name ()) pretty x pretty y end From 798a3d8098e8bd35a07882c5ded9b727ae5628d2 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 2 Oct 2024 17:13:31 +0300 Subject: [PATCH 3/3] Remove IntDomain.MakeBooleans --- src/cdomain/value/cdomains/concDomain.ml | 18 +++---- src/cdomain/value/cdomains/intDomain.ml | 60 ------------------------ src/cdomain/value/cdomains/intDomain.mli | 20 -------- src/cdomains/threadFlagDomain.ml | 7 +-- src/domain/boolDomain.ml | 39 ++++++++++++--- 5 files changed, 47 insertions(+), 97 deletions(-) diff --git a/src/cdomain/value/cdomains/concDomain.ml b/src/cdomain/value/cdomains/concDomain.ml index 5f609a31d8..467159c9da 100644 --- a/src/cdomain/value/cdomains/concDomain.ml +++ b/src/cdomain/value/cdomains/concDomain.ml @@ -1,7 +1,7 @@ (** Domains for thread sets and their uniqueness. *) -module ThreadSet = -struct +module ThreadSet = +struct include SetDomain.Make (ThreadIdDomain.Thread) let is_top = mem UnknownThread @@ -27,10 +27,11 @@ module CreatedThreadSet = ThreadSet module ThreadCreation = struct module UNames = struct - let truename = "repeated" - let falsename = "unique" + let name = "unique" + let true_name = "repeated" + let false_name = "unique" end - module Uniqueness = IntDomain.MakeBooleans (UNames) + module Uniqueness = BoolDomain.MakeMayBool (UNames) module ParentThreadSet = struct include ThreadSet @@ -38,12 +39,13 @@ struct end module DirtyExitNames = struct - let truename = "dirty exit" - let falsename = "clean exit" + let name = "exit" + let true_name = "dirty exit" + let false_name = "clean exit" end (* A thread exits cleanly iff it joined all threads it started, and they also all exit cleanly *) - module DirtyExit = IntDomain.MakeBooleans (DirtyExitNames) + module DirtyExit = BoolDomain.MakeMayBool (DirtyExitNames) include Lattice.Prod3 (Uniqueness) (ParentThreadSet) (DirtyExit) end diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 1e84e8365d..e50b3f26cc 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -2376,66 +2376,6 @@ struct let project ik p t = t end -(* BOOLEAN DOMAINS *) - -module type BooleansNames = -sig - val truename: string - val falsename: string -end - -module MakeBooleans (N: BooleansNames) = -struct - type int_t = IntOps.Int64Ops.t - type t = bool [@@deriving eq, ord, hash, to_yojson] - let name () = "booleans" - let top () = true - let bot () = false - let top_of ik = top () - let bot_of ik = bot () - let show x = if x then N.truename else N.falsename - include Std (struct type nonrec t = t let name = name let top_of = top_of let bot_of = bot_of let show = show let equal = equal end) - let is_top x = x (* override Std *) - - let equal_to i x = if x then `Top else failwith "unsupported: equal_to with bottom" - let cast_to ?(suppress_ovwarn=false) ?torg _ x = x (* ok since there's no smaller ikind to cast to *) - - let leq x y = not x || y - let join = (||) - let widen = join - let meet = (&&) - let narrow = meet - - let of_bool x = x - let to_bool x = Some x - let of_int x = x = Int64.zero - let to_int x = if x then None else Some Int64.zero - - let neg x = x - let add x y = x || y - let sub x y = x || y - let mul x y = x && y - let div x y = true - let rem x y = true - let lt n1 n2 = true - let gt n1 n2 = true - let le n1 n2 = true - let ge n1 n2 = true - let eq n1 n2 = true - let ne n1 n2 = true - let lognot x = true - let logand x y = x && y - let logor x y = x || y - let logxor x y = x && not y || not x && y - let shift_left n1 n2 = n1 - let shift_right n1 n2 = n1 - let c_lognot = (not) - let c_logand = (&&) - let c_logor = (||) - let arbitrary () = QCheck.bool - let invariant _ _ = Invariant.none (* TODO *) -end - (* Inclusion/Exclusion sets. Go to top on arithmetic operations (except for some easy cases, e.g. multiplication with 0). Joins on widen, i.e. precise integers as long as not derived from arithmetic expressions. *) module Enums : S with type int_t = Z.t = struct module R = Interval32 (* range for exclusion *) diff --git a/src/cdomain/value/cdomains/intDomain.mli b/src/cdomain/value/cdomains/intDomain.mli index 74588b94d8..e7667c9b14 100644 --- a/src/cdomain/value/cdomains/intDomain.mli +++ b/src/cdomain/value/cdomains/intDomain.mli @@ -436,23 +436,3 @@ module Reverse (Base: IkindUnawareS): IkindUnawareS with type t = Base.t and typ (* module IncExcInterval : S with type t = [ | `Excluded of Interval.t| `Included of Interval.t ] *) (** Inclusive and exclusive intervals. Warning: NOT A LATTICE *) module Enums : S with type int_t = Z.t - -(** {b Boolean domains} *) - -module type BooleansNames = -sig - val truename: string - (** The name of the [true] abstract value *) - - val falsename: string - (** The name of the [false] abstract value *) -end -(** Parameter signature for the [MakeBooleans] functor. *) - -module MakeBooleans (Names: BooleansNames): IkindUnawareS with type t = bool -(** Creates an abstract domain for integers represented by boolean values. *) - -(* -module None: S with type t = unit -(** Domain with nothing in it. *) -*) diff --git a/src/cdomains/threadFlagDomain.ml b/src/cdomains/threadFlagDomain.ml index 80ba9b7a52..42571656e7 100644 --- a/src/cdomains/threadFlagDomain.ml +++ b/src/cdomains/threadFlagDomain.ml @@ -15,10 +15,11 @@ module Trivial: S = struct module TrivialNames = struct - let truename = "Multithreaded" - let falsename = "Singlethreaded" + let name = "MT mode" + let true_name = "Multithreaded" + let false_name = "Singlethreaded" end - include IntDomain.MakeBooleans (TrivialNames) + include BoolDomain.MakeMayBool (TrivialNames) let is_multi x = x let is_not_main x = x diff --git a/src/domain/boolDomain.ml b/src/domain/boolDomain.ml index 90337f1879..18399365a5 100644 --- a/src/domain/boolDomain.ml +++ b/src/domain/boolDomain.ml @@ -1,17 +1,23 @@ (** Boolean domains. *) -module Bool = +module type Names = +sig + val name: string + val true_name: string + val false_name: string +end + +module MakeBool (Names: Names) = struct include Printable.StdLeaf type t = bool [@@deriving eq, ord, hash] - let name () = "bool" + let name () = Names.name - let show x = if x then "true" else "false" + let show x = if x then Names.true_name else Names.false_name include Printable.SimpleShow (struct type nonrec t = t let show = show end) - let to_yojson = [%to_yojson: bool] (* override to_yojson from SimpleShow *) let arbitrary () = QCheck.bool @@ -19,9 +25,22 @@ struct let pretty_diff () (x,y) = GoblintCil.Pretty.dprintf "%s: %a not leq %a" (name ()) pretty x pretty y end -module MayBool: Lattice.S with type t = bool = +module StdNames: Names = struct - include Bool + let name = "bool" + let true_name = "true" + let false_name = "false" +end + +module Bool = +struct + include MakeBool (StdNames) + let to_yojson = [%to_yojson: bool] (* override to_yojson from SimpleShow *) +end + +module MakeMayBool (Names: Names): Lattice.S with type t = bool = +struct + include MakeBool (Names) let bot () = false let is_bot x = x = false let top () = true @@ -33,6 +52,14 @@ struct let narrow = (&&) end +module MayBool: Lattice.S with type t = bool = +struct + include MakeMayBool (StdNames) + let to_yojson = [%to_yojson: bool] (* override to_yojson from SimpleShow *) +end + +(* TODO: MakeMustBool? *) + module MustBool: Lattice.S with type t = bool = struct include Bool