Skip to content

Commit 09b8d91

Browse files
arkocalarkocal
committed
Factor out commons from fwdsolver as well
1 parent 12d0b07 commit 09b8d91

File tree

4 files changed

+57
-308
lines changed

4 files changed

+57
-308
lines changed

‎src/framework/bu.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ module FwdBuSolver (System: FwdGlobConstrSys) = struct
2727
and get_local _ = raise (Failure "Locals should not be queried in rhs")
2828

2929
and set_local contributor y d =
30-
match Lcl.update_contribution contributor y d with
30+
match Lcl.update_contribution contributor y d false with
3131
| Updated y_record -> (
3232
if y_record.called then y_record.aborted <- true
3333
else (iterate[@tailcall]) y

‎src/framework/fwdCommon.ml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -136,12 +136,12 @@ module SolverLocals (Sys: FwdGlobConstrSys) (LM: Hashtbl.S with type key=Sys.LVa
136136

137137
type updated_contribution = Updated of t | NotUpdated of t
138138

139-
let update_contribution contributor y d =
139+
let update_contribution contributor y d always_warrow =
140140
let y_record = get y in
141141
let old_contribution = get_contribution contributor y_record in
142142
let new_contribution =
143143
(* Automatic detection of warrowing points *)
144-
if y_record.called then warrow old_contribution d
144+
if (always_warrow || y_record.called) then warrow old_contribution d
145145
else {old_contribution with value=d} in
146146

147147
if (D.equal new_contribution.value old_contribution.value) then NotUpdated y_record

‎src/framework/fwdSolver.ml‎

Lines changed: 53 additions & 304 deletions
Original file line numberDiff line numberDiff line change
@@ -3,319 +3,68 @@ open Messages
33

44
module FwdSolver (System: FwdGlobConstrSys) = struct
55

6-
module D = System.D
7-
module G = System.G
6+
open FwdCommon.BaseFwdSolver(System)
7+
open FwdCommon.SolverStats(System)
88

9-
module LS = Set.Make (System.LVar)
9+
module WorkSet = struct
10+
let list = ref ([]: System.LVar.t list)
11+
let set = ref LS.empty
1012

11-
module GM = Hashtbl.Make(System.GVar)
12-
module LM = Hashtbl.Make(System.LVar)
13-
(*
14-
module OM = LM
15-
let source x = x
16-
*)
17-
18-
module OM = Hashtbl.Make(Node)
19-
let source = System.LVar.node
20-
21-
let rhs_eval_count = ref 0
22-
23-
module LWarrow = FwdCommon.Warrow(System.D)
24-
let lwarrow = LWarrow.warrow
25-
let gas_default = FwdCommon.gas_default
26-
27-
module GWarrow = FwdCommon.Warrow(System.G)
28-
let gwarrow = GWarrow.warrow
29-
30-
let work = ref (([] : System.LVar.t list), LS.empty)
31-
32-
let add_work x = let (l,s) = !work in
33-
if LS.mem x s then ()
34-
else work := (x::l, LS.add x s)
35-
36-
let rem_work () = let (l,s) = !work in
37-
match l with
38-
| [] -> None
39-
| x::xs ->
40-
let s = LS.remove x s in
41-
let _ = work := (xs,s) in
42-
Some x
43-
44-
type glob = {value : G.t; init : G.t; infl : LS.t; last : G.t LM.t; from : (G.t * int * int * bool * LS.t) OM.t}
45-
(*
46-
now table from with widening delay and narrowing gas to ensure termination
47-
*)
48-
49-
let glob: glob GM.t = GM.create 100
50-
51-
(* auxiliary functions for globals *)
52-
53-
let get_global_ref g =
54-
try GM.find glob g
55-
with _ ->
56-
(let rglob = {value = G.bot (); init = G.bot (); infl = LS.empty; last = LM.create 10; from = OM.create 10} in
57-
GM.add glob g rglob;
58-
rglob
13+
let add x =
14+
if not (LS.mem x !set) then (
15+
list := x::!list;
16+
set := LS.add x !set
5917
)
6018

61-
let init_global (g, d) =
62-
GM.add glob g {
63-
value = d;
64-
init = d;
65-
infl = LS.empty;
66-
last = LM.create 10;
67-
from = OM.create 10
68-
}
69-
70-
let get_global_value init from = OM.fold (fun _ (b,_,_,_,_) a -> G.join a b) from init
71-
72-
let get_old_global_value x from =
73-
let sx = source x in
74-
try OM.find from sx
75-
with _ ->
76-
let (delay,gas) = !gas_default in
77-
OM.add from sx (G.bot (),delay,gas,false, LS.empty);
78-
(G. bot (),delay,gas,false, LS.empty)
79-
80-
(* now the getters and setters for globals, setters with warrowing per origin *)
19+
let rec map_until_empty f =
20+
match !list with
21+
| [] -> ()
22+
| x::xs -> (
23+
set := LS.remove x !set;
24+
list := xs;
25+
f x;
26+
map_until_empty f
27+
)
28+
end
8129

8230
let get_global x g =
83-
let rglob = get_global_ref g in
84-
GM.replace glob g { rglob with infl = LS.add x rglob.infl };
85-
(* ensure the global is in the hashtable *)
86-
rglob.value
31+
let glob_data = Gbl.get g in
32+
Gbl.add_infl glob_data g x;
33+
glob_data.value
8734

8835
let set_global x g d =
89-
let sx = source x in
90-
(*
91-
replaces old contribution with the new one;
92-
reconstructs value of g from contributions;
93-
propagates infl and updates value - if value has changed
94-
*)
95-
let {value;init;infl;last;from} = get_global_ref g in
96-
let (old_xg,delay,gas,narrow,set) = get_old_global_value x from in
97-
let () = LM.add last x d in
98-
let set = LS.add x set in
99-
let d = LS.fold (fun x d -> G.join d (LM.find last x)) set d in
100-
let (new_xg,delay,gas,narrow) = gwarrow (old_xg,delay,gas,narrow) d in
101-
if G.equal new_xg old_xg then ()
102-
else
103-
let _ = OM.replace from sx (new_xg,delay,gas,narrow,set) in
104-
let new_g = if G.leq old_xg new_xg then G.join value new_xg
105-
else get_global_value init from in
106-
if G.equal value new_g then
107-
()
108-
else
109-
begin
110-
GM.replace glob g {value = new_g; init = init; infl = LS.empty; last; from};
111-
LS.iter add_work infl
112-
end
113-
114-
type loc = {mutable loc_value : D.t; loc_init : D.t; loc_from : (D.t * int * int * bool) LM.t}
115-
(*
116-
init may contain some initial value not provided by separate origin;
117-
perhaps, dynamic tracking of dependencies required for certain locals?
118-
119-
One might additionally maintain in table loc the set of previous contribs
120-
for rewoking vacuous previous contributions - important if large values
121-
are prematurely propagated which later become obsolete (no contrib from that
122-
origin anymore ...
123-
*)
124-
125-
let loc: loc LM.t = LM.create 100
126-
127-
(* auxiliary functions for locals *)
128-
129-
130-
let get_local_ref x =
131-
try LM.find loc x
132-
with _ ->
133-
(let rloc = {loc_value = D.bot (); loc_init = D.bot (); loc_from = LM.create 10} in
134-
LM.add loc x rloc;
135-
rloc)
136-
137-
let init_local (x, d) =
138-
LM.add loc x {
139-
loc_value = d;
140-
loc_init = d;
141-
loc_from = LM.create 10
142-
}
143-
144-
let get_local_value init from = LM.fold (fun _ (b,_,_,_) a -> D.join a b) from init
145-
146-
let get_old_local_value x from =
147-
try LM.find from x
148-
with _ -> let (delay,gas) = !gas_default in
149-
LM.add from x (D.bot (),delay,gas,false);
150-
(D.bot (),delay,gas,false)
151-
152-
(* now the getters and setters for locals, setters with warrowing per origin *)
153-
154-
let get_local x y = raise (Failure "locals should not be queried!")
155-
156-
let set_local x y d =
157-
(*
158-
replaces old contribution with the new one;
159-
reconstructs value of y from contributions;
160-
propagates infl together with y and updates value - if value has changed
161-
*)
162-
let {loc_value;loc_init;loc_from} as y_record = get_local_ref y in
163-
let (old_xy,delay,gas,narrow) = get_old_local_value x loc_from in
164-
let (new_xy,delay,gas,narrow) = lwarrow (old_xy,delay,gas,narrow) d in
165-
if D.equal new_xy old_xy then ()
166-
else
167-
let _ = LM.replace loc_from x (new_xy,delay,gas,narrow) in
168-
let new_y = if D.leq old_xy new_xy then
169-
D.join loc_value new_xy
170-
else get_local_value loc_init loc_from in
171-
if D.equal loc_value new_y then
172-
()
173-
else (
174-
y_record.loc_value <- new_y;
175-
add_work y
36+
match Gbl.update_contribution x g d with
37+
| Updated g_record -> (
38+
let work = g_record.infl in
39+
Gbl.replace g {g_record with infl = LS.empty};
40+
LS.iter WorkSet.add work
17641
)
177-
178-
(*
179-
wrapper around propagation function to collect multiple contributions to same unknowns;
180-
contributions are delayed until the very end
181-
*)
182-
183-
let wrap (x,f) d =
184-
rhs_eval_count := !rhs_eval_count + 1;
185-
let sigma = LM.create 10 in
186-
let tau = GM.create 10 in
187-
let add_sigma y d =
188-
let d = try D.join d (LM.find sigma y) with _ -> d in
189-
LM.replace sigma y d in
190-
let add_tau g d =
191-
let d = try G.join d (GM.find tau g) with _ -> d in
192-
GM.replace tau g d in
193-
let _ = f d (get_local x) add_sigma (get_global x) add_tau in
194-
let _ = GM.iter (set_global x) tau in
195-
let _ = LM.iter (set_local x) sigma in
196-
()
197-
198-
(* ... now the main solver loop ... *)
199-
200-
let solve xs =
201-
if tracing then trace "solver" "fwd";
202-
let _ = List.iter add_work xs in
203-
let rec doit () = match rem_work () with
204-
| None -> ()
205-
| Some x -> (
206-
match System.system x with
207-
| None -> doit ()
208-
| Some f ->
209-
(let rloc = get_local_ref x in
210-
wrap (x,f) rloc.loc_value;
211-
(doit[@tailcall]) ())
212-
) in
213-
let _ = doit () in
214-
let sigma = LM.to_seq loc |> Seq.map (fun (k,l) -> (k,l.loc_value)) in
215-
let tau = GM.to_seq glob |> Seq.map (fun (k,l) -> (k,l.value)) in
216-
(sigma, tau)
217-
218-
219-
let solve localinit globalinit startvars =
220-
let starttime_ms = int_of_float (Unix.gettimeofday () *. 1000.) in
221-
Logs.info "Solver start: %d" starttime_ms;
222-
let _ = List.iter init_local localinit in
223-
let _ = List.iter init_global globalinit in
224-
(*
225-
ignore (solve startvars);
226-
*)
227-
let solution = solve startvars in
228-
let endtime_ms = int_of_float (Unix.gettimeofday () *. 1000.) in
229-
Logs.info "Solver end: %d" endtime_ms;
230-
Logs.info "RHS: %d" !rhs_eval_count;
42+
| NotUpdated _ -> ()
43+
44+
let get_local _ = raise (Failure "Locals should not be queried in rhs")
45+
46+
let set_local contributor y d =
47+
match Lcl.update_contribution contributor y d true with
48+
| Updated y_record -> WorkSet.add y
49+
| NotUpdated _ -> ()
50+
51+
let wrapped rhs x d = (wrap get_local get_global set_local set_global) rhs x d
52+
53+
let evaluate x =
54+
match System.system x with
55+
| None -> ()
56+
| Some f -> wrapped f x (Lcl.get x).loc_value
57+
58+
let solve localinit globalinit start_unknowns =
59+
solver_start_event ();
60+
List.iter Lcl.init localinit;
61+
List.iter Gbl.init globalinit;
62+
List.iter WorkSet.add start_unknowns;
63+
WorkSet.map_until_empty evaluate;
64+
let solution = (Lcl.to_seq (), Gbl.to_seq ()) in
65+
solver_end_event ();
23166
solution
23267

233-
(* ... now the checker! *)
234-
235-
let check localinit globalinit xs =
236-
237-
let sigma_out = LM.create 100 in
238-
let tau_out = GM.create 100 in
239-
240-
let get_local x = try (LM.find loc x).loc_value with _ -> D.bot () in
241-
242-
let check_local x d = if D.leq d (D.bot ()) then ()
243-
else let {loc_value:D.t;loc_init;loc_from} = get_local_ref x in
244-
if D.leq d loc_value then
245-
if LM.mem sigma_out x then ()
246-
else (
247-
LM.add sigma_out x loc_value;
248-
add_work x
249-
)
250-
else (
251-
Logs.error "Fixpoint not reached for local %a" System.LVar.pretty_trace x;
252-
AnalysisState.verified := Some false;
253-
if LM.mem sigma_out x then ()
254-
else (
255-
LM.add sigma_out x loc_value;
256-
add_work x
257-
)
258-
) in
259-
260-
let get_global g = try (GM.find glob g).value with _ -> G.bot () in
261-
262-
let check_global x g d =
263-
if G.leq d (G.bot ()) then
264-
()
265-
else if System.GVar.is_write_only g then
266-
GM.replace tau_out g (G.join (GM.find_opt tau_out g |> BatOption.default (G.bot ())) d)
267-
else
268-
let {value;infl;_} = get_global_ref g in
269-
if G.leq d value then
270-
if GM.mem tau_out g then ()
271-
else (
272-
GM.add tau_out g value;
273-
LS.iter add_work infl
274-
)
275-
else (
276-
Logs.error "Fixpoint not reached for global %a\n Side from %a is %a \n Solver Computed %a\n Diff is %a" System.GVar.pretty_trace g System.LVar.pretty_trace x G.pretty d G.pretty value G.pretty_diff (d,value);
277-
AnalysisState.verified := Some false;
278-
if GM.mem tau_out g then ()
279-
else (
280-
GM.add tau_out g value;
281-
LS.iter add_work infl
282-
)
283-
) in
284-
285-
let rec doit () =
286-
match rem_work () with
287-
| None -> (LM.to_seq sigma_out, GM.to_seq tau_out)
288-
| Some x -> (match System.system x with
289-
| None -> doit ()
290-
| Some f -> (
291-
f (get_local x)
292-
get_local check_local
293-
get_global (check_global x);
294-
doit ()
295-
)
296-
) in
297-
298-
List.iter (fun (x,_) -> let value = get_local x in LM.add sigma_out x value) localinit;
299-
List.iter (fun (g, _) -> let value = get_global g in GM.add tau_out g value) globalinit;
300-
List.iter add_work xs;
301-
doit ()
302-
303-
let check localinit globalinit xs =
304-
let check_local (x,d) =
305-
if D.leq d (get_local_ref x).loc_value then ()
306-
else (
307-
Logs.error "initialization not subsumed for local %a" System.LVar.pretty_trace x;
308-
AnalysisState.verified := Some false)
309-
in
310-
let check_global (g,d) =
311-
if G.leq d (get_global_ref g).value then ()
312-
else (
313-
Logs.error "initialization not subsumed for global %a" System.GVar.pretty_trace g;
314-
AnalysisState.verified := Some false;
315-
) in
316-
317-
let _ = List.iter check_local localinit in
318-
let _ = List.iter check_global globalinit in
319-
320-
check localinit globalinit xs
68+
module Checker = FwdCommon.Checker(System)(Lcl)(Gbl)
69+
let check = Checker.check
32170
end

0 commit comments

Comments
 (0)