diff --git a/conf/zstd-race.json b/conf/zstd-race.json index 407e823017..9a8ae0a87f 100644 --- a/conf/zstd-race.json +++ b/conf/zstd-race.json @@ -41,9 +41,6 @@ } }, "incremental": { - "reluctant": { - "compare": "leq" - }, "restart": { "sided": { "enabled": false diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 1b14d028f3..9a4c839175 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -721,15 +721,13 @@ module Base = if reluctant then ( (* solve on the return node of changed functions. Only destabilize the function's return node if the analysis result changed *) print_endline "Separately solving changed functions..."; - let op = if GobConfig.get_string "incremental.reluctant.compare" = "leq" then S.Dom.leq else S.Dom.equal in + HM.iter (fun x (old_rho, old_infl) -> HM.replace rho x old_rho; HM.replace infl x old_infl) old_ret; HM.iter (fun x (old_rho, old_infl) -> ignore @@ Pretty.printf "test for %a\n" Node.pretty_trace (S.Var.node x); solve x Widen; - if not (op (HM.find rho x) old_rho) then ( - print_endline "Destabilization required..."; - HM.replace infl x old_infl; - destabilize x; - HM.replace stable x () + VS.iter (fun k -> ignore @@ Pretty.printf "in infl after solving: %a\n" Node.pretty_trace (S.Var.node k)) (HM.find_default infl x VS.empty); + if not (S.Dom.equal (HM.find rho x) old_rho) then ( + print_endline "Further destabilization happened ..."; ) else ( print_endline "Destabilization not required..."; diff --git a/src/util/options.schema.json b/src/util/options.schema.json index f9aa19db0f..230d94097c 100644 --- a/src/util/options.schema.json +++ b/src/util/options.schema.json @@ -1053,14 +1053,6 @@ "Destabilize nodes in changed functions reluctantly", "type": "boolean", "default": false - }, - "compare": { - "title": "incremental.reluctant.compare", - "description": - "In order to reuse the function's old abstract value the new abstract value must be leq (focus on efficiency) or equal (focus on precision) compared to the old.", - "type": "string", - "enum": ["leq", "equal"], - "default": "equal" } }, "additionalProperties": false diff --git a/tests/incremental/00-basic/15-reluctant-test.c b/tests/incremental/00-basic/15-reluctant-test.c new file mode 100644 index 0000000000..6328061b29 --- /dev/null +++ b/tests/incremental/00-basic/15-reluctant-test.c @@ -0,0 +1,34 @@ +#include +// This test used to resulted in an unreached fixpoint in the incremental implementation. + +int g = 3; + +int bar(){ + int x = foo(); + return x; +} + +int foo(){ + int top; + int r = 0; + if(top){ + r = g; + } else { + // bar(); + // r = 5; + } + return r; +} + +int main(){ + int x; + + x = foo(); + if(x == 5){ + g = 4; + int i = bar(); + + + } + return x; +} diff --git a/tests/incremental/00-basic/15-reluctant-test.json b/tests/incremental/00-basic/15-reluctant-test.json new file mode 100644 index 0000000000..f8b6a3af51 --- /dev/null +++ b/tests/incremental/00-basic/15-reluctant-test.json @@ -0,0 +1,15 @@ +{ + "ana": { + "int": { + "enums": true + } + }, + "incremental": { + "reluctant": { + "enabled": true + } + }, + "exp": { + "earlyglobs": true + } +} \ No newline at end of file diff --git a/tests/incremental/00-basic/15-reluctant-test.patch b/tests/incremental/00-basic/15-reluctant-test.patch new file mode 100644 index 0000000000..a2e1988f74 --- /dev/null +++ b/tests/incremental/00-basic/15-reluctant-test.patch @@ -0,0 +1,22 @@ +--- tests/incremental/00-basic/15-reluctant-test.c ++++ tests/incremental/00-basic/15-reluctant-test.c +@@ -14,8 +14,8 @@ int foo(){ + if(top){ + r = g; + } else { +- // bar(); +- // r = 5; ++ bar(); ++ r = 5; + } + return r; + } +@@ -28,7 +28,7 @@ int main(){ + g = 4; + int i = bar(); + +- ++ __goblint_check(i == 4); //UNKNOWN! + } + return x; + }