source: Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml @ 740

Last change on this file since 740 was 740, checked in by ayache, 9 years ago

New memory model and bug fixes in 8051 branch. Added primitive operations in interpreters from Clight to LIN.

File size: 23.1 KB
Line 
1
2(** This module provides a translation of [RTLabs] programs to [RTL]
3    programs. *)
4
5
6let error_prefix = "RTLabs to RTL"
7let error = Error.global_error error_prefix
8
9let error_int () = error "int16 and int32 not supported."
10let error_float () = error "float not supported."
11let error_shift () = error "Shift operations not supported."
12
13let add_graph lbl stmt def =
14  { def with RTL.f_graph = Label.Map.add lbl stmt def.RTL.f_graph }
15
16let fresh_label def = Label.Gen.fresh def.RTL.f_luniverse
17
18let fresh_reg def =
19  let r = Register.fresh def.RTL.f_runiverse in
20  let locals = Register.Set.add r def.RTL.f_locals in
21  ({ def with RTL.f_locals = locals }, r)
22
23let rec fresh_regs def n =
24  if n = 0 then (def, [])
25  else
26    let (def, res) = fresh_regs def (n-1) in
27    let (def, r) = fresh_reg def in
28    (def, r :: res)
29
30let addr_regs regs = match regs with
31  | r1 :: r2 :: _ -> (r1, r2)
32  | _ -> error "Function pointer is not an address."
33
34
35(* Local environments associate one (in case of an integer) or two (in case of a
36   pointer) RTL pseudo-registers to one RTLabs pseudo-register. *)
37
38type reg_type =
39  | Int of Register.t
40  | Ptr of Register.t * Register.t
41
42type local_env = reg_type Register.Map.t
43
44let initialize_local_env runiverse ptrs registers =
45  let f lenv r =
46    let rt =
47      if List.mem r ptrs then Ptr (r, Register.fresh runiverse)
48      else Int r in
49    Register.Map.add r rt lenv in
50  List.fold_left f Register.Map.empty registers
51
52let filter_and_to_list_local_env lenv registers =
53  let f l r =
54    l @ (match Register.Map.find r lenv with
55      | Int r -> [r]
56      | Ptr (r1, r2) -> [r1 ; r2]) in
57  List.fold_left f [] registers
58
59let list_of_reg_type = function
60  | Int r -> [r]
61  | Ptr (r1, r2) -> [r1 ; r2]
62
63let find_and_list r lenv = list_of_reg_type (Register.Map.find r lenv)
64
65let find_and_list_args args lenv =
66  List.map (fun r -> find_and_list r lenv) args
67
68let find_and_addr r lenv = match find_and_list r lenv with
69  | r1 :: r2 :: _ -> (r1, r2)
70  | _ -> assert false (* do not use on these arguments *)
71
72let rtl_args regs_list lenv = List.flatten (find_and_list_args regs_list lenv)
73   
74
75
76let change_label lbl = function
77  | RTL.St_skip _ -> RTL.St_skip lbl
78  | RTL.St_cost (cost_lbl, _) -> RTL.St_cost (cost_lbl, lbl)
79  | RTL.St_addr (r1, r2, id, _) -> RTL.St_addr (r1, r2, id, lbl)
80  | RTL.St_stackaddr (r1, r2, _) -> RTL.St_stackaddr (r1, r2, lbl)
81  | RTL.St_int (r, i, _) -> RTL.St_int (r, i, lbl)
82  | RTL.St_move (r1, r2, _) -> RTL.St_move (r1, r2, lbl)
83  | RTL.St_opaccs (opaccs, dstr, srcr1, srcr2, _) ->
84    RTL.St_opaccs (opaccs, dstr, srcr1, srcr2, lbl)
85  | RTL.St_op1 (op1, dstr, srcr, _) -> RTL.St_op1 (op1, dstr, srcr, lbl)
86  | RTL.St_op2 (op2, dstr, srcr1, srcr2, _) ->
87    RTL.St_op2 (op2, dstr, srcr1, srcr2, lbl)
88  | RTL.St_clear_carry _ -> RTL.St_clear_carry lbl
89  | RTL.St_load (dstrs, addr1, addr2, _) ->
90    RTL.St_load (dstrs, addr1, addr2, lbl)
91  | RTL.St_store (addr1, addr2, srcrs, _) ->
92    RTL.St_store (addr1, addr2, srcrs, lbl)
93  | RTL.St_call_id (f, args, retrs, _) -> RTL.St_call_id (f, args, retrs, lbl)
94  | RTL.St_call_ptr (f1, f2, args, retrs, _) ->
95    RTL.St_call_ptr (f1, f2, args, retrs, lbl)
96  | RTL.St_tailcall_id (f, args) -> RTL.St_tailcall_id (f, args)
97  | RTL.St_tailcall_ptr (f1, f2, args) -> RTL.St_tailcall_ptr (f1, f2, args)
98  | RTL.St_condacc _ as inst -> inst
99  | RTL.St_return regs -> RTL.St_return regs
100
101(* Add a list of instruction in a graph, from one label to another, by creating
102   fresh labels inbetween. *)
103
104let rec adds_graph stmt_list start_lbl dest_lbl def = match stmt_list with
105  | [] -> def
106  | [stmt] ->
107    add_graph start_lbl (change_label dest_lbl stmt) def
108  | stmt :: stmt_list ->
109    let tmp_lbl = fresh_label def in
110    let stmt = change_label tmp_lbl stmt in
111    let def = add_graph start_lbl stmt def in
112    adds_graph stmt_list tmp_lbl dest_lbl def
113
114(* Process a list of function that adds a list of instructions to a graph, from
115   one label to another, and by creating fresh labels inbetween. *)
116
117let rec add_translates translate_list start_lbl dest_lbl def =
118  match translate_list with
119    | [] -> def
120    | [trans] -> trans start_lbl dest_lbl def
121    | trans :: translate_list ->
122      let tmp_lbl = fresh_label def in
123      let def = trans start_lbl tmp_lbl def in
124      add_translates translate_list tmp_lbl dest_lbl def
125
126
127let rec translate_move destrs srcrs start_lbl dest_lbl def =
128  match destrs, srcrs with
129    | [], [] -> def
130    | [destr], [srcr] ->
131      add_graph start_lbl (RTL.St_move (destr, srcr, dest_lbl)) def
132    | destr :: destrs, srcr :: srcrs ->
133      let tmp_lbl = fresh_label def in
134      let def =
135        add_graph start_lbl (RTL.St_move (destr, srcr, tmp_lbl)) def in
136      translate_move destrs srcrs tmp_lbl dest_lbl def
137    | _ -> assert false (* wrong number of arguments *)
138
139
140let translate_cst cst destrs start_lbl dest_lbl def = match cst, destrs with
141
142  | AST.Cst_int i, [r] ->
143    add_graph start_lbl (RTL.St_int (r, i, dest_lbl)) def
144
145  | AST.Cst_addrsymbol id, [r1 ; r2] ->
146    add_graph start_lbl (RTL.St_addr (r1, r2, id, dest_lbl)) def
147
148  | AST.Cst_stackoffset off, [r1 ; r2] ->
149    let (def, tmpr) = fresh_reg def in
150    adds_graph
151      [RTL.St_stackaddr (r1, r2, start_lbl) ;
152       RTL.St_int (tmpr, off, start_lbl) ;
153       RTL.St_op2 (I8051.Add, r1, r1, tmpr, start_lbl) ;
154       RTL.St_int (tmpr, 0, start_lbl) ;
155       RTL.St_op2 (I8051.Addc, r2, r2, tmpr, start_lbl)]
156      start_lbl dest_lbl def
157
158  | AST.Cst_float _, _ ->
159    error_float ()
160
161  | _, _ -> assert false (* wrong number of arguments *)
162
163
164let translate_op1 op1 destrs srcrs start_lbl dest_lbl def =
165  match op1, destrs, srcrs with
166
167    | AST.Op_cast8unsigned, _, _ | AST.Op_cast8signed, _, _
168    | AST.Op_cast16unsigned, _, _ | AST.Op_cast16signed, _, _ ->
169      translate_move destrs srcrs start_lbl dest_lbl def
170
171    | AST.Op_negint, [destr], [srcr] ->
172      adds_graph
173        [RTL.St_op1 (I8051.Cmpl, destr, srcr, start_lbl) ;
174         RTL.St_op1 (I8051.Inc, destr, destr, start_lbl)]
175        start_lbl dest_lbl def
176
177    | AST.Op_notint, [destr], [srcr] ->
178      adds_graph
179        [RTL.St_op1 (I8051.Cmpl, destr, srcr, start_lbl)]
180        start_lbl dest_lbl def
181
182    | AST.Op_id, _, _ ->
183      translate_move destrs srcrs start_lbl dest_lbl def
184
185    | AST.Op_ptrofint, [destr1 ; destr2], [srcr] ->
186      adds_graph
187        [RTL.St_move (destr1, srcr, dest_lbl) ;
188         RTL.St_int (destr2, 0, start_lbl)]
189        start_lbl dest_lbl def
190
191    | AST.Op_intofptr, [destr], [srcr ; _] ->
192      add_graph start_lbl (RTL.St_move (destr, srcr, dest_lbl)) def
193
194    | AST.Op_notbool, [destr], [srcr] ->
195      let (def, tmpr) = fresh_reg def in
196      adds_graph
197        [RTL.St_int (tmpr, 0, start_lbl) ;
198         RTL.St_clear_carry start_lbl ;
199         RTL.St_op2 (I8051.Sub, destr, tmpr, srcr, start_lbl) ;
200         RTL.St_int (destr, 0, dest_lbl) ;
201         RTL.St_op2 (I8051.Addc, destr, destr, destr, start_lbl) ;
202         RTL.St_int (tmpr, 1, dest_lbl) ;
203         RTL.St_op2 (I8051.Xor, destr, destr, tmpr, start_lbl)]
204        start_lbl dest_lbl def
205
206    | AST.Op_negf, _, _ | AST.Op_absf, _, _ | AST.Op_singleoffloat, _, _
207    | AST.Op_intoffloat, _, _ | AST.Op_intuoffloat, _, _
208    | AST.Op_floatofint, _, _ | AST.Op_floatofintu, _, _ ->
209      error_float ()
210
211    | _ -> assert false (* wrong number of arguments *)
212
213
214let rec translate_op2 op2 destrs srcrs1 srcrs2 start_lbl dest_lbl def =
215  match op2, destrs, srcrs1, srcrs2 with
216
217    | AST.Op_add, [destr], [srcr1], [srcr2] ->
218      adds_graph
219        [RTL.St_op2 (I8051.Add, destr, srcr1, srcr2, start_lbl)]
220        start_lbl dest_lbl def
221
222    | AST.Op_sub, [destr], [srcr1], [srcr2] ->
223      adds_graph
224        [RTL.St_clear_carry start_lbl ;
225         RTL.St_op2 (I8051.Sub, destr, srcr1, srcr2, start_lbl)]
226        start_lbl dest_lbl def
227
228    | AST.Op_mul, [destr], [srcr1], [srcr2] ->
229      adds_graph
230        [RTL.St_opaccs (I8051.Mul, destr, srcr1, srcr2, start_lbl)]
231        start_lbl dest_lbl def
232
233    | AST.Op_div, _, _, _ ->
234      error "Signed division not supported."
235
236    | AST.Op_divu, [destr], [srcr1], [srcr2] ->
237      adds_graph
238        [RTL.St_opaccs (I8051.Divu, destr, srcr1, srcr2, start_lbl)]
239        start_lbl dest_lbl def
240
241    | AST.Op_modu, [destr], [srcr1], [srcr2] ->
242      adds_graph
243        [RTL.St_opaccs (I8051.Modu, destr, srcr1, srcr2, start_lbl)]
244        start_lbl dest_lbl def
245
246    | AST.Op_mod, _, _, _ ->
247      error "Signed modulo not supported."
248
249    | AST.Op_and, [destr], [srcr1], [srcr2] ->
250      adds_graph
251        [RTL.St_op2 (I8051.And, destr, srcr1, srcr2, start_lbl)]
252        start_lbl dest_lbl def
253
254    | AST.Op_or, [destr], [srcr1], [srcr2] ->
255      adds_graph
256        [RTL.St_op2 (I8051.Or, destr, srcr1, srcr2, start_lbl)]
257        start_lbl dest_lbl def
258
259    | AST.Op_xor, [destr], [srcr1], [srcr2] ->
260      adds_graph
261        [RTL.St_op2 (I8051.Xor, destr, srcr1, srcr2, start_lbl)]
262        start_lbl dest_lbl def
263
264    | AST.Op_shru, _, _, _ | AST.Op_shr, _, _, _ | AST.Op_shl, _, _, _ ->
265      error_shift ()
266
267    | AST.Op_addf, _, _, _ | AST.Op_subf, _, _, _ | AST.Op_mulf, _, _, _
268    | AST.Op_divf, _, _, _ | AST.Op_cmpf _, _, _, _ ->
269      error_float ()
270
271    | AST.Op_addp, [destr1 ; destr2], [srcr11 ; srcr12], [srcr2]
272    | AST.Op_addp, [destr1 ; destr2], [srcr2], [srcr11 ; srcr12] ->
273      let (def, tmpr1) = fresh_reg def in
274      let (def, tmpr2) = fresh_reg def in
275      adds_graph
276        [RTL.St_op2 (I8051.Add, tmpr1, srcr11, srcr2, start_lbl) ;
277         RTL.St_int (tmpr2, 0, start_lbl) ;
278         RTL.St_op2 (I8051.Addc, destr2, tmpr2, srcr12, start_lbl) ;
279         RTL.St_move (destr1, tmpr1, start_lbl)]
280        start_lbl dest_lbl def
281
282    | AST.Op_subp, [destr], [srcr1 ; _], [srcr2 ; _] ->
283      let (def, tmpr1) = fresh_reg def in
284      let (def, tmpr2) = fresh_reg def in
285      adds_graph
286        [RTL.St_op1 (I8051.Cmpl, tmpr1, srcr2, start_lbl) ;
287         RTL.St_int (tmpr2, 1, start_lbl) ;
288         RTL.St_op2 (I8051.Add, tmpr1, tmpr1, tmpr2, start_lbl) ;
289         RTL.St_op2 (I8051.Add, destr, srcr1, tmpr1, start_lbl)]
290        start_lbl dest_lbl def
291
292    | AST.Op_subp, [destr1 ; destr2], [srcr11 ; srcr12], [srcr2] ->
293      adds_graph
294        [RTL.St_clear_carry start_lbl ;
295         RTL.St_op2 (I8051.Sub, destr1, srcr11, srcr2, start_lbl) ;
296         RTL.St_int (destr2, 0, start_lbl) ;
297         RTL.St_op2 (I8051.Sub, destr2, srcr12, destr2, start_lbl)]
298        start_lbl dest_lbl def
299
300    | AST.Op_cmp AST.Cmp_eq, _, _, _
301    | AST.Op_cmpu AST.Cmp_eq, _, _, _ ->
302      add_translates
303        [translate_op2 AST.Op_sub destrs srcrs1 srcrs2 ;
304         translate_op1 AST.Op_notbool destrs destrs]
305        start_lbl dest_lbl def
306
307    | AST.Op_cmp AST.Cmp_ne, _, _, _
308    | AST.Op_cmpu AST.Cmp_ne, _, _, _ ->
309      translate_op2 AST.Op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
310
311    | AST.Op_cmpu AST.Cmp_lt, [destr], [srcr1], [srcr2] ->
312      let (def, tmpr) = fresh_reg def in
313      adds_graph
314        [RTL.St_clear_carry start_lbl ;
315         RTL.St_op2 (I8051.Sub, destr, srcr1, srcr2, start_lbl) ;
316         RTL.St_int (destr, 0, start_lbl) ;
317         RTL.St_op2 (I8051.Addc, destr, destr, destr, start_lbl)]
318        start_lbl dest_lbl def
319
320    | AST.Op_cmpu AST.Cmp_gt, _, _, _ ->
321      translate_op2 (AST.Op_cmpu AST.Cmp_lt)
322        destrs srcrs2 srcrs1 start_lbl dest_lbl def
323
324    | AST.Op_cmpu AST.Cmp_le, _, _, _ ->
325      add_translates
326        [translate_op2 (AST.Op_cmpu AST.Cmp_gt) destrs srcrs1 srcrs2 ;
327         translate_op1 AST.Op_notbool destrs destrs]
328        start_lbl dest_lbl def
329
330    | AST.Op_cmpu AST.Cmp_ge, _, _, _ ->
331      add_translates
332        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs1 srcrs2 ;
333         translate_op1 AST.Op_notbool destrs destrs]
334        start_lbl dest_lbl def
335
336    | AST.Op_cmp cmp, _, _, _ ->
337      let (def, tmprs1) = fresh_regs def (List.length srcrs1) in
338      let (def, tmprs2) = fresh_regs def (List.length srcrs2) in
339      add_translates
340        [translate_cst (AST.Cst_int 128) tmprs1 ;
341         translate_cst (AST.Cst_int 128) tmprs2 ;
342         translate_op2 AST.Op_add tmprs1 srcrs1 tmprs1 ;
343         translate_op2 AST.Op_add tmprs2 srcrs2 tmprs2 ;
344         translate_op2 (AST.Op_cmpu cmp) destrs tmprs1 tmprs2] 
345        start_lbl dest_lbl def
346
347    | AST.Op_cmpp AST.Cmp_eq, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] ->
348      let (def, tmpr) = fresh_reg def in
349      add_translates
350        [translate_op2 (AST.Op_cmpu AST.Cmp_ne) [tmpr] [srcr11] [srcr21] ;
351         translate_op2 (AST.Op_cmpu AST.Cmp_ne) [destr] [srcr21] [srcr22] ;
352         translate_op2 AST.Op_or [destr] [destr] [tmpr] ;
353         adds_graph [RTL.St_int (tmpr, 1, start_lbl)] ;
354         translate_op2 AST.Op_xor [destr] [destr] [tmpr]]
355        start_lbl dest_lbl def
356
357    | AST.Op_cmpp AST.Cmp_lt, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] ->
358      let (def, tmpr1) = fresh_reg def in
359      let (def, tmpr2) = fresh_reg def in
360      add_translates
361        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) [tmpr1] [srcr12] [srcr22] ;
362         translate_op2 (AST.Op_cmpu AST.Cmp_eq) [tmpr2] [srcr12] [srcr22] ;
363         translate_op2 (AST.Op_cmpu AST.Cmp_lt) [destr] [srcr11] [srcr21] ;
364         translate_op2 AST.Op_and [tmpr2] [tmpr2] [destr] ;
365         translate_op2 AST.Op_or [destr] [tmpr1] [tmpr2]]
366        start_lbl dest_lbl def
367
368    | AST.Op_cmpp AST.Cmp_gt, _, _, _ ->
369      translate_op2 (AST.Op_cmpp AST.Cmp_lt)
370        destrs srcrs2 srcrs1 start_lbl dest_lbl def
371
372    | AST.Op_cmpp AST.Cmp_le, _, _, _ ->
373      add_translates
374        [translate_op2 (AST.Op_cmpp AST.Cmp_gt) destrs srcrs1 srcrs2 ;
375         translate_op1 AST.Op_notbool destrs destrs]
376        start_lbl dest_lbl def
377
378    | AST.Op_cmpp AST.Cmp_ge, _, _, _ ->
379      add_translates
380        [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
381         translate_op1 AST.Op_notbool destrs destrs]
382        start_lbl dest_lbl def
383
384    | _ -> assert false (* wrong number of arguments *)
385
386
387let translate_condptr r1 r2 start_lbl lbl_true lbl_false def =
388  let (def, tmpr) = fresh_reg def in
389  adds_graph
390    [RTL.St_op2 (I8051.Or, tmpr, r1, r2, start_lbl) ;
391     RTL.St_condacc (tmpr, lbl_true, lbl_false)]
392    start_lbl start_lbl def
393
394
395let translate_condcst cst start_lbl lbl_true lbl_false def = match cst with
396
397  | AST.Cst_int i ->
398    let (def, tmpr) = fresh_reg def in
399    adds_graph
400      [RTL.St_int (tmpr, i, start_lbl) ;
401       RTL.St_condacc (tmpr, lbl_true, lbl_false)]
402      start_lbl start_lbl def
403
404  | AST.Cst_addrsymbol x ->
405    let (def, r1) = fresh_reg def in
406    let (def, r2) = fresh_reg def in
407    let lbl = fresh_label def in
408    let def = add_graph start_lbl (RTL.St_addr (r1, r2, x, lbl)) def in
409    translate_condptr r1 r2 lbl lbl_true lbl_false def
410
411  | AST.Cst_stackoffset off ->
412    let (def, r1) = fresh_reg def in
413    let (def, r2) = fresh_reg def in
414    let tmp_lbl = fresh_label def in
415    let def =
416      translate_cst (AST.Cst_stackoffset off) [r1 ; r2] start_lbl tmp_lbl def in
417    translate_condptr r1 r2 tmp_lbl lbl_true lbl_false def
418
419  | AST.Cst_float _ ->
420    error_float ()
421
422
423let size_of_op1_ret = function
424  | AST.Op_cast8unsigned
425  | AST.Op_cast8signed
426  | AST.Op_cast16unsigned
427  | AST.Op_cast16signed
428  | AST.Op_negint
429  | AST.Op_notbool
430  | AST.Op_notint
431  | AST.Op_intofptr -> 1
432  | AST.Op_ptrofint -> 2
433  | AST.Op_id -> raise (Invalid_argument "RTLabsToRTL.size_of_op1_ret")
434  | AST.Op_negf
435  | AST.Op_absf
436  | AST.Op_singleoffloat
437  | AST.Op_intoffloat
438  | AST.Op_intuoffloat
439  | AST.Op_floatofint
440  | AST.Op_floatofintu -> error_float ()
441
442let rec translate_cond1 op1 srcrs start_lbl lbl_true lbl_false def =
443  match op1, srcrs with
444
445    | AST.Op_id, [srcr] ->
446      adds_graph
447        [RTL.St_condacc (srcr, lbl_true, lbl_false)]
448        start_lbl start_lbl def
449
450    | AST.Op_id, [srcr1 ; srcr2] ->
451      translate_condptr srcr1 srcr2 start_lbl lbl_true lbl_false def
452
453    | AST.Op_id, _ -> assert false (* wrong number of arguments *)
454
455    | _, srcrs ->
456      let (def, destrs) = fresh_regs def (size_of_op1_ret op1) in
457      let lbl = fresh_label def in
458      let def = translate_op1 op1 destrs srcrs start_lbl lbl def in
459      translate_cond1 AST.Op_id destrs lbl lbl_true lbl_false def
460
461
462let size_of_op2_ret n = function
463  | AST.Op_add
464  | AST.Op_sub
465  | AST.Op_mul
466  | AST.Op_div
467  | AST.Op_divu
468  | AST.Op_mod
469  | AST.Op_modu
470  | AST.Op_and
471  | AST.Op_or
472  | AST.Op_xor
473  | AST.Op_shl
474  | AST.Op_shr
475  | AST.Op_shru
476  | AST.Op_cmp _
477  | AST.Op_cmpu _
478  | AST.Op_cmpp _ -> 1
479  | AST.Op_addp -> 2
480  | AST.Op_subp ->
481    if n = 4 (* sub between two pointers, result is an integer *) then 1
482    else (* sub between a pointer and an integer, result is a pointer *) 2
483  | AST.Op_addf
484  | AST.Op_subf
485  | AST.Op_mulf
486  | AST.Op_divf
487  | AST.Op_cmpf _ -> error_float ()
488
489let translate_cond2 op2 srcrs1 srcrs2 start_lbl lbl_true lbl_false def =
490  match op2, srcrs1, srcrs2 with
491
492    | AST.Op_cmp AST.Cmp_eq, [srcr1], [srcr2] ->
493      let (def, tmpr) = fresh_reg def in
494      adds_graph
495        [RTL.St_clear_carry start_lbl ;
496         RTL.St_op2 (I8051.Sub, tmpr, srcr1, srcr2, start_lbl) ;
497         RTL.St_condacc (tmpr, lbl_false, lbl_true)]
498        start_lbl start_lbl def
499
500    | _, _, _ ->
501      let n = (List.length srcrs1) + (List.length srcrs2) in
502      let (def, destrs) = fresh_regs def (size_of_op2_ret n op2) in
503      let lbl = fresh_label def in
504      let def = translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def in
505      translate_cond1 AST.Op_id destrs lbl lbl_true lbl_false def
506
507
508let rec addressing_pointer mode args destr1 destr2 start_lbl dest_lbl def =
509  let destrs = [destr1 ; destr2] in
510  match mode, args with
511
512    | RTLabs.Aindexed off, [[srcr1 ; srcr2]] ->
513      let (def, tmpr) = fresh_reg def in
514      add_translates
515        [adds_graph [RTL.St_int (tmpr, off, start_lbl)] ;
516         translate_op2 AST.Op_addp destrs [srcr1 ; srcr2] [tmpr]]
517        start_lbl dest_lbl def
518
519    | RTLabs.Aindexed2, [[srcr11 ; srcr12] ; [srcr2]]
520    | RTLabs.Aindexed2, [[srcr2] ; [srcr11 ; srcr12]] ->
521      translate_op2 AST.Op_addp destrs [srcr11 ; srcr12] [srcr2]
522        start_lbl dest_lbl def
523
524    | RTLabs.Aglobal (x, off), _ ->
525      let (def, tmpr) = fresh_reg def in
526      add_translates
527        [adds_graph [RTL.St_int (tmpr, off, start_lbl) ;
528                     RTL.St_addr (destr1, destr2, x, start_lbl)] ;
529         translate_op2 AST.Op_addp destrs destrs [tmpr]]
530        start_lbl dest_lbl def
531
532    | RTLabs.Abased (x, off), [srcrs] ->
533      let (def, tmpr1) = fresh_reg def in
534      let (def, tmpr2) = fresh_reg def in
535      add_translates
536        [addressing_pointer (RTLabs.Aglobal (x, off)) [] tmpr1 tmpr2 ;
537         translate_op2 AST.Op_addp destrs [tmpr1 ; tmpr2] srcrs]
538        start_lbl dest_lbl def
539
540    | RTLabs.Ainstack off, _ ->
541      let (def, tmpr) = fresh_reg def in
542      add_translates
543        [adds_graph [RTL.St_int (tmpr, off, start_lbl) ;
544                     RTL.St_stackaddr (destr1, destr2, start_lbl)] ;
545         translate_op2 AST.Op_addp destrs destrs [tmpr]]
546        start_lbl dest_lbl def
547
548    | _ -> assert false (* wrong number of arguments *)
549
550
551let translate_load q mode args destrs start_lbl dest_lbl def =
552  match q, destrs with
553
554    | Memory.QInt 1, [destr] ->
555      let (def, addr1) = fresh_reg def in
556      let (def, addr2) = fresh_reg def in
557      add_translates
558        [addressing_pointer mode args addr1 addr2 ;
559         adds_graph [RTL.St_load (destr, addr1, addr2, start_lbl)]]
560        start_lbl dest_lbl def
561
562    | Memory.QPtr, [destr1 ; destr2] ->
563      let (def, addr1) = fresh_reg def in
564      let (def, addr2) = fresh_reg def in
565      let addr = [addr1 ; addr2] in
566      let (def, tmpr) = fresh_reg def in
567      add_translates
568        [addressing_pointer mode args addr1 addr2 ;
569         adds_graph [RTL.St_load (destr1, addr1, addr2, start_lbl) ;
570                     RTL.St_int (tmpr, 1, start_lbl)] ;
571         translate_op2 AST.Op_addp addr addr [tmpr] ;
572         adds_graph [RTL.St_load (destr2, addr1, addr2, start_lbl)]]
573        start_lbl dest_lbl def
574
575    | _ -> error "Size error in load."
576
577
578let translate_store q mode args srcrs start_lbl dest_lbl def =
579  match q, srcrs with
580
581    | Memory.QInt 1, [srcr] ->
582      let (def, addr1) = fresh_reg def in
583      let (def, addr2) = fresh_reg def in
584      add_translates
585        [addressing_pointer mode args addr1 addr2 ;
586         adds_graph [RTL.St_store (addr1, addr2, srcr, dest_lbl)]]
587        start_lbl dest_lbl def
588
589    | Memory.QPtr, [srcr1 ; srcr2] ->
590      let (def, addr1) = fresh_reg def in
591      let (def, addr2) = fresh_reg def in
592      let addr = [addr1 ; addr2] in
593      let (def, tmpr) = fresh_reg def in
594      add_translates
595        [addressing_pointer mode args addr1 addr2 ;
596         adds_graph [RTL.St_store (addr1, addr2, srcr1, start_lbl) ;
597                     RTL.St_int (tmpr, 1, start_lbl)] ;
598         translate_op2 AST.Op_addp addr addr [tmpr] ;
599         adds_graph [RTL.St_store (addr1, addr2, srcr2, dest_lbl)]]
600        start_lbl dest_lbl def
601
602    | _ -> error "Size error in store."
603
604
605let translate_stmt lenv lbl stmt def = match stmt with
606
607  | RTLabs.St_skip lbl' ->
608    add_graph lbl (RTL.St_skip lbl') def
609
610  | RTLabs.St_cost (cost_lbl, lbl') ->
611    add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def
612
613  | RTLabs.St_cst (destr, cst, lbl') ->
614    translate_cst cst (find_and_list destr lenv) lbl lbl' def
615
616  | RTLabs.St_op1 (op1, destr, srcr, lbl') ->
617    translate_op1 op1 (find_and_list destr lenv) (find_and_list srcr lenv)
618      lbl lbl' def
619
620  | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') ->
621    translate_op2 op2 (find_and_list destr lenv)
622      (find_and_list srcr1 lenv) (find_and_list srcr2 lenv) lbl lbl' def
623
624  | RTLabs.St_load (q, mode, args, destr, lbl') ->
625    translate_load q mode (find_and_list_args args lenv)
626      (find_and_list destr lenv) lbl lbl' def
627
628  | RTLabs.St_store (q, mode, args, srcr, lbl') ->
629    translate_store q mode (find_and_list_args args lenv)
630      (find_and_list srcr lenv) lbl lbl' def
631
632  | RTLabs.St_call_id (f, args, retr, _, lbl') ->
633    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv,
634                                   find_and_list retr lenv, lbl')) def
635
636  | RTLabs.St_call_ptr (f, args, retr, _, lbl') ->
637    let (f1, f2) = find_and_addr f lenv in
638    add_graph lbl
639      (RTL.St_call_ptr
640         (f1, f2, rtl_args args lenv, find_and_list retr lenv, lbl')) def
641
642  | RTLabs.St_tailcall_id (f, args, _) ->
643    add_graph lbl (RTL.St_tailcall_id (f, rtl_args args lenv)) def
644
645  | RTLabs.St_tailcall_ptr (f, args, _) ->
646    let (f1, f2) = find_and_addr f lenv in
647    add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args lenv)) def
648
649  | RTLabs.St_condcst (cst, lbl_true, lbl_false) ->
650    translate_condcst cst lbl lbl_true lbl_false def
651
652  | RTLabs.St_cond1 (op1, srcr, lbl_true, lbl_false) ->
653    translate_cond1 op1 (find_and_list srcr lenv)
654      lbl lbl_true lbl_false def
655
656  | RTLabs.St_cond2 (op2, srcr1, srcr2, lbl_true, lbl_false) ->
657    translate_cond2 op2 (find_and_list srcr1 lenv)
658      (find_and_list srcr2 lenv) lbl lbl_true lbl_false def
659
660  | RTLabs.St_jumptable _ ->
661    error "Jump tables not supported yet."
662
663  | RTLabs.St_return r ->
664    add_graph lbl (RTL.St_return (find_and_list r lenv)) def
665
666
667let translate_internal def =
668  let runiverse = def.RTLabs.f_runiverse in
669  let lenv =
670    initialize_local_env runiverse def.RTLabs.f_ptrs
671      (def.RTLabs.f_params @ def.RTLabs.f_locals) in
672  let result = find_and_list def.RTLabs.f_result lenv in
673  let set_of_list l = List.fold_right Register.Set.add l Register.Set.empty in
674  let params = filter_and_to_list_local_env lenv def.RTLabs.f_params in
675  let locals = filter_and_to_list_local_env lenv def.RTLabs.f_locals in
676  let locals = set_of_list locals in
677  let res =
678    { RTL.f_luniverse = def.RTLabs.f_luniverse ;
679      RTL.f_runiverse = runiverse ;
680      RTL.f_sig       = def.RTLabs.f_sig ;
681      RTL.f_result    = result ;
682      RTL.f_params    = params ;
683      RTL.f_locals    = locals ;
684      RTL.f_stacksize = def.RTLabs.f_stacksize ;
685      RTL.f_graph     = Label.Map.empty ;
686      RTL.f_entry     = def.RTLabs.f_entry ;
687      RTL.f_exit      = def.RTLabs.f_exit } in
688  Label.Map.fold (translate_stmt lenv) def.RTLabs.f_graph res
689
690
691let translate_fun_def = function
692  | RTLabs.F_int def -> RTL.F_int (translate_internal def)
693  | RTLabs.F_ext def -> RTL.F_ext def
694
695
696let translate p =
697  let f (id, fun_def) = (id, translate_fun_def fun_def) in
698  { RTL.vars   = p.RTLabs.vars ;
699    RTL.functs = List.map f p.RTLabs.functs ;
700    RTL.main   = p.RTLabs.main }
Note: See TracBrowser for help on using the repository browser.