Merge branch 'master' into null-byte-arrayDomain

.mailmap

@@ -23,6 +23,7 @@ Kerem Çakırer <[email protected]> <[email protected]>
 Sarah Tilscher <[email protected]>
 Karoliine Holter <[email protected]>
 <[email protected]> <[email protected]>
+<[email protected]> <[email protected]>
 
 Elias Brandstetter <[email protected]> <[email protected]>
 wherekonshade <[email protected]> <[email protected]>
@@ -37,3 +38,6 @@ Mireia Cano Pujol <[email protected]>
 Felix Krayer <[email protected]>
 Felix Krayer <[email protected]> <[email protected]>
 Manuel Pietsch <[email protected]>
+Tim Ortel <[email protected]>
+Tomáš Dacík <[email protected]>
+<[email protected]> <[email protected]>

conf/examples/very-precise.json

@@ -61,7 +61,9 @@
       "structs" : {
         "domain" : "combined-sk"
       },
-      "limit-string-addresses": false
+      "strings": {
+        "domain": "disjoint"
+      }
     }
   },
   "exp": {

docs/developer-guide/releasing.md

@@ -37,13 +37,11 @@
     2. Extract distribution archive.
     3. Run Docker container in extracted directory: `docker run -it --rm -v $(pwd):/goblint ocaml/opam:ubuntu-22.04-ocaml-4.14` (or newer).
     4. Navigate to distribution archive inside Docker container: `cd /goblint`.
-    5. Pin package from distribution archive: `opam pin add --no-action .`.
-    6. Install depexts: `opam depext --with-test goblint`.
-    7. Install and test package: `opam install --with-test goblint`.
-    8. Activate opam environment: `eval $(opam env)`.
-    9. Check version: `goblint --version`.
-    10. Check that analysis works: `goblint -v tests/regression/04-mutex/01-simple_rc.c`.
-    11. Exit Docker container.
+    5. Install and test package from distribution archive: `opam-2.1 install --with-test .`.
+    6. Activate opam environment: `eval $(opam env)`.
+    7. Check version: `goblint --version`.
+    8. Check that analysis works: `goblint -v tests/regression/04-mutex/01-simple_rc.c`.
+    9. Exit Docker container.
 
 12. Temporarily enable Zenodo GitHub webhook.
 
@@ -59,6 +57,7 @@
 
 15. Create an opam package: `dune-release opam pkg`.
 16. Submit the opam package to opam-repository: `dune-release opam submit`.
+17. Revert temporary removal of opam pins.
 
 
 ## SV-COMP

goblint.opam

@@ -74,12 +74,12 @@ 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-distribution != "alpine" & arch != "arm64"
-# pin-depends: [
+pin-depends: [
   # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
   # [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#d2760bacfbfdb25a374254de44f2ff1cb5f42abd" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
-  # [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
-# ]
+  [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
+]
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]

goblint.opam.locked

@@ -128,3 +128,10 @@ conflicts: [
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]
+# TODO: manually reordered to avoid opam pin crash: https://github.com/ocaml/opam/issues/4936
+pin-depends: [
+  [
+    "ppx_deriving.5.2.1"
+    "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6"
+  ]
+]

goblint.opam.template

@@ -1,12 +1,12 @@
 # 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-distribution != "alpine" & arch != "arm64"
-# pin-depends: [
+pin-depends: [
   # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
   # [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#d2760bacfbfdb25a374254de44f2ff1cb5f42abd" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
-  # [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
-# ]
+  [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
+]
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]

src/analyses/base.ml

@@ -1486,7 +1486,7 @@ struct
             Priv.read_global a priv_getg st x
         in
         let new_value = update_offset old_value in
-        M.tracel "hgh" "update_offset %a -> %a\n" VD.pretty old_value VD.pretty new_value;
+        if M.tracing then M.tracel "set" "update_offset %a -> %a\n" VD.pretty old_value VD.pretty new_value;
         let r = Priv.write_global ~invariant a priv_getg (priv_sideg ctx.sideg) st x new_value in
         if M.tracing then M.tracel "set" ~var:x.vname "update_one_addr: updated a global var '%s' \nstate:%a\n\n" x.vname D.pretty r;
         r
@@ -2132,7 +2132,7 @@ struct
     let invalidate_ret_lv st = match lv with
       | Some lv ->
         if M.tracing then M.tracel "invalidate" "Invalidating lhs %a for function call %s\n" d_plainlval lv f.vname;
-        invalidate ~ctx (Analyses.ask_of_ctx ctx) ctx.global st [Cil.mkAddrOrStartOf lv]
+        invalidate ~deep:false ~ctx (Analyses.ask_of_ctx ctx) ctx.global st [Cil.mkAddrOrStartOf lv]
       | None -> st
     in
     let addr_type_of_exp exp =

src/analyses/memLeak.ml

@@ -205,12 +205,12 @@ struct
     | Malloc _
     | Calloc _
     | Realloc _ ->
-      (ctx.sideg () true;
+      ctx.sideg () true;
       begin match ctx.ask (Queries.AllocVar {on_stack = false}) with
         | `Lifted var ->
           ToppedVarInfoSet.add var state
         | _ -> state
-      end)
+      end
     | Free ptr ->
       begin match ctx.ask (Queries.MayPointTo ptr) with
         | ad when (not (Queries.AD.is_top ad)) && Queries.AD.cardinal ad = 1 ->
@@ -233,16 +233,15 @@ struct
         | a when Queries.ID.is_bot a -> M.warn ~category:Assert "assert expression %a is bottom" d_exp exp
         | a ->
           begin match Queries.ID.to_bool a with
-            | Some b -> (
+            | Some b ->
               (* If we know for sure that the expression in "assert" is false => need to check for memory leaks *)
-                if b = false then (
-                  warn_for_multi_threaded_due_to_abort ctx;
-                  check_for_mem_leak ctx
-                )
-                else ())
+              if b = false then (
+                warn_for_multi_threaded_due_to_abort ctx;
+                check_for_mem_leak ctx
+              )
             | None ->
-              (warn_for_multi_threaded_due_to_abort ctx;
-               check_for_mem_leak ctx ~assert_exp_imprecise:true ~exp:(Some exp))
+              warn_for_multi_threaded_due_to_abort ctx;
+              check_for_mem_leak ctx ~assert_exp_imprecise:true ~exp:(Some exp)
           end
       in
       warn_for_assert_exp;

src/autoTune.ml

@@ -224,7 +224,7 @@ let focusOnMemSafetySpecification (spec: Svcomp.Specification.t) =
     print_endline "Setting \"cil.addNestedScopeAttr\" to true";
     set_bool "cil.addNestedScopeAttr" true;
     print_endline @@ "Specification: ValidDeref -> enabling memOutOfBounds analysis \"" ^ (String.concat ", " memOobAna) ^ "\"";
-    enableAnalyses memOobAna
+    enableAnalyses memOobAna;
   | ValidMemtrack
   | ValidMemcleanup -> (* Enable the memLeak analysis *)
     let memLeakAna = ["memLeak"] in

src/build-info/dune

@@ -27,3 +27,6 @@
   (mode (promote (until-clean) (only configOcaml.ml))) ; replace existing file in source tree, even if releasing (only overrides)
   (action (write-file %{target} "(* Automatically regenerated, changes do not persist! *)\nlet flambda = \"%{ocaml-config:flambda}\"")))
 
+(env
+  (_
+    (flags (:standard -w -no-cmx-file)))) ; suppress warning from flambda compiler bug: https://github.com/ocaml/dune/issues/3277

src/cdomains/addressDomain.ml

@@ -5,6 +5,7 @@ open IntOps
 
 module M = Messages
 module Mval_outer = Mval
+module SD = StringDomain
 
 
 module AddressBase (Mval: Printable.S) =
@@ -14,23 +15,14 @@ struct
     | Addr of Mval.t
     | NullPtr
     | UnknownPtr
-    | StrPtr of string option
+    | StrPtr of SD.t
   [@@deriving eq, ord, hash] (* TODO: StrPtr equal problematic if the same literal appears more than once *)
 
   let name () = Format.sprintf "address (%s)" (Mval.name ())
 
-  let hash x = match x with
-    | StrPtr _ ->
-      if GobConfig.get_bool "ana.base.limit-string-addresses" then
-        13859
-      else
-        hash x
-    | _ -> hash x
-
   let show = function
     | Addr m -> Mval.show m
-    | StrPtr (Some x)   -> "\"" ^ x ^ "\""
-    | StrPtr None -> "(unknown string)"
+    | StrPtr s   -> StringDomain.show s
     | UnknownPtr -> "?"
     | NullPtr    -> "NULL"
 
@@ -42,31 +34,18 @@ struct
     )
 
   (* strings *)
-  let of_string x = StrPtr (Some x)
+  let of_string x = StrPtr (SD.of_string x)
   let to_string = function
-    | StrPtr (Some x) -> Some x
+    | StrPtr s -> SD.to_string s
     | _        -> None
-  (* only keep part before first null byte *)
   let to_c_string = function
-    | StrPtr (Some x) ->
-      begin match String.split_on_char '\x00' x with
-        | s::_ -> Some s
-        | [] -> None
-      end
+    | StrPtr s -> SD.to_c_string s
     | _ -> None
-  let to_n_c_string n x =
-    match to_c_string x with
-    | Some x ->
-      if n > String.length x then
-        Some x
-      else if n < 0 then
-        None
-      else
-        Some (String.sub x 0 n)
+  let to_n_c_string n = function
+    | StrPtr s -> SD.to_n_c_string n s
     | _ -> None
-  let to_string_length x =
-    match to_c_string x with
-    | Some x -> Some (String.length x)
+  let to_string_length = function
+    | StrPtr s -> SD.to_string_length s
     | _ -> None
 
   let arbitrary () = QCheck.always UnknownPtr (* S TODO: non-unknown *)
@@ -101,8 +80,7 @@ struct
   (* TODO: seems to be unused *)
   let to_exp = function
     | Addr m -> AddrOf (Mval.to_cil m)
-    | StrPtr (Some x) -> mkString x
-    | StrPtr None -> raise (Lattice.Unsupported "Cannot express unknown string pointer as expression.")
+    | StrPtr s -> SD.to_exp s
     | NullPtr -> integer 0
     | UnknownPtr -> raise Lattice.TopValue
   (* TODO: unused *)
@@ -123,9 +101,7 @@ struct
 
   let semantic_equal x y = match x, y with
     | Addr x, Addr y -> Mval.semantic_equal x y
-    | StrPtr None, StrPtr _
-    | StrPtr _, StrPtr None -> Some true
-    | StrPtr (Some a), StrPtr (Some b) -> if a = b then None else Some false
+    | StrPtr s1, StrPtr s2 -> SD.semantic_equal s1 s2
     | NullPtr, NullPtr -> Some true
     | UnknownPtr, UnknownPtr
     | UnknownPtr, Addr _
@@ -135,35 +111,14 @@ struct
     | _, _ -> Some false
 
   let leq x y = match x, y with
-    | StrPtr _, StrPtr None -> true
-    | StrPtr a, StrPtr b   -> a = b
+    | StrPtr s1, StrPtr s2   -> SD.leq s1 s2
     | Addr x, Addr y -> Mval.leq x y
     | _                      -> x = y
 
   let top_indices = function
     | Addr x -> Addr (Mval.top_indices x)
     | x -> x
 
-  let join_string_ptr x y = match x, y with
-    | None, _
-    | _, None -> None
-    | Some a, Some b when a = b -> Some a
-    | Some a, Some b (* when a <> b *) ->
-      if GobConfig.get_bool "ana.base.limit-string-addresses" then
-        None
-      else
-        raise Lattice.Uncomparable
-
-  let meet_string_ptr x y = match x, y with
-    | None, a
-    | a, None -> a
-    | Some a, Some b when a = b -> Some a
-    | Some a, Some b (* when a <> b *) ->
-      if GobConfig.get_bool "ana.base.limit-string-addresses" then
-        raise Lattice.BotValue
-      else
-        raise Lattice.Uncomparable
-
   let merge mop sop x y =
     match x, y with
     | UnknownPtr, UnknownPtr -> UnknownPtr
@@ -172,10 +127,10 @@ struct
     | Addr x, Addr y -> Addr (mop x y)
     | _ -> raise Lattice.Uncomparable
 
-  let join = merge Mval.join join_string_ptr
-  let widen = merge Mval.widen join_string_ptr
-  let meet = merge Mval.meet meet_string_ptr
-  let narrow = merge Mval.narrow meet_string_ptr
+  let join = merge Mval.join SD.join
+  let widen = merge Mval.widen SD.join
+  let meet = merge Mval.meet SD.meet
+  let narrow = merge Mval.narrow SD.meet
 
   include Lattice.NoBotTop
 
@@ -194,8 +149,7 @@ struct
 
     let of_elt (x: elt): t = match x with
       | Addr (v, o) -> Addr v
-      | StrPtr _ when GobConfig.get_bool "ana.base.limit-string-addresses" -> StrPtr None (* all strings together if limited *)
-      | StrPtr x -> StrPtr x (* everything else is kept separate, including strings if not limited *)
+      | StrPtr s -> StrPtr (SD.repr s)
       | NullPtr -> NullPtr
       | UnknownPtr -> UnknownPtr
   end
@@ -211,8 +165,7 @@ struct
 
     let of_elt (x: elt): t = match x with
       | Addr (v, o) -> Addr (v, Offset.Unit.of_offs o) (* addrs grouped by var and part of offset *)
-      | StrPtr _ when GobConfig.get_bool "ana.base.limit-string-addresses" -> StrPtr None (* all strings together if limited *)
-      | StrPtr x -> StrPtr x (* everything else is kept separate, including strings if not limited *)
+      | StrPtr s -> StrPtr (SD.repr s)
       | NullPtr -> NullPtr
       | UnknownPtr -> UnknownPtr
   end

src/cdomains/addressDomain_intf.ml

@@ -7,7 +7,7 @@ sig
       | Addr of Mval.t (** Pointer to mvalue. *)
       | NullPtr (** NULL pointer. *)
       | UnknownPtr (** Unknown pointer. Could point to globals, heap and escaped variables. *)
-      | StrPtr of string option (** String literal pointer. [StrPtr None] abstracts any string pointer *)
+      | StrPtr of StringDomain.t (** String literal pointer. [StrPtr None] abstracts any string pointer *)
     include Printable.S with type t := t (** @closed *)
 
     val of_string: string -> t
@@ -16,8 +16,6 @@ sig
     val to_string: t -> string option
     (** Convert {!StrPtr} to string if possible. *)
 
-    (** C strings are different from OCaml strings as they are not processed after the first [NUL] byte, even though the OCaml string (and a C string literal) may be longer. *)
-
     val to_c_string: t -> string option
     (** Convert {!StrPtr} to C string if possible. *)
 
@@ -71,7 +69,7 @@ sig
       - Each {!Addr}, modulo precise index expressions in the offset, is a sublattice with ordering induced by {!Mval}.
       - {!NullPtr} is a singleton sublattice.
       - {!UnknownPtr} is a singleton sublattice.
-      - If [ana.base.limit-string-addresses] is enabled, then all {!StrPtr} are together in one sublattice with flat ordering. If [ana.base.limit-string-addresses] is disabled, then each {!StrPtr} is a singleton sublattice. *)
+      - If [ana.base.strings.domain] is disjoint, then each {!StrPtr} is a singleton sublattice. Otherwise, all {!StrPtr} are together in one sublattice with flat ordering. *)
   module AddressLattice (Mval: Mval.Lattice):
   sig
     include module type of AddressPrintable (Mval)