Merge branch 'master' into traces-vojdani

goblint · Sep 6, 2024 · 1e70e33 · 1e70e33
2 parents 0c29208 + f27ae52
commit 1e70e33
Show file tree

Hide file tree

Showing 47 changed files with 1,033 additions and 317 deletions.
diff --git a/dune-project b/dune-project
@@ -45,6 +45,7 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e
     (ppx_deriving (>= 6.0.2))
     (ppx_deriving_hash (>= 0.1.2))
     (ppx_deriving_yojson (>= 3.7.0))
+    (ppxlib (>= 0.30.0)) ; ppx_easy_deriving
     (ounit2 :with-test)
     (qcheck-ounit :with-test)
     (odoc :with-doc)

diff --git a/goblint.opam b/goblint.opam
@@ -45,6 +45,7 @@ depends: [
   "ppx_deriving" {>= "6.0.2"}
   "ppx_deriving_hash" {>= "0.1.2"}
   "ppx_deriving_yojson" {>= "3.7.0"}
+  "ppxlib" {>= "0.30.0"}
   "ounit2" {with-test}
   "qcheck-ounit" {with-test}
   "odoc" {with-doc}
@@ -93,13 +94,17 @@ build: [
 dev-repo: "git+https://github.com/goblint/analyzer.git"
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
-available: os-family != "bsd" & os-distribution != "alpine"
+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#317e26d48b06d5cdc4acff3df1a6824587052b53" ]
+  [ "goblint-cil.2.0.4" "git+https://github.com/goblint/cil.git#04b8a45a7d20425c7b6c8abe1ad094abc063922b" ]
 ]
 depexts: [
   ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}
 ]
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]
+x-ci-accept-failures: [
+  "macos-homebrew" # newer MacOS headers cannot be parsed (https://github.com/ocaml/opam-repository/pull/26307#issuecomment-2258080206)
+  "opensuse-tumbleweed" # not GNU diff, so some cram tests fail (https://discuss.ocaml.org/t/opensuse-and-opam-tests/14641/2)
+]
diff --git a/goblint.opam.locked b/goblint.opam.locked
@@ -128,7 +128,7 @@ build: [
   ["dune" "install" "-p" name "--create-install-files" name]
 ]
 dev-repo: "git+https://github.com/goblint/analyzer.git"
-available: os-family != "bsd" & os-distribution != "alpine"
+available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 conflicts: [
   "result" {< "1.5"}
   "ez-conf-lib" {= "1"}
@@ -139,7 +139,7 @@ post-messages: [
 pin-depends: [
   [
     "goblint-cil.2.0.4"
-    "git+https://github.com/goblint/cil.git#317e26d48b06d5cdc4acff3df1a6824587052b53"
+    "git+https://github.com/goblint/cil.git#04b8a45a7d20425c7b6c8abe1ad094abc063922b"
   ]
 ]
 depexts: ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}

diff --git a/goblint.opam.template b/goblint.opam.template
@@ -1,12 +1,16 @@
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
-available: os-family != "bsd" & os-distribution != "alpine"
+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#317e26d48b06d5cdc4acff3df1a6824587052b53" ]
+  [ "goblint-cil.2.0.4" "git+https://github.com/goblint/cil.git#04b8a45a7d20425c7b6c8abe1ad094abc063922b" ]
 ]
 depexts: [
   ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}
 ]
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]
+x-ci-accept-failures: [
+  "macos-homebrew" # newer MacOS headers cannot be parsed (https://github.com/ocaml/opam-repository/pull/26307#issuecomment-2258080206)
+  "opensuse-tumbleweed" # not GNU diff, so some cram tests fail (https://discuss.ocaml.org/t/opensuse-and-opam-tests/14641/2)
+]
diff --git a/scripts/goblint-lib-modules.py b/scripts/goblint-lib-modules.py
@@ -42,6 +42,10 @@
     "Goblint_build_info",
     "Dune_build_info",
 
+    # ppx-s
+    "Ppx_deriving_printable",
+    "Ppx_deriving_lattice",
+
     "MessageCategory", # included in Messages
     "PreValueDomain", # included in ValueDomain
 

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -2168,7 +2168,7 @@ struct
       end
     | _, _ when get_bool "sem.unknown_function.spawn" ->
       (* TODO: Remove sem.unknown_function.spawn check because it is (and should be) really done in LibraryFunctions.
-         But here we consider all non-ThreadCrate functions also unknown, so old-style LibraryFunctions access
+         But here we consider all non-ThreadCreate functions also unknown, so old-style LibraryFunctions access
          definitions using `Write would still spawn because they are not truly unknown functions (missing from LibraryFunctions).
          Need this to not have memmove spawn in SV-COMP. *)
       let shallow_args = LibraryDesc.Accesses.find desc.accs { kind = Spawn; deep = false } args in

diff --git a/src/cdomain/value/cdomains/floatDomain.ml b/src/cdomain/value/cdomains/floatDomain.ml
@@ -1134,7 +1134,7 @@ module FloatDomTupleImpl = struct
   module F1 = FloatIntervalImplLifted
   open Batteries
 
-  type t = F1.t option [@@deriving to_yojson, eq, ord]
+  type t = F1.t option [@@deriving eq, ord, hash]
 
   let name () = "floatdomtuple"
 
@@ -1181,10 +1181,6 @@ module FloatDomTupleImpl = struct
     Option.map_default identity ""
       (mapp { fp= (fun (type a) (module F : FloatDomain with type t = a) x -> F.name () ^ ":" ^ F.show x); } x)
 
-  let hash x =
-    Option.map_default identity 0
-      (mapp { fp= (fun (type a) (module F : FloatDomain with type t = a) -> F.hash); } x)
-
   let of_const fkind =
     create { fi= (fun (type a) (module F : FloatDomain with type t = a) -> F.of_const fkind); }
 

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
@@ -582,6 +582,59 @@ module IntervalArith (Ints_t : IntOps.IntOps) = struct
     List.exists (Z.equal l) ts
 end
 
+module IntInvariant =
+struct
+  let of_int e ik x =
+    if get_bool "witness.invariant.exact" then
+      Invariant.of_exp Cil.(BinOp (Eq, e, kintegerCilint ik x, intType))
+    else
+      Invariant.none
+
+  let of_incl_list e ik ps =
+    match ps with
+    | [_; _] when ik = IBool && not (get_bool "witness.invariant.inexact-type-bounds") ->
+      assert (List.mem Z.zero ps);
+      assert (List.mem Z.one ps);
+      Invariant.none
+    | [_] when get_bool "witness.invariant.exact" ->
+      Invariant.none
+    | _ :: _ :: _
+    | [_] | [] ->
+      List.fold_left (fun a x ->
+          let i = Invariant.of_exp Cil.(BinOp (Eq, e, kintegerCilint ik x, intType)) in
+          Invariant.(a || i) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
+        ) (Invariant.bot ()) ps
+
+  let of_interval_opt e ik = function
+    | (Some x1, Some x2) when Z.equal x1 x2 ->
+      of_int e ik x1
+    | x1_opt, x2_opt ->
+      let (min_ik, max_ik) = Size.range ik in
+      let inexact_type_bounds = get_bool "witness.invariant.inexact-type-bounds" in
+      let i1 =
+        match x1_opt, inexact_type_bounds with
+        | Some x1, false when Z.equal min_ik x1 -> Invariant.none
+        | Some x1, _ -> Invariant.of_exp Cil.(BinOp (Le, kintegerCilint ik x1, e, intType))
+        | None, _ -> Invariant.none
+      in
+      let i2 =
+        match x2_opt, inexact_type_bounds with
+        | Some x2, false when Z.equal x2 max_ik -> Invariant.none
+        | Some x2, _ -> Invariant.of_exp Cil.(BinOp (Le, e, kintegerCilint ik x2, intType))
+        | None, _ -> Invariant.none
+      in
+      Invariant.(i1 && i2)
+
+  let of_interval e ik (x1, x2) =
+    of_interval_opt e ik (Some x1, Some x2)
+
+  let of_excl_list e ik ns =
+    List.fold_left (fun a x ->
+        let i = Invariant.of_exp Cil.(BinOp (Ne, e, kintegerCilint ik x, intType)) in
+        Invariant.(a && i)
+      ) (Invariant.top ()) ns
+end
+
 module IntervalFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) option =
 struct
   let name () = "intervals"
@@ -915,21 +968,10 @@ struct
       else if Ints_t.compare y2 x1 <= 0 then of_bool ik false
       else top_bool
 
-  let invariant_ikind e ik x =
-    match x with
-    | Some (x1, x2) when Ints_t.compare x1 x2 = 0 ->
-      if get_bool "witness.invariant.exact" then
-        let x1 = Ints_t.to_bigint x1 in
-        Invariant.of_exp Cil.(BinOp (Eq, e, kintegerCilint ik x1, intType))
-      else
-        Invariant.top ()
+  let invariant_ikind e ik = function
     | Some (x1, x2) ->
-      let (min_ik, max_ik) = range ik in
-      let (x1', x2') = BatTuple.Tuple2.mapn (Ints_t.to_bigint) (x1, x2) in
-      let inexact_type_bounds = get_bool "witness.invariant.inexact-type-bounds" in
-      let i1 = if inexact_type_bounds || Ints_t.compare min_ik x1 <> 0 then Invariant.of_exp Cil.(BinOp (Le, kintegerCilint ik x1', e, intType)) else Invariant.none in
-      let i2 = if inexact_type_bounds || Ints_t.compare x2 max_ik <> 0 then Invariant.of_exp Cil.(BinOp (Le, e, kintegerCilint ik x2', intType)) else Invariant.none in
-      Invariant.(i1 && i2)
+      let (x1', x2') = BatTuple.Tuple2.mapn Ints_t.to_bigint (x1, x2) in
+      IntInvariant.of_interval e ik (x1', x2')
     | None -> Invariant.none
 
   let arbitrary ik =
@@ -2297,25 +2339,14 @@ struct
   let invariant_ikind e ik (x:t) =
     match x with
     | `Definite x ->
-      if get_bool "witness.invariant.exact" then
-        Invariant.of_exp Cil.(BinOp (Eq, e, kintegerCilint ik x, intType))
-      else
-        Invariant.top ()
+      IntInvariant.of_int e ik x
     | `Excluded (s, r) ->
       (* Emit range invariant if tighter than ikind bounds.
          This can be more precise than interval, which has been widened. *)
       let (rmin, rmax) = (Exclusion.min_of_range r, Exclusion.max_of_range r) in
-      let (ikmin, ikmax) =
-        let ikr = size ik in
-        (Exclusion.min_of_range ikr, Exclusion.max_of_range ikr)
-      in
-      let inexact_type_bounds = get_bool "witness.invariant.inexact-type-bounds" in
-      let imin = if inexact_type_bounds || Z.compare ikmin rmin <> 0 then Invariant.of_exp Cil.(BinOp (Le, kintegerCilint ik rmin, e, intType)) else Invariant.none in
-      let imax = if inexact_type_bounds || Z.compare rmax ikmax <> 0 then Invariant.of_exp Cil.(BinOp (Le, e, kintegerCilint ik rmax, intType)) else Invariant.none in
-      S.fold (fun x a ->
-          let i = Invariant.of_exp Cil.(BinOp (Ne, e, kintegerCilint ik x, intType)) in
-          Invariant.(a && i)
-        ) s Invariant.(imin && imax)
+      let ri = IntInvariant.of_interval e ik (rmin, rmax) in
+      let si = IntInvariant.of_excl_list e ik (S.elements s) in
+      Invariant.(ri && si)
     | `Bot -> Invariant.none
 
   let arbitrary ik =
@@ -2731,32 +2762,16 @@ module Enums : S with type int_t = Z.t = struct
   let ne ik x y = c_lognot ik (eq ik x y)
 
   let invariant_ikind e ik x =
-    let inexact_type_bounds = get_bool "witness.invariant.inexact-type-bounds" in
     match x with
-    | Inc ps when not inexact_type_bounds && ik = IBool && is_top_of ik x ->
-      Invariant.none
     | Inc ps ->
-      if BISet.cardinal ps > 1 || get_bool "witness.invariant.exact" then
-        BISet.fold (fun x a ->
-            let i = Invariant.of_exp Cil.(BinOp (Eq, e, kintegerCilint ik x, intType)) in
-            Invariant.(a || i) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
-          ) ps (Invariant.bot ())
-      else
-        Invariant.top ()
+      IntInvariant.of_incl_list e ik (BISet.elements ps)
     | Exc (ns, r) ->
       (* Emit range invariant if tighter than ikind bounds.
          This can be more precise than interval, which has been widened. *)
       let (rmin, rmax) = (Exclusion.min_of_range r, Exclusion.max_of_range r) in
-      let (ikmin, ikmax) =
-        let ikr = size ik in
-        (Exclusion.min_of_range ikr, Exclusion.max_of_range ikr)
-      in
-      let imin = if inexact_type_bounds || Z.compare ikmin rmin <> 0 then Invariant.of_exp Cil.(BinOp (Le, kintegerCilint ik rmin, e, intType)) else Invariant.none in
-      let imax = if inexact_type_bounds || Z.compare rmax ikmax <> 0 then Invariant.of_exp Cil.(BinOp (Le, e, kintegerCilint ik rmax, intType)) else Invariant.none in
-      BISet.fold (fun x a ->
-          let i = Invariant.of_exp Cil.(BinOp (Ne, e, kintegerCilint ik x, intType)) in
-          Invariant.(a && i)
-        ) ns Invariant.(imin && imax)
+      let ri = IntInvariant.of_interval e ik (rmin, rmax) in
+      let nsi = IntInvariant.of_excl_list e ik (BISet.elements ns) in
+      Invariant.(ri && nsi)
 
 
   let arbitrary ik =
@@ -2779,7 +2794,7 @@ module Enums : S with type int_t = Z.t = struct
     | Inc e, Some (c, m) -> Inc (BISet.filter (contains c m) e)
     | _ -> a
 
-  let refine_with_interval ik a b = a
+  let refine_with_interval ik a b = a (* TODO: refine inclusion (exclusion?) set *)
 
   let refine_with_excl_list ik a b =
     match b with
@@ -3243,10 +3258,7 @@ struct
     match x with
     | x when is_top x -> Invariant.top ()
     | Some (c, m) when m =: Z.zero ->
-      if get_bool "witness.invariant.exact" then
-        Invariant.of_exp Cil.(BinOp (Eq, e, Cil.kintegerCilint ik c, intType))
-      else
-        Invariant.top ()
+      IntInvariant.of_int e ik c
     | Some (c, m) ->
       let open Cil in
       let (c, m) = BatTuple.Tuple2.mapn (fun a -> kintegerCilint ik a) (c, m) in
@@ -3338,7 +3350,7 @@ module IntDomTupleImpl = struct
   module I5 = IntervalSetFunctor (IntOps.BigIntOps)
 
   type t = I1.t option * I2.t option * I3.t option * I4.t option * I5.t option
-  [@@deriving to_yojson, eq, ord]
+  [@@deriving eq, ord, hash]
 
   let name () = "intdomtuple"
 
@@ -3524,7 +3536,7 @@ module IntDomTupleImpl = struct
     let merge ps =
       let (vs, rs) = List.split ps in
       let (mins, maxs) = List.split rs in
-      (List.concat vs, (List.min mins, List.max maxs))
+      (List.concat vs |> List.sort_uniq Z.compare, (List.min mins, List.max maxs))
     in
     mapp2 { fp2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.to_excl_list } x |> flat merge
 
@@ -3565,7 +3577,7 @@ module IntDomTupleImpl = struct
     in
     [(fun (a, b, c, d, e) -> refine_with_excl_list ik (a, b, c, d, e) (to_excl_list (a, b, c, d, e)));
      (fun (a, b, c, d, e) -> refine_with_incl_list ik (a, b, c, d, e) (to_incl_list (a, b, c, d, e)));
-     (fun (a, b, c, d, e) -> maybe refine_with_interval ik (a, b, c, d, e) b);
+     (fun (a, b, c, d, e) -> maybe refine_with_interval ik (a, b, c, d, e) b); (* TODO: get interval across all domains with minimal and maximal *)
      (fun (a, b, c, d, e) -> maybe refine_with_congruence ik (a, b, c, d, e) d)]
 
   let refine ik ((a, b, c, d, e) : t ) : t =
@@ -3665,7 +3677,6 @@ module IntDomTupleImpl = struct
            |> to_list
            |> String.concat "; "
   let to_yojson = [%to_yojson: Yojson.Safe.t list] % to_list % mapp { fp = fun (type a) (module I:SOverflow with type t = a) x -> I.to_yojson x }
-  let hash = List.fold_left (lxor) 0 % to_list % mapp { fp = fun (type a) (module I:SOverflow with type t = a) -> I.hash }
 
   (* `map/opt_map` are used by `project` *)
   let opt_map b f =
@@ -3778,19 +3789,47 @@ module IntDomTupleImpl = struct
     | Some v when not (GobConfig.get_bool "dbg.full-output") -> BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (Z.to_string v)
     | _ -> BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (show x)
 
-  let invariant_ikind e ik x =
-    match to_int x with
-    | Some v ->
-      if get_bool "witness.invariant.exact" then
-        (* If definite, output single equality instead of every subdomain repeating same equality *)
-        Invariant.of_exp Cil.(BinOp (Eq, e, kintegerCilint ik v, intType))
-      else
-        Invariant.top ()
-    | None ->
-      let is = to_list (mapp { fp = fun (type a) (module I:SOverflow with type t = a) -> I.invariant_ikind e ik } x)
-      in List.fold_left (fun a i ->
+  let invariant_ikind e ik ((_, _, _, x_cong, x_intset) as x) =
+    (* TODO: do refinement before to ensure incl_list being more precise than intervals, etc (https://github.com/goblint/analyzer/pull/1517#discussion_r1693998515), requires refine functions to actually refine that *)
+    let simplify_int fallback =
+      match to_int x with
+      | Some v ->
+        (* If definite, output single equality instead of every subdomain repeating same equality (or something less precise). *)
+        IntInvariant.of_int e ik v
+      | None ->
+        fallback ()
+    in
+    let simplify_all () =
+      match to_incl_list x with
+      | Some ps ->
+        (* If inclusion set, output disjunction of equalities because it subsumes interval(s), exclusion set and congruence. *)
+        IntInvariant.of_incl_list e ik ps
+      | None ->
+        (* Get interval bounds from all domains (intervals and exclusion set ranges). *)
+        let min = minimal x in
+        let max = maximal x in
+        let ns = Option.map fst (to_excl_list x) |? [] in (* Ignore exclusion set bit range, known via interval bounds already. *)
+        (* "Refine" out-of-bounds exclusions for simpler output. *)
+        let ns = Option.map_default (fun min -> List.filter (Z.leq min) ns) ns min in
+        let ns = Option.map_default (fun max -> List.filter (Z.geq max) ns) ns max in
+        Invariant.(
+          IntInvariant.of_interval_opt e ik (min, max) && (* Output best interval bounds once instead of multiple subdomains repeating them (or less precise ones). *)
+          IntInvariant.of_excl_list e ik ns &&
+          Option.map_default (I4.invariant_ikind e ik) Invariant.none x_cong && (* Output congruence as is. *)
+          Option.map_default (I5.invariant_ikind e ik) Invariant.none x_intset (* Output interval sets as is. *)
+        )
+    in
+    let simplify_none () =
+      let is = to_list (mapp { fp = fun (type a) (module I:SOverflow with type t = a) -> I.invariant_ikind e ik } x) in
+      List.fold_left (fun a i ->
           Invariant.(a && i)
         ) (Invariant.top ()) is
+    in
+    match GobConfig.get_string "ana.base.invariant.int.simplify" with
+    | "none" -> simplify_none ()
+    | "int" -> simplify_int simplify_none
+    | "all" -> simplify_int simplify_all
+    | _ -> assert false
 
   let arbitrary ik = QCheck.(set_print show @@ tup5 (option (I1.arbitrary ik)) (option (I2.arbitrary ik)) (option (I3.arbitrary ik)) (option (I4.arbitrary ik)) (option (I5.arbitrary ik)))
 

diff --git a/src/cdomain/value/cdomains/mutexAttrDomain.ml b/src/cdomain/value/cdomains/mutexAttrDomain.ml
@@ -25,7 +25,7 @@ let recursive_int = lazy (
   let res = ref (Z.of_int 2) in (* Use OS X as the default, it doesn't have the enum *)
   GoblintCil.iterGlobals !Cilfacade.current_file (function
       | GEnumTag (einfo, _) ->
-        List.iter (fun (name, exp, _) ->
+        List.iter (fun (name, _, exp, _) ->
             if name = "PTHREAD_MUTEX_RECURSIVE" then
               res := Option.get @@ GoblintCil.getInteger exp
           ) einfo.eitems