From ae29b7c56e3a462f64da3fc04c3f22a3723de027 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Mon, 19 Dec 2022 21:38:59 +0100 Subject: [PATCH 01/11] Add test example where reluctant incremental analysis does not reach the fixpoint and is unsound. --- .../incremental/00-basic/15-reluctant-test.c | 34 +++++++++++++++++++ .../00-basic/15-reluctant-test.json | 15 ++++++++ .../00-basic/15-reluctant-test.patch | 25 ++++++++++++++ 3 files changed, 74 insertions(+) create mode 100644 tests/incremental/00-basic/15-reluctant-test.c create mode 100644 tests/incremental/00-basic/15-reluctant-test.json create mode 100644 tests/incremental/00-basic/15-reluctant-test.patch 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..eb4c59f6b1 --- /dev/null +++ b/tests/incremental/00-basic/15-reluctant-test.c @@ -0,0 +1,34 @@ +#include +// This test used to resulted in an unreachd 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; +} \ No newline at end of file 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..1c1d7ef925 --- /dev/null +++ b/tests/incremental/00-basic/15-reluctant-test.patch @@ -0,0 +1,25 @@ +diff --git tests/incremental/00-basic/15-reluctant-test.c tests/incremental/00-basic/15-reluctant-test.c +index eb4c59f6b..5be065852 100644 +--- 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; + } +\ No newline at end of file From 617cb2fcbe3b17e8548f46cf6884e4ca59fea2a4 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Mon, 19 Dec 2022 21:51:25 +0100 Subject: [PATCH 02/11] Fix test so that code of main is not changed to ensure that test case is robust. --- tests/incremental/00-basic/15-reluctant-test.c | 3 ++- tests/incremental/00-basic/15-reluctant-test.patch | 8 ++++---- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/tests/incremental/00-basic/15-reluctant-test.c b/tests/incremental/00-basic/15-reluctant-test.c index eb4c59f6b1..df47393549 100644 --- a/tests/incremental/00-basic/15-reluctant-test.c +++ b/tests/incremental/00-basic/15-reluctant-test.c @@ -28,7 +28,8 @@ int main(){ g = 4; int i = bar(); - + // At first unreachable, then UNKNOWN! + __goblint_check(i == 4); } return x; } \ 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 index 1c1d7ef925..06e1f27ea6 100644 --- a/tests/incremental/00-basic/15-reluctant-test.patch +++ b/tests/incremental/00-basic/15-reluctant-test.patch @@ -1,5 +1,5 @@ diff --git tests/incremental/00-basic/15-reluctant-test.c tests/incremental/00-basic/15-reluctant-test.c -index eb4c59f6b..5be065852 100644 +index df4739354..a9117d577 100644 --- tests/incremental/00-basic/15-reluctant-test.c +++ tests/incremental/00-basic/15-reluctant-test.c @@ -14,8 +14,8 @@ int foo(){ @@ -13,11 +13,11 @@ index eb4c59f6b..5be065852 100644 } return r; } -@@ -28,7 +28,7 @@ int main(){ - g = 4; +@@ -29,7 +29,7 @@ int main(){ int i = bar(); -- + // At first unreachable, then UNKNOWN! +- __goblint_check(i == 4); + __goblint_check(i == 4); //UNKNOWN! } return x; From 502296dede01a54f87fb8b02d0dd800b3bd3cb7e Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Mon, 19 Dec 2022 23:04:31 +0100 Subject: [PATCH 03/11] Reluctant: Before destabilizing reludtant unknown x, Set infl x to union of old and new value of infl x. --- src/solvers/td3.ml | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 1b14d028f3..79ca50a97f 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -727,9 +727,21 @@ module Base = solve x Widen; if not (op (HM.find rho x) old_rho) then ( print_endline "Destabilization required..."; - HM.replace infl x old_infl; + + let infl_x = HM.find_default infl x (VS.empty) in + + let print_set vs s = + print_endline s; + VS.iter (fun v -> ignore @@ Pretty.printf "%a\n" S.Var.pretty_trace v) vs + in + ignore @@ Pretty.printf "infl_x: %d, old_infl: %d, intersction: %d\n" (VS.cardinal infl_x) (VS.cardinal old_infl) (VS.cardinal (VS.inter infl_x old_infl)); + print_set infl_x "new infl:"; + print_set old_infl "old infl:"; + + let infl_new = VS.union infl_x old_infl in + + HM.replace infl x infl_new; destabilize x; - HM.replace stable x () ) else ( print_endline "Destabilization not required..."; From ebd890d1b0d53ad499598650ab8b14f564775df2 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Mon, 19 Dec 2022 23:12:56 +0100 Subject: [PATCH 04/11] Revert "Fix test so that code of main is not changed to ensure that test case is robust." This reverts commit 617cb2fcbe3b17e8548f46cf6884e4ca59fea2a4. --- tests/incremental/00-basic/15-reluctant-test.c | 3 +-- tests/incremental/00-basic/15-reluctant-test.patch | 8 ++++---- 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/tests/incremental/00-basic/15-reluctant-test.c b/tests/incremental/00-basic/15-reluctant-test.c index df47393549..eb4c59f6b1 100644 --- a/tests/incremental/00-basic/15-reluctant-test.c +++ b/tests/incremental/00-basic/15-reluctant-test.c @@ -28,8 +28,7 @@ int main(){ g = 4; int i = bar(); - // At first unreachable, then UNKNOWN! - __goblint_check(i == 4); + } return x; } \ 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 index 06e1f27ea6..1c1d7ef925 100644 --- a/tests/incremental/00-basic/15-reluctant-test.patch +++ b/tests/incremental/00-basic/15-reluctant-test.patch @@ -1,5 +1,5 @@ diff --git tests/incremental/00-basic/15-reluctant-test.c tests/incremental/00-basic/15-reluctant-test.c -index df4739354..a9117d577 100644 +index eb4c59f6b..5be065852 100644 --- tests/incremental/00-basic/15-reluctant-test.c +++ tests/incremental/00-basic/15-reluctant-test.c @@ -14,8 +14,8 @@ int foo(){ @@ -13,11 +13,11 @@ index df4739354..a9117d577 100644 } return r; } -@@ -29,7 +29,7 @@ int main(){ +@@ -28,7 +28,7 @@ int main(){ + g = 4; int i = bar(); - // At first unreachable, then UNKNOWN! -- __goblint_check(i == 4); +- + __goblint_check(i == 4); //UNKNOWN! } return x; From 6b24bf42a17441d1657161a6e8e73828e711e250 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Mon, 19 Dec 2022 23:15:56 +0100 Subject: [PATCH 05/11] Remove debug printout, rename variables. --- src/solvers/td3.ml | 16 +++------------- 1 file changed, 3 insertions(+), 13 deletions(-) diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 79ca50a97f..3470145630 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -728,19 +728,9 @@ module Base = if not (op (HM.find rho x) old_rho) then ( print_endline "Destabilization required..."; - let infl_x = HM.find_default infl x (VS.empty) in - - let print_set vs s = - print_endline s; - VS.iter (fun v -> ignore @@ Pretty.printf "%a\n" S.Var.pretty_trace v) vs - in - ignore @@ Pretty.printf "infl_x: %d, old_infl: %d, intersction: %d\n" (VS.cardinal infl_x) (VS.cardinal old_infl) (VS.cardinal (VS.inter infl_x old_infl)); - print_set infl_x "new infl:"; - print_set old_infl "old infl:"; - - let infl_new = VS.union infl_x old_infl in - - HM.replace infl x infl_new; + let infl_new = HM.find_default infl x (VS.empty) in + let infl_combined = VS.union infl_new old_infl in + HM.replace infl x infl_combined; destabilize x; ) else ( From 28df0568bb0cc4121aa5d68f2a0bd39d829c3e5e Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 20 Dec 2022 08:53:31 +0100 Subject: [PATCH 06/11] Typo --- tests/incremental/00-basic/15-reluctant-test.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/incremental/00-basic/15-reluctant-test.c b/tests/incremental/00-basic/15-reluctant-test.c index eb4c59f6b1..6328061b29 100644 --- a/tests/incremental/00-basic/15-reluctant-test.c +++ b/tests/incremental/00-basic/15-reluctant-test.c @@ -1,5 +1,5 @@ #include -// This test used to resulted in an unreachd fixpoint in the incremental implementation. +// This test used to resulted in an unreached fixpoint in the incremental implementation. int g = 3; @@ -31,4 +31,4 @@ int main(){ } return x; -} \ No newline at end of file +} From c1429f30ed9b63cf392cb9b0dad3f131a09f9c11 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Tue, 20 Dec 2022 10:55:42 +0100 Subject: [PATCH 07/11] reset infl before solve, explicit destabilization not required then --- src/solvers/td3.ml | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 3470145630..9b51a43675 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -722,16 +722,13 @@ module Base = (* 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 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; + 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 (op (HM.find rho x) old_rho) then ( - print_endline "Destabilization required..."; - - let infl_new = HM.find_default infl x (VS.empty) in - let infl_combined = VS.union infl_new old_infl in - HM.replace infl x infl_combined; - destabilize x; + print_endline "Further destabilization happened ..."; ) else ( print_endline "Destabilization not required..."; From fb319f73c4beb05489f92828d305ad1332ef5473 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Tue, 20 Dec 2022 11:00:24 +0100 Subject: [PATCH 08/11] remove option for reluctant comparison --- src/solvers/td3.ml | 3 +-- src/util/options.schema.json | 8 -------- 2 files changed, 1 insertion(+), 10 deletions(-) diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 9b51a43675..0e78be935a 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -721,13 +721,12 @@ 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 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; 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 (op (HM.find rho x) old_rho) then ( + if not (S.Dom.equal (HM.find rho x) old_rho) then ( print_endline "Further destabilization happened ..."; ) else ( 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 From 12759cba2e88263c875b0e0c723dd52532ae506f Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Tue, 20 Dec 2022 11:05:31 +0100 Subject: [PATCH 09/11] remove option from configs also --- conf/zstd-race.json | 3 --- 1 file changed, 3 deletions(-) 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 From 078c5b40a328411520acd06bf3668ed076f68b50 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Tue, 20 Dec 2022 11:12:18 +0100 Subject: [PATCH 10/11] fix patch --- tests/incremental/00-basic/15-reluctant-test.patch | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/tests/incremental/00-basic/15-reluctant-test.patch b/tests/incremental/00-basic/15-reluctant-test.patch index 1c1d7ef925..a2e1988f74 100644 --- a/tests/incremental/00-basic/15-reluctant-test.patch +++ b/tests/incremental/00-basic/15-reluctant-test.patch @@ -1,5 +1,3 @@ -diff --git tests/incremental/00-basic/15-reluctant-test.c tests/incremental/00-basic/15-reluctant-test.c -index eb4c59f6b..5be065852 100644 --- tests/incremental/00-basic/15-reluctant-test.c +++ tests/incremental/00-basic/15-reluctant-test.c @@ -14,8 +14,8 @@ int foo(){ @@ -16,10 +14,9 @@ index eb4c59f6b..5be065852 100644 @@ -28,7 +28,7 @@ int main(){ g = 4; int i = bar(); - + - -+ __goblint_check(i == 4); //UNKNOWN! ++ __goblint_check(i == 4); //UNKNOWN! } return x; } -\ No newline at end of file From 17716e55a6052096e0326e4aa1b1cd7ac0b5fcd2 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Tue, 20 Dec 2022 13:53:53 +0100 Subject: [PATCH 11/11] fix destabilization beyond return node --- src/solvers/td3.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 0e78be935a..9a4c839175 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -721,7 +721,7 @@ 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..."; - HM.iter (fun x (old_rho, old_infl) -> HM.replace infl x old_infl) old_ret; + 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;