Skip to content

Commit c0da7a7

Browse files
sim642sim642
committed
Merge branch 'master' into priv-atomic
2 parents 6a2d078 + aec0d79 commit c0da7a7

File tree

165 files changed

+2525
-1810
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

165 files changed

+2525
-1810
lines changed

‎.git-blame-ignore-revs

+3
Original file line numberDiff line numberDiff line change
@@ -31,3 +31,6 @@ ec8611a3a72ae0d95ec82ffee16c5c4785111aa1
3131

3232
# fix indentation in baseInvariant
3333
f3ffd5e45c034574020f56519ccdb021da2a1479
34+
35+
# Fix indentation in various non-legacy code
36+
c3e2cc848479ae86de5542b6ab0e75a74e9cf8c9

‎.github/workflows/unlocked.yml

-3
Original file line numberDiff line numberDiff line change
@@ -34,9 +34,6 @@ jobs:
3434
- os: ubuntu-latest
3535
ocaml-compiler: 4.14.x
3636
z3: true
37-
- os: ubuntu-latest
38-
ocaml-compiler: 5.0.0
39-
apron: false
4037

4138
# customize name to use readable string for apron instead of just a boolean
4239
# workaround for missing ternary operator: https://github.com/actions/runner/issues/409

‎.semgrep/logs.yml

+38
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
rules:
2+
- id: print-not-logging
3+
pattern-either:
4+
- pattern: printf
5+
- pattern: Printf.printf
6+
- pattern: BatPrintf.printf
7+
- pattern: Format.printf
8+
- pattern: Pretty.printf
9+
10+
- pattern: eprintf
11+
- pattern: Printf.eprintf
12+
- pattern: BatPrintf.eprintf
13+
- pattern: Format.eprintf
14+
- pattern: Pretty.eprintf
15+
16+
- pattern: print_endline
17+
- pattern: prerr_endline
18+
- pattern: print_string
19+
paths:
20+
exclude:
21+
- logs.ml
22+
- bench/
23+
message: printing should be replaced with logging
24+
languages: [ocaml]
25+
severity: WARNING
26+
27+
- id: print-newline-not-logging
28+
pattern-either:
29+
- pattern: print_newline
30+
- pattern: prerr_newline
31+
paths:
32+
exclude:
33+
- logs.ml
34+
- bench/
35+
fix: Logs.newline
36+
message: use Logs instead
37+
languages: [ocaml]
38+
severity: WARNING

‎README.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ For benchmarking Goblint, please follow the [Benchmarking guide on Read the Docs
2424
6. _Optional:_ See [`scripts/bash-completion.sh`](./scripts/bash-completion.sh) for setting up bash completion for Goblint arguments.
2525

2626
### MacOS
27-
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.
27+
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.
2828
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/`.
2929
3. Continue using Linux instructions (the formulae in brew for `patch`, `libgmp-dev`, `libmpfr-dev` are `gpatch`, `gmp`, `mpfr`, respectively).
3030

‎conf/incremental.json

+1-1
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@
2424
"earlyglobs": true
2525
},
2626
"dbg": {
27-
"verbose": true,
27+
"level": "debug",
2828
"trace": {
2929
"context": true
3030
},

‎conf/minimal_incremental.json

+1-1
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@
2323
"earlyglobs": true
2424
},
2525
"dbg": {
26-
"verbose": true,
26+
"level": "debug",
2727
"trace": {
2828
"context": true
2929
},

‎docs/artifact-descriptions/vmcai24.md

+83
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
1+
# VMCAI '24 Artifact Description
2+
## Correctness Witness Validation by Abstract Interpretation
3+
4+
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).
5+
The artifact is available on [Zenodo](https://doi.org/10.5281/zenodo.8253000).
6+
7+
This artifact contains everything mentioned in the evaluation section of the paper: Goblint implementation, scripts, benchmarks, manual witnesses and other tools.
8+
9+
**The description here is provided for convenience and not maintained.**
10+
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).
11+
12+
## Requirements
13+
* [VirtualBox](https://www.virtualbox.org/).
14+
* 2 CPU cores.
15+
* 8 GB RAM.
16+
* 7 GB disk space.
17+
* ~45min.
18+
19+
## Layout
20+
* `README.md`/`README.pdf` — this file.
21+
* `LICENSE`.
22+
* `unassume.ova` — VirtualBox virtual machine.
23+
24+
In `/home/vagrant` contains:
25+
26+
* `goblint/` ­— Goblint with unassume support, including source code.
27+
* `CPAchecker-2.2-unix/` — CPAchecker from [SV-COMP 2023 archives](https://gitlab.com/sosy-lab/sv-comp/archives-2023).
28+
* `UAutomizer-linux/` — Ultimate Automizer from [SV-COMP 2023 archives](https://gitlab.com/sosy-lab/sv-comp/archives-2023).
29+
* `eval-prec/` — precision evaluation (script, benchmarks, manual witnesses).
30+
* `eval-perf/` — performance evaluation (script, benchmarks, manual witnesses).
31+
* `results/` — results (initially empty).
32+
33+
* `results/` — evaluation results tables with data used for the paper.
34+
35+
## Reproduction
36+
1. Import the virtual machine into VirtualBox.
37+
2. Start the virtual machine and log in with username "vagrant" (not "Ubuntu"!) and password "vagrant".
38+
3. Right click on the desktop and open Applications → Accessories → Terminal Emulator.
39+
40+
### Precision evaluation
41+
1. Run `./eval-prec/run.sh` in the terminal emulator. This takes ~42min.
42+
2. Run `firefox results/eval-prec/table-generator.table.html` to view the results.
43+
44+
The HTML table contains the following status columns (cputime, walltime and memory can be ignored):
45+
46+
1. Goblint w/o witness (true means verified).
47+
2. Goblint w/ manual witness (true means witness validated).
48+
3. Goblint w/ witness from CPAchecker (true means program verified with witness-guidance).
49+
4. Goblint w/ witness from CPAchecker (true means witness validated).
50+
5. Goblint w/ witness from UAutomizer (true means program verified with witness-guidance).
51+
6. Goblint w/ witness from UAutomizer (true means witness validated).
52+
53+
Table 1 in the paper presents these results, except the rows are likely in a different order.
54+
55+
### Performance evaluation
56+
1. Run `./eval-perf/run.sh` in the terminal emulator. This takes ~30s.
57+
2. Run `firefox results/eval-perf/table-generator.table.html` to view the results.
58+
59+
The HTML table contains the following relevant columns (others can be ignored):
60+
61+
1. Goblint w/o witness, evals.
62+
2. Goblint w/o witness, cputime.
63+
3. Goblint w/ manual witness, evals.
64+
4. Goblint w/ manual witness, cputime.
65+
66+
Table 2 in the paper presents these results, except the rows are likely in a different order.
67+
68+
69+
## Goblint implementation
70+
[Goblint](https://github.com/goblint/analyzer) is an open source static analysis framework for C.
71+
Goblint itself is written in OCaml.
72+
Being open source, it allows existing implementations of analyses and abstract domains to be reused and modified.
73+
As a framework, it also allows new ones to be easily added.
74+
For more details, refer to the linked GitHub repository and related documentation.
75+
76+
Key parts of the code related to this paper are the following:
77+
78+
1. `src/analyses/unassumeAnalysis.ml`: analysis, which emits unassume operation events to other analyses for YAML-witness–guided verification.
79+
2. `src/analyses/base.ml` lines 2551–2641: propagating unassume for non-relational domains of the `base` analysis.
80+
3. `src/analyses/apron/relationAnalysis.apron.ml` lines 668–693: strengthening-based dual-narrowing unassume for relational Apron domains of the `apron` analysis.
81+
4. `src/cdomains/apron/apronDomain.apron.ml` lines 625–679: strengthening operator used for dual-narrowing of Apron domains.
82+
5. `src/util/wideningTokens.ml`: analysis lifter that adds widening tokens for delaying widenings from unassuming.
83+
6. `src/witness/yamlWitness.ml` lines 398–683: YAML witness validation.

‎docs/developer-guide/debugging.md

+19-12
Original file line numberDiff line numberDiff line change
@@ -1,39 +1,46 @@
11
# Debugging
22

3-
## Printing
4-
Goblint extensively uses [CIL's `Pretty`](https://people.eecs.berkeley.edu/~necula/cil/api/Pretty.html) module for printing due to many non-primitive values.
3+
## Logging
4+
Instead of debug printing directly to `stdout`, all logging should be done using the `Logs` module.
5+
This allows for consistent pretty terminal output, as well as avoiding interference with server mode.
6+
There are five logging levels: result, error, warning, info and debug.
7+
Log output is controlled by the `dbg.level` option, which defaults to "info".
58

6-
* Printing CIL values (e.g. an expression `exp`) using the corresponding pretty-printer `d_exp` from `Cil` module:
9+
Logs are written to `stderr`, except for result level, which go to `stdout` by default.
10+
11+
Goblint extensively uses [CIL's `Pretty`](https://people.eecs.berkeley.edu/~necula/cil/api/Pretty.html) module for output due to many non-primitive values.
12+
13+
* Logging CIL values (e.g. an expression `exp`) using the corresponding pretty-printer `d_exp` from `Cil` module:
714

815
```ocaml
9-
ignore (Pretty.printf "A CIL exp: %a\n" d_exp exp);
16+
Logs.debug "A CIL exp: %a\n" d_exp exp;
1017
```
1118

12-
* Printing Goblint's `Printable` values (e.g. a domain `D` element `d`) using the corresponding pretty-printer `D.pretty`:
19+
* Logging Goblint's `Printable` values (e.g. a domain `D` element `d`) using the corresponding pretty-printer `D.pretty`:
1320

1421
```ocaml
15-
ignore (Pretty.printf "A domain element: %a\n" D.pretty d);
22+
Logs.debug "A domain element: %a\n" D.pretty d;
1623
```
1724

18-
* Printing primitives (e.g. OCaml ints, strings, etc) using the standard [OCaml `Printf`](https://ocaml.org/api/Printf.html) specifiers:
25+
* Logging primitives (e.g. OCaml ints, strings, etc) using the standard [OCaml `Printf`](https://ocaml.org/api/Printf.html) specifiers:
1926

2027
```ocaml
21-
ignore (Pretty.printf "An int and a string: %d %s\n" 42 "magic");
28+
Logs.debug "An int and a string: %d %s\n" 42 "magic";
2229
```
2330

24-
* Printing lists of pretty-printables (e.g. expressions list `exps`) using `d_list`:
31+
* Logging lists of pretty-printables (e.g. expressions list `exps`) using `d_list`:
2532

2633
```ocaml
27-
ignore (Pretty.printf "Some expressions: %a\n" (d_list ", " d_exp) exps);
34+
Logs.debug "Some expressions: %a\n" (d_list ", " d_exp) exps;
2835
```
2936

3037

3138
## Tracing
32-
Tracing is a nicer alternative to debug printing, because it can be disabled for best performance and it can be used to only see relevant tracing output.
39+
Tracing is a nicer alternative to some logging, because it can be disabled for best performance and it can be used to only see relevant tracing output.
3340

3441
Recompile with tracing enabled: `./scripts/trace_on.sh`.
3542

36-
Instead of debug printing use a tracing function from the `Messages` module, which is often aliased to just `M` (and pick a relevant name instead of `mything`):
43+
Instead of logging use a tracing function from the `Messages` module, which is often aliased to just `M` (and pick a relevant name instead of `mything`):
3744
```ocaml
3845
if M.tracing then M.trace "mything" "A domain element: %a\n" D.pretty d;
3946
```

‎docs/developer-guide/messaging.md

+2-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,8 @@
11
# Messaging
22

3-
The message system in `Messages` module should be used for outputting all (non-[tracing](./debugging.md#tracing)) information instead of printing them directly to `stdout`.
3+
The message system in `Messages` module should be used for outputting all analysis results of the program to the user, instead of printing them directly to `stdout`.
44
This allows for consistent pretty terminal output, as well as export to Goblint result viewers and IDEs.
5+
For other kinds of (debug) output, see [Debugging](./debugging.md).
56

67
## Message structure
78

‎docs/requirements.txt

+1-4
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,3 @@
11
# Python requirements for MkDocs and Read the Docs
22

3-
mkdocs==1.2.3
4-
5-
# TODO: temporary workaround for deprecated usage (https://github.com/mkdocs/mkdocs/issues/2794#issuecomment-1077705509)
6-
jinja2==3.0.3
3+
mkdocs==1.5.3

‎g2html

‎goblint.opam

+1-1
Original file line numberDiff line numberDiff line change
@@ -77,7 +77,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
7777
available: os-distribution != "alpine" & arch != "arm64"
7878
pin-depends: [
7979
# published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
80-
# [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#d2760bacfbfdb25a374254de44f2ff1cb5f42abd" ]
80+
[ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#3cb720fe333289aca998d67bd210c57a87248c51" ]
8181
# TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
8282
[ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
8383
]

‎goblint.opam.locked

+4
Original file line numberDiff line numberDiff line change
@@ -131,6 +131,10 @@ post-messages: [
131131
]
132132
# TODO: manually reordered to avoid opam pin crash: https://github.com/ocaml/opam/issues/4936
133133
pin-depends: [
134+
[
135+
"goblint-cil.2.0.3"
136+
"git+https://github.com/goblint/cil.git#3cb720fe333289aca998d67bd210c57a87248c51"
137+
]
134138
[
135139
"ppx_deriving.5.2.1"
136140
"git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6"

‎goblint.opam.template

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
available: os-distribution != "alpine" & arch != "arm64"
44
pin-depends: [
55
# published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
6-
# [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#d2760bacfbfdb25a374254de44f2ff1cb5f42abd" ]
6+
[ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#3cb720fe333289aca998d67bd210c57a87248c51" ]
77
# TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
88
[ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
99
]

‎gobview

Submodule gobview updated 57 files

‎mkdocs.yml

+1
Original file line numberDiff line numberDiff line change
@@ -39,3 +39,4 @@ nav:
3939
- '📦 Artifact descriptions':
4040
- "🇸 SAS '21": artifact-descriptions/sas21.md
4141
- "🇪 ESOP '23": artifact-descriptions/esop23.md
42+
- "🇻 VMCAI '24": artifact-descriptions/vmcai24.md

‎scripts/test-gobview.py

+66
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,72 @@ def serve():
6161
panel = browser.find_element(By.CLASS_NAME, "panel")
6262
print("found DOM elements main, sidebar-left, sidebar-right, content and panel")
6363

64+
# test syntactic search
65+
leftS.find_element(By.LINK_TEXT, "Search").click()
66+
leftS.find_element(By.CLASS_NAME, "switch-to-json").click()
67+
textfield = leftS.find_element(By.CLASS_NAME, "form-control")
68+
textfield.clear()
69+
textfield.send_keys('{"kind":["var"],"target":["name","fail"],"find":["uses"],"mode":["Must"]}')
70+
leftS.find_element(By.CLASS_NAME, "exec-button").click()
71+
results = leftS.find_elements(By.CLASS_NAME, "list-group-item")
72+
locations = []
73+
for r in results:
74+
for tr in r.find_elements(By.TAG_NAME, "tr"):
75+
if tr.find_element(By.TAG_NAME, "th").text == "Location":
76+
locations.insert(0,tr.find_element(By.TAG_NAME, "td").find_element(By.TAG_NAME, "a").text)
77+
78+
print("syntactic search for variable use of 'fail' found", len(results), "results")
79+
for l in locations:
80+
print(l)
81+
assert(len(results) == 2)
82+
assert("tests/regression/00-sanity/01-assert.c:7" in locations)
83+
assert("tests/regression/00-sanity/01-assert.c:12" in locations)
84+
85+
# clear results
86+
leftS.find_element(By.CLASS_NAME, "clear-btn").click()
87+
88+
# test semantic search 1
89+
textfield = leftS.find_element(By.CLASS_NAME, "form-control")
90+
textfield.clear()
91+
textfield.send_keys('{"kind":["var"],"target":["name","success"],"find":["uses"],"expression":"success == 1","mode":["Must"]}')
92+
leftS.find_element(By.CLASS_NAME, "exec-button").click()
93+
results = leftS.find_elements(By.CLASS_NAME, "list-group-item")
94+
locations = []
95+
for r in results:
96+
for tr in r.find_elements(By.TAG_NAME, "tr"):
97+
if tr.find_element(By.TAG_NAME, "th").text == "Location":
98+
locations.insert(0,tr.find_element(By.TAG_NAME, "td").find_element(By.TAG_NAME, "a").text)
99+
100+
print("semantic search for variable use of 'success' where it must be 1 found", len(results), "results")
101+
for l in locations:
102+
print(l)
103+
assert(len(results) == 2)
104+
assert("tests/regression/00-sanity/01-assert.c:10" in locations)
105+
assert("tests/regression/00-sanity/01-assert.c:5" in locations)
106+
107+
# clear results
108+
leftS.find_element(By.CLASS_NAME, "clear-btn").click()
109+
110+
# test semantic search 2
111+
textfield = leftS.find_element(By.CLASS_NAME, "form-control")
112+
textfield.clear()
113+
textfield.send_keys('{"kind":["var"],"target":["name","success"],"find":["uses"],"expression":"success == 0","mode":["Must"]}')
114+
leftS.find_element(By.CLASS_NAME, "exec-button").click()
115+
results = leftS.find_elements(By.CLASS_NAME, "list-group-item")
116+
locations = []
117+
for r in results:
118+
for tr in r.find_elements(By.TAG_NAME, "tr"):
119+
if tr.find_element(By.TAG_NAME, "th").text == "Location":
120+
locations.insert(0,tr.find_element(By.TAG_NAME, "td").find_element(By.TAG_NAME, "a").text)
121+
122+
print("semantic search for variable use of 'success' where it must be 0 found", len(results), "results")
123+
for l in locations:
124+
print(l)
125+
assert(len(results) == 0)
126+
127+
# close "No results found" alert
128+
leftS.find_element(By.CLASS_NAME, "btn-close").click()
129+
64130
cleanup(browser, thread)
65131

66132
except Exception as e:

‎src/analyses/apron/affineEqualityAnalysis.apron.ml

+1-7
Original file line numberDiff line numberDiff line change
@@ -9,16 +9,10 @@ include RelationAnalysis
99
let spec_module: (module MCPSpec) Lazy.t =
1010
lazy (
1111
let module AD = AffineEqualityDomain.D2 (VectorMatrix.ArrayVector) (VectorMatrix.ArrayMatrix) in
12-
let module RD: RelationDomain.RD =
13-
struct
14-
module V = AffineEqualityDomain.V
15-
include AD
16-
end
17-
in
1812
let module Priv = (val RelationPriv.get_priv ()) in
1913
let module Spec =
2014
struct
21-
include SpecFunctor (Priv) (RD) (RelationPrecCompareUtil.DummyUtil)
15+
include SpecFunctor (Priv) (AD) (RelationPrecCompareUtil.DummyUtil)
2216
let name () = "affeq"
2317
end
2418
in

‎src/analyses/apron/apronAnalysis.apron.ml

+2-9
Original file line numberDiff line numberDiff line change
@@ -9,18 +9,11 @@ let spec_module: (module MCPSpec) Lazy.t =
99
let module Man = (val ApronDomain.get_manager ()) in
1010
let module AD = ApronDomain.D2 (Man) in
1111
let diff_box = GobConfig.get_bool "ana.apron.invariant.diff-box" in
12-
let module AD = (val if diff_box then (module ApronDomain.BoxProd (AD): ApronDomain.S3) else (module AD)) in
13-
let module RD: RelationDomain.RD =
14-
struct
15-
module V = ApronDomain.V
16-
include AD
17-
type var = Apron.Var.t
18-
end
19-
in
12+
let module AD = (val if diff_box then (module ApronDomain.BoxProd (AD): RelationDomain.RD) else (module AD)) in
2013
let module Priv = (val RelationPriv.get_priv ()) in
2114
let module Spec =
2215
struct
23-
include SpecFunctor (Priv) (RD) (ApronPrecCompareUtil.Util)
16+
include SpecFunctor (Priv) (AD) (ApronPrecCompareUtil.Util)
2417
let name () = "apron"
2518
end
2619
in

0 commit comments

Comments
 (0)