Merge branch 'master' into issue-1192

README.md

@@ -24,7 +24,7 @@ For benchmarking Goblint, please follow the [Benchmarking guide on Read the Docs
 6. _Optional:_ See [`scripts/bash-completion.sh`](./scripts/bash-completion.sh) for setting up bash completion for Goblint arguments.
 
 ### MacOS
-1. Install GCC with `brew install gcc` (first run `xcode-select --install` if you don't want to build it from source). Goblint requires GCC while macOS's default `cpp` is Clang, which will not work.
+1. Install GCC with `brew install gcc grep` (first run `xcode-select --install` if you don't want to build it from source). Goblint requires GCC while macOS's default `cpp` is Clang, which will not work.
 2. ONLY for M1 (ARM64) processor: homebrew changed its install location from `/usr/local/` to `/opt/homebrew/`. For packages to find their dependecies execute `sudo ln -s /opt/homebrew/{include,lib} /usr/local/`.
 3. Continue using Linux instructions (the formulae in brew for `patch`, `libgmp-dev`, `libmpfr-dev` are `gpatch`, `gmp`, `mpfr`, respectively).
 

conf/ldv-races.json

@@ -29,7 +29,9 @@
       "escape",
       "expRelation",
       "mhp",
-      "assert"
+      "assert",
+      "var_eq",
+      "symb_locks"
     ],
     "malloc": {
       "wrappers": [
@@ -52,6 +54,19 @@
       ]
     }
   },
+  "lib": {
+    "activated": [
+      "c",
+      "posix",
+      "pthread",
+      "gcc",
+      "glibc",
+      "linux-userspace",
+      "goblint",
+      "ncurses",
+      "klever"
+    ]
+  },
   "witness": {
     "graphml": {
       "enabled": true,

conf/min-unsound.json

@@ -0,0 +1,6 @@
+{
+    "ana": {
+        "activated": [
+        ]
+    }
+}

docs/artifact-descriptions/vmcai24.md

@@ -0,0 +1,83 @@
+# VMCAI '24 Artifact Description
+## Correctness Witness Validation by Abstract Interpretation
+
+This is the artifact description for our [VMCAI '24 paper "Correctness Witness Validation by Abstract Interpretation"](https://doi.org/10.1007/978-3-031-50524-9_4).
+The artifact is available on [Zenodo](https://doi.org/10.5281/zenodo.8253000).
+
+This artifact contains everything mentioned in the evaluation section of the paper: Goblint implementation, scripts, benchmarks, manual witnesses and other tools.
+
+**The description here is provided for convenience and not maintained.**
+The artifact is based on [Goblint at `vmcai24` git tag](https://github.com/goblint/analyzer/releases/tag/vmcai24) and [Goblint benchmarks at `vmcai24` git tag](https://github.com/goblint/bench/releases/tag/vmcai24).
+
+## Requirements
+* [VirtualBox](https://www.virtualbox.org/).
+* 2 CPU cores.
+* 8 GB RAM.
+* 7 GB disk space.
+* ~45min.
+
+## Layout
+* `README.md`/`README.pdf` — this file.
+* `LICENSE`.
+* `unassume.ova` — VirtualBox virtual machine.
+
+    In `/home/vagrant` contains:
+
+    * `goblint/` ­— Goblint with unassume support, including source code.
+    * `CPAchecker-2.2-unix/` — CPAchecker from [SV-COMP 2023 archives](https://gitlab.com/sosy-lab/sv-comp/archives-2023).
+    * `UAutomizer-linux/` — Ultimate Automizer from [SV-COMP 2023 archives](https://gitlab.com/sosy-lab/sv-comp/archives-2023).
+    * `eval-prec/` — precision evaluation (script, benchmarks, manual witnesses).
+    * `eval-perf/` — performance evaluation (script, benchmarks, manual witnesses).
+    * `results/` — results (initially empty).
+
+* `results/` — evaluation results tables with data used for the paper.
+
+## Reproduction
+1. Import the virtual machine into VirtualBox.
+2. Start the virtual machine and log in with username "vagrant" (not "Ubuntu"!) and password "vagrant".
+3. Right click on the desktop and open Applications → Accessories → Terminal Emulator.
+
+### Precision evaluation
+1. Run `./eval-prec/run.sh` in the terminal emulator. This takes ~42min.
+2. Run `firefox results/eval-prec/table-generator.table.html` to view the results.
+
+    The HTML table contains the following status columns (cputime, walltime and memory can be ignored):
+
+    1. Goblint w/o witness (true means verified).
+    2. Goblint w/ manual witness (true means witness validated).
+    3. Goblint w/ witness from CPAchecker (true means program verified with witness-guidance).
+    4. Goblint w/ witness from CPAchecker (true means witness validated).
+    5. Goblint w/ witness from UAutomizer (true means program verified with witness-guidance).
+    6. Goblint w/ witness from UAutomizer (true means witness validated).
+
+   Table 1 in the paper presents these results, except the rows are likely in a different order.
+
+### Performance evaluation
+1. Run `./eval-perf/run.sh` in the terminal emulator. This takes ~30s.
+2. Run `firefox results/eval-perf/table-generator.table.html` to view the results.
+
+    The HTML table contains the following relevant columns (others can be ignored):
+
+    1. Goblint w/o witness, evals.
+    2. Goblint w/o witness, cputime.
+    3. Goblint w/ manual witness, evals.
+    4. Goblint w/ manual witness, cputime.
+
+   Table 2 in the paper presents these results, except the rows are likely in a different order.
+
+
+## Goblint implementation
+[Goblint](https://github.com/goblint/analyzer) is an open source static analysis framework for C.
+Goblint itself is written in OCaml.
+Being open source, it allows existing implementations of analyses and abstract domains to be reused and modified.
+As a framework, it also allows new ones to be easily added.
+For more details, refer to the linked GitHub repository and related documentation.
+
+Key parts of the code related to this paper are the following:
+
+1. `src/analyses/unassumeAnalysis.ml`: analysis, which emits unassume operation events to other analyses for YAML-witness–guided verification.
+2. `src/analyses/base.ml` lines 2551–2641: propagating unassume for non-relational domains of the `base` analysis.
+3. `src/analyses/apron/relationAnalysis.apron.ml` lines 668–693: strengthening-based dual-narrowing unassume for relational Apron domains of the `apron` analysis.
+4. `src/cdomains/apron/apronDomain.apron.ml` lines 625–679: strengthening operator used for dual-narrowing of Apron domains.
+5. `src/util/wideningTokens.ml`: analysis lifter that adds widening tokens for delaying widenings from unassuming.
+6. `src/witness/yamlWitness.ml` lines 398–683: YAML witness validation.

docs/developer-guide/debugging.md

@@ -60,14 +60,14 @@ This will create a file called `goblint.byte`.
 ### Debugging Goblint with VS Code
 
 To debug OCaml programs, you can use the command line interface of `ocamldebug` or make use of the Visual Studio Code
-integration provided by `hackwaly.ocamlearlybird`.
+integration provided by `ocamllabs.ocaml-platform`.
 In the following, we describe the steps necessary to set up this VS Code extension to
 debug Goblint.
 
 ### Setting-up Earlybird
 
-Install the [`hackwaly.ocamlearlybird` extension](https://marketplace.visualstudio.com/items?itemName=hackwaly.ocamlearlybird) in your installation of Visual Studio Code.
-To be able to use this extension, you additionally need to install `ocamlearlybird` on the opam switch you use for Goblint.
+Install the [`ocamllabs.ocaml-platform` extension](https://marketplace.visualstudio.com/items?itemName=ocamllabs.ocaml-platform) in your installation of Visual Studio Code.
+To be able to use this extension, you additionally need to install `earlybird` on the opam switch you use for Goblint.
 To do so, run the following command in the `analyzer` directory:
 
 ```console
@@ -76,7 +76,7 @@ opam install earlybird
 
 ### Providing a Launch Configuration
 
-To let the `hackwaly.ocamlearlybird` extension know which executable it should debug, and which arguments it should pass, we have to provide a configuration file.
+To let the `ocamllabs.ocaml-platform` extension know which executable it should debug, and which arguments it should pass, we have to provide a configuration file.
 The configuration file has to be named `launch.json` and must reside in the `./.vscode` directory. Here is an example `launch.json`:
 
 ```JSON
@@ -92,6 +92,9 @@ The configuration file has to be named `launch.json` and must reside in the `./.
           "tests/regression/00-sanity/01-assert.c",
           "--enable", "ana.int.interval",
         ],
+        "env": {
+          "LD_LIBRARY_PATH": "$LD_LIBRARY_PATH:_build/default/src/common"
+        },
         "stopOnEntry": false,
       }
     ]

docs/developer-guide/messaging.md

@@ -18,7 +18,8 @@ A message consists of the following:
         3. **Context.** Optional. Currently completely abstract, so not very useful.
     * **Group.** For messages related to numerous locations with different texts. Contains the following:
         1. **Group text.** An overall description of the group message.
-        2. **Pieces.** A list of single messages as described above.
+        2. **Group location.** Optional. An overall location of the group message.
+        3. **Pieces.** A list of single messages as described above.
 
 ## Creating
 

docs/requirements.txt

@@ -1,6 +1,3 @@
 # Python requirements for MkDocs and Read the Docs
 
-mkdocs==1.2.3
-
-# TODO: temporary workaround for deprecated usage (https://github.com/mkdocs/mkdocs/issues/2794#issuecomment-1077705509)
-jinja2==3.0.3
+mkdocs==1.5.3

dune-project

@@ -16,7 +16,7 @@
 (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
-(maintainers "Simmo Saan <[email protected]>" "Michael Schwarz <[email protected]>")
+(maintainers "Simmo Saan <[email protected]>" "Michael Schwarz <[email protected]>" "Karoliine Holter")
 (license MIT)
 
 (package

goblint.opam

@@ -4,6 +4,7 @@ synopsis: "Static analysis framework for C"
 maintainer: [
   "Simmo Saan <[email protected]>"
   "Michael Schwarz <[email protected]>"
+  "Karoliine Holter"
 ]
 authors: [
   "Simmo Saan"

goblint.opam.locked

@@ -5,6 +5,7 @@ synopsis: "Static analysis framework for C"
 maintainer: [
   "Simmo Saan <[email protected]>"
   "Michael Schwarz <[email protected]>"
+  "Karoliine Holter"
 ]
 authors: [
   "Simmo Saan"

mkdocs.yml

@@ -39,3 +39,4 @@ nav:
   - '📦 Artifact descriptions':
     - "🇸 SAS '21": artifact-descriptions/sas21.md
     - "🇪 ESOP '23": artifact-descriptions/esop23.md
+    - "🇻 VMCAI '24": artifact-descriptions/vmcai24.md

scripts/goblint-lib-modules.py

@@ -8,6 +8,7 @@
 
 goblint_lib_paths = [
     src_root_path / "goblint_lib.ml",
+    src_root_path / "solver" / "goblint_solver.ml",
     src_root_path / "util" / "std" / "goblint_std.ml",
 ]
 goblint_lib_modules = set()
@@ -33,6 +34,7 @@
 
     # libraries
     "Goblint_std",
+    "Goblint_solver",
     "Goblint_timing",
     "Goblint_backtrace",
     "Goblint_tracing",
@@ -63,5 +65,5 @@
 
 missing_modules = src_modules - goblint_lib_modules
 if len(missing_modules) > 0:
-    print(f"Modules missing from {goblint_lib_path}: {missing_modules}")
+    print(f"Modules missing from {goblint_lib_paths[0]}: {missing_modules}")
     sys.exit(1)

scripts/test-gobview.py

@@ -61,6 +61,72 @@ def serve():
     panel = browser.find_element(By.CLASS_NAME, "panel")
     print("found DOM elements main, sidebar-left, sidebar-right, content and panel")
 
+    # test syntactic search
+    leftS.find_element(By.LINK_TEXT,  "Search").click()
+    leftS.find_element(By.CLASS_NAME, "switch-to-json").click()
+    textfield = leftS.find_element(By.CLASS_NAME, "form-control")
+    textfield.clear()
+    textfield.send_keys('{"kind":["var"],"target":["name","fail"],"find":["uses"],"mode":["Must"]}')
+    leftS.find_element(By.CLASS_NAME, "exec-button").click()
+    results = leftS.find_elements(By.CLASS_NAME, "list-group-item")
+    locations = []
+    for r in results:
+        for tr in r.find_elements(By.TAG_NAME, "tr"):
+            if tr.find_element(By.TAG_NAME, "th").text == "Location":
+                locations.insert(0,tr.find_element(By.TAG_NAME, "td").find_element(By.TAG_NAME, "a").text)
+
+    print("syntactic search for variable use of 'fail' found", len(results), "results")
+    for l in locations:
+        print(l)
+    assert(len(results) == 2)
+    assert("tests/regression/00-sanity/01-assert.c:7" in locations)
+    assert("tests/regression/00-sanity/01-assert.c:12" in locations)
+
+    # clear results
+    leftS.find_element(By.CLASS_NAME, "clear-btn").click()
+
+    # test semantic search 1
+    textfield = leftS.find_element(By.CLASS_NAME, "form-control")
+    textfield.clear()
+    textfield.send_keys('{"kind":["var"],"target":["name","success"],"find":["uses"],"expression":"success == 1","mode":["Must"]}')
+    leftS.find_element(By.CLASS_NAME, "exec-button").click()
+    results = leftS.find_elements(By.CLASS_NAME, "list-group-item")
+    locations = []
+    for r in results:
+        for tr in r.find_elements(By.TAG_NAME, "tr"):
+            if tr.find_element(By.TAG_NAME, "th").text == "Location":
+                locations.insert(0,tr.find_element(By.TAG_NAME, "td").find_element(By.TAG_NAME, "a").text)
+
+    print("semantic search for variable use of 'success' where it must be 1 found", len(results), "results")
+    for l in locations:
+        print(l)
+    assert(len(results) == 2)
+    assert("tests/regression/00-sanity/01-assert.c:10" in locations)
+    assert("tests/regression/00-sanity/01-assert.c:5" in locations)
+
+    # clear results
+    leftS.find_element(By.CLASS_NAME, "clear-btn").click()
+
+    # test semantic search 2
+    textfield = leftS.find_element(By.CLASS_NAME, "form-control")
+    textfield.clear()
+    textfield.send_keys('{"kind":["var"],"target":["name","success"],"find":["uses"],"expression":"success == 0","mode":["Must"]}')
+    leftS.find_element(By.CLASS_NAME, "exec-button").click()
+    results = leftS.find_elements(By.CLASS_NAME, "list-group-item")
+    locations = []
+    for r in results:
+        for tr in r.find_elements(By.TAG_NAME, "tr"):
+            if tr.find_element(By.TAG_NAME, "th").text == "Location":
+                locations.insert(0,tr.find_element(By.TAG_NAME, "td").find_element(By.TAG_NAME, "a").text)
+
+    print("semantic search for variable use of 'success' where it must be 0 found", len(results), "results")
+    for l in locations:
+        print(l)
+    assert(len(results) == 0)
+
+    # close "No results found" alert
+    leftS.find_element(By.CLASS_NAME, "btn-close").click()
+
     cleanup(browser, thread)
 
 except Exception as e:

src/analyses/apron/affineEqualityAnalysis.apron.ml

@@ -9,16 +9,10 @@ include RelationAnalysis
 let spec_module: (module MCPSpec) Lazy.t =
   lazy (
     let module AD = AffineEqualityDomain.D2 (VectorMatrix.ArrayVector) (VectorMatrix.ArrayMatrix) in
-    let module RD: RelationDomain.RD =
-    struct
-      module V = AffineEqualityDomain.V
-      include AD
-    end
-    in
     let module Priv = (val RelationPriv.get_priv ()) in
     let module Spec =
     struct
-      include SpecFunctor (Priv) (RD) (RelationPrecCompareUtil.DummyUtil)
+      include SpecFunctor (Priv) (AD) (RelationPrecCompareUtil.DummyUtil)
       let name () = "affeq"
     end
     in

src/analyses/apron/apronAnalysis.apron.ml

@@ -9,18 +9,11 @@ let spec_module: (module MCPSpec) Lazy.t =
     let module Man = (val ApronDomain.get_manager ()) in
     let module AD = ApronDomain.D2 (Man) in
     let diff_box = GobConfig.get_bool "ana.apron.invariant.diff-box" in
-    let module AD = (val if diff_box then (module ApronDomain.BoxProd (AD): ApronDomain.S3) else (module AD)) in
-    let module RD: RelationDomain.RD =
-    struct
-      module V = ApronDomain.V
-      include AD
-      type var = Apron.Var.t
-    end
-    in
+    let module AD = (val if diff_box then (module ApronDomain.BoxProd (AD): RelationDomain.RD) else (module AD)) in
     let module Priv = (val RelationPriv.get_priv ()) in
     let module Spec =
     struct
-      include SpecFunctor (Priv) (RD) (ApronPrecCompareUtil.Util)
+      include SpecFunctor (Priv) (AD) (ApronPrecCompareUtil.Util)
       let name () = "apron"
     end
     in