Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Sanity test all solvers and fix topdown_term & slr3 #1605

Merged
merged 7 commits into from
Dec 16, 2024
Merged

Sanity test all solvers and fix topdown_term & slr3 #1605

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
3bb17bc
Add cram tests for some solvers
sim642 Oct 24, 2024
e57072f
Fix option name in topdown_space_cache_term
sim642 Oct 24, 2024
f0a15f6
Fix basic functionality of topdown_term
sim642 Oct 24, 2024
1eb63b9
Fix invalid widen call in topdown_term for side effects
sim642 Oct 24, 2024
c348dd6
Add cram tests for remaining solvers
sim642 Oct 24, 2024
4a9b52f
Fix invalid widen call in slr3 for globals
sim642 Dec 16, 2024
b0243f9
Disable broken two solver
sim642 Dec 16, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions src/solver/sLR.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,7 @@ module SLR3 =
if tracing then trace "sol" "Contrib:%a" S.Dom.pretty tmp;
let tmp =
if wpx then
if HM.mem globals x then S.Dom.widen old tmp
if HM.mem globals x then S.Dom.widen old (S.Dom.join old tmp)
else box old tmp
else tmp
in
Expand Down Expand Up @@ -527,7 +527,7 @@ let _ =
Selector.add_solver ("widen2", (module PostSolver.EqIncrSolverFromEqSolver (W2)));
Selector.add_solver ("widen3", (module PostSolver.EqIncrSolverFromEqSolver (W3)));
let module S2 = TwoPhased (struct let ver = 1 end) in
Selector.add_solver ("two", (module PostSolver.EqIncrSolverFromEqSolver (S2)));
(* Selector.add_solver ("two", (module PostSolver.EqIncrSolverFromEqSolver (S2))); (* TODO: broken even on 00-sanity/01-assert *) *)
let module S1 = Make (struct let ver = 1 end) in
Selector.add_solver ("new", (module PostSolver.EqIncrSolverFromEqSolver (S1)));
Selector.add_solver ("slr+", (module PostSolver.EqIncrSolverFromEqSolver (S1)))
Expand Down
2 changes: 1 addition & 1 deletion src/solver/topDown_space_cache_term.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -170,7 +170,7 @@ module WP =
)
in
(* restore values for non-widening-points *)
if GobConfig.get_bool "solvers.wp.restore" then (
if GobConfig.get_bool "solvers.td3.space_restore" then (
Logs.debug "Restoring missing values.";
let restore () =
let get x =
Expand Down
8 changes: 4 additions & 4 deletions src/solver/topDown_term.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,8 +24,8 @@ module WP =
let stable = HM.create 10 in
let infl = HM.create 10 in (* y -> xs *)
let called = HM.create 10 in
let rho = HM.create 10 in
let rho' = HM.create 10 in
let rho = HM.create 10 in (* rho for right-hand side values *)
let rho' = HM.create 10 in (* rho for start and side effect values *)
let wpoint = HM.create 10 in

let add_infl y x =
Expand Down Expand Up @@ -85,7 +85,7 @@ module WP =
and side y d =
let old = try HM.find rho' y with Not_found -> S.Dom.bot () in
if not (S.Dom.leq d old) then (
HM.replace rho' y (S.Dom.widen old d);
HM.replace rho' y (S.Dom.widen old (S.Dom.join old d));
HM.remove stable y;
init y;
solve y Widen;
Expand All @@ -101,7 +101,7 @@ module WP =
let set_start (x,d) =
if tracing then trace "sol2" "set_start %a ## %a" S.Var.pretty_trace x S.Dom.pretty d;
init x;
HM.replace rho x d;
HM.replace rho' x d;
solve x Widen
in

Expand Down
272 changes: 272 additions & 0 deletions tests/regression/00-sanity/01-assert.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,3 +9,275 @@
live: 7
dead: 2
total lines: 9


Test ancient solvers:

$ goblint --enable warn.deterministic --set solver WL 01-assert.c
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
on lines 13..14 (01-assert.c:13-14)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
live: 7
dead: 2
total lines: 9

$ goblint --enable warn.deterministic --set solver effectWConEq 01-assert.c
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
on lines 13..14 (01-assert.c:13-14)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
live: 7
dead: 2
total lines: 9


Test topdown solvers:

$ goblint --enable warn.deterministic --set solver topdown_deprecated 01-assert.c
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
on lines 13..14 (01-assert.c:13-14)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
live: 7
dead: 2
total lines: 9

$ goblint --enable warn.deterministic --set solver topdown 01-assert.c
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
on lines 13..14 (01-assert.c:13-14)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
live: 7
dead: 2
total lines: 9

$ goblint --enable warn.deterministic --set solver topdown_term 01-assert.c
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
on lines 13..14 (01-assert.c:13-14)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
live: 7
dead: 2
total lines: 9

$ goblint --enable warn.deterministic --set solver topdown_space_cache_term 01-assert.c
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
on lines 13..14 (01-assert.c:13-14)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
live: 7
dead: 2
total lines: 9

$ goblint --enable warn.deterministic --set solver td3 01-assert.c
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
on lines 13..14 (01-assert.c:13-14)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
live: 7
dead: 2
total lines: 9


Test SLR solvers:

$ goblint --enable warn.deterministic --set solver widen1 01-assert.c
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
on lines 13..14 (01-assert.c:13-14)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
live: 7
dead: 2
total lines: 9

$ goblint --enable warn.deterministic --set solver widen2 01-assert.c
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
on lines 13..14 (01-assert.c:13-14)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
live: 7
dead: 2
total lines: 9

$ goblint --enable warn.deterministic --set solver widen3 01-assert.c
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
on lines 13..14 (01-assert.c:13-14)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
live: 7
dead: 2
total lines: 9

$ goblint --enable warn.deterministic --set solver new 01-assert.c
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
on lines 13..14 (01-assert.c:13-14)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
live: 7
dead: 2
total lines: 9

$ goblint --enable warn.deterministic --set solver slr+ 01-assert.c
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
on lines 13..14 (01-assert.c:13-14)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
live: 7
dead: 2
total lines: 9

$ goblint --enable warn.deterministic --set solver slr1 01-assert.c
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
on lines 13..14 (01-assert.c:13-14)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
live: 7
dead: 2
total lines: 9

$ goblint --enable warn.deterministic --set solver slr2 01-assert.c
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
on lines 13..14 (01-assert.c:13-14)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
live: 7
dead: 2
total lines: 9

$ goblint --enable warn.deterministic --set solver slr3 01-assert.c
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
on lines 13..14 (01-assert.c:13-14)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
live: 7
dead: 2
total lines: 9

$ goblint --enable warn.deterministic --set solver slr4 01-assert.c
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
on lines 13..14 (01-assert.c:13-14)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
live: 7
dead: 2
total lines: 9

$ goblint --enable warn.deterministic --set solver slr1p 01-assert.c
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
on lines 13..14 (01-assert.c:13-14)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
live: 7
dead: 2
total lines: 9
$ goblint --enable warn.deterministic --set solver slr2p 01-assert.c
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
on lines 13..14 (01-assert.c:13-14)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
live: 7
dead: 2
total lines: 9

$ goblint --enable warn.deterministic --set solver slr3p 01-assert.c
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
on lines 13..14 (01-assert.c:13-14)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
live: 7
dead: 2
total lines: 9

$ goblint --enable warn.deterministic --set solver slr4p 01-assert.c
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
on lines 13..14 (01-assert.c:13-14)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
live: 7
dead: 2
total lines: 9

$ goblint --enable warn.deterministic --set solver slr3t 01-assert.c
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
on lines 13..14 (01-assert.c:13-14)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
live: 7
dead: 2
total lines: 9

$ goblint --enable warn.deterministic --set solver slr3tp 01-assert.c
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
on lines 13..14 (01-assert.c:13-14)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
live: 7
dead: 2
total lines: 9
Loading