Source file prog.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
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
open Utils
open Wsize
include CoreIdent
module E = Expr
type 'len gvar_i = 'len gvar L.located
type 'len ggvar = {
gv : 'len gvar_i;
gs : E.v_scope;
}
type 'len gexpr =
| Pconst of Z.t
| Pbool of bool
| Parr_init of 'len
| Pvar of 'len ggvar
| Pget of Memory_model.aligned * Warray_.arr_access * wsize * 'len ggvar * 'len gexpr
| Psub of Warray_.arr_access * wsize * 'len * 'len ggvar * 'len gexpr
| Pload of Memory_model.aligned * wsize * 'len gexpr
| Papp1 of E.sop1 * 'len gexpr
| Papp2 of E.sop2 * 'len gexpr * 'len gexpr
| PappN of E.opN * 'len gexpr list
| Pif of 'len gty * 'len gexpr * 'len gexpr * 'len gexpr
type 'len gexprs = 'len gexpr list
let kind_i v = (L.unloc v).v_kind
let ty_i v = (L.unloc v).v_ty
let is_stack_kind k =
match k with
| Stack _ -> true
| _ -> false
let is_reg_kind k =
match k with
| Reg _ -> true
| _ -> false
let reg_kind k =
match k with
| Reg (k, _) -> k
| _ -> assert false
let is_reg_direct_kind k =
match k with
| Reg (_, Direct) -> true
| _ -> false
let is_reg_ptr_kind k =
match k with
| Reg (_, Pointer _) -> true
| _ -> false
let is_stk_ptr_kind k =
match k with
| Stack (Pointer _) -> true
| _ -> false
let is_ptr k =
match k with
| Stack k | Reg(_, k) -> k <> Direct
| _ -> false
let is_regx x =
match x.v_kind with
| Reg (Extra, _) -> true
| _ -> false
type 'len glval =
| Lnone of L.t * 'len gty
| Lvar of 'len gvar_i
| Lmem of Memory_model.aligned * wsize * L.t * 'len gexpr
| Laset of Memory_model.aligned * Warray_.arr_access * wsize * 'len gvar_i * 'len gexpr
| Lasub of Warray_.arr_access * wsize * 'len * 'len gvar_i * 'len gexpr
type 'len glvals = 'len glval list
type 'len grange = E.dir * 'len gexpr * 'len gexpr
type ('len, 'info, 'asm) ginstr_r =
| Cassgn of 'len glval * E.assgn_tag * 'len gty * 'len gexpr
| Copn of 'len glvals * E.assgn_tag * 'asm Sopn.sopn * 'len gexprs
| Csyscall of 'len glvals * BinNums.positive Syscall_t.syscall_t * 'len gexprs
| Cif of 'len gexpr * ('len, 'info, 'asm) gstmt * ('len, 'info, 'asm) gstmt
| Cfor of 'len gvar_i * 'len grange * ('len, 'info, 'asm) gstmt
| Cwhile of E.align * ('len, 'info, 'asm) gstmt * 'len gexpr * (IInfo.t * 'info) * ('len, 'info, 'asm) gstmt
| Ccall of 'len glvals * funname * 'len gexprs
and ('len,'info,'asm) ginstr = {
i_desc : ('len, 'info, 'asm) ginstr_r;
i_loc : L.i_loc;
i_info : 'info;
i_annot : Annotations.annotations;
}
and ('len, 'info, 'asm) gstmt = ('len, 'info, 'asm) ginstr list
type ('len, 'info, 'asm) gfunc = {
f_loc : L.t;
f_annot: FInfo.f_annot;
f_info : 'info;
f_cc : FInfo.call_conv;
f_name : funname;
f_tyin : 'len gty list;
f_args : 'len gvar list;
f_body : ('len, 'info, 'asm) gstmt;
f_tyout : 'len gty list;
f_ret_info : FInfo.return_info;
f_ret : 'len gvar_i list
}
type 'len ggexpr =
| GEword of 'len gexpr
| GEarray of 'len gexprs
type ('len, 'info, 'asm) gmod_item =
| MIfun of ('len, 'info, 'asm) gfunc
| MIparam of ('len gvar * 'len gexpr)
| MIglobal of ('len gvar * 'len ggexpr)
type ('len, 'info, 'asm) gprog = ('len, 'info, 'asm) gmod_item list
let gkglob x = { gv = x; gs = E.Sglob}
let gkvar x = { gv = x; gs = E.Slocal}
let is_gkvar x = x.gs = E.Slocal
type pty = pexpr_ gty
and pvar = pexpr_ gvar
and pvar_i = pexpr_ gvar_i
and plval = pexpr_ glval
and plvals = pexpr_ glvals
and pexpr = pexpr_ gexpr
and pexpr_ = PE of pexpr [@@unboxed]
type range = int grange
type epty = pexpr_ gety
type ('info, 'asm) pinstr_r = (pexpr_, 'info, 'asm) ginstr_r
type ('info, 'asm) pinstr = (pexpr_, 'info, 'asm) ginstr
type ('info, 'asm) pstmt = (pexpr_, 'info, 'asm) gstmt
type ('info, 'asm) pfunc = (pexpr_, 'info, 'asm) gfunc
type ('info, 'asm) pmod_item = (pexpr_, 'info, 'asm) gmod_item
type ('info, 'asm) pprog = (pexpr_, 'info, 'asm) gprog
module PV = struct
type t = pvar
include GV
let gequal x1 x2 = equal (L.unloc x1.gv) (L.unloc x2.gv) && (x1.gs = x2.gs)
end
module Mpv : Map.S with type key = pvar = Map.Make (PV)
module Spv = Set.Make (PV)
let rec pty_equal t1 t2 =
match t1, t2 with
| Bty b1, Bty b2 -> b1 = b2
| Arr(b1, e1), Arr(b2, e2) ->
(b1 = b2) && pexpr__equal e1 e2
| _, _ -> false
and pexpr_equal e1 e2 =
match e1, e2 with
| Pconst n1, Pconst n2 -> Z.equal n1 n2
| Pbool b1, Pbool b2 -> b1 = b2
| Pvar v1, Pvar v2 -> PV.gequal v1 v2
| Pget(al1, a1,b1,v1,e1), Pget(al2, a2, b2,v2,e2) -> al1 = al2 && a1 = a2 && b1 = b2 && PV.gequal v1 v2 && pexpr_equal e1 e2
| Psub(a1,b1,l1,v1,e1), Psub(a2,b2,l2,v2,e2) ->
a1 = a2 && b1 = b2 && pexpr__equal l1 l2 && PV.gequal v1 v2 && pexpr_equal e1 e2
| Pload(al1,b1,e1), Pload(al2,b2,e2) -> al1 = al2 && b1 = b2 && pexpr_equal e1 e2
| Papp1(o1,e1), Papp1(o2,e2) -> o1 = o2 && pexpr_equal e1 e2
| Papp2(o1,e11,e12), Papp2(o2,e21,e22) -> o1 = o2 && pexpr_equal e11 e21 && pexpr_equal e12 e22
| Pif(_,e11,e12,e13), Pif(_,e21,e22,e23) -> pexpr_equal e11 e21 && pexpr_equal e12 e22 && pexpr_equal e13 e23
| _, _ -> false
and pexpr__equal (PE e1) (PE e2) = pexpr_equal e1 e2
let epty_equal t1 t2 =
match t1, t2 with
| ETbool, ETbool | ETint, ETint -> true
| ETword(s1,sz1), ETword(s2, sz2) -> s1 = s2 && sz1 = sz2
| ETarr(b1, e1) , ETarr(b2,e2) -> b1 = b1 && pexpr__equal e1 e2
| _, _ -> false
let ws_of_ety = function
| ETword(_, ws) -> ws
| _ -> assert false
type ty = int gty
type var = int gvar
type var_i = int gvar_i
type lval = int glval
type lvals = int glval list
type expr = int gexpr
type exprs = int gexpr list
type ('info, 'asm) instr = (int, 'info, 'asm) ginstr
type ('info, 'asm) instr_r = (int,'info,'asm) ginstr_r
type ('info, 'asm) stmt = (int, 'info, 'asm) gstmt
type ('info, 'asm) func = (int, 'info, 'asm) gfunc
type ('info, 'asm) mod_item = (int, 'info, 'asm) gmod_item
type global_decl = var * Global.glob_value
type ('info,'asm) prog = global_decl list * ('info, 'asm) func list
module Sv = Set.Make (V)
module Mv = Map.Make (V)
module Hv = Hash.Make (V)
let var_of_ident (x: CoreIdent.var) : var = x
let ident_of_var (x:var) : CoreIdent.var = x
let rvars_v f x s =
if is_gkvar x then f (L.unloc x.gv) s
else s
let rec rvars_e f s = function
| Pconst _ | Pbool _ | Parr_init _ -> s
| Pvar x -> rvars_v f x s
| Pget(_,_,_,x,e) | Psub (_, _, _, x, e) -> rvars_e f (rvars_v f x s) e
| Pload(_,_,e)
| Papp1(_, e) -> rvars_e f s e
| Papp2(_,e1,e2) -> rvars_e f (rvars_e f s e1) e2
| PappN (_, es) -> rvars_es f s es
| Pif(_,e,e1,e2) -> rvars_e f (rvars_e f (rvars_e f s e) e1) e2
and rvars_es f s es = List.fold_left (rvars_e f) s es
let rvars_lv f s = function
| Lnone _ -> s
| Lvar x -> f (L.unloc x) s
| Lmem (_,_,_ ,e) -> rvars_e f s e
| Laset (_,_,_,x,e)
| Lasub (_,_,_,x,e) -> rvars_e f (f (L.unloc x) s) e
let rvars_lvs f s lvs = List.fold_left (rvars_lv f) s lvs
let rec rvars_i f s i =
match i.i_desc with
| Cassgn(x, _, _, e) -> rvars_e f (rvars_lv f s x) e
| Copn(x,_,_,e) | Csyscall (x, _, e) -> rvars_es f (rvars_lvs f s x) e
| Cif(e,c1,c2) -> rvars_c f (rvars_c f (rvars_e f s e) c1) c2
| Cfor(x,(_,e1,e2), c) ->
rvars_c f (rvars_e f (rvars_e f (f (L.unloc x) s) e1) e2) c
| Cwhile(_, c, e, _, c') -> rvars_c f (rvars_e f (rvars_c f s c') e) c
| Ccall(x,_,e) -> rvars_es f (rvars_lvs f s x) e
and rvars_c f s c = List.fold_left (rvars_i f) s c
let fold_vars_ret f init fd =
List.fold_left (fun a x -> f (L.unloc x) a) init fd.f_ret
let fold_vars_fc f z fc =
let a = fold_vars_ret f z fc in
rvars_c f a fc.f_body
let vars_ret fd = fold_vars_ret Sv.add Sv.empty fd
let vars_lv z x = rvars_lv Sv.add z x
let vars_e e = rvars_e Sv.add Sv.empty e
let vars_es es = rvars_es Sv.add Sv.empty es
let vars_i i = rvars_i Sv.add Sv.empty i
let vars_c c = rvars_c Sv.add Sv.empty c
let pvars_c c = rvars_c Spv.add Spv.empty c
let params fc =
List.fold_left (fun s v -> Sv.add v s) Sv.empty fc.f_args
let vars_fc fc =
let s = params fc in
let s = List.fold_left (fun s v -> Sv.add (L.unloc v) s) s fc.f_ret in
rvars_c Sv.add s fc.f_body
let locals fc =
let s1 = params fc in
let s2 = Sv.diff (vars_fc fc) s1 in
Sv.filter V.is_local s2
let written_lv s =
function
| Lvar x
| Laset (_, _, _, x, _)
| Lasub (_, _, _, x, _)
-> Sv.add (L.unloc x) s
| _ -> s
let rec written_vars_i ((v, f) as acc) i =
match i.i_desc with
| Cassgn(x, _, _, _) -> written_lv v x, f
| Copn(xs, _, _, _) | Csyscall(xs, _, _)
-> List.fold_left written_lv v xs, f
| Ccall(xs, fn, _) ->
List.fold_left written_lv v xs, Mf.modify_def [] fn (fun old -> i.i_loc :: old) f
| Cif(_, s1, s2)
| Cwhile(_, s1, _, _, s2)
-> written_vars_stmt (written_vars_stmt acc s1) s2
| Cfor(_, _, s) -> written_vars_stmt acc s
and written_vars_stmt acc s =
List.fold_left written_vars_i acc s
let written_vars_fc fc =
written_vars_stmt (Sv.empty, Mf.empty) fc.f_body
let rec refresh_i_loc_i (i:('info, 'asm) instr) : ('info, 'asm) instr =
let i_desc =
match i.i_desc with
| Cassgn _ | Copn _ | Csyscall _ | Ccall _ -> i.i_desc
| Cif(e, c1, c2) ->
Cif(e, refresh_i_loc_c c1, refresh_i_loc_c c2)
| Cfor(x, r, c) ->
Cfor(x, r, refresh_i_loc_c c)
| Cwhile(a, c1, e, ((loc, annot), info), c2) ->
Cwhile(a, refresh_i_loc_c c1, e, ((L.refresh_i_loc loc, annot), info), refresh_i_loc_c c2)
in
{ i with i_desc; i_loc = L.refresh_i_loc i.i_loc }
and refresh_i_loc_c (c:('info, 'asm) stmt) : ('info, 'asm) stmt =
List.map refresh_i_loc_i c
let refresh_i_loc_f (f:('info, 'asm) func) : ('info, 'asm) func =
{ f with f_body = refresh_i_loc_c f.f_body }
let refresh_i_loc_p (p:('info, 'asm) prog) : ('info, 'asm) prog =
fst p, List.map refresh_i_loc_f (snd p)
let int_of_ws = Annotations.int_of_ws
let size_of_ws = function
| U8 -> 1
| U16 -> 2
| U32 -> 4
| U64 -> 8
| U128 -> 16
| U256 -> 32
let string_of_ws = Annotations.string_of_ws
let wsize_lt ws1 ws2 = Wsize.wsize_cmp ws1 ws2 = Datatypes.Lt
let wsize_le ws1 ws2 = Wsize.wsize_cmp ws1 ws2 <> Datatypes.Gt
let int_of_pe =
function
| PE1 -> 1
| PE2 -> 2
| PE4 -> 4
| PE8 -> 8
| PE16 -> 16
| PE32 -> 32
| PE64 -> 64
| PE128 -> 128
let int_of_velem ve = int_of_ws (wsize_of_velem ve)
let is_ty_arr = function
| Arr _ -> true
| _ -> false
let array_kind = function
| Arr(ws, n) -> ws, n
| _ -> assert false
let ws_of_ty = function
| Bty (U ws) -> ws
| _ -> assert false
let arr_size ws i = size_of_ws ws * i
let size_of t =
match t with
| Bty (U ws) -> size_of_ws ws
| Arr (ws', n) -> arr_size ws' n
| _ -> assert false
let is_stack_var v =
is_stack_kind v.v_kind
let is_reg_arr v =
is_reg_direct_kind v.v_kind && is_ty_arr v.v_ty
let is_stack_array x =
let x = L.unloc x in
is_ty_arr x.v_ty && x.v_kind = Stack Direct
let ( ++ ) e1 e2 =
match e1, e2 with
| Pconst n1, Pconst n2 -> Pconst (Z.add n1 n2)
| _, _ -> Papp2(E.Oadd Op_int, e1, e2)
let ( ** ) e1 e2 =
match e1, e2 with
| Pconst n1, Pconst n2 -> Pconst (Z.mul n1 n2)
| _, _ -> Papp2(E.Omul Op_int, e1, e2)
let cnst i = Pconst i
let icnst i = cnst (Z.of_int i)
let is_var = function
| Pvar _ -> true
| _ -> false
let access_offset aa ws i =
match aa with
| Warray_.AAscale -> size_of_ws ws * i
| Warray_.AAdirect -> i
let get_ofs aa ws e =
match e with
| Pconst i -> Some (access_offset aa ws (Z.to_int i))
| _ -> None
let expr_of_lval = function
| Lnone _ -> None
| Lvar x -> Some (Pvar (gkvar x))
| Lmem (al, ws, _, e) -> Some (Pload(al,ws,e))
| Laset(al, a, ws, x, e) -> Some (Pget(al, a,ws,gkvar x,e))
| Lasub(a, ws, l, x, e) -> Some (Psub(a,ws,l,gkvar x, e))
let rec has_syscall_i i =
match i.i_desc with
| Csyscall _ -> true
| Cassgn _ | Copn _ | Ccall _ -> false
| Cif (_, c1, c2) | Cwhile(_, c1, _, _, c2) -> has_syscall c1 || has_syscall c2
| Cfor (_, _, c) -> has_syscall c
and has_syscall c = List.exists has_syscall_i c
let rec has_call_or_syscall_i i =
match i.i_desc with
| Csyscall _ | Ccall _ -> true
| Cassgn _ | Copn _ -> false
| Cif (_, c1, c2) | Cwhile(_, c1, _, _, c2) -> has_call_or_syscall c1 || has_call_or_syscall c2
| Cfor (_, _, c) -> has_call_or_syscall c
and has_call_or_syscall c = List.exists has_call_or_syscall_i c
let has_annot a { i_annot; _ } = Annotations.has_symbol a i_annot
let is_inline annot cc =
Annotations.has_symbol "inline" annot || cc = FInfo.Internal
let rec spilled_i s i =
match i.i_desc with
| Copn(_, _, Sopn.Opseudo_op (Pseudo_operator.Ospill _), es) -> rvars_es Sv.add s es
| Cassgn _ | Csyscall _ | Ccall _ | Copn _-> s
| Cif(_e, c1, c2) -> spilled_c (spilled_c s c1) c2
| Cfor(_, _, c) -> spilled_c s c
| Cwhile(_, c, _, _, c') -> spilled_c (spilled_c s c) c'
and spilled_c s c = List.fold_left spilled_i s c
let spilled fc = spilled_c Sv.empty fc.f_body
let assigns = function
| Cassgn (x, _, _, _) -> written_lv Sv.empty x
| Copn (xs, _, _, _) | Csyscall (xs, _, _) | Ccall (xs, _, _) ->
List.fold_left written_lv Sv.empty xs
| Cif _ | Cwhile _ |Cfor _ -> Sv.empty
let rec iter_instr f stmt = List.iter (iter_instr_i f) stmt
and iter_instr_i f gi =
f gi;
iter_instr_ir f gi.i_desc
and iter_instr_ir f = function
| Cassgn _ | Copn _ | Csyscall _ | Ccall _ -> ()
| Cfor (_, _, c) -> iter_instr f c
| Cif (_, c1, c2) | Cwhile (_, c1, _, _, c2) ->
iter_instr f c1;
iter_instr f c2
let clamp (sz : wsize) (z : Z.t) =
Z.erem z (Z.shift_left Z.one (int_of_ws sz))
type ('info,'asm) sfundef = Expr.stk_fun_extra * ('info, 'asm) func
type ('info,'asm) sprog = ('info, 'asm) sfundef list * Expr.sprog_extra