Merge branch 'master' into loop-unroll-ignore-breaks

conf/svcomp-validate.json

@@ -46,27 +46,6 @@
     "context": {
       "widen": false
     },
-    "malloc": {
-      "wrappers": [
-        "kmalloc",
-        "__kmalloc",
-        "usb_alloc_urb",
-        "__builtin_alloca",
-        "kzalloc",
-
-        "ldv_malloc",
-
-        "kzalloc_node",
-        "ldv_zalloc",
-        "kmalloc_array",
-        "kcalloc",
-
-        "ldv_xmalloc",
-        "ldv_xzalloc",
-        "ldv_calloc",
-        "ldv_kzalloc"
-      ]
-    },
     "base": {
       "arrays": {
         "domain": "partitioned"

conf/svcomp.json

@@ -45,27 +45,6 @@
     "context": {
       "widen": false
     },
-    "malloc": {
-      "wrappers": [
-        "kmalloc",
-        "__kmalloc",
-        "usb_alloc_urb",
-        "__builtin_alloca",
-        "kzalloc",
-
-        "ldv_malloc",
-
-        "kzalloc_node",
-        "ldv_zalloc",
-        "kmalloc_array",
-        "kcalloc",
-
-        "ldv_xmalloc",
-        "ldv_xzalloc",
-        "ldv_calloc",
-        "ldv_kzalloc"
-      ]
-    },
     "base": {
       "arrays": {
         "domain": "partitioned"

goblint.opam

@@ -98,6 +98,10 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
   [ "goblint-cil.2.0.4" "git+https://github.com/goblint/cil.git#9f4fac450c02bc61a13717784515056b185794cd" ]
+  # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new camlidl release
+  [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ]
+  # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
+  [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
 ]
 depexts: [
   ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}

goblint.opam.locked

@@ -142,6 +142,14 @@ pin-depends: [
     "goblint-cil.2.0.4"
     "git+https://github.com/goblint/cil.git#9f4fac450c02bc61a13717784515056b185794cd"
   ]
+  [
+    "camlidl.1.12"
+    "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0"
+  ]
+  [
+    "apron.v0.9.15"
+    "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a"
+  ]
 ]
 depexts: ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}
 description: """\

goblint.opam.template

@@ -3,6 +3,10 @@
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
   [ "goblint-cil.2.0.4" "git+https://github.com/goblint/cil.git#9f4fac450c02bc61a13717784515056b185794cd" ]
+  # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new camlidl release
+  [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ]
+  # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
+  [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
 ]
 depexts: [
   ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}

src/analyses/base.ml

@@ -34,8 +34,6 @@ module MainFunctor (Priv:BasePriv.S) (RVEval:BaseDomain.ExpEvaluator with type t
 struct
   include Analyses.DefaultSpec
 
-  exception Top
-
   module Dom    = BaseDomain.DomFunctor (Priv.D) (RVEval)
   type t = Dom.t
   module D      = Dom

src/analyses/symbLocks.ml

@@ -21,8 +21,6 @@ module Spec =
 struct
   include Analyses.DefaultSpec
 
-  exception Top
-
   module D = SymbLocksDomain.Symbolic
   include Analyses.ValueContexts(D)
 

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

src/analyses/varEq.ml

@@ -11,8 +11,6 @@ open Analyses
 
 module Spec =
 struct
-  exception Top
-
   include Analyses.DefaultSpec
 
   module D =

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

src/cdomain/value/cdomains/intDomain.mli

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

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

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

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/common/cdomains/basetype.ml

@@ -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

src/domain/boolDomain.ml

@@ -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
@@ -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