Skip to content

Commit b68df11

Browse files
sim642sim642
authored
Merge pull request #1605 from goblint/topdown_term
Sanity test all solvers and fix `topdown_term` & `slr3`
2 parents b7747c9 + b0243f9 commit b68df11

File tree

4 files changed

+279
-7
lines changed

4 files changed

+279
-7
lines changed

‎src/solver/sLR.ml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -66,7 +66,7 @@ module SLR3 =
6666
if tracing then trace "sol" "Contrib:%a" S.Dom.pretty tmp;
6767
let tmp =
6868
if wpx then
69-
if HM.mem globals x then S.Dom.widen old tmp
69+
if HM.mem globals x then S.Dom.widen old (S.Dom.join old tmp)
7070
else box old tmp
7171
else tmp
7272
in
@@ -527,7 +527,7 @@ let _ =
527527
Selector.add_solver ("widen2", (module PostSolver.EqIncrSolverFromEqSolver (W2)));
528528
Selector.add_solver ("widen3", (module PostSolver.EqIncrSolverFromEqSolver (W3)));
529529
let module S2 = TwoPhased (struct let ver = 1 end) in
530-
Selector.add_solver ("two", (module PostSolver.EqIncrSolverFromEqSolver (S2)));
530+
(* Selector.add_solver ("two", (module PostSolver.EqIncrSolverFromEqSolver (S2))); (* TODO: broken even on 00-sanity/01-assert *) *)
531531
let module S1 = Make (struct let ver = 1 end) in
532532
Selector.add_solver ("new", (module PostSolver.EqIncrSolverFromEqSolver (S1)));
533533
Selector.add_solver ("slr+", (module PostSolver.EqIncrSolverFromEqSolver (S1)))

‎src/solver/topDown_space_cache_term.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -170,7 +170,7 @@ module WP =
170170
)
171171
in
172172
(* restore values for non-widening-points *)
173-
if GobConfig.get_bool "solvers.wp.restore" then (
173+
if GobConfig.get_bool "solvers.td3.space_restore" then (
174174
Logs.debug "Restoring missing values.";
175175
let restore () =
176176
let get x =

‎src/solver/topDown_term.ml‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -24,8 +24,8 @@ module WP =
2424
let stable = HM.create 10 in
2525
let infl = HM.create 10 in (* y -> xs *)
2626
let called = HM.create 10 in
27-
let rho = HM.create 10 in
28-
let rho' = HM.create 10 in
27+
let rho = HM.create 10 in (* rho for right-hand side values *)
28+
let rho' = HM.create 10 in (* rho for start and side effect values *)
2929
let wpoint = HM.create 10 in
3030

3131
let add_infl y x =
@@ -85,7 +85,7 @@ module WP =
8585
and side y d =
8686
let old = try HM.find rho' y with Not_found -> S.Dom.bot () in
8787
if not (S.Dom.leq d old) then (
88-
HM.replace rho' y (S.Dom.widen old d);
88+
HM.replace rho' y (S.Dom.widen old (S.Dom.join old d));
8989
HM.remove stable y;
9090
init y;
9191
solve y Widen;
@@ -101,7 +101,7 @@ module WP =
101101
let set_start (x,d) =
102102
if tracing then trace "sol2" "set_start %a ## %a" S.Var.pretty_trace x S.Dom.pretty d;
103103
init x;
104-
HM.replace rho x d;
104+
HM.replace rho' x d;
105105
solve x Widen
106106
in
107107

‎tests/regression/00-sanity/01-assert.t‎

Lines changed: 272 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,3 +9,275 @@
99
live: 7
1010
dead: 2
1111
total lines: 9
12+
13+
14+
Test ancient solvers:
15+
16+
$ goblint --enable warn.deterministic --set solver WL 01-assert.c
17+
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
18+
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
19+
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
20+
[Warning][Deadcode] Function 'main' does not return
21+
[Warning][Deadcode] Function 'main' has dead code:
22+
on lines 13..14 (01-assert.c:13-14)
23+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
24+
live: 7
25+
dead: 2
26+
total lines: 9
27+
28+
$ goblint --enable warn.deterministic --set solver effectWConEq 01-assert.c
29+
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
30+
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
31+
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
32+
[Warning][Deadcode] Function 'main' does not return
33+
[Warning][Deadcode] Function 'main' has dead code:
34+
on lines 13..14 (01-assert.c:13-14)
35+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
36+
live: 7
37+
dead: 2
38+
total lines: 9
39+
40+
41+
Test topdown solvers:
42+
43+
$ goblint --enable warn.deterministic --set solver topdown_deprecated 01-assert.c
44+
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
45+
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
46+
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
47+
[Warning][Deadcode] Function 'main' does not return
48+
[Warning][Deadcode] Function 'main' has dead code:
49+
on lines 13..14 (01-assert.c:13-14)
50+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
51+
live: 7
52+
dead: 2
53+
total lines: 9
54+
55+
$ goblint --enable warn.deterministic --set solver topdown 01-assert.c
56+
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
57+
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
58+
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
59+
[Warning][Deadcode] Function 'main' does not return
60+
[Warning][Deadcode] Function 'main' has dead code:
61+
on lines 13..14 (01-assert.c:13-14)
62+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
63+
live: 7
64+
dead: 2
65+
total lines: 9
66+
67+
$ goblint --enable warn.deterministic --set solver topdown_term 01-assert.c
68+
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
69+
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
70+
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
71+
[Warning][Deadcode] Function 'main' does not return
72+
[Warning][Deadcode] Function 'main' has dead code:
73+
on lines 13..14 (01-assert.c:13-14)
74+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
75+
live: 7
76+
dead: 2
77+
total lines: 9
78+
79+
$ goblint --enable warn.deterministic --set solver topdown_space_cache_term 01-assert.c
80+
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
81+
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
82+
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
83+
[Warning][Deadcode] Function 'main' does not return
84+
[Warning][Deadcode] Function 'main' has dead code:
85+
on lines 13..14 (01-assert.c:13-14)
86+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
87+
live: 7
88+
dead: 2
89+
total lines: 9
90+
91+
$ goblint --enable warn.deterministic --set solver td3 01-assert.c
92+
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
93+
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
94+
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
95+
[Warning][Deadcode] Function 'main' does not return
96+
[Warning][Deadcode] Function 'main' has dead code:
97+
on lines 13..14 (01-assert.c:13-14)
98+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
99+
live: 7
100+
dead: 2
101+
total lines: 9
102+
103+
104+
Test SLR solvers:
105+
106+
$ goblint --enable warn.deterministic --set solver widen1 01-assert.c
107+
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
108+
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
109+
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
110+
[Warning][Deadcode] Function 'main' does not return
111+
[Warning][Deadcode] Function 'main' has dead code:
112+
on lines 13..14 (01-assert.c:13-14)
113+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
114+
live: 7
115+
dead: 2
116+
total lines: 9
117+
118+
$ goblint --enable warn.deterministic --set solver widen2 01-assert.c
119+
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
120+
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
121+
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
122+
[Warning][Deadcode] Function 'main' does not return
123+
[Warning][Deadcode] Function 'main' has dead code:
124+
on lines 13..14 (01-assert.c:13-14)
125+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
126+
live: 7
127+
dead: 2
128+
total lines: 9
129+
130+
$ goblint --enable warn.deterministic --set solver widen3 01-assert.c
131+
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
132+
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
133+
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
134+
[Warning][Deadcode] Function 'main' does not return
135+
[Warning][Deadcode] Function 'main' has dead code:
136+
on lines 13..14 (01-assert.c:13-14)
137+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
138+
live: 7
139+
dead: 2
140+
total lines: 9
141+
142+
$ goblint --enable warn.deterministic --set solver new 01-assert.c
143+
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
144+
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
145+
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
146+
[Warning][Deadcode] Function 'main' does not return
147+
[Warning][Deadcode] Function 'main' has dead code:
148+
on lines 13..14 (01-assert.c:13-14)
149+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
150+
live: 7
151+
dead: 2
152+
total lines: 9
153+
154+
$ goblint --enable warn.deterministic --set solver slr+ 01-assert.c
155+
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
156+
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
157+
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
158+
[Warning][Deadcode] Function 'main' does not return
159+
[Warning][Deadcode] Function 'main' has dead code:
160+
on lines 13..14 (01-assert.c:13-14)
161+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
162+
live: 7
163+
dead: 2
164+
total lines: 9
165+
166+
$ goblint --enable warn.deterministic --set solver slr1 01-assert.c
167+
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
168+
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
169+
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
170+
[Warning][Deadcode] Function 'main' does not return
171+
[Warning][Deadcode] Function 'main' has dead code:
172+
on lines 13..14 (01-assert.c:13-14)
173+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
174+
live: 7
175+
dead: 2
176+
total lines: 9
177+
178+
$ goblint --enable warn.deterministic --set solver slr2 01-assert.c
179+
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
180+
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
181+
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
182+
[Warning][Deadcode] Function 'main' does not return
183+
[Warning][Deadcode] Function 'main' has dead code:
184+
on lines 13..14 (01-assert.c:13-14)
185+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
186+
live: 7
187+
dead: 2
188+
total lines: 9
189+
190+
$ goblint --enable warn.deterministic --set solver slr3 01-assert.c
191+
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
192+
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
193+
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
194+
[Warning][Deadcode] Function 'main' does not return
195+
[Warning][Deadcode] Function 'main' has dead code:
196+
on lines 13..14 (01-assert.c:13-14)
197+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
198+
live: 7
199+
dead: 2
200+
total lines: 9
201+
202+
$ goblint --enable warn.deterministic --set solver slr4 01-assert.c
203+
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
204+
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
205+
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
206+
[Warning][Deadcode] Function 'main' does not return
207+
[Warning][Deadcode] Function 'main' has dead code:
208+
on lines 13..14 (01-assert.c:13-14)
209+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
210+
live: 7
211+
dead: 2
212+
total lines: 9
213+
214+
$ goblint --enable warn.deterministic --set solver slr1p 01-assert.c
215+
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
216+
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
217+
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
218+
[Warning][Deadcode] Function 'main' does not return
219+
[Warning][Deadcode] Function 'main' has dead code:
220+
on lines 13..14 (01-assert.c:13-14)
221+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
222+
live: 7
223+
dead: 2
224+
total lines: 9
225+
$ goblint --enable warn.deterministic --set solver slr2p 01-assert.c
226+
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
227+
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
228+
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
229+
[Warning][Deadcode] Function 'main' does not return
230+
[Warning][Deadcode] Function 'main' has dead code:
231+
on lines 13..14 (01-assert.c:13-14)
232+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
233+
live: 7
234+
dead: 2
235+
total lines: 9
236+
237+
$ goblint --enable warn.deterministic --set solver slr3p 01-assert.c
238+
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
239+
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
240+
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
241+
[Warning][Deadcode] Function 'main' does not return
242+
[Warning][Deadcode] Function 'main' has dead code:
243+
on lines 13..14 (01-assert.c:13-14)
244+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
245+
live: 7
246+
dead: 2
247+
total lines: 9
248+
249+
$ goblint --enable warn.deterministic --set solver slr4p 01-assert.c
250+
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
251+
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
252+
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
253+
[Warning][Deadcode] Function 'main' does not return
254+
[Warning][Deadcode] Function 'main' has dead code:
255+
on lines 13..14 (01-assert.c:13-14)
256+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
257+
live: 7
258+
dead: 2
259+
total lines: 9
260+
261+
$ goblint --enable warn.deterministic --set solver slr3t 01-assert.c
262+
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
263+
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
264+
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
265+
[Warning][Deadcode] Function 'main' does not return
266+
[Warning][Deadcode] Function 'main' has dead code:
267+
on lines 13..14 (01-assert.c:13-14)
268+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
269+
live: 7
270+
dead: 2
271+
total lines: 9
272+
273+
$ goblint --enable warn.deterministic --set solver slr3tp 01-assert.c
274+
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
275+
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
276+
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
277+
[Warning][Deadcode] Function 'main' does not return
278+
[Warning][Deadcode] Function 'main' has dead code:
279+
on lines 13..14 (01-assert.c:13-14)
280+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
281+
live: 7
282+
dead: 2
283+
total lines: 9

0 commit comments

Comments
 (0)