Source file liveness.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
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
open Utils
open Prog
let dep_lv s_o x =
match x with
| Lvar x -> Sv.remove (L.unloc x) s_o
| _ -> vars_lv s_o x
let dep_lvs s_o xs =
List.fold_left dep_lv s_o xs
(** Adds to [s] variables that are used as destination or to compute a
destination (array index, memory offset) *)
let weak_dep_lv s = function
| Lnone _ -> s
| Lvar x -> Sv.add (L.unloc x) s
| Lmem(_, _, _, e) -> Sv.union (vars_e e) s
| Laset(_, _, _, x, e)
| Lasub(_, _, _, x, e) -> Sv.add (L.unloc x) (Sv.union (vars_e e) s)
let weak_dep_lvs s lvs = List.fold_left weak_dep_lv s lvs
let rec live_i weak i s_o =
let s_i, s_o, d = live_d weak i.i_desc s_o in
s_i, { i with i_desc = d; i_info = (s_i, s_o); }
and live_d weak d (s_o: Sv.t) =
match d with
| Cassgn(x, tg, ty, e) ->
let s_i = Sv.union (vars_e e) (dep_lv s_o x) in
let s_o =
if weak then weak_dep_lv s_o x
else s_o in
s_i, s_o, Cassgn(x, tg, ty, e)
| Copn(xs,t,o,es) ->
let s_i = Sv.union (vars_es es) (dep_lvs s_o xs) in
let s_o =
if weak
then weak_dep_lvs s_o xs
else s_o in
s_i, s_o, Copn(xs,t,o,es)
| Cif(e,c1,c2) ->
let s1, c1 = live_c weak c1 s_o in
let s2, c2 = live_c weak c2 s_o in
Sv.union (vars_e e) (Sv.union s1 s2), s_o, Cif(e, c1, c2)
| Cfor (x, (_dir, e1, e2 as r), c) ->
let rec loop s_o =
let s_i, c = live_c weak c s_o in
let s_i = Sv.remove (L.unloc x) s_i in
if Sv.subset s_i s_o then s_o, c
else loop (Sv.union s_i s_o) in
let s_i, c = loop s_o in
Sv.union (vars_es [ e1; e2 ]) s_i, s_o, Cfor (x, r, c)
| Cwhile(a, c, e, (info, _), c') ->
let ve = (vars_e e) in
let rec loop s_o =
let s_o' = Sv.union ve s_o in
let s_i, c = live_c weak c s_o' in
let s_i', c' = live_c weak c' s_i in
if Sv.subset s_i' s_o then s_i, (s_o', s_i'), (c, c')
else loop (Sv.union s_i' s_o) in
let s_i, se, (c,c') = loop s_o in
s_i, s_o, Cwhile(a, c, e, (info, se), c')
| Ccall(xs,f,es) ->
let s_i = Sv.union (vars_es es) (dep_lvs s_o xs) in
s_i, (if weak then weak_dep_lvs s_o xs else s_o), Ccall(xs,f,es)
| Csyscall(xs,o,es) ->
let s_i = Sv.union (vars_es es) (dep_lvs s_o xs) in
s_i, (if weak then weak_dep_lvs s_o xs else s_o), Csyscall(xs,o,es)
and live_c weak c s_o =
List.fold_right
(fun i (s_o, c) ->
let s_i, i = live_i weak i s_o in
(s_i, i :: c))
c
(s_o, [])
let live_fd weak fd =
let s_o = vars_ret fd in
let s_i, c = live_c weak fd.f_body s_o in
{ fd with f_body = c; f_info = (s_i, s_o) }
let liveness weak prog =
let fds = List.map (live_fd weak) (snd prog) in
fst prog, fds
let iter_call_sites (cbf: L.i_loc -> funname -> lvals -> Sv.t * Sv.t -> unit)
(cbs: L.i_loc -> BinNums.positive Syscall_t.syscall_t -> lvals -> Sv.t * Sv.t -> unit)
(f: (Sv.t * Sv.t, 'asm) func) : unit =
iter_instr (fun i ->
match i.i_desc with
| Ccall (xs, fn, _) -> cbf i.i_loc fn xs i.i_info
| Csyscall (xs, op, _) -> cbs i.i_loc op xs i.i_info
| (Cassgn _ | Copn _ | Cif _ | Cfor _ | Cwhile _) -> ()
) f.f_body
let pp_info fmt (s1, s2) =
Format.fprintf fmt "before: %a; after %a@ "
(pp_list " " (Printer.pp_var ~debug:true)) (Sv.elements s1)
(pp_list " " (Printer.pp_var ~debug:true)) (Sv.elements s2)
let merge_class cf s =
let add_conflict x cf =
Mv.modify_def Sv.empty x (Sv.union (Sv.remove x s)) cf
in
Sv.fold add_conflict s cf
let rec conflicts_i cf i =
let (s1, s2) = i.i_info in
let cf = merge_class cf s1 in
match i.i_desc with
| Cassgn _ | Copn _ | Csyscall _ | Ccall _ ->
merge_class cf s2
| Cfor( _, _, c) ->
conflicts_c (merge_class cf s2) c
| Cif(_, c1, c2) | Cwhile(_, c1, _, _, c2) ->
conflicts_c (conflicts_c (merge_class cf s2) c1) c2
and conflicts_c cf c =
List.fold_left conflicts_i cf c
type conflicts = Sv.t Mv.t
let conflicts f =
let ca = Sv.of_list f.f_args in
let cr = Sv.of_list (List.map L.unloc f.f_ret) in
let cf = merge_class Mv.empty ca in
let cf = merge_class cf cr in
conflicts_c cf f.f_body
type var_classes = conflicts * var Mv.t
let init_classes cf = cf, Mv.empty
let get_conflict (cf,_) x =
Mv.find_default Sv.empty x cf
let rec get_repr m x =
if Mv.mem x m then get_repr m (Mv.find x m)
else x
let normalize_repr (_c,m) =
Mv.mapi (fun x _ -> get_repr m x) m
exception SetSameConflict
let merge_class1 cf rx xc ry yc =
let add_conflict x y cf =
Mv.modify_def Sv.empty y (Sv.add x) cf
in
let cf = Sv.fold (add_conflict rx) yc cf in
let cf = Sv.fold (add_conflict ry) xc cf in
let c = Sv.union xc yc in
let cf = Mv.add rx c cf in
let cf = Mv.add ry c cf in
cf
let set_same (cf, m as cfm) x y =
let rx = get_repr m x in
let ry = get_repr m y in
if V.equal rx ry then cfm
else
let xc = Mv.find_default Sv.empty rx cf in
let yc = Mv.find_default Sv.empty ry cf in
if Sv.mem rx yc then
begin
raise SetSameConflict
end;
merge_class1 cf rx xc ry yc, Mv.add rx ry m
let var_classes_merge cfm1 (_cf2, m2) =
Mv.fold (fun x _ cfm ->
let r = get_repr m2 x in
set_same cfm x r
) m2 cfm1
let var_classes_incl (_cf1, m1) (_cf2, m2) =
Mv.for_all (fun x y ->
V.equal (get_repr m2 x) (get_repr m2 y)
) m1