Source file topDown_deprecated.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
(** Deprecated top-down solver ([topdown_deprecated]). *)
open Batteries
open Goblint_constraint.ConstrSys
open Messages
(** modified SLR3 as top down solver *)
module TD3 =
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)
module P =
struct
type t = S.Var.t * S.Var.t [@@deriving eq, hash]
end
module HPM = Hashtbl.Make (P)
let solve st vs =
let wpoint = HM.create 10 in
let stable = HM.create 10 in
let infl = HM.create 10 in
let set = HM.create 10 in
let sidevs = HM.create 10 in
let called = HM.create 10 in
let rho = HM.create 10 in
let rho' = HPM.create 10 in
let add_infl y x = HM.replace infl y (VS.add x (try HM.find infl y with Not_found -> VS.empty)) in
let add_set x y d = HM.replace set y (VS.add x (try HM.find set y with Not_found -> VS.empty)); HPM.add rho' (x,y) d; HM.add sidevs y () in
let is_side x = HM.mem set x in
let make_wpoint x =
if tracing then trace "sol2" "make_wpoint %a" S.Var.pretty_trace x;
HM.replace wpoint x ()
in
let rec destabilize x =
if tracing then trace "sol2" "destabilize %a" S.Var.pretty_trace x;
let t = HM.find_default infl x VS.empty in
HM.replace infl x VS.empty;
VS.iter (fun y -> HM.remove stable y; if not (HM.mem called y) then destabilize y) t
and solve x =
if tracing then trace "sol2" "solve %a, called: %b, stable: %b" S.Var.pretty_trace x (HM.mem called x) (HM.mem stable x);
if not (HM.mem called x || HM.mem stable x) then begin
HM.replace called x ();
let wpx = HM.mem wpoint x in
HM.remove wpoint x;
HM.replace stable x ();
let old = HM.find rho x in
let tmp = eq x (eval x) (side x) in
let tmp = S.Dom.join tmp (sides x) in
if tracing then trace "sol" "Var: %a" S.Var.pretty_trace x ;
if tracing then trace "sol" "Contrib:%a" S.Dom.pretty tmp;
let tmp = if is_side x then S.Dom.widen old (S.Dom.join old tmp) else if wpx then box old tmp else tmp in
HM.remove called x;
if not (S.Dom.equal old tmp) then begin
update_var_event x old tmp;
if tracing then trace "sol" "New Value:%a" S.Dom.pretty tmp;
if tracing then trace "sol2" "new value for %a (wpx: %b, is_side: %b) is %a. Old value was %a" S.Var.pretty_trace x wpx (is_side x) S.Dom.pretty tmp S.Dom.pretty old;
HM.replace rho x tmp;
destabilize x;
(solve[@tailcall]) x;
end;
end;
and eq x get set =
if tracing then trace "sol2" "eq %a" S.Var.pretty_trace x;
eval_rhs_event x;
match S.system x with
| None -> S.Dom.bot ()
| Some f ->
let effects = ref Set.empty in
let sidef y d =
if not (Set.mem y !effects) then (
HPM.replace rho' (x,y) (S.Dom.bot ());
effects := Set.add y !effects
);
set y d
in
f get sidef
and eval x y =
if tracing then trace "sol2" "eval %a ## %a" S.Var.pretty_trace x S.Var.pretty_trace y;
get_var_event y;
if not (HM.mem rho y) then init y;
if HM.mem called y then make_wpoint y else if neg is_side y then solve y;
add_infl y x;
HM.find rho y
and sides x =
let w = try HM.find set x with Not_found -> VS.empty in
let d = VS.fold (fun z d -> try S.Dom.join d (HPM.find rho' (z,x)) with Not_found -> d) w (S.Dom.bot ()) in
if tracing then trace "sol2" "sides %a ## %a" S.Var.pretty_trace x S.Dom.pretty d;
d
and side x y d =
if S.Dom.is_bot d then () else
if tracing then trace "sol2" "side %a ## %a (wpx: %b) ## %a" S.Var.pretty_trace x S.Var.pretty_trace y (HM.mem wpoint y) S.Dom.pretty d;
if not (HM.mem rho y) then begin
init y;
add_set x y d;
solve y
end else begin
let old = HPM.find rho' (x,y) in
if not (S.Dom.equal old d) then begin
add_set x y (S.Dom.join old d);
HM.remove stable y;
HM.replace sidevs y ();
end
end
and init x =
if tracing then trace "sol2" "init %a" S.Var.pretty_trace x;
if not (HM.mem rho x) then begin
new_var_event x;
HM.replace rho x (S.Dom.bot ());
HM.replace infl x (VS.add x VS.empty)
end
in
let set_start (x,d) =
if tracing then trace "sol2" "set_start %a ## %a" S.Var.pretty_trace x S.Dom.pretty d;
init x;
add_set x x d;
solve x
in
start_event ();
List.iter set_start st;
List.iter init vs;
List.iter solve vs;
let get_gs () =
let vs = ref [] in
HM.iter (fun k _ -> vs := k :: !vs) sidevs;
HM.clear sidevs;
!vs
in
let rec solveg () =
let gs = get_gs () in
if gs <> [] then (
List.iter solve gs;
List.iter solve vs;
solveg ()
)
in
solveg ();
stop_event ();
HM.clear wpoint;
HM.clear stable;
HM.clear infl ;
HM.clear set ;
HPM.clear rho' ;
rho
end
let _ =
Selector.add_solver ("topdown_deprecated", (module PostSolver.DemandEqIncrSolverFromEqSolver (TD3)));