Skip to content

Commit 9ce9249

Browse files
sim642sim642
authored
Merge pull request #796 from goblint/yaml-witness-unassume
Unassume witness invariants during solving
2 parents ca7b8ce + 6e76ea6 commit 9ce9249

File tree

110 files changed

+4802
-887
lines changed

Some content is hidden

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

110 files changed

+4802
-887
lines changed

‎bench/zarith/benchZarith.ml‎

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
(** Benchmark calculation of powers of 2 with Zarith.
2+
Originally for https://github.com/goblint/cil/pull/115.
3+
4+
dune exec bench/zarith/benchZarith.exe -- -a *)
5+
6+
open Benchmark
7+
open Benchmark.Tree
8+
9+
10+
let () =
11+
let pow2_pow n = Big_int_Z.power_int_positive_int 2 n in
12+
let pow2_lsl n = Big_int_Z.shift_left_big_int Big_int_Z.unit_big_int n in
13+
14+
15+
register (
16+
"pow2" @>>> [
17+
"8" @> lazy (
18+
let arg = 8 in
19+
throughputN 1 [
20+
("pow", pow2_pow, arg);
21+
("lsl", pow2_lsl, arg);
22+
]
23+
);
24+
"16" @> lazy (
25+
let arg = 16 in
26+
throughputN 1 [
27+
("pow", pow2_pow, arg);
28+
("lsl", pow2_lsl, arg);
29+
]
30+
);
31+
"32" @> lazy (
32+
let arg = 32 in
33+
throughputN 1 [
34+
("pow", pow2_pow, arg);
35+
("lsl", pow2_lsl, arg);
36+
]
37+
);
38+
"64" @> lazy (
39+
let arg = 64 in
40+
throughputN 1 [
41+
("pow", pow2_pow, arg);
42+
("lsl", pow2_lsl, arg);
43+
]
44+
);
45+
]
46+
)
47+
48+
49+
let () =
50+
run_global ()

‎bench/zarith/dune‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
(executable
2+
(name benchZarith)
3+
(optional) ; TODO: for some reason this doesn't work: `dune build` still tries to compile if benchmark missing (https://github.com/ocaml/dune/issues/4065)
4+
(libraries benchmark zarith))

‎conf/bench-yaml-validate.json‎

Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,76 @@
1+
{
2+
"ana": {
3+
"int": {
4+
"def_exc": true,
5+
"enums": false,
6+
"interval": true
7+
},
8+
"activated": [
9+
"expRelation",
10+
"base",
11+
"threadid",
12+
"threadflag",
13+
"threadreturn",
14+
"escape",
15+
"mutexEvents",
16+
"mutex",
17+
"access",
18+
"mallocWrapper",
19+
"mhp",
20+
"assert",
21+
"unassume"
22+
],
23+
"malloc": {
24+
"wrappers": [
25+
"kmalloc",
26+
"__kmalloc",
27+
"usb_alloc_urb",
28+
"__builtin_alloca",
29+
"kzalloc",
30+
31+
"ldv_malloc",
32+
33+
"kzalloc_node",
34+
"ldv_zalloc",
35+
"kmalloc_array",
36+
"kcalloc",
37+
38+
"ldv_xmalloc",
39+
"ldv_xzalloc",
40+
"ldv_calloc"
41+
]
42+
},
43+
"widen": {
44+
"tokens": true
45+
}
46+
},
47+
"witness": {
48+
"enabled": false,
49+
"invariant": {
50+
"loop-head": true,
51+
"after-lock": true,
52+
"other": false
53+
}
54+
},
55+
"sem": {
56+
"unknown_function": {
57+
"invalidate": {
58+
"globals": false
59+
},
60+
"spawn": true
61+
},
62+
"builtin_unreachable": {
63+
"dead_code": true
64+
},
65+
"int": {
66+
"signed_overflow": "assume_none"
67+
}
68+
},
69+
"pre": {
70+
"cppflags": [
71+
"-DGOBLINT_NO_PTHREAD_ONCE",
72+
"-DGOBLINT_NO_QSORT",
73+
"-DGOBLINT_NO_BSEARCH"
74+
]
75+
}
76+
}

‎conf/bench-yaml.json‎

Lines changed: 78 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,78 @@
1+
{
2+
"ana": {
3+
"int": {
4+
"def_exc": true,
5+
"enums": false,
6+
"interval": true
7+
},
8+
"activated": [
9+
"expRelation",
10+
"base",
11+
"threadid",
12+
"threadflag",
13+
"threadreturn",
14+
"escape",
15+
"mutexEvents",
16+
"mutex",
17+
"access",
18+
"mallocWrapper",
19+
"mhp",
20+
"assert"
21+
],
22+
"malloc": {
23+
"wrappers": [
24+
"kmalloc",
25+
"__kmalloc",
26+
"usb_alloc_urb",
27+
"__builtin_alloca",
28+
"kzalloc",
29+
30+
"ldv_malloc",
31+
32+
"kzalloc_node",
33+
"ldv_zalloc",
34+
"kmalloc_array",
35+
"kcalloc",
36+
37+
"ldv_xmalloc",
38+
"ldv_xzalloc",
39+
"ldv_calloc"
40+
]
41+
}
42+
},
43+
"witness": {
44+
"enabled": false,
45+
"yaml": {
46+
"enabled": true
47+
},
48+
"invariant": {
49+
"exact": false,
50+
"exclude-vars": [
51+
"tmp\\(___[0-9]+\\)?",
52+
"cond",
53+
"RETURN"
54+
]
55+
}
56+
},
57+
"sem": {
58+
"unknown_function": {
59+
"invalidate": {
60+
"globals": false
61+
},
62+
"spawn": true
63+
},
64+
"builtin_unreachable": {
65+
"dead_code": true
66+
},
67+
"int": {
68+
"signed_overflow": "assume_none"
69+
}
70+
},
71+
"pre": {
72+
"cppflags": [
73+
"-DGOBLINT_NO_PTHREAD_ONCE",
74+
"-DGOBLINT_NO_QSORT",
75+
"-DGOBLINT_NO_BSEARCH"
76+
]
77+
}
78+
}

‎conf/svcomp-yaml-validate.json‎

Lines changed: 94 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,94 @@
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+
},
15+
"activated": [
16+
"base",
17+
"threadid",
18+
"threadflag",
19+
"threadreturn",
20+
"mallocWrapper",
21+
"mutexEvents",
22+
"mutex",
23+
"access",
24+
"race",
25+
"escape",
26+
"expRelation",
27+
"mhp",
28+
"assert",
29+
"var_eq",
30+
"symb_locks",
31+
"region",
32+
"thread",
33+
"threadJoins",
34+
"unassume"
35+
],
36+
"context": {
37+
"widen": false
38+
},
39+
"malloc": {
40+
"wrappers": [
41+
"kmalloc",
42+
"__kmalloc",
43+
"usb_alloc_urb",
44+
"__builtin_alloca",
45+
"kzalloc",
46+
47+
"ldv_malloc",
48+
49+
"kzalloc_node",
50+
"ldv_zalloc",
51+
"kmalloc_array",
52+
"kcalloc",
53+
54+
"ldv_xmalloc",
55+
"ldv_xzalloc",
56+
"ldv_calloc"
57+
]
58+
},
59+
"base": {
60+
"arrays": {
61+
"domain": "partitioned"
62+
}
63+
},
64+
"autotune": {
65+
"enabled": false
66+
},
67+
"widen": {
68+
"tokens": true
69+
}
70+
},
71+
"exp": {
72+
"region-offsets": true
73+
},
74+
"witness": {
75+
"enabled": false,
76+
"invariant": {
77+
"loop-head": true,
78+
"after-lock": false,
79+
"other": false
80+
}
81+
},
82+
"solver": "td3",
83+
"sem": {
84+
"unknown_function": {
85+
"spawn": false
86+
},
87+
"int": {
88+
"signed_overflow": "assume_none"
89+
},
90+
"null-pointer": {
91+
"dereference": "assume_none"
92+
}
93+
}
94+
}

0 commit comments

Comments
 (0)