Skip to content

Commit 7fe1a05

Browse files
michael-schwarzmichael-schwarz
authored
Merge pull request #1751 from goblint/td_simplified_ref
Introduce solver td_simplified_ref.ml
2 parents 5f36c9b + a1d437e commit 7fe1a05

File tree

3 files changed

+233
-0
lines changed

3 files changed

+233
-0
lines changed

‎src/solver/goblint_solver.ml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@
66

77
module Td3 = Td3
88
module Td_simplified = Td_simplified
9+
module Td_simplified_ref = Td_simplified_ref
910
module TopDown = TopDown
1011
module TopDown_term = TopDown_term
1112
module TopDown_space_cache_term = TopDown_space_cache_term

‎src/solver/td_simplified_ref.ml‎

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

‎tests/regression/00-sanity/01-assert.t‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -112,6 +112,18 @@ Test topdown solvers:
112112
dead: 2
113113
total lines: 9
114114

115+
$ goblint --enable warn.deterministic --set solver td_simplified_ref 01-assert.c
116+
[Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
117+
[Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
118+
[Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
119+
[Warning][Deadcode] Function 'main' does not return
120+
[Warning][Deadcode] Function 'main' has dead code:
121+
on lines 13..14 (01-assert.c:13-14)
122+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
123+
live: 7
124+
dead: 2
125+
total lines: 9
126+
115127

116128
Test SLR solvers:
117129

0 commit comments

Comments
 (0)