Skip to content

Commit 56128fd

Browse files
FelixKrayerFelixKrayer
committed
td_simplified w/ some suggestions
1 parent e36e738 commit 56128fd

File tree

1 file changed

+208
-0
lines changed

1 file changed

+208
-0
lines changed

‎src/solver/td_simplified.ml‎

Lines changed: 208 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,208 @@
1+
(** Top-down solver with side effects. Simplified version of the td3 solver ([td_simplified]).*)
2+
3+
(** Top down solver that uses the box-operator for widening/narrowing at widening points. *)
4+
5+
open Batteries
6+
open ConstrSys
7+
open Messages
8+
9+
module M = Messages
10+
11+
module Base : GenericEqSolver =
12+
functor (S:EqConstrSys) ->
13+
functor (HM:Hashtbl.S with type key = S.v) ->
14+
struct
15+
open SolverBox.Warrow (S.Dom)
16+
include Generic.SolverStats (S) (HM)
17+
module VS = Set.Make (S.Var)
18+
19+
let solve st vs =
20+
let called = HM.create 10 in
21+
let infl = HM.create 10 in
22+
let rho = HM.create 10 in
23+
let wpoint = HM.create 10 in
24+
let stable = HM.create 10 in
25+
26+
let () = print_solver_stats := fun () ->
27+
Logs.debug "|rho|=%d" (HM.length rho);
28+
Logs.debug "|stable|=%d" (HM.length stable);
29+
Logs.debug "|infl|=%d" (HM.length infl);
30+
Logs.debug "|wpoint|=%d" (HM.length wpoint);
31+
Logs.info "|called|=%d" (HM.length called);
32+
print_context_stats rho
33+
in
34+
35+
let add_infl y x =
36+
if tracing then trace "infl" "add_infl %a %a" S.Var.pretty_trace y S.Var.pretty_trace x;
37+
HM.replace infl y (VS.add x (HM.find_default infl y VS.empty));
38+
in
39+
40+
let init x =
41+
if not (HM.mem rho x) then (
42+
new_var_event x;
43+
if tracing then trace "init" "init %a" S.Var.pretty_trace x;
44+
HM.replace rho x (S.Dom.bot ())
45+
)
46+
in
47+
48+
let eq x get set =
49+
if tracing then trace "eq" "eq %a" S.Var.pretty_trace x;
50+
match S.system x with
51+
| None -> S.Dom.bot ()
52+
| Some f -> f get set
53+
in
54+
55+
let rec destabilize x =
56+
if tracing then trace "destab" "destabilize %a" S.Var.pretty_trace x;
57+
let w = HM.find_default infl x VS.empty in
58+
HM.replace infl x VS.empty;
59+
VS.iter (fun y ->
60+
if tracing then trace "destab" "stable remove %a" S.Var.pretty_trace y;
61+
HM.remove stable y;
62+
destabilize y
63+
) w
64+
in
65+
66+
let rec iterate x = (* ~(inner) solve in td3*)
67+
let query x y = (* ~eval in td3 *)
68+
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);
69+
get_var_event y;
70+
if not (HM.mem called y) then (
71+
if S.system y = None then (
72+
init y;
73+
HM.replace stable y ()
74+
) else (
75+
HM.replace called y ();
76+
if tracing then trace "iter" "iterate called from query";
77+
iterate y;
78+
HM.remove called y)
79+
) else (
80+
if tracing && not (HM.mem wpoint y) then trace "wpoint" "query adding wpoint %a" S.Var.pretty_trace y;
81+
HM.replace wpoint y ();
82+
);
83+
let tmp = HM.find rho y in
84+
add_infl y x;
85+
if tracing then trace "answer" "exiting query for %a\nanswer: %a" S.Var.pretty_trace y S.Dom.pretty tmp;
86+
tmp
87+
in
88+
89+
let side x y d = (* side from x to y; only to variables y w/o rhs; x only used for trace *)
90+
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;
91+
assert (S.system y = None);
92+
init y;
93+
let widen a b =
94+
if M.tracing then M.trace "wpoint" "side widen %a" S.Var.pretty_trace y;
95+
S.Dom.widen a (S.Dom.join a b)
96+
in
97+
let op a b = if HM.mem wpoint y then widen a b else S.Dom.join a b
98+
in
99+
let old = HM.find rho y in
100+
let tmp = op old d in
101+
HM.replace stable y ();
102+
if not (S.Dom.leq tmp old) then (
103+
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;
104+
HM.replace rho y tmp;
105+
destabilize y;
106+
(* make y a widening point. This will only matter for the next side _ y. *)
107+
if tracing && not (HM.mem wpoint y) then trace "wpoint" "side adding wpoint %a" S.Var.pretty_trace y;
108+
HM.replace wpoint y ()
109+
)
110+
in
111+
112+
(* begining of iterate*)
113+
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);
114+
init x;
115+
assert (S.system x <> None);
116+
if not (HM.mem stable x) then (
117+
HM.replace stable x ();
118+
let wp = HM.mem wpoint x in (* if x becomes a wpoint during eq, checking this will delay widening until next iterate *)
119+
let eqd = eq x (query x) (side x) in (* d from equation/rhs *)
120+
let old = HM.find rho x in (* d from older iterate *)
121+
let wpd = (* d after widen/narrow (if wp) *)
122+
if not wp then eqd
123+
else (
124+
if M.tracing then M.trace "wpoint" "widen %a" S.Var.pretty_trace x;
125+
box old eqd)
126+
in
127+
if not (Timing.wrap "S.Dom.equal" (fun () -> S.Dom.equal old wpd) ()) then (
128+
(* old != wpd *)
129+
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);
130+
update_var_event x old wpd;
131+
HM.replace rho x wpd;
132+
destabilize x;
133+
if tracing then trace "iter" "iterate changed %a" S.Var.pretty_trace x;
134+
(iterate[@tailcall]) x
135+
) else (
136+
(* old == wpd *)
137+
if not (HM.mem stable x) then (
138+
(* value unchanged, but not stable, i.e. destabilized itself during rhs *)
139+
if tracing then trace "iter" "iterate still unstable %a" S.Var.pretty_trace x;
140+
(iterate[@tailcall]) x
141+
) else (
142+
(* 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. *)
143+
if tracing && (HM.mem wpoint x) then trace "wpoint" "iterate removing wpoint %a" S.Var.pretty_trace x;
144+
HM.remove wpoint x
145+
)
146+
)
147+
)
148+
in
149+
150+
let set_start (x,d) =
151+
init x;
152+
HM.replace rho x d;
153+
HM.replace stable x ();
154+
in
155+
156+
(* beginning of main solve *)
157+
start_event ();
158+
159+
List.iter set_start st;
160+
161+
List.iter init vs;
162+
(* 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. *)
163+
let i = ref 0 in
164+
let rec solver () = (* as while loop in paper *)
165+
incr i;
166+
let unstable_vs = List.filter (neg (HM.mem stable)) vs in
167+
if unstable_vs <> [] then (
168+
if Logs.Level.should_log Debug then (
169+
if !i = 1 then Logs.newline ();
170+
Logs.debug "Unstable solver start vars in %d. phase:" !i;
171+
List.iter (fun v -> Logs.debug "\t%a" S.Var.pretty_trace v) unstable_vs;
172+
Logs.newline ();
173+
flush_all ();
174+
);
175+
List.iter (fun x -> HM.replace called x ();
176+
if tracing then trace "multivar" "solving for %a" S.Var.pretty_trace x;
177+
iterate x;
178+
HM.remove called x
179+
) unstable_vs;
180+
solver ();
181+
)
182+
in
183+
solver ();
184+
(* After termination, only those variables are stable which are
185+
* - reachable from any of the queried variables vs, or
186+
* - effected by side-effects and have no constraints on their own (this should be the case for all of our analyses). *)
187+
188+
stop_event ();
189+
if Logs.Level.should_log Debug then (
190+
Logs.debug "Data after iterate completed";
191+
Logs.debug "|rho|=%d" (HM.length rho);
192+
Logs.debug "|stable|=%d" (HM.length stable);
193+
Logs.debug "|infl|=%d" (HM.length infl);
194+
Logs.debug "|wpoint|=%d" (HM.length wpoint)
195+
);
196+
197+
if GobConfig.get_bool "dbg.print_wpoints" then (
198+
Logs.newline ();
199+
Logs.debug "Widening points:";
200+
HM.iter (fun k () -> Logs.debug "%a" S.Var.pretty_trace k) wpoint;
201+
Logs.newline ();
202+
);
203+
204+
rho
205+
end
206+
207+
let () =
208+
Selector.add_solver ("td_simplified", (module PostSolver.EqIncrSolverFromEqSolver (Base)));

0 commit comments

Comments
 (0)