From 678f0d89810c69f95b4c5a6d2459249531a86799 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 29 Sep 2021 16:23:21 +0300 Subject: [PATCH 01/12] Add incremental test where local wpoint must be restarted after global restart --- tests/incremental/05-local-wpoint.c | 23 +++++++++++++++++++++++ tests/incremental/05-local-wpoint.json | 10 ++++++++++ tests/incremental/05-local-wpoint.patch | 10 ++++++++++ 3 files changed, 43 insertions(+) create mode 100644 tests/incremental/05-local-wpoint.c create mode 100644 tests/incremental/05-local-wpoint.json create mode 100644 tests/incremental/05-local-wpoint.patch diff --git a/tests/incremental/05-local-wpoint.c b/tests/incremental/05-local-wpoint.c new file mode 100644 index 0000000000..cdd9c48541 --- /dev/null +++ b/tests/incremental/05-local-wpoint.c @@ -0,0 +1,23 @@ +#include +#include + +int g = 1; + +void* t_fun(void *arg) { + g = 0; + return NULL; +} + +int main() { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); // just go multithreaded + + int x; + x = g; + while (1) { + assert(x == 1); // unknown before, success after + x = g; + } + + return 0; +} \ No newline at end of file diff --git a/tests/incremental/05-local-wpoint.json b/tests/incremental/05-local-wpoint.json new file mode 100644 index 0000000000..ff773f6993 --- /dev/null +++ b/tests/incremental/05-local-wpoint.json @@ -0,0 +1,10 @@ +{ + "ana": { + "int": { + "interval": true + } + }, + "incremental": { + "wpoint": false + } +} \ No newline at end of file diff --git a/tests/incremental/05-local-wpoint.patch b/tests/incremental/05-local-wpoint.patch new file mode 100644 index 0000000000..2342e07535 --- /dev/null +++ b/tests/incremental/05-local-wpoint.patch @@ -0,0 +1,10 @@ +--- tests/incremental/05-local-wpoint.c 2021-09-29 16:30:17.199899879 +0300 ++++ "tests/incremental/05-local-wpoint copy.c" 2021-09-29 16:30:30.231977751 +0300 +@@ -4,7 +4,6 @@ + int g = 1; + + void* t_fun(void *arg) { +- g = 0; + return NULL; + } + From e028893b9b680ce0fc35a2f7102abc5b2a98f6be Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 29 Sep 2021 16:56:59 +0300 Subject: [PATCH 02/12] Add incremental test where local wpoint must be restarted after global restart due to read from old rho --- tests/incremental/06-local-wpoint-read.c | 24 ++++++++++++++++++++ tests/incremental/06-local-wpoint-read.json | 10 ++++++++ tests/incremental/06-local-wpoint-read.patch | 10 ++++++++ 3 files changed, 44 insertions(+) create mode 100644 tests/incremental/06-local-wpoint-read.c create mode 100644 tests/incremental/06-local-wpoint-read.json create mode 100644 tests/incremental/06-local-wpoint-read.patch diff --git a/tests/incremental/06-local-wpoint-read.c b/tests/incremental/06-local-wpoint-read.c new file mode 100644 index 0000000000..d6900bd3a5 --- /dev/null +++ b/tests/incremental/06-local-wpoint-read.c @@ -0,0 +1,24 @@ +#include +#include + +int g = 1; + +void* t_fun(void *arg) { + g = 0; + return NULL; +} + +int main() { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); // just go multithreaded + + int x; + x = g; + while (1) { + g = x; + assert(x == 1); // unknown before, success after + x = g; + } + + return 0; +} \ No newline at end of file diff --git a/tests/incremental/06-local-wpoint-read.json b/tests/incremental/06-local-wpoint-read.json new file mode 100644 index 0000000000..ff773f6993 --- /dev/null +++ b/tests/incremental/06-local-wpoint-read.json @@ -0,0 +1,10 @@ +{ + "ana": { + "int": { + "interval": true + } + }, + "incremental": { + "wpoint": false + } +} \ No newline at end of file diff --git a/tests/incremental/06-local-wpoint-read.patch b/tests/incremental/06-local-wpoint-read.patch new file mode 100644 index 0000000000..1767552a45 --- /dev/null +++ b/tests/incremental/06-local-wpoint-read.patch @@ -0,0 +1,10 @@ +--- tests/incremental/06-local-wpoint-read.c 2021-09-29 16:55:20.461556453 +0300 ++++ "tests/incremental/06-local-wpoint-read copy.c" 2021-09-29 16:55:51.013749361 +0300 +@@ -4,7 +4,6 @@ + int g = 1; + + void* t_fun(void *arg) { +- g = 0; + return NULL; + } + From 5d64c6f8416ab2e48091616bdda1e08b12a97752 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 30 Sep 2021 10:36:11 +0300 Subject: [PATCH 03/12] Remove 80 character width from tracing output --- src/util/tracing.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/tracing.ml b/src/util/tracing.ml index d66be4fc48..90aa00db63 100644 --- a/src/util/tracing.ml +++ b/src/util/tracing.ml @@ -83,7 +83,7 @@ let traceTag (sys : string) : Pretty.doc = (text ((ind !indent_level) ^ "%%% " ^ sys ^ ": ")) let printtrace sys d: unit = - fprint stderr 80 ((traceTag sys) ++ d); + fprint stderr max_int ((traceTag sys) ++ d); flush stderr let gtrace always f sys var ?loc do_subsys fmt = From 9ee28513f7a07036f34764546f0f28e7f7a8d536 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 30 Sep 2021 10:40:07 +0300 Subject: [PATCH 04/12] Add variable splitting workaround for verify incompleteness --- src/framework/constraints.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 6c4c3755d0..301e814630 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -830,7 +830,10 @@ module GlobSolverFromEqSolver (Sol:GenericEqBoxSolver) | `L x -> begin match d with | `Lifted2 d -> LH.replace l' x d - | `Bot -> () + (* | `Bot -> () *) + (* Since Verify2 is broken and only checks existing keys, add it with local bottom value. + This works around some cases, where Verify2 would not detect a problem due to completely missing variable. *) + | `Bot -> LH.replace l' x (S.D.bot ()) | `Top -> failwith "GlobSolverFromEqSolver.split_vars: local variable has top value" | `Lifted1 _ -> failwith "GlobSolverFromEqSolver.split_vars: local variable has global value" end From 5a484bc110ba51a669c77de7fdf2edb801cb83d6 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 30 Sep 2021 10:44:26 +0300 Subject: [PATCH 05/12] Add local wpoint restarting to TD3 --- src/solvers/td3.ml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 475593efb8..64d7a38d68 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -178,7 +178,15 @@ module WP = and eval l x y = if tracing then trace "sol2" "eval %a ## %a\n" S.Var.pretty_trace x S.Var.pretty_trace y; get_var_event y; - if HM.mem called y then HM.replace wpoint y (); + if HM.mem called y then ( + if not (HM.mem wpoint y) then ( + (* TODO: add boolean flag *) + if tracing then trace "sol2" "wpoint restart %a ## %a\n" S.Var.pretty_trace y S.Dom.pretty (HM.find_default rho y (S.Dom.bot ())); + HM.replace rho y (S.Dom.bot ()); + (* destabilize y *) (* TODO: would this do anything on called? *) + ); + HM.replace wpoint y (); + ); let tmp = simple_solve l x y in if HM.mem rho y then add_infl y x; tmp From 35d553c29158ab01287f1a9ec58fb55156f64877 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 30 Sep 2021 10:48:17 +0300 Subject: [PATCH 06/12] Fix unsound wpoint restart in TD3 by using non-outdated old value Since wpoint restart changes `HM.find rho x` during `eq`, the following non-equality check should use the new value, not the old outdated one. The TD3 paper does the comparison using the non-cached value anyway. --- 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 64d7a38d68..315e7b295c 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -124,13 +124,13 @@ module WP = HM.replace stable x (); HM.replace called x (); let wp = HM.mem wpoint x in - let old = HM.find rho x in let l = HM.create 10 in let tmp = eq x (eval l x) (side x) in (* let tmp = if GobConfig.get_bool "ana.opt.hashcons" then S.Dom.join (S.Dom.bot ()) tmp else tmp in (* Call hashcons via dummy join so that the tag of the rhs value is up to date. Otherwise we might get the same value as old, but still with a different tag (because no lattice operation was called after a change), and since Printable.HConsed.equal just looks at the tag, we would uneccessarily destabilize below. Seems like this does not happen. *) *) if tracing then trace "sol" "Var: %a\n" S.Var.pretty_trace x ; if tracing then trace "sol" "Contrib:%a\n" S.Dom.pretty tmp; HM.remove called x; + let old = HM.find rho x in let tmp = if not wp then tmp else From d29ef61ebb9064b8b78db0cf7ca1c9ab9f4ce2d9 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 30 Sep 2021 10:51:35 +0300 Subject: [PATCH 07/12] Add regression test for TD3 wpoint restart soundness --- .../00-sanity/28-wpoint-restart-sound.c | 24 +++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 tests/regression/00-sanity/28-wpoint-restart-sound.c diff --git a/tests/regression/00-sanity/28-wpoint-restart-sound.c b/tests/regression/00-sanity/28-wpoint-restart-sound.c new file mode 100644 index 0000000000..511d0b5d25 --- /dev/null +++ b/tests/regression/00-sanity/28-wpoint-restart-sound.c @@ -0,0 +1,24 @@ +// PARAM: --enable ana.int.interval +#include +#include + +int g = 0; + +void *worker(void *arg ) +{ + return NULL; +} + +int main(int argc , char **argv ) +{ + pthread_t tid; + pthread_create(& tid, NULL, & worker, NULL); + + while (g >= 10) { + + } + assert(1); // reachable + g++; + assert(1); // reachable + return 0; +} From 617452f532c8a1873ff0faf247e75dd017374ca8 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 30 Sep 2021 10:54:36 +0300 Subject: [PATCH 08/12] Add restart_wpoint to TD3 --- src/solvers/td3.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 315e7b295c..e6933c229d 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -83,6 +83,9 @@ module WP = (* If true, incremental side-effected var restart will only restart destabilized globals (using hack). If false, it will restart all destabilized side-effected vars. *) let restart_only_globals = false in + (* If true, wpoint will be restarted to bot when added. + This allows incremental to avoid reusing and republishing imprecise local values due to globals (which get restarted). *) + let restart_wpoint = true in let () = print_solver_stats := fun () -> Printf.printf "|rho|=%d\n|called|=%d\n|stable|=%d\n|infl|=%d\n|wpoint|=%d\n|side_dep|=%d\n|side_infl|=%d\n" @@ -179,8 +182,7 @@ module WP = if tracing then trace "sol2" "eval %a ## %a\n" S.Var.pretty_trace x S.Var.pretty_trace y; get_var_event y; if HM.mem called y then ( - if not (HM.mem wpoint y) then ( - (* TODO: add boolean flag *) + if restart_wpoint && not (HM.mem wpoint y) then ( if tracing then trace "sol2" "wpoint restart %a ## %a\n" S.Var.pretty_trace y S.Dom.pretty (HM.find_default rho y (S.Dom.bot ())); HM.replace rho y (S.Dom.bot ()); (* destabilize y *) (* TODO: would this do anything on called? *) From 36889e8c842947ef4af5f970b52e4e1da9db026a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 30 Sep 2021 11:03:34 +0300 Subject: [PATCH 09/12] Comment local wpoint restarting in TD3 --- src/solvers/td3.ml | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index e6933c229d..4cdd1e0926 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -126,6 +126,11 @@ module WP = if not (HM.mem called x || HM.mem stable x) then ( HM.replace stable x (); HM.replace called x (); + (* Here we cache HM.mem wpoint x before eq. If during eq eval makes x wpoint, then be still don't apply widening the first time, but just overwrite. + It means that the first iteration at wpoint is still precise. + This doesn't matter during normal solving (?), because old would be bot. + This matters during incremental loading, when wpoints have been removed (or not marshaled) and are redetected. + Then the previous local wpoint value is discarded automagically and not joined/widened, providing limited restarting of local wpoints. (See eval for more complete restarting.) *) let wp = HM.mem wpoint x in let l = HM.create 10 in let tmp = eq x (eval l x) (side x) in @@ -183,6 +188,9 @@ module WP = get_var_event y; if HM.mem called y then ( if restart_wpoint && not (HM.mem wpoint y) then ( + (* Even though solve cleverly restarts redetected wpoints during incremental load, the loop body would be calculated based on the old wpoint value. + The loop body might then side effect the old value, see tests/incremental/06-local-wpoint-read. + Here we avoid this, by setting it to bottom for the loop body eval. *) if tracing then trace "sol2" "wpoint restart %a ## %a\n" S.Var.pretty_trace y S.Dom.pretty (HM.find_default rho y (S.Dom.bot ())); HM.replace rho y (S.Dom.bot ()); (* destabilize y *) (* TODO: would this do anything on called? *) From a6912084d19b583e2e5b60cf3642b59f29e4f249 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 6 Oct 2021 11:13:27 +0300 Subject: [PATCH 10/12] Add option to restart wpoint only once in TD3 --- src/solvers/td3.ml | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 636d6fb20b..26e0fc4fc0 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -86,6 +86,10 @@ module WP = (* If true, wpoint will be restarted to bot when added. This allows incremental to avoid reusing and republishing imprecise local values due to globals (which get restarted). *) let restart_wpoint = true in + (* If true, each wpoint will be restarted once when added. + If false, it will be restarted each time it is added again (wpoints are removed after Narrow). *) + let restart_once = true in + let restarted_wpoint = HM.create 10 in let () = print_solver_stats := fun () -> Printf.printf "|rho|=%d\n|called|=%d\n|stable|=%d\n|infl|=%d\n|wpoint|=%d\n|side_dep|=%d\n|side_infl|=%d\n" @@ -191,9 +195,13 @@ module WP = (* Even though solve cleverly restarts redetected wpoints during incremental load, the loop body would be calculated based on the old wpoint value. The loop body might then side effect the old value, see tests/incremental/06-local-wpoint-read. Here we avoid this, by setting it to bottom for the loop body eval. *) - if tracing then trace "sol2" "wpoint restart %a ## %a\n" S.Var.pretty_trace y S.Dom.pretty (HM.find_default rho y (S.Dom.bot ())); - HM.replace rho y (S.Dom.bot ()); - (* destabilize y *) (* TODO: would this do anything on called? *) + if not (restart_once && HM.mem restarted_wpoint y) then ( + if tracing then trace "sol2" "wpoint restart %a ## %a\n" S.Var.pretty_trace y S.Dom.pretty (HM.find_default rho y (S.Dom.bot ())); + HM.replace rho y (S.Dom.bot ()); + (* destabilize y *) (* TODO: would this do anything on called? *) + if restart_once then (* avoid populating hashtable unnecessarily *) + HM.replace restarted_wpoint y (); + ) ); HM.replace wpoint y (); ); From e45b904e154406809b76854446dda92d12bb4a42 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 6 Oct 2021 11:14:38 +0300 Subject: [PATCH 11/12] Add options for wpoint restarting in incremental --- src/solvers/td3.ml | 4 ++-- src/util/defaults.ml | 2 ++ 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 26e0fc4fc0..6609dbcb35 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -85,10 +85,10 @@ module WP = let restart_only_globals = GobConfig.get_bool "incremental.restart.sided.only-global" in (* If true, wpoint will be restarted to bot when added. This allows incremental to avoid reusing and republishing imprecise local values due to globals (which get restarted). *) - let restart_wpoint = true in + let restart_wpoint = GobConfig.get_bool "incremental.restart.wpoint.enabled" in (* If true, each wpoint will be restarted once when added. If false, it will be restarted each time it is added again (wpoints are removed after Narrow). *) - let restart_once = true in + let restart_once = GobConfig.get_bool "incremental.restart.wpoint.once" in let restarted_wpoint = HM.create 10 in let () = print_solver_stats := fun () -> diff --git a/src/util/defaults.ml b/src/util/defaults.ml index 272a83aa7f..4e84715dd0 100644 --- a/src/util/defaults.ml +++ b/src/util/defaults.ml @@ -154,6 +154,8 @@ let _ = () ; reg Incremental "incremental.wpoint" "false" "Reuse the wpoint set (not recommended). Reusing the wpoint will combine existing results at previous widening points." ; reg Incremental "incremental.restart.sided.enabled" "true" "TODO" ; reg Incremental "incremental.restart.sided.only-global" "false" "TODO" + ; reg Incremental "incremental.restart.wpoint.enabled" "true" "TODO" + ; reg Incremental "incremental.restart.wpoint.once" "true" "TODO" (* {4 category [Semantics]} *) let _ = () From 437a07f6100a31c8347e06b0bc6256a7f4606478 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 6 Oct 2021 11:22:03 +0300 Subject: [PATCH 12/12] Add comment about finding old value after eq in TD3 --- 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 6609dbcb35..a635c71b16 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -142,7 +142,7 @@ module WP = if tracing then trace "sol" "Var: %a\n" S.Var.pretty_trace x ; if tracing then trace "sol" "Contrib:%a\n" S.Dom.pretty tmp; HM.remove called x; - let old = HM.find rho x in + let old = HM.find rho x in (* find old value after eq since wpoint restarting in eq/eval might have changed it meanwhile *) let tmp = if not wp then tmp else