Skip to content

Commit

Permalink
Merge pull request #1588 from goblint/booldomain
Browse files Browse the repository at this point in the history 
Remove `IntDomain.MakeBooleans`
  • Loading branch information
@sim642
sim642 authored Oct 5, 2024
2 parents 4acdae5 + 798a3d8 commit 0deedb9
Show file tree
Hide file tree
Showing 11 changed files with 70 additions and 137 deletions.
2 changes: 1 addition & 1 deletion src/analyses/threadReturn.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand Down
18 changes: 10 additions & 8 deletions src/cdomain/value/cdomains/concDomain.ml
View file
Original file line number Diff line number Diff line change
@@ -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
Expand All @@ -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

Expand Down
66 changes: 0 additions & 66 deletions src/cdomain/value/cdomains/intDomain.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2376,72 +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

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 *)
Expand Down
24 changes: 0 additions & 24 deletions src/cdomain/value/cdomains/intDomain.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -436,27 +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 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. *)
*)
2 changes: 1 addition & 1 deletion src/cdomain/value/cdomains/valueDomain.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/cdomains/lockDomain.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) =
Expand Down
7 changes: 4 additions & 3 deletions src/cdomains/threadFlagDomain.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
11 changes: 0 additions & 11 deletions src/common/cdomains/basetype.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,17 +33,6 @@ struct
let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\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 "<value>\n<data>\n%s\n</data>\n</value>\n" (show x)
end

module CilExp =
struct
include CilType.Exp
Expand Down
52 changes: 43 additions & 9 deletions src/domain/boolDomain.ml
View file
Original file line number Diff line number Diff line change
@@ -1,20 +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 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 () = Names.name

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 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
Expand All @@ -26,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
Expand Down
20 changes: 10 additions & 10 deletions tests/regression/00-sanity/33-hoare-over-paths.t
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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:(),
Expand All @@ -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:(),
Expand All @@ -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:(),
Expand All @@ -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:(),
Expand All @@ -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:(),
Expand All @@ -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:(),
Expand All @@ -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:(),
Expand All @@ -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:(),
Expand All @@ -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:(),
Expand All @@ -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:(),
Expand Down
3 changes: 0 additions & 3 deletions tests/unit/maindomaintest.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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); *)
Expand Down

0 comments on commit 0deedb9

Please sign in to comment.