Skip to content

Commit

Permalink
Merge pull request #1605 from goblint/topdown_term
Browse files Browse the repository at this point in the history 
Sanity test all solvers and fix `topdown_term` & `slr3`
  • Loading branch information
@sim642
sim642 authored Dec 16, 2024
2 parents b7747c9 + b0243f9 commit b68df11
Show file tree
Hide file tree
Showing 4 changed files with 279 additions and 7 deletions.
4 changes: 2 additions & 2 deletions src/solver/sLR.ml
View file
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
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
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
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

0 comments on commit b68df11

Please sign in to comment.