From 56128fd85eb161d07ad970abf88f66e6c9d2ee3b Mon Sep 17 00:00:00 2001 From: Felix Krayer Date: Sun, 10 Nov 2024 10:31:15 +0100 Subject: [PATCH 1/3] td_simplified w/ some suggestions --- src/solver/td_simplified.ml | 208 ++++++++++++++++++++++++++++++++++++ 1 file changed, 208 insertions(+) create mode 100644 src/solver/td_simplified.ml diff --git a/src/solver/td_simplified.ml b/src/solver/td_simplified.ml new file mode 100644 index 0000000000..75fe8bda00 --- /dev/null +++ b/src/solver/td_simplified.ml @@ -0,0 +1,208 @@ +(** Top-down solver with side effects. Simplified version of the td3 solver ([td_simplified]).*) + +(** Top down solver that uses the box-operator for widening/narrowing at widening points. *) + +open Batteries +open ConstrSys +open Messages + +module M = Messages + +module Base : GenericEqSolver = + functor (S:EqConstrSys) -> + functor (HM:Hashtbl.S with type key = S.v) -> + struct + open SolverBox.Warrow (S.Dom) + include Generic.SolverStats (S) (HM) + module VS = Set.Make (S.Var) + + let solve st vs = + let called = HM.create 10 in + let infl = HM.create 10 in + let rho = HM.create 10 in + let wpoint = HM.create 10 in + let stable = HM.create 10 in + + let () = print_solver_stats := fun () -> + Logs.debug "|rho|=%d" (HM.length rho); + Logs.debug "|stable|=%d" (HM.length stable); + Logs.debug "|infl|=%d" (HM.length infl); + Logs.debug "|wpoint|=%d" (HM.length wpoint); + Logs.info "|called|=%d" (HM.length called); + print_context_stats rho + in + + let add_infl y x = + if tracing then trace "infl" "add_infl %a %a" S.Var.pretty_trace y S.Var.pretty_trace x; + HM.replace infl y (VS.add x (HM.find_default infl y VS.empty)); + in + + let init x = + if not (HM.mem rho x) then ( + new_var_event x; + if tracing then trace "init" "init %a" S.Var.pretty_trace x; + HM.replace rho x (S.Dom.bot ()) + ) + in + + let eq x get set = + if tracing then trace "eq" "eq %a" S.Var.pretty_trace x; + match S.system x with + | None -> S.Dom.bot () + | Some f -> f get set + in + + let rec destabilize x = + if tracing then trace "destab" "destabilize %a" S.Var.pretty_trace x; + let w = HM.find_default infl x VS.empty in + HM.replace infl x VS.empty; + VS.iter (fun y -> + if tracing then trace "destab" "stable remove %a" S.Var.pretty_trace y; + HM.remove stable y; + destabilize y + ) w + in + + let rec iterate x = (* ~(inner) solve in td3*) + let query x y = (* ~eval in td3 *) + if tracing then trace "solver_query" "entering query for %a; stable %b; called %b" S.Var.pretty_trace y (HM.mem stable y) (HM.mem called y); + get_var_event y; + if not (HM.mem called y) then ( + if S.system y = None then ( + init y; + HM.replace stable y () + ) else ( + HM.replace called y (); + if tracing then trace "iter" "iterate called from query"; + iterate y; + HM.remove called y) + ) else ( + if tracing && not (HM.mem wpoint y) then trace "wpoint" "query adding wpoint %a" S.Var.pretty_trace y; + HM.replace wpoint y (); + ); + let tmp = HM.find rho y in + add_infl y x; + if tracing then trace "answer" "exiting query for %a\nanswer: %a" S.Var.pretty_trace y S.Dom.pretty tmp; + tmp + in + + let side x y d = (* side from x to y; only to variables y w/o rhs; x only used for trace *) + if tracing then trace "side" "side to %a (wpx: %b) from %a; value: %a" S.Var.pretty_trace y (HM.mem wpoint y) S.Var.pretty_trace x S.Dom.pretty d; + assert (S.system y = None); + init y; + let widen a b = + if M.tracing then M.trace "wpoint" "side widen %a" S.Var.pretty_trace y; + S.Dom.widen a (S.Dom.join a b) + in + let op a b = if HM.mem wpoint y then widen a b else S.Dom.join a b + in + let old = HM.find rho y in + let tmp = op old d in + HM.replace stable y (); + if not (S.Dom.leq tmp old) then ( + if tracing && not (S.Dom.is_bot old) then trace "update" "side to %a (wpx: %b) from %a new: %a" S.Var.pretty_trace y (HM.mem wpoint y) S.Var.pretty_trace x S.Dom.pretty tmp; + HM.replace rho y tmp; + destabilize y; + (* make y a widening point. This will only matter for the next side _ y. *) + if tracing && not (HM.mem wpoint y) then trace "wpoint" "side adding wpoint %a" S.Var.pretty_trace y; + HM.replace wpoint y () + ) + in + + (* begining of iterate*) + if tracing then trace "iter" "begin iterate %a, called: %b, stable: %b, wpoint: %b" S.Var.pretty_trace x (HM.mem called x) (HM.mem stable x) (HM.mem wpoint x); + init x; + assert (S.system x <> None); + if not (HM.mem stable x) then ( + HM.replace stable x (); + let wp = HM.mem wpoint x in (* if x becomes a wpoint during eq, checking this will delay widening until next iterate *) + let eqd = eq x (query x) (side x) in (* d from equation/rhs *) + let old = HM.find rho x in (* d from older iterate *) + let wpd = (* d after widen/narrow (if wp) *) + if not wp then eqd + else ( + if M.tracing then M.trace "wpoint" "widen %a" S.Var.pretty_trace x; + box old eqd) + in + if not (Timing.wrap "S.Dom.equal" (fun () -> S.Dom.equal old wpd) ()) then ( + (* old != wpd *) + if tracing && not (S.Dom.is_bot old) then trace "update" "%a (wpx: %b): %a" S.Var.pretty_trace x (HM.mem wpoint x) S.Dom.pretty_diff (wpd, old); + update_var_event x old wpd; + HM.replace rho x wpd; + destabilize x; + if tracing then trace "iter" "iterate changed %a" S.Var.pretty_trace x; + (iterate[@tailcall]) x + ) else ( + (* old == wpd *) + if not (HM.mem stable x) then ( + (* value unchanged, but not stable, i.e. destabilized itself during rhs *) + if tracing then trace "iter" "iterate still unstable %a" S.Var.pretty_trace x; + (iterate[@tailcall]) x + ) else ( + (* this makes e.g. nested loops precise, ex. tests/regression/34-localization/01-nested.c - if we do not remove wpoint, the inner loop head will stay a wpoint and widen the outer loop variable. *) + if tracing && (HM.mem wpoint x) then trace "wpoint" "iterate removing wpoint %a" S.Var.pretty_trace x; + HM.remove wpoint x + ) + ) + ) + in + + let set_start (x,d) = + init x; + HM.replace rho x d; + HM.replace stable x (); + in + + (* beginning of main solve *) + start_event (); + + List.iter set_start st; + + List.iter init vs; + (* If we have multiple start variables vs, we might solve v1, then while solving v2 we side some global which v1 depends on with a new value. Then v1 is no longer stable and we have to solve it again. *) + let i = ref 0 in + let rec solver () = (* as while loop in paper *) + incr i; + let unstable_vs = List.filter (neg (HM.mem stable)) vs in + if unstable_vs <> [] then ( + if Logs.Level.should_log Debug then ( + if !i = 1 then Logs.newline (); + Logs.debug "Unstable solver start vars in %d. phase:" !i; + List.iter (fun v -> Logs.debug "\t%a" S.Var.pretty_trace v) unstable_vs; + Logs.newline (); + flush_all (); + ); + List.iter (fun x -> HM.replace called x (); + if tracing then trace "multivar" "solving for %a" S.Var.pretty_trace x; + iterate x; + HM.remove called x + ) unstable_vs; + solver (); + ) + in + solver (); + (* After termination, only those variables are stable which are + * - reachable from any of the queried variables vs, or + * - effected by side-effects and have no constraints on their own (this should be the case for all of our analyses). *) + + stop_event (); + if Logs.Level.should_log Debug then ( + Logs.debug "Data after iterate completed"; + Logs.debug "|rho|=%d" (HM.length rho); + Logs.debug "|stable|=%d" (HM.length stable); + Logs.debug "|infl|=%d" (HM.length infl); + Logs.debug "|wpoint|=%d" (HM.length wpoint) + ); + + if GobConfig.get_bool "dbg.print_wpoints" then ( + Logs.newline (); + Logs.debug "Widening points:"; + HM.iter (fun k () -> Logs.debug "%a" S.Var.pretty_trace k) wpoint; + Logs.newline (); + ); + + rho + end + +let () = + Selector.add_solver ("td_simplified", (module PostSolver.EqIncrSolverFromEqSolver (Base))); From 4755400febd549079ef629d6a8d1b9ec5194d808 Mon Sep 17 00:00:00 2001 From: Felix Krayer Date: Sun, 10 Nov 2024 10:58:20 +0100 Subject: [PATCH 2/3] move query and side out of iterate --- src/solver/td_simplified.ml | 85 ++++++++++++++++++------------------- 1 file changed, 41 insertions(+), 44 deletions(-) diff --git a/src/solver/td_simplified.ml b/src/solver/td_simplified.ml index 75fe8bda00..d39230adf7 100644 --- a/src/solver/td_simplified.ml +++ b/src/solver/td_simplified.ml @@ -63,53 +63,50 @@ module Base : GenericEqSolver = ) w in - let rec iterate x = (* ~(inner) solve in td3*) - let query x y = (* ~eval in td3 *) - if tracing then trace "solver_query" "entering query for %a; stable %b; called %b" S.Var.pretty_trace y (HM.mem stable y) (HM.mem called y); - get_var_event y; - if not (HM.mem called y) then ( - if S.system y = None then ( - init y; - HM.replace stable y () - ) else ( - HM.replace called y (); - if tracing then trace "iter" "iterate called from query"; - iterate y; - HM.remove called y) + let rec query x y = (* ~eval in td3 *) + if tracing then trace "solver_query" "entering query for %a; stable %b; called %b" S.Var.pretty_trace y (HM.mem stable y) (HM.mem called y); + get_var_event y; + if not (HM.mem called y) then ( + if S.system y = None then ( + init y; + HM.replace stable y () ) else ( - if tracing && not (HM.mem wpoint y) then trace "wpoint" "query adding wpoint %a" S.Var.pretty_trace y; - HM.replace wpoint y (); - ); - let tmp = HM.find rho y in - add_infl y x; - if tracing then trace "answer" "exiting query for %a\nanswer: %a" S.Var.pretty_trace y S.Dom.pretty tmp; - tmp + HM.replace called y (); + if tracing then trace "iter" "iterate called from query"; + iterate y; + HM.remove called y) + ) else ( + if tracing && not (HM.mem wpoint y) then trace "wpoint" "query adding wpoint %a" S.Var.pretty_trace y; + HM.replace wpoint y (); + ); + let tmp = HM.find rho y in + add_infl y x; + if tracing then trace "answer" "exiting query for %a\nanswer: %a" S.Var.pretty_trace y S.Dom.pretty tmp; + tmp + + and side x y d = (* side from x to y; only to variables y w/o rhs; x only used for trace *) + if tracing then trace "side" "side to %a (wpx: %b) from %a; value: %a" S.Var.pretty_trace y (HM.mem wpoint y) S.Var.pretty_trace x S.Dom.pretty d; + assert (S.system y = None); + init y; + let widen a b = + if M.tracing then M.trace "wpoint" "side widen %a" S.Var.pretty_trace y; + S.Dom.widen a (S.Dom.join a b) in + let op a b = if HM.mem wpoint y then widen a b else S.Dom.join a b + in + let old = HM.find rho y in + let tmp = op old d in + HM.replace stable y (); + if not (S.Dom.leq tmp old) then ( + if tracing && not (S.Dom.is_bot old) then trace "update" "side to %a (wpx: %b) from %a new: %a" S.Var.pretty_trace y (HM.mem wpoint y) S.Var.pretty_trace x S.Dom.pretty tmp; + HM.replace rho y tmp; + destabilize y; + (* make y a widening point. This will only matter for the next side _ y. *) + if tracing && not (HM.mem wpoint y) then trace "wpoint" "side adding wpoint %a" S.Var.pretty_trace y; + HM.replace wpoint y () + ) - let side x y d = (* side from x to y; only to variables y w/o rhs; x only used for trace *) - if tracing then trace "side" "side to %a (wpx: %b) from %a; value: %a" S.Var.pretty_trace y (HM.mem wpoint y) S.Var.pretty_trace x S.Dom.pretty d; - assert (S.system y = None); - init y; - let widen a b = - if M.tracing then M.trace "wpoint" "side widen %a" S.Var.pretty_trace y; - S.Dom.widen a (S.Dom.join a b) - in - let op a b = if HM.mem wpoint y then widen a b else S.Dom.join a b - in - let old = HM.find rho y in - let tmp = op old d in - HM.replace stable y (); - if not (S.Dom.leq tmp old) then ( - if tracing && not (S.Dom.is_bot old) then trace "update" "side to %a (wpx: %b) from %a new: %a" S.Var.pretty_trace y (HM.mem wpoint y) S.Var.pretty_trace x S.Dom.pretty tmp; - HM.replace rho y tmp; - destabilize y; - (* make y a widening point. This will only matter for the next side _ y. *) - if tracing && not (HM.mem wpoint y) then trace "wpoint" "side adding wpoint %a" S.Var.pretty_trace y; - HM.replace wpoint y () - ) - in - - (* begining of iterate*) + and iterate x = (* ~(inner) solve in td3*) if tracing then trace "iter" "begin iterate %a, called: %b, stable: %b, wpoint: %b" S.Var.pretty_trace x (HM.mem called x) (HM.mem stable x) (HM.mem wpoint x); init x; assert (S.system x <> None); From 4385b73b04d5db90c5be701b104ba46257f52516 Mon Sep 17 00:00:00 2001 From: Felix Krayer Date: Sat, 21 Dec 2024 18:20:09 +0100 Subject: [PATCH 3/3] add td_simplified to Goblint_lib and cram test 00/01 --- src/solver/goblint_solver.ml | 1 + tests/regression/00-sanity/01-assert.t | 12 ++++++++++++ 2 files changed, 13 insertions(+) diff --git a/src/solver/goblint_solver.ml b/src/solver/goblint_solver.ml index 0a264d7dea..946fff070b 100644 --- a/src/solver/goblint_solver.ml +++ b/src/solver/goblint_solver.ml @@ -5,6 +5,7 @@ The top-down solver family. *) module Td3 = Td3 +module Td_simplified = Td_simplified module TopDown = TopDown module TopDown_term = TopDown_term module TopDown_space_cache_term = TopDown_space_cache_term diff --git a/tests/regression/00-sanity/01-assert.t b/tests/regression/00-sanity/01-assert.t index 9b3b55f530..6dcebd71df 100644 --- a/tests/regression/00-sanity/01-assert.t +++ b/tests/regression/00-sanity/01-assert.t @@ -100,6 +100,18 @@ Test topdown solvers: dead: 2 total lines: 9 + $ goblint --enable warn.deterministic --set solver td_simplified 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: