Merge branch 'master' into z-module

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

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.

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

src/analyses/apron/relationAnalysis.apron.ml

@@ -158,13 +158,14 @@ struct
         {st' with rel = rel''}
       )
     | (Mem v, NoOffset) ->
-      begin match ask.f (Queries.MayPointTo v) with
-        | ad when Queries.AD.is_top ad -> st
-        | ad ->
-          let mvals = Queries.AD.to_mval ad in
-          let ass' = List.map (fun mval -> assign_to_global_wrapper ask getg sideg st (ValueDomain.Addr.Mval.to_cil mval) f) mvals in
-          List.fold_right D.join ass' (D.bot ())
-      end
+      let ad = ask.f (Queries.MayPointTo v) in
+      Queries.AD.fold (fun addr acc ->
+          match addr with
+          | ValueDomain.Addr.Addr mval ->
+            D.join acc (assign_to_global_wrapper ask getg sideg st (ValueDomain.Addr.Mval.to_cil mval) f)
+          | UnknownPtr | NullPtr | StrPtr _ ->
+            D.join acc st (* Ignore assign *)
+        ) ad (D.bot ())
     (* Ignoring all other assigns *)
     | _ ->
       st
@@ -381,6 +382,8 @@ struct
     if M.tracing then M.tracel "combine" "relation f: %a\n" CilType.Varinfo.pretty f.svar;
     if M.tracing then M.tracel "combine" "relation formals: %a\n" (d_list "," CilType.Varinfo.pretty) f.sformals;
     if M.tracing then M.tracel "combine" "relation args: %a\n" (d_list "," d_exp) args;
+    if M.tracing then M.tracel "combine" "relation st: %a\n" D.pretty st;
+    if M.tracing then M.tracel "combine" "relation fun_st: %a\n" D.pretty fun_st;
     let new_fun_rel = RD.add_vars fun_st.rel (RD.vars st.rel) in
     let arg_substitutes =
       let filter_actuals (x,e) =