Skip to content

Commit fa83790

Browse files
sim642sim642
authored
Merge pull request #391 from goblint/interactive
Interactive analysis
2 parents 712c6ce + 4b5e3d9 commit fa83790

File tree

205 files changed

+4681
-565
lines changed

Some content is hidden

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

205 files changed

+4681
-565
lines changed

‎.github/workflows/locked.yml‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -44,8 +44,9 @@ jobs:
4444
run: |
4545
ruby scripts/update_suite.rb group apron -s
4646
ruby scripts/update_suite.rb group apron2 -s
47+
4748
- name: Test apron octagon regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
48-
run: ruby scripts/update_suite.rb group octagon -s
49+
run: ruby scripts/update_suite.rb group octagon -s
4950

5051
- name: Test apron regression (Mukherjee et. al SAS '17 paper') # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
5152
run: ruby scripts/update_suite.rb group apron-mukherjee -s

‎.github/workflows/unlocked.yml‎

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -64,7 +64,7 @@ jobs:
6464
6565
- name: Test apron octagon regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
6666
if: ${{ matrix.apron }}
67-
run: ruby scripts/update_suite.rb group octagon -s
67+
run: ruby scripts/update_suite.rb group octagon -s
6868

6969
- name: Test apron regression (Mukherjee et. al SAS '17 paper') # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
7070
if: ${{ matrix.apron }}
@@ -135,10 +135,12 @@ jobs:
135135

136136
- name: Test apron regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
137137
# if: ${{ matrix.apron }}
138-
run: ruby scripts/update_suite.rb group apron -s
138+
run: |
139+
ruby scripts/update_suite.rb group apron -s
140+
ruby scripts/update_suite.rb group apron2 -s
139141
140142
- name: Test apron octagon regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
141-
run: ruby scripts/update_suite.rb group octagon -s
143+
run: ruby scripts/update_suite.rb group octagon -s
142144

143145
- name: Test apron regression (Mukherjee et. al SAS '17 paper') # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
144146
# if: ${{ matrix.apron }}
@@ -228,10 +230,12 @@ jobs:
228230

229231
- name: Test apron regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
230232
# if: ${{ matrix.apron }}
231-
run: ruby scripts/update_suite.rb group apron -s
233+
run: |
234+
ruby scripts/update_suite.rb group apron -s
235+
ruby scripts/update_suite.rb group apron2 -s
232236
233237
- name: Test apron octagon regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
234-
run: ruby scripts/update_suite.rb group octagon -s
238+
run: ruby scripts/update_suite.rb group octagon -s
235239

236240
- name: Test apron regression (Mukherjee et. al SAS '17 paper') # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
237241
# if: ${{ matrix.apron }}

‎.semgrep/cil.yml‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,10 @@ rules:
77
- pattern: Cil.typeOffset
88
- pattern: Cil.mkCast
99
- pattern: Cil.get_stmtLoc
10+
- pattern: Cil.get_instrLoc
1011
paths:
1112
exclude:
13+
- cilfacade0.ml
1214
- cilfacade.ml
1315
message: use Cilfacade instead
1416
languages: [ocaml]

‎conf/zstd-race.json‎

Lines changed: 96 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,96 @@
1+
{
2+
"ana": {
3+
"activated": [
4+
"expRelation", "base", "threadid", "threadflag", "threadreturn",
5+
"escape", "mutexEvents", "mutex", "access", "mallocWrapper", "mhp",
6+
"symb_locks", "var_eq", "mallocFresh"
7+
],
8+
"ctx_insens": [
9+
"var_eq"
10+
],
11+
"base": {
12+
"privatization": "none",
13+
"context": {
14+
"non-ptr": false
15+
}
16+
},
17+
"thread": {
18+
"domain": "plain",
19+
"include-node": false
20+
},
21+
"malloc": {
22+
"wrappers": [
23+
"ZSTD_customMalloc",
24+
"ZSTD_customCalloc"
25+
]
26+
},
27+
"race": {
28+
"free": false
29+
},
30+
"dead-code": {
31+
"lines": true
32+
}
33+
},
34+
"sem": {
35+
"unknown_function": {
36+
"spawn": false,
37+
"invalidate": {
38+
"globals": false,
39+
"args": false
40+
}
41+
}
42+
},
43+
"incremental": {
44+
"reluctant": {
45+
"compare": "leq"
46+
},
47+
"restart": {
48+
"sided": {
49+
"enabled": false
50+
}
51+
}
52+
},
53+
"solvers": {
54+
"td3": {
55+
"restart": {
56+
"wpoint": {
57+
"enabled": false
58+
}
59+
}
60+
}
61+
},
62+
"exp": {
63+
"earlyglobs": true,
64+
"extraspecials": [
65+
"ZSTD_customMalloc",
66+
"ZSTD_customCalloc",
67+
"ZSTD_customFree"
68+
]
69+
},
70+
"pre": {
71+
"cppflags": ["-DZSTD_NO_INTRINSICS", "-D_FORTIFY_SOURCE=0", "-DGOBLINT_NO_ASSERT", "-DGOBLINT_NO_BSEARCH"]
72+
},
73+
"cil": {
74+
"merge": {
75+
"inlines": false
76+
}
77+
},
78+
"printstats": true,
79+
"warn": {
80+
"assert": false,
81+
"behavior": false,
82+
"integer": false,
83+
"cast": false,
84+
"race": true,
85+
"deadcode": true,
86+
"analyzer": false,
87+
"unsound": false,
88+
"imprecise": false,
89+
"unknown": false,
90+
"error": false,
91+
"warning": true,
92+
"info": false,
93+
"debug": false,
94+
"success": true
95+
}
96+
}

‎docs/user-guide/annotating.md‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,3 +25,11 @@ The following string arguments are supported:
2525
3. `base.non-ptr`/`base.no-non-ptr` to override the `ana.base.context.non-ptr` option.
2626
4. `apron.context`/`apron.no-context` to override the `ana.apron.context` option.
2727
5. `widen`/`no-widen` to override the `ana.context.widen` option.
28+
29+
30+
## Functions
31+
Goblint-specific functions can be called in the code, where they assist the analyzer but have no runtime effect.
32+
33+
* `__goblint_assume_join(id)` is like `pthread_join(id)`, but considers the given thread IDs must-joined even if Goblint cannot, e.g. due to non-uniqueness.
34+
Notably, this annotation can be used after a threads joining loop to make the assumption that the loop correctly joined all those threads.
35+
_Misuse of this annotation can cause unsoundness._

‎docs/user-guide/configuring.md‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,8 @@ In `.vscode/settings.json` add the following:
2121
"json.schemas": [
2222
{
2323
"fileMatch": [
24-
"/conf/*.json"
24+
"/conf/*.json",
25+
"/tests/incremental/*/*.json"
2526
],
2627
"url": "/src/util/options.schema.json"
2728
}

‎gobview‎

‎scripts/fix_patch_headers.sh‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
#!/bin/bash
2+
#Run from root, e.g.,: ./scripts/fix_patch_headers.sh tests/incremental/11-restart/*.patch
3+
for file in "$@"
4+
do
5+
echo $file
6+
cfile="${file%.patch}.c"
7+
efile="${cfile//\//\\/}"
8+
perl -0777 -i -pe "s/.*?@/--- $efile\n+++ $efile\n@/is" $file
9+
done

‎scripts/test-incremental.sh‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,15 +11,15 @@ source=$base/$test.c
1111
conf=$base/$test.json
1212
patch=$base/$test.patch
1313

14-
args="--enable dbg.debug --enable printstats -v"
14+
args="--enable dbg.debug --enable printstats -v --enable allglobs"
1515

1616
./goblint --conf $conf $args --enable incremental.save $source &> $base/$test.before.log
1717

1818
patch -p0 -b <$patch
1919

2020
./goblint --conf $conf $args --enable incremental.load --set save_run $base/$test-incrementalrun $source &> $base/$test.after.incr.log
2121
./goblint --conf $conf $args --enable incremental.only-rename --set save_run $base/$test-originalrun $source &> $base/$test.after.scratch.log
22-
./goblint --conf $conf --enable dbg.compare_runs.diff --compare_runs $base/$test-originalrun $base/$test-incrementalrun $source
22+
./goblint --conf $conf --disable dbg.compare_runs.globsys --enable dbg.compare_runs.diff --compare_runs $base/$test-originalrun $base/$test-incrementalrun $source
2323

2424
patch -p0 -b -R <$patch
2525
rm -r $base/$test-originalrun $base/$test-incrementalrun

‎scripts/update_suite.rb‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -161,6 +161,7 @@ def collect_warnings
161161
when /invariant refuted/ then "fail"
162162
when /^\[Warning\]/ then "warn"
163163
when /^\[Error\]/ then "warn"
164+
when /^\[Info\]/ then "warn"
164165
when /^\[Success\]/ then "success"
165166
when /\[Debug\]/ then next # debug "warnings" shouldn't count as other warnings (against NOWARN)
166167
when /^ on line \d+ $/ then next # dead line warnings shouldn't count (used for unreachability with NOWARN)
@@ -416,8 +417,13 @@ def create_test_set(lines)
416417
super(lines)
417418
@testset.p = self
418419
`patch -p0 -b <#{patch_path}`
420+
status = $?.exitstatus
419421
lines_incr = IO.readlines(path)
420422
`patch -p0 -b -R <#{patch_path}`
423+
if status != 0
424+
puts "Failed to apply patch: #{patch_path}"
425+
exit 1
426+
end
421427
@testset_incr = parse_tests(lines_incr)
422428
@testset_incr.p = self
423429
@testset_incr.warnfile = File.join($testresults, group, name + ".incr.warn.txt")

0 commit comments

Comments
 (0)