Merge branch 'master' into yaml-witness-ghost-eval

goblint · Jul 4, 2024 · c0f14bb · c0f14bb
2 parents d3594c9 + 502cf9f
commit c0f14bb
Show file tree

Hide file tree

Showing 32 changed files with 338 additions and 87 deletions.
diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml
@@ -35,10 +35,9 @@ jobs:
           # otherwise setup-ocaml pins non-locked dependencies
           # https://github.com/ocaml/setup-ocaml/issues/166
           OPAMLOCKED: locked
-        uses: ocaml/setup-ocaml@v2
+        uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
-          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
 
       - name: Install graph-easy # TODO: remove if depext --with-test works
         if: ${{ matrix.os == 'ubuntu-latest' }}

diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
@@ -35,7 +35,7 @@ jobs:
           # otherwise setup-ocaml pins non-locked dependencies
           # https://github.com/ocaml/setup-ocaml/issues/166
           OPAMLOCKED: locked
-        uses: ocaml/setup-ocaml@v2
+        uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 

diff --git a/.github/workflows/indentation.yml b/.github/workflows/indentation.yml
@@ -25,7 +25,7 @@ jobs:
           fetch-depth: 0
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
-        uses: ocaml/setup-ocaml@v2
+        uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 

diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml
@@ -37,10 +37,9 @@ jobs:
           # otherwise setup-ocaml pins non-locked dependencies
           # https://github.com/ocaml/setup-ocaml/issues/166
           OPAMLOCKED: locked
-        uses: ocaml/setup-ocaml@v2
+        uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
-          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
 
       - name: Install graph-easy # TODO: remove if depext --with-test works
         if: ${{ matrix.os == 'ubuntu-latest' }}
@@ -87,10 +86,9 @@ jobs:
           # otherwise setup-ocaml pins non-locked dependencies
           # https://github.com/ocaml/setup-ocaml/issues/166
           OPAMLOCKED: locked
-        uses: ocaml/setup-ocaml@v2
+        uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
-          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
 
       - name: Install graph-easy # TODO: remove if depext --with-test works
         if: ${{ matrix.os == 'ubuntu-latest' }}
@@ -132,7 +130,7 @@ jobs:
           # otherwise setup-ocaml pins non-locked dependencies
           # https://github.com/ocaml/setup-ocaml/issues/166
           OPAMLOCKED: locked
-        uses: ocaml/setup-ocaml@v2
+        uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 

diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml
@@ -45,10 +45,9 @@ jobs:
         uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
-        uses: ocaml/setup-ocaml@v2
+        uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
-          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
 
       - name: Install graph-easy # TODO: remove if depext --with-test works
         if: ${{ matrix.os == 'ubuntu-latest' }}
@@ -109,7 +108,6 @@ jobs:
         uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
-          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
 
       - name: Install graph-easy # TODO: remove if depext --with-test works
         if: ${{ matrix.os == 'ubuntu-latest' }}
@@ -199,10 +197,9 @@ jobs:
         uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
-        uses: ocaml/setup-ocaml@v2
+        uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
-          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
 
       - name: Install graph-easy # TODO: remove if depext --with-test works
         if: ${{ matrix.os == 'ubuntu-latest' }}

diff --git a/.zenodo.json b/.zenodo.json
@@ -23,6 +23,11 @@
       "affiliation": "Technische Universität München",
       "orcid": "0009-0009-9644-7475"
     },
+    {
+      "name": "Holter, Karoliine",
+      "affiliation": "University of Tartu",
+      "orcid": "0009-0008-3725-4131"
+    },
     {
       "name": "Vogler, Ralf",
       "affiliation": "Technische Universität München"

diff --git a/CITATION.cff b/CITATION.cff
@@ -21,6 +21,10 @@ authors: # same authors as in .zenodo.json and dune-project
     family-names: Tilscher
     affiliation: "Technische Universität München"
     orcid: "https://orcid.org/0009-0009-9644-7475"
+  - given-names: Karoliine
+    family-names: Holter
+    affiliation: "University of Tartu"
+    orcid: "https://orcid.org/0009-0008-3725-4131"
   - given-names: Ralf
     family-names: Vogler
     affiliation: "Technische Universität München"

diff --git a/conf/examples/medium-program.json b/conf/examples/medium-program.json
@@ -9,6 +9,7 @@
       "base",
       "threadid",
       "threadflag",
+      "threadreturn",
       "mallocWrapper",
       "mutexEvents",
       "mutex",
@@ -18,6 +19,7 @@
       "expRelation",
       "mhp",
       "assert",
+      "pthreadMutexType",
       "var_eq",
       "symb_locks",
       "region",

diff --git a/conf/examples/very-precise.json b/conf/examples/very-precise.json
@@ -22,6 +22,7 @@
       "base",
       "threadid",
       "threadflag",
+      "threadreturn",
       "mallocWrapper",
       "mutexEvents",
       "mutex",
@@ -31,6 +32,7 @@
       "expRelation",
       "mhp",
       "assert",
+      "pthreadMutexType",
       "var_eq",
       "symb_locks",
       "region",

diff --git a/docs/user-guide/assumptions.md b/docs/user-guide/assumptions.md
@@ -17,3 +17,22 @@ _NB! This list is likely incomplete._
 
     See [PR #1414](https://github.com/goblint/analyzer/pull/1414).
 
+2.  Pointer arithmetic does not overflow.
+
+    [C11's N1570][n1570] at 6.5.6.8 states that
+
+    > When an expression that has integer type is added to or subtracted from a pointer, the result has the type of the pointer operand.
+    > [...]
+    > the evaluation shall not produce an overflow; otherwise, the behavior is undefined.
+
+    after a long list of defined behaviors.
+
+    Goblint does not report overflow and out-of-bounds pointer arithmetic (when the pointer _is not dereferenced_).
+    This affects the overflow analysis (SV-COMP no-overflow property) in the `base` analysis.
+
+    This _does not_ affect the `memOutOfBounds` analysis (SV-COMP valid-memsafety property), which is for undefined behavior from _dereferencing_ such out-of-bounds pointers.
+
+    See [PR #1511](https://github.com/goblint/analyzer/pull/1511).
+
+
+[n1570]: https://www.open-std.org/jtc1/sc22/wg14/www/docs/n1570.pdf
diff --git a/dune-project b/dune-project
@@ -15,13 +15,26 @@
 (source (github goblint/analyzer))
 (homepage "https://goblint.in.tum.de")
 (documentation "https://goblint.readthedocs.io/en/latest/")
-(authors "Simmo Saan" "Michael Schwarz" "Julian Erhard" "Sarah Tilscher" "Ralf Vogler" "Kalmer Apinis" "Vesal Vojdani" ) ; same authors as in .zenodo.json and CITATION.cff
+(authors "Simmo Saan" "Michael Schwarz" "Julian Erhard" "Sarah Tilscher" "Karoliine Holter" "Ralf Vogler" "Kalmer Apinis" "Vesal Vojdani" ) ; same authors as in .zenodo.json and CITATION.cff
 (maintainers "Simmo Saan <[email protected]>" "Michael Schwarz <[email protected]>" "Karoliine Holter")
 (license MIT)
 
 (package
   (name goblint)
   (synopsis "Static analysis framework for C")
+  (description "\
+Goblint is a sound static analysis framework for C programs using abstract interpretation.
+It specializes in thread-modular verification of multi-threaded programs, especially regarding data races.
+Goblint includes analyses for assertions, overflows, deadlocks, etc and can be extended with new analyses.
+")
+  (tags (
+    "program analysis"
+    "program verification"
+    "static analysis"
+    "abstract interpretation"
+    "C"
+    "data race analysis"
+    "concurrency"))
   (depends
     (ocaml (>= 4.14))
     (goblint-cil (>= 2.0.3)) ; TODO no way to define as pin-depends? Used goblint.opam.template to add it for now. https://github.com/ocaml/dune/issues/3231. Alternatively, removing this line and adding cil as a git submodule and `(vendored_dirs cil)` as ./dune also works. This way, no more need to reinstall the pinned cil opam package on changes. However, then cil is cleaned and has to be rebuild together with goblint.

diff --git a/goblint.opam b/goblint.opam
@@ -1,6 +1,11 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
 synopsis: "Static analysis framework for C"
+description: """
+Goblint is a sound static analysis framework for C programs using abstract interpretation.
+It specializes in thread-modular verification of multi-threaded programs, especially regarding data races.
+Goblint includes analyses for assertions, overflows, deadlocks, etc and can be extended with new analyses.
+"""
 maintainer: [
   "Simmo Saan <[email protected]>"
   "Michael Schwarz <[email protected]>"
@@ -11,11 +16,21 @@ authors: [
   "Michael Schwarz"
   "Julian Erhard"
   "Sarah Tilscher"
+  "Karoliine Holter"
   "Ralf Vogler"
   "Kalmer Apinis"
   "Vesal Vojdani"
 ]
 license: "MIT"
+tags: [
+  "program analysis"
+  "program verification"
+  "static analysis"
+  "abstract interpretation"
+  "C"
+  "data race analysis"
+  "concurrency"
+]
 homepage: "https://goblint.in.tum.de"
 doc: "https://goblint.readthedocs.io/en/latest/"
 bug-reports: "https://github.com/goblint/analyzer/issues"

diff --git a/goblint.opam.locked b/goblint.opam.locked
@@ -12,6 +12,7 @@ authors: [
   "Michael Schwarz"
   "Julian Erhard"
   "Sarah Tilscher"
+  "Karoliine Holter"
   "Ralf Vogler"
   "Kalmer Apinis"
   "Vesal Vojdani"
@@ -142,3 +143,16 @@ pin-depends: [
   ]
 ]
 depexts: ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}
+description: """\
+Goblint is a sound static analysis framework for C programs using abstract interpretation.
+It specializes in thread-modular verification of multi-threaded programs, especially regarding data races.
+Goblint includes analyses for assertions, overflows, deadlocks, etc and can be extended with new analyses."""
+tags: [
+  "program analysis"
+  "program verification"
+  "static analysis"
+  "abstract interpretation"
+  "C"
+  "data race analysis"
+  "concurrency"
+]
diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
@@ -768,7 +768,7 @@ struct
 
   let sync ctx reason =
     (* After the solver is finished, store the results (for later comparison) *)
-    if !AnalysisState.postsolving then begin
+    if !AnalysisState.postsolving && GobConfig.get_string "exp.relation.prec-dump" <> "" then begin
       let keep_local = GobConfig.get_bool "ana.relation.invariant.local" in
       let keep_global = GobConfig.get_bool "ana.relation.invariant.global" in
 

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -261,6 +261,8 @@ struct
       (* adds n to the last offset *)
       let rec addToOffset n (t:typ option) = function
         | `Index (i, `NoOffset) ->
+          (* Binary operations on pointer types should not generate warnings in SV-COMP *)
+          GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () ->
           (* If we have arrived at the last Offset and it is an Index, we add our integer to it *)
           `Index(IdxDom.add i (iDtoIdx n), `NoOffset)
         | `Field (f, `NoOffset) ->

diff --git a/src/analyses/mutexTypeAnalysis.ml b/src/analyses/mutexTypeAnalysis.ml
@@ -12,16 +12,17 @@ struct
 
   let name () = "pthreadMutexType"
 
-  (* Removing indexes here avoids complicated lookups and allows to have the LVals as vars here, at the price that different types of mutexes in arrays are not dinstinguished *)
-  module O = Offset.Unit
-
-  module V = struct
-    include Printable.Prod(CilType.Varinfo)(O) (* TODO: use Mval.Unit *)
+  module V =
+  struct
+    (* Removing indexes here avoids complicated lookups and allows to have the LVals as vars here, at the price that different types of mutexes in arrays are not dinstinguished *)
+    include Mval.Unit
     let is_write_only _ = false
   end
 
   module G = MAttr
 
+  module O = Offset.Unit
+
   (* transfer functions *)
   let assign ctx (lval:lval) (rval:exp) : D.t =
     match lval with

diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml
@@ -85,7 +85,9 @@ struct
 
     let yaml = match Yaml_unix.of_file (Fpath.v (GobConfig.get_string "witness.yaml.unassume")) with
       | Ok yaml -> yaml
-      | Error (`Msg m) -> failwith ("Yaml_unix.of_file: " ^ m)
+      | Error (`Msg m) ->
+        Logs.error "Yaml_unix.of_file: %s" m;
+        Svcomp.errorwith "witness missing"
     in
     let yaml_entries = yaml |> GobYaml.list |> BatResult.get_ok in
 

diff --git a/src/autoTune.ml b/src/autoTune.ml
@@ -186,7 +186,7 @@ let enableAnalyses anas =
 (*escape is also still enabled, because otherwise we get a warning*)
 (*does not consider dynamic calls!*)
 
-let notNeccessaryThreadAnalyses = ["race"; "deadlock"; "maylocks"; "symb_locks"; "thread"; "threadid"; "threadJoins"; "threadreturn"; "mhp"; "region"]
+let notNeccessaryThreadAnalyses = ["race"; "deadlock"; "maylocks"; "symb_locks"; "thread"; "threadid"; "threadJoins"; "threadreturn"; "mhp"; "region"; "pthreadMutexType"]
 let reduceThreadAnalyses () =
   let isThreadCreate = function
     | LibraryDesc.ThreadCreate _ -> true

diff --git a/src/build-info/dune b/src/build-info/dune
@@ -15,7 +15,7 @@
   (target configVersion.ml)
   (mode (promote (until-clean) (only configVersion.ml))) ; replace existing file in source tree, even if releasing (only overrides)
   (deps (universe)) ; do not cache, always regenerate
-  (action (pipe-stdout (bash "git describe --all --long --dirty || echo \"n/a\"") (with-stdout-to %{target} (bash "xargs printf '(* Automatically regenerated, changes do not persist! *)\nlet version = \"%s\"'")))))
+  (action (pipe-stdout (bash "git describe --all --long --dirty || echo \"n/a\"") (with-stdout-to %{target} (bash "xargs printf '(* Automatically regenerated, changes do not persist! *)\nlet version = Sys.opaque_identity \"%s\"'")))))
 
 (rule
   (target configProfile.ml)
@@ -31,7 +31,7 @@
   (target configDatetime.ml)
   (mode (promote (until-clean) (only configDatetime.ml))) ; replace existing file in source tree, even if releasing (only overrides)
   (deps (universe)) ; do not cache, always regenerate
-  (action (pipe-stdout (bash "date +\"%Y-%m-%dT%H:%M:%S\" || echo \"n/a\"") (with-stdout-to %{target} (bash "xargs printf '(* Automatically regenerated, changes do not persist! *)\nlet datetime = \"%s\"'")))))
+  (action (pipe-stdout (bash "date +\"%Y-%m-%dT%H:%M:%S\" || echo \"n/a\"") (with-stdout-to %{target} (bash "xargs printf '(* Automatically regenerated, changes do not persist! *)\nlet datetime = Sys.opaque_identity \"%s\"'")))))
 
 (env
   (_

diff --git a/src/cdomain/value/cdomains/offset.ml b/src/cdomain/value/cdomains/offset.ml
@@ -213,7 +213,7 @@ struct
         let bits_offset, _size = GoblintCil.bitsOffset (TComp (field.fcomp, [])) field_as_offset  in
         let bits_offset = idx_of_int bits_offset in
         let remaining_offset = offset_to_index_offset ~typ:field.ftype o in
-        Idx.add bits_offset remaining_offset
+        GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> Idx.add bits_offset remaining_offset
       | `Index (x, o) ->
         let (item_typ, item_size_in_bits) =
           match Option.map unrollType typ with
@@ -223,9 +223,10 @@ struct
           | _ ->
             (None, Idx.top ())
         in
-        let bits_offset = Idx.mul item_size_in_bits x in
+        (* Binary operations on offsets should not generate overflow warnings in SV-COMP *)
+        let bits_offset = GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> Idx.mul item_size_in_bits x in
         let remaining_offset = offset_to_index_offset ?typ:item_typ o in
-        Idx.add bits_offset remaining_offset
+        GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> Idx.add bits_offset remaining_offset
     in
     offset_to_index_offset ?typ offs