From 380979e71c0d3e2b47a05b59b3eee67ea5cf7785 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 23 Jan 2024 13:50:39 +0200 Subject: [PATCH 1/3] Copy VMCAI 2024 artifact description from bench repo --- docs/artifact-descriptions/vmcai24.md | 76 +++++++++++++++++++++++++++ mkdocs.yml | 1 + 2 files changed, 77 insertions(+) create mode 100644 docs/artifact-descriptions/vmcai24.md diff --git a/docs/artifact-descriptions/vmcai24.md b/docs/artifact-descriptions/vmcai24.md new file mode 100644 index 0000000000..3673937dc6 --- /dev/null +++ b/docs/artifact-descriptions/vmcai24.md @@ -0,0 +1,76 @@ +# Correctness Witness Validation by Abstract Interpretation +## Artifact + +This artifact contains everything mentioned in the evaluation section of the paper: Goblint implementation, scripts, benchmarks, manual witnesses and other tools. + +**Note to artifact reviewers:** in the smoke test phase, try to only run the performance evaluation since it is very quick compared to the precision evaluation. + +## 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. diff --git a/mkdocs.yml b/mkdocs.yml index 428e28078d..8064703c12 100644 --- a/mkdocs.yml +++ b/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 From 3625b6719c2e41064809900c9d408667846c932a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 23 Jan 2024 13:51:23 +0200 Subject: [PATCH 2/3] Fix lists in VMACI24 artifact description --- docs/artifact-descriptions/vmcai24.md | 41 ++++++++++++++------------- 1 file changed, 22 insertions(+), 19 deletions(-) diff --git a/docs/artifact-descriptions/vmcai24.md b/docs/artifact-descriptions/vmcai24.md index 3673937dc6..9f44bd20e4 100644 --- a/docs/artifact-descriptions/vmcai24.md +++ b/docs/artifact-descriptions/vmcai24.md @@ -17,13 +17,14 @@ This artifact contains everything mentioned in the evaluation section of the pap * `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). + 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. @@ -36,13 +37,14 @@ This artifact contains everything mentioned in the evaluation section of the pap 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). + 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. @@ -50,11 +52,12 @@ This artifact contains everything mentioned in the evaluation section of the pap 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. + 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. From d57d3c1193253ce69f36c7be4e618ad94e7be12c Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 23 Jan 2024 14:26:16 +0200 Subject: [PATCH 3/3] Rewrite VMCAI24 artifact description intro --- docs/artifact-descriptions/vmcai24.md | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/docs/artifact-descriptions/vmcai24.md b/docs/artifact-descriptions/vmcai24.md index 9f44bd20e4..860ef6c9fd 100644 --- a/docs/artifact-descriptions/vmcai24.md +++ b/docs/artifact-descriptions/vmcai24.md @@ -1,9 +1,13 @@ -# Correctness Witness Validation by Abstract Interpretation -## Artifact +# 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. -**Note to artifact reviewers:** in the smoke test phase, try to only run the performance evaluation since it is very quick compared to the precision evaluation. +**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/).