diff --git a/src/solver/sLR.ml b/src/solver/sLR.ml index 3b46f36f5e..03ba9307aa 100644 --- a/src/solver/sLR.ml +++ b/src/solver/sLR.ml @@ -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 @@ -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))) diff --git a/src/solver/topDown_space_cache_term.ml b/src/solver/topDown_space_cache_term.ml index 0022756a31..df44c376e1 100644 --- a/src/solver/topDown_space_cache_term.ml +++ b/src/solver/topDown_space_cache_term.ml @@ -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 = diff --git a/src/solver/topDown_term.ml b/src/solver/topDown_term.ml index 9d89a42898..5560c50f4f 100644 --- a/src/solver/topDown_term.ml +++ b/src/solver/topDown_term.ml @@ -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 = @@ -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; @@ -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 diff --git a/tests/regression/00-sanity/01-assert.t b/tests/regression/00-sanity/01-assert.t index 9142f805f9..9b3b55f530 100644 --- a/tests/regression/00-sanity/01-assert.t +++ b/tests/regression/00-sanity/01-assert.t @@ -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