From 18ee07c0c7b4fc0fa505a28e968fd7a9a2c52746 Mon Sep 17 00:00:00 2001 From: Felix Krayer Date: Sun, 10 Nov 2024 10:31:15 +0100 Subject: [PATCH 1/2] 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 e95b1ec77d6a934dc423fc331426df0693e3a3aa Mon Sep 17 00:00:00 2001 From: Felix Krayer Date: Sun, 10 Nov 2024 10:58:20 +0100 Subject: [PATCH 2/2] 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);