Remove IntDomain.MakeBooleans

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,23 +27,25 @@ 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
     let name () = "parents"
   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
 

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 *)

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. *)
-*)

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

src/domain/boolDomain.ml

@@ -1,27 +1,46 @@
 (** 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
 
   (* For Lattice.S *)
   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