Skip to content

Commit 55de434

Browse files
sim642sim642
authored
Merge pull request #1601 from goblint/svcomp25-dev
SV-COMP 2025 development
2 parents d287916 + 0ca1bb3 commit 55de434

File tree

26 files changed

+402
-15
lines changed

26 files changed

+402
-15
lines changed

‎CHANGELOG.md

+12-1
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,14 @@
1+
## v2.5.0 (unreleased)
2+
Functionally equivalent to Goblint in SV-COMP 2025.
3+
4+
* Add 32bit vs 64bit architecture support (#54, #1574).
5+
* Add per-function context gas analysis (#1569, #1570, #1598).
6+
* Adapt automatic static loop unrolling (#1516, #1582, #1583, #1584, #1590, #1595, #1599).
7+
* Adapt automatic configuration tuning (#1450, #1612, #1181, #1604).
8+
* Simplify non-relational integer invariants in witnesses (#1517).
9+
* Fix excessive hash collisions (#1594, #1602).
10+
* Clean up various code (#1095, #1523, #1554, #1575, #1588, #1597, #1614).
11+
112
## v2.4.0
213
* Remove unmaintained analyses: spec, file (#1281).
314
* Add linear two-variable equalities analysis (#1297, #1412, #1466).
@@ -10,7 +21,7 @@
1021
* Fix mutex type analysis unsoundness and enable it by default (#1414, #1416, #1510).
1122
* Add points-to set refinement on mutex path splitting (#1287, #1343, #1374, #1396, #1407).
1223
* Improve narrowing operators (#1502, #1540, #1543).
13-
* Extract automatic configuration tuning for soundness (#1369).
24+
* Extract automatic configuration tuning for soundness (#1469).
1425
* Fix many locations in witnesses (#1355, #1372, #1400, #1403).
1526
* Improve output readability (#1294, #1312, #1405, #1497).
1627
* Refactor logging (#1117).

‎conf/svcomp25-validate.json

+123
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,123 @@
1+
{
2+
"ana": {
3+
"sv-comp": {
4+
"enabled": true,
5+
"functions": true
6+
},
7+
"int": {
8+
"def_exc": true,
9+
"enums": false,
10+
"interval": true
11+
},
12+
"float": {
13+
"interval": true,
14+
"evaluate_math_functions": true
15+
},
16+
"activated": [
17+
"base",
18+
"threadid",
19+
"threadflag",
20+
"threadreturn",
21+
"mallocWrapper",
22+
"mutexEvents",
23+
"mutex",
24+
"access",
25+
"race",
26+
"escape",
27+
"expRelation",
28+
"mhp",
29+
"assert",
30+
"var_eq",
31+
"symb_locks",
32+
"region",
33+
"thread",
34+
"threadJoins",
35+
"abortUnless",
36+
"unassume"
37+
],
38+
"path_sens": [
39+
"mutex",
40+
"malloc_null",
41+
"uninit",
42+
"expsplit",
43+
"activeSetjmp",
44+
"memLeak",
45+
"threadflag"
46+
],
47+
"context": {
48+
"widen": false
49+
},
50+
"base": {
51+
"arrays": {
52+
"domain": "partitioned"
53+
}
54+
},
55+
"race": {
56+
"free": false,
57+
"call": false
58+
},
59+
"autotune": {
60+
"enabled": true,
61+
"activated": [
62+
"singleThreaded",
63+
"mallocWrappers",
64+
"noRecursiveIntervals",
65+
"enums",
66+
"congruence",
67+
"octagon",
68+
"wideningThresholds",
69+
"loopUnrollHeuristic",
70+
"memsafetySpecification",
71+
"noOverflows",
72+
"termination",
73+
"tmpSpecialAnalysis"
74+
]
75+
},
76+
"widen": {
77+
"tokens": true
78+
}
79+
},
80+
"exp": {
81+
"region-offsets": true
82+
},
83+
"solver": "td3",
84+
"sem": {
85+
"unknown_function": {
86+
"spawn": false
87+
},
88+
"int": {
89+
"signed_overflow": "assume_none"
90+
},
91+
"null-pointer": {
92+
"dereference": "assume_none"
93+
}
94+
},
95+
"witness": {
96+
"graphml": {
97+
"enabled": false
98+
},
99+
"yaml": {
100+
"enabled": false,
101+
"strict": true,
102+
"format-version": "2.0",
103+
"entry-types": [
104+
"location_invariant",
105+
"loop_invariant",
106+
"invariant_set",
107+
"violation_sequence"
108+
],
109+
"invariant-types": [
110+
"location_invariant",
111+
"loop_invariant"
112+
]
113+
},
114+
"invariant": {
115+
"loop-head": true,
116+
"after-lock": true,
117+
"other": true
118+
}
119+
},
120+
"pre": {
121+
"enabled": false
122+
}
123+
}

‎conf/svcomp25.json

+118
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,118 @@
1+
{
2+
"ana": {
3+
"sv-comp": {
4+
"enabled": true,
5+
"functions": true
6+
},
7+
"int": {
8+
"def_exc": true,
9+
"enums": false,
10+
"interval": true
11+
},
12+
"float": {
13+
"interval": true,
14+
"evaluate_math_functions": true
15+
},
16+
"activated": [
17+
"base",
18+
"threadid",
19+
"threadflag",
20+
"threadreturn",
21+
"mallocWrapper",
22+
"mutexEvents",
23+
"mutex",
24+
"access",
25+
"race",
26+
"escape",
27+
"expRelation",
28+
"mhp",
29+
"assert",
30+
"var_eq",
31+
"symb_locks",
32+
"region",
33+
"thread",
34+
"threadJoins",
35+
"abortUnless"
36+
],
37+
"path_sens": [
38+
"mutex",
39+
"malloc_null",
40+
"uninit",
41+
"expsplit",
42+
"activeSetjmp",
43+
"memLeak",
44+
"threadflag"
45+
],
46+
"context": {
47+
"widen": false
48+
},
49+
"base": {
50+
"arrays": {
51+
"domain": "partitioned"
52+
}
53+
},
54+
"race": {
55+
"free": false,
56+
"call": false
57+
},
58+
"autotune": {
59+
"enabled": true,
60+
"activated": [
61+
"singleThreaded",
62+
"mallocWrappers",
63+
"noRecursiveIntervals",
64+
"enums",
65+
"congruence",
66+
"octagon",
67+
"wideningThresholds",
68+
"loopUnrollHeuristic",
69+
"memsafetySpecification",
70+
"noOverflows",
71+
"termination",
72+
"tmpSpecialAnalysis"
73+
]
74+
}
75+
},
76+
"exp": {
77+
"region-offsets": true
78+
},
79+
"solver": "td3",
80+
"sem": {
81+
"unknown_function": {
82+
"spawn": false
83+
},
84+
"int": {
85+
"signed_overflow": "assume_none"
86+
},
87+
"null-pointer": {
88+
"dereference": "assume_none"
89+
}
90+
},
91+
"witness": {
92+
"graphml": {
93+
"enabled": true,
94+
"id": "enumerate",
95+
"unknown": false
96+
},
97+
"yaml": {
98+
"enabled": true,
99+
"format-version": "2.0",
100+
"entry-types": [
101+
"invariant_set"
102+
],
103+
"invariant-types": [
104+
"loop_invariant"
105+
]
106+
},
107+
"invariant": {
108+
"loop-head": true,
109+
"after-lock": false,
110+
"other": false,
111+
"accessed": false,
112+
"exact": true
113+
}
114+
},
115+
"pre": {
116+
"enabled": false
117+
}
118+
}

‎docs/developer-guide/releasing.md

+2
Original file line numberDiff line numberDiff line change
@@ -77,6 +77,8 @@
7777

7878
This includes: git tag name, git tag message and zipped conf file.
7979

80+
5. Open MR with conf file name to the [bench-defs](https://gitlab.com/sosy-lab/sv-comp/bench-defs) repository.
81+
8082
### For each prerun
8183

8284
1. Update opam pins:

‎lib/sv-comp/stub/src/sv-comp.c

+4-4
Original file line numberDiff line numberDiff line change
@@ -35,10 +35,10 @@ __VERIFIER_nondet2(unsigned int, u32)
3535
__VERIFIER_nondet2(unsigned short int, u16) // not in rules
3636
__VERIFIER_nondet2(unsigned char, u8) // not in rules
3737
__VERIFIER_nondet2(unsigned char, unsigned_char) // not in rules
38-
__VERIFIER_nondet2(long long, longlong) // not in rules yet (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1341)
39-
__VERIFIER_nondet2(unsigned long long, ulonglong) // not in rules yet (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1341)
40-
__VERIFIER_nondet2(__uint128_t, uint128) // not in rules yet (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1341)
41-
__VERIFIER_nondet2(__int128_t, int128) // not in rules yet (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1341)
38+
__VERIFIER_nondet2(long long, longlong)
39+
__VERIFIER_nondet2(unsigned long long, ulonglong)
40+
__VERIFIER_nondet2(__uint128_t, uint128)
41+
__VERIFIER_nondet2(__int128_t, int128)
4242
__VERIFIER_nondet2(unsigned char, uchar)
4343
__VERIFIER_nondet2(unsigned int, uint)
4444
__VERIFIER_nondet2(unsigned long, ulong)

‎scripts/sv-comp/archive.sh

+3-3
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44

55
make clean
66

7-
git tag -m "SV-COMP 2024" svcomp24
7+
git tag -m "SV-COMP 2025" svcomp25
88

99
dune build --profile=release src/goblint.exe
1010
rm -f goblint
@@ -32,8 +32,8 @@ zip goblint/scripts/sv-comp/goblint.zip \
3232
goblint/lib/libboxD.so \
3333
goblint/lib/libpolkaMPQ.so \
3434
goblint/lib/LICENSE.APRON \
35-
goblint/conf/svcomp24.json \
36-
goblint/conf/svcomp24-validate.json \
35+
goblint/conf/svcomp25.json \
36+
goblint/conf/svcomp25-validate.json \
3737
goblint/lib/libc/stub/include/assert.h \
3838
goblint/lib/goblint/runtime/include/goblint.h \
3939
goblint/lib/libc/stub/src/stdlib.c \

‎src/analyses/unassumeAnalysis.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -71,7 +71,7 @@ struct
7171
| _ -> ()
7272
);
7373

74-
let yaml = match Yaml_unix.of_file (Fpath.v (GobConfig.get_string "witness.yaml.unassume")) with
74+
let yaml = match GobResult.Syntax.(Fpath.of_string (GobConfig.get_string "witness.yaml.unassume") >>= Yaml_unix.of_file) with
7575
| Ok yaml -> yaml
7676
| Error (`Msg m) ->
7777
Logs.error "Yaml_unix.of_file: %s" m;

‎src/config/options.schema.json

+1-1
Original file line numberDiff line numberDiff line change
@@ -2674,7 +2674,7 @@
26742674
},
26752675
"strict": {
26762676
"title": "witness.yaml.strict",
2677-
"description": "",
2677+
"description": "Fail YAML witness validation if there's an error/unsupported/disabled entry.",
26782678
"type": "boolean",
26792679
"default": false
26802680
},

‎src/util/std/gobYaml.ml

+2
Original file line numberDiff line numberDiff line change
@@ -44,3 +44,5 @@ let list = function
4444
let entries = function
4545
| `O assoc -> Ok assoc
4646
| _ -> Error (`Msg "Failed to get entries from non-object value")
47+
48+
let int i = float (float_of_int i)

0 commit comments

Comments
 (0)