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

Last change on this file since 1568 was 1568, checked in by tranquil, 8 years ago
  • Immediates introduced (but not fully used yet in RTLabs to RTL pass)
  • translation streamlined
  • BUGGY: interpretation fails in LTL, trying to fetch a function with incorrect address
File size: 33.6 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
13
14let add_graph lbl stmt def =
15  { def with RTL.f_graph = Label.Map.add lbl stmt def.RTL.f_graph }
16
17let fresh_label def = Label.Gen.fresh def.RTL.f_luniverse
18
19let fresh_reg def =
20  let r = Register.fresh def.RTL.f_runiverse in
21  let locals = Register.Set.add r def.RTL.f_locals in
22  ({ def with RTL.f_locals = locals }, r)
23
24let rec fresh_regs def n =
25  if n = 0 then (def, [])
26  else
27    let (def, res) = fresh_regs def (n-1) in
28    let (def, r) = fresh_reg def in
29    (def, r :: res)
30
31let addr_regs regs = match regs with
32  | r1 :: r2 :: _ -> (r1, r2)
33  | _ -> error "registers are not an address."
34
35let rec register_freshes runiverse n =
36  if n <= 0 then []
37  else (Register.fresh runiverse) :: (register_freshes runiverse (n-1))
38
39let choose_rest rest1 rest2 = match rest1, rest2 with
40  | [], _ -> rest2
41  | _, [] -> rest1
42  | _ -> assert false (* do not use on these arguments *)
43
44let complete_regs def srcrs1 srcrs2 =
45  let nb_added = (List.length srcrs1) - (List.length srcrs2) in
46  let (def, added_regs) = fresh_regs def nb_added in
47  if nb_added > 0 then (srcrs1, srcrs2 @ added_regs, added_regs)
48  else (srcrs1 @ added_regs, srcrs2, added_regs)
49
50
51let size_of_sig_type = function
52  | AST.Sig_int (i, _) -> i / Driver.TargetArch.int_size
53  | AST.Sig_float _ -> error_float ()
54  | AST.Sig_offset -> Driver.TargetArch.int_size
55  | AST.Sig_ptr -> Driver.TargetArch.ptr_size
56
57let concrete_size = Driver.RTLMemory.concrete_size
58
59let concrete_offset = Driver.RTLMemory.concrete_offset
60
61
62(* Local environments *)
63
64type local_env = Register.t list Register.Map.t
65
66let mem_local_env = Register.Map.mem
67let add_local_env = Register.Map.add
68let find_local_env = Register.Map.find
69
70let initialize_local_env runiverse registers result =
71  let registers =
72    registers @ (match result with None -> [] | Some (r, t) -> [(r, t)]) in
73  let f lenv (r, t) =
74    let rs = register_freshes runiverse (size_of_sig_type t) in
75    add_local_env r rs lenv in
76  List.fold_left f Register.Map.empty registers
77
78let map_list_local_env lenv regs =
79  let f res r = res @ (find_local_env r lenv) in
80  List.fold_left f [] regs
81
82let make_addr = function
83  | r1 :: r2 :: _ -> (r1, r2)
84  | _ -> assert false (* do not use on these arguments *)
85
86let find_and_addr r lenv = make_addr (find_local_env r lenv)
87
88let rtl_args regs_list lenv =
89  List.flatten (List.map (fun r -> find_local_env r lenv) regs_list)
90
91
92let change_label lbl = function
93  | RTL.St_skip _ -> RTL.St_skip lbl
94  | RTL.St_cost (cost_lbl, _) -> RTL.St_cost (cost_lbl, lbl)
95  | RTL.St_ind_0 (i, _) -> RTL.St_ind_0 (i, lbl)
96  | RTL.St_ind_inc (i, _) -> RTL.St_ind_inc (i, lbl)
97  | RTL.St_addr (r1, r2, id, _) -> RTL.St_addr (r1, r2, id, lbl)
98  | RTL.St_stackaddr (r1, r2, _) -> RTL.St_stackaddr (r1, r2, lbl)
99  (* | RTL.St_int (r, i, _) -> RTL.St_int (r, i, lbl) *)
100  | RTL.St_move (r1, r2, _) -> RTL.St_move (r1, r2, lbl)
101  | RTL.St_opaccs (opaccs, dstr1, dstr2, srcr1, srcr2, _) ->
102    RTL.St_opaccs (opaccs, dstr1, dstr2, srcr1, srcr2, lbl)
103  | RTL.St_op1 (op1, dstr, srcr, _) -> RTL.St_op1 (op1, dstr, srcr, lbl)
104  | RTL.St_op2 (op2, dstr, srcr1, srcr2, _) ->
105    RTL.St_op2 (op2, dstr, srcr1, srcr2, lbl)
106  | RTL.St_clear_carry _ -> RTL.St_clear_carry lbl
107  | RTL.St_set_carry _ -> RTL.St_set_carry lbl
108  | RTL.St_load (dstrs, addr1, addr2, _) ->
109    RTL.St_load (dstrs, addr1, addr2, lbl)
110  | RTL.St_store (addr1, addr2, srcrs, _) ->
111    RTL.St_store (addr1, addr2, srcrs, lbl)
112  | RTL.St_call_id (f, args, retrs, _) -> RTL.St_call_id (f, args, retrs, lbl)
113  | RTL.St_call_ptr (f1, f2, args, retrs, _) ->
114    RTL.St_call_ptr (f1, f2, args, retrs, lbl)
115  | RTL.St_tailcall_id (f, args) -> RTL.St_tailcall_id (f, args)
116  | RTL.St_tailcall_ptr (f1, f2, args) -> RTL.St_tailcall_ptr (f1, f2, args)
117  | RTL.St_cond _ as inst -> inst
118  | RTL.St_return regs -> RTL.St_return regs
119
120(* Add a list of instruction in a graph, from one label to another, by creating
121   fresh labels inbetween. *)
122
123let rec adds_graph stmt_list start_lbl dest_lbl def = match stmt_list with
124  | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
125  | [stmt] ->
126    add_graph start_lbl (change_label dest_lbl stmt) def
127  | stmt :: stmt_list ->
128    let tmp_lbl = fresh_label def in
129    let stmt = change_label tmp_lbl stmt in
130    let def = add_graph start_lbl stmt def in
131    adds_graph stmt_list tmp_lbl dest_lbl def
132
133(* Process a list of function that adds a list of instructions to a graph, from
134   one label to another, and by creating fresh labels inbetween. *)
135
136let rec add_translates translate_list start_lbl dest_lbl def =
137  match translate_list with
138    | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
139    | [trans] -> trans start_lbl dest_lbl def
140    | trans :: translate_list ->
141      let tmp_lbl = fresh_label def in
142      let def = trans start_lbl tmp_lbl def in
143      add_translates translate_list tmp_lbl dest_lbl def
144
145
146(*
147
148let rec translate_op2 op2 destrs srcrs1 srcrs2 start_lbl dest_lbl def =
149  match op2, destrs, srcrs1, srcrs2 with
150
151    | AST.Op_mul (1, _), [destr], [srcr1], [srcr2] ->
152      adds_graph
153        [RTL.St_opaccs (I8051.Mul, destr, srcr1, srcr2, start_lbl)]
154        start_lbl dest_lbl def
155
156    | AST.Op_shr _, _, _, _ ->
157      error_shift ()
158
159    | AST.Op_cmp (AST.Cmp_lt, (1, AST.Unsigned)), [destr], [srcr1], [srcr2] ->
160      let (def, tmpr) = fresh_reg def in
161      adds_graph
162        [RTL.St_clear_carry start_lbl ;
163         RTL.St_op2 (I8051.Sub, destr, srcr1, srcr2, start_lbl) ;
164         RTL.St_int (destr, 0, start_lbl) ;
165         RTL.St_op2 (I8051.Addc, destr, destr, destr, start_lbl)]
166        start_lbl dest_lbl def
167
168    | AST.Op_cmp (cmp, ((size, AST.Signed) as int_type)), _, _, _ ->
169      let (def, tmprs1) = fresh_regs def (List.length srcrs1) in
170      let (def, tmprs2) = fresh_regs def (List.length srcrs2) in
171      add_translates
172        [translate_cst (AST.Cst_int 128) tmprs1 ;
173         translate_cst (AST.Cst_int 128) tmprs2 ;
174         translate_op2 (AST.Op_add int_type) tmprs1 srcrs1 tmprs1 ;
175         translate_op2 (AST.Op_add int_type) tmprs2 srcrs2 tmprs2 ;
176         translate_op2 (AST.Op_cmp (cmp, (size, AST.Unsigned)))
177           destrs tmprs1 tmprs2]
178        start_lbl dest_lbl def
179
180    | AST.Op_cmpp AST.Cmp_lt, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] ->
181      let (def, tmpr1) = fresh_reg def in
182      let (def, tmpr2) = fresh_reg def in
183      add_translates
184        [translate_op2 (AST.Op_cmp (AST.Cmp_lt, uint))
185            [tmpr1] [srcr12] [srcr22] ;
186         translate_op2 (AST.Op_cmp (AST.Cmp_eq, uint))
187            [tmpr2] [srcr12] [srcr22] ;
188         translate_op2 (AST.Op_cmp (AST.Cmp_lt, uint))
189            [destr] [srcr11] [srcr21] ;
190         translate_op2 AST.Op_and [tmpr2] [tmpr2] [destr] ;
191         translate_op2 AST.Op_or [destr] [tmpr1] [tmpr2]]
192        start_lbl dest_lbl def
193
194    | _ -> error_int ()
195*)
196
197let rec translate_cst cst destrs start_lbl dest_lbl def = match cst with
198
199  | AST.Cst_int _ when destrs = [] ->
200    add_graph start_lbl (RTL.St_skip dest_lbl) def
201
202  | AST.Cst_int i ->
203    let size = List.length destrs in
204    let module M = IntValue.Make (struct let size = size end) in
205    let is = List.map M.to_int (M.break (M.of_int i) size) in
206    let f r i = RTL.St_move (r, RTL.Imm i, dest_lbl) in
207    let l = List.map2 f destrs is in
208    adds_graph l start_lbl dest_lbl def
209
210  | AST.Cst_float _ -> error_float ()
211
212  | AST.Cst_addrsymbol id ->
213    let (r1, r2) = make_addr destrs in
214    add_graph start_lbl (RTL.St_addr (r1, r2, id, dest_lbl)) def
215
216  | AST.Cst_stack ->
217    let (r1, r2) = make_addr destrs in
218    add_graph start_lbl (RTL.St_stackaddr (r1, r2, dest_lbl)) def
219
220  | AST.Cst_offset off ->
221    let i = concrete_offset off in
222    translate_cst (AST.Cst_int i) destrs start_lbl dest_lbl def
223
224  | AST.Cst_sizeof size ->
225    let i = concrete_size size in
226    translate_cst (AST.Cst_int i) destrs start_lbl dest_lbl def
227
228
229let rec translate_move destrs srcrs start_lbl =
230  let ((common1, rest1), (common2, rest2)) = MiscPottier.reduce destrs srcrs in
231  let f_common destr srcr = RTL.St_move (destr, RTL.Reg srcr, start_lbl) in
232  let translates1 = adds_graph (List.map2 f_common common1 common2) in
233  let translates2 = translate_cst (AST.Cst_int 0) rest1 in
234  add_translates [translates1 ; translates2] start_lbl
235
236let rec translate_imm destrs vals start_lbl =
237  let ((common1, rest1), (common2, _)) = MiscPottier.reduce destrs vals in
238  let f_common destr srcr = RTL.St_move (destr, RTL.Imm srcr, start_lbl) in
239  let translates1 = adds_graph (List.map2 f_common common1 common2) in
240  let translates2 = translate_cst (AST.Cst_int 0) rest1 in
241  add_translates [translates1 ; translates2] start_lbl
242
243
244let translate_cast_unsigned destrs start_lbl dest_lbl def =
245  translate_cst (AST.Cst_int 0) destrs start_lbl dest_lbl def
246
247let translate_cast_signed destrs srcr start_lbl dest_lbl def =
248  let (def, tmpr) = fresh_reg def in
249  let insts =
250    (* this sets tmpr to 0xFF if s is neg, 0x00 o.w. Done like that:
251       byte in tmpr if srcr is: neg   |  pos
252       tmpr ← srcr | 127       11...1 | 01...1
253       tmpr ← tmpr <rot< 1     1...11 | 1...10
254       tmpr ← INC tmpr         0....0 | 1....1
255       tmpr ← CPL tmpr         1....1 | 0....0
256
257     *)
258    [RTL.St_op2 (I8051.Or, tmpr, srcr, RTL.Imm 127, start_lbl) ;
259     RTL.St_op1 (I8051.Rl, tmpr, tmpr, start_lbl) ;
260     RTL.St_op1 (I8051.Inc, tmpr, tmpr, start_lbl) ;
261     RTL.St_op1 (I8051.Cmpl, tmpr, tmpr, start_lbl) ] in
262  let srcrs = MiscPottier.make tmpr (List.length destrs) in
263  add_translates [adds_graph insts ; translate_move destrs srcrs]
264    start_lbl dest_lbl def
265
266let translate_cast src_size src_sign dest_size destrs srcrs =
267  if List.length srcrs = 0 then adds_graph []
268  else
269    if dest_size < src_size then translate_move destrs srcrs
270    else
271      let ((common1, rest1), (common2, _)) = MiscPottier.reduce destrs srcrs in
272      let insts_common = translate_move common1 common2 in
273      let sign_reg = MiscPottier.last srcrs in
274      let insts_sign = match src_sign with
275        | AST.Unsigned -> translate_cast_unsigned rest1
276        | AST.Signed -> translate_cast_signed rest1 sign_reg in
277      add_translates [insts_common ; insts_sign]
278
279
280let translate_negint destrs srcrs start_lbl dest_lbl def =
281  assert (List.length destrs = List.length srcrs && List.length destrs > 0) ;
282  let f_cmpl destr srcr = RTL.St_op1 (I8051.Cmpl, destr, srcr, start_lbl) in
283  let insts_cmpl = List.map2 f_cmpl destrs srcrs in
284  let first, rest = List.hd destrs, List.tl destrs in
285  let inst_init =
286    RTL.St_op2 (I8051.Add, first, first, RTL.Imm 0, start_lbl) in
287  let f_add destr =
288    RTL.St_op2 (I8051.Addc, destr, destr, RTL.Imm 0, start_lbl) in
289  let insts_add = List.map f_add rest in
290  adds_graph (insts_cmpl @ inst_init :: insts_add)
291    start_lbl dest_lbl def
292
293
294let translate_notbool destrs srcrs start_lbl dest_lbl def =
295  match destrs,srcrs with
296    | [], _ -> adds_graph [] start_lbl dest_lbl def
297    | destr :: destrs, srcr :: srcrs ->
298      let (def, tmpr) = fresh_reg def in
299      let init_destr = RTL.St_move (destr, RTL.Reg srcr, start_lbl) in
300      let f r =
301        RTL.St_op2 (I8051.Or, destr, destr, RTL.Reg r, start_lbl) in
302      let big_or = List.map f srcrs in
303      let finalize_destr =
304        [RTL.St_move (tmpr, RTL.Imm 0, start_lbl) ;
305         RTL.St_clear_carry start_lbl ;
306         RTL.St_op2 (I8051.Sub, tmpr, tmpr, RTL.Reg destr, start_lbl) ;
307         (* carry bit is set iff destr is non-zero iff destrs was non-zero *)
308         RTL.St_move (tmpr, RTL.Imm 0, start_lbl) ;
309         RTL.St_op2 (I8051.Addc, destr, tmpr, RTL.Reg tmpr, start_lbl) ;
310         (* destr = carry bit = bigor of old destrs *)
311         RTL.St_op2 (I8051.Xor, destr, destr, RTL.Imm 1, start_lbl)] in
312      let epilogue = translate_cst (AST.Cst_int 0) destrs in
313      add_translates [adds_graph (init_destr :: big_or @ finalize_destr) ;
314                      epilogue]
315        start_lbl dest_lbl def
316    | destr :: destrs, [] ->
317      translate_cst (AST.Cst_int 1) destrs start_lbl dest_lbl def
318
319
320let translate_op1 op1 destrs srcrs start_lbl dest_lbl def = match op1 with
321
322  | AST.Op_cast ((src_size, src_sign), dest_size) ->
323    translate_cast src_size src_sign dest_size destrs srcrs start_lbl dest_lbl
324      def
325
326  | AST.Op_negint ->
327    translate_negint destrs srcrs start_lbl dest_lbl def
328
329  | AST.Op_notbool ->
330    translate_notbool destrs srcrs start_lbl dest_lbl def
331
332  | AST.Op_notint ->
333    let f destr srcr = RTL.St_op1 (I8051.Cmpl, destr, srcr, start_lbl) in
334    let l = List.map2 f destrs srcrs in
335    adds_graph l start_lbl dest_lbl def
336
337  | AST.Op_ptrofint | AST.Op_intofptr | AST.Op_id ->
338    translate_move destrs srcrs start_lbl dest_lbl def
339
340
341let translate_op op destrs srcrs1 srcrs2 start_lbl dest_lbl def =
342  let ((srcrs1_common, srcrs1_rest), (srcrs2_common, srcrs2_rest)) =
343    MiscPottier.reduce srcrs1 srcrs2 in
344  let srcrs_rest = choose_rest srcrs1_rest srcrs2_rest in
345  let ((destrs_common, destrs_rest), _) =
346    MiscPottier.reduce destrs srcrs1_common in
347  let ((destrs_cted, destrs_rest), (srcrs_cted, _)) =
348    MiscPottier.reduce destrs_rest srcrs_rest in
349  let (def, tmpr) = fresh_reg def in
350  let carry_init = match op with
351    | I8051.Addc | I8051.Sub ->
352      (* depend on carry bit *)
353      [RTL.St_clear_carry start_lbl]
354    | I8051.Add -> assert false (* should not call with add, not correct *)
355    | _ -> [] in
356  let inst_init = RTL.St_move (tmpr, RTL.Imm 0, start_lbl) :: carry_init in
357  let f_add destr srcr1 srcr2 =
358    RTL.St_op2 (op, destr, srcr1, RTL.Reg srcr2, start_lbl) in
359  let insts_add =
360    MiscPottier.map3 f_add destrs_common srcrs1_common srcrs2_common in
361  let f_add_cted destr srcr =
362    RTL.St_op2 (op, destr, srcr, RTL.Reg tmpr, start_lbl) in
363  let insts_add_cted = List.map2 f_add_cted destrs_cted srcrs_cted in
364  let f_rest destr =
365    RTL.St_op2 (op, destr, tmpr, RTL.Reg tmpr, start_lbl) in
366  let insts_rest = List.map f_rest destrs_rest in
367  adds_graph (inst_init @ insts_add @ insts_add_cted @ insts_rest)
368    start_lbl dest_lbl def
369
370
371let rec translate_mul1 dummy tmpr destrs srcrs1 srcr2 start_lbl =
372  match destrs, srcrs1 with
373    | [], _ -> adds_graph [RTL.St_skip start_lbl] start_lbl
374    | [destr], [] ->
375      adds_graph [RTL.St_op2 (I8051.Addc, destr, destr, RTL.Imm 0, start_lbl)]
376        start_lbl
377    | destr1 :: destr2 :: destrs, [] ->
378      add_translates
379        [adds_graph
380            [RTL.St_move (tmpr, RTL.Imm 0, start_lbl) ;
381             RTL.St_op2 (I8051.Addc, destr1, destr1, RTL.Imm 0, start_lbl) ;
382             RTL.St_op2 (I8051.Addc, destr2, tmpr, RTL.Imm 0, start_lbl)] ;
383         translate_cst (AST.Cst_int 0) destrs]
384        start_lbl
385    | [destr], srcr1 :: _ ->
386      adds_graph
387        [RTL.St_opaccs (I8051.Mul, tmpr, dummy, srcr2, srcr1, start_lbl) ;
388         RTL.St_op2 (I8051.Addc, destr, destr, RTL.Reg tmpr, start_lbl)]
389        start_lbl
390    | destr1 :: destr2 :: destrs, srcr1 :: srcrs1 ->
391      add_translates
392        [adds_graph
393            [RTL.St_opaccs
394                (I8051.Mul, tmpr, destr2, srcr2, srcr1, start_lbl) ;
395             RTL.St_op2 (I8051.Addc, destr1, destr1, RTL.Reg tmpr, start_lbl)] ;
396         translate_mul1 dummy tmpr (destr2 :: destrs) srcrs1 srcr2]
397        start_lbl
398
399let translate_muli dummy tmpr destrs tmp_destrs srcrs1 dummy_lbl i translates
400    srcr2i =
401  let (tmp_destrs1, tmp_destrs2) = MiscPottier.split tmp_destrs i in
402  translates @
403    (match tmp_destrs2 with
404      | [] -> []
405      | tmp_destr2 :: tmp_destrs2 ->
406        [adds_graph [RTL.St_clear_carry dummy_lbl ;
407                     RTL.St_move (tmp_destr2, RTL.Imm 0, dummy_lbl)] ;
408         translate_mul1 dummy tmpr (tmp_destr2 :: tmp_destrs2) srcrs1 srcr2i ;
409         translate_cst (AST.Cst_int 0) tmp_destrs1 ;
410         translate_op I8051.Addc destrs destrs tmp_destrs])
411
412let translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def =
413  let (def, dummy) = fresh_reg def in
414  let (def, tmpr) = fresh_reg def in
415  let (def, tmp_destrs) = fresh_regs def (List.length destrs) in
416  let (def, fresh_srcrs1) = fresh_regs def (List.length srcrs1) in
417  let (def, fresh_srcrs2) = fresh_regs def (List.length srcrs2) in
418  let insts_init =
419    [translate_move fresh_srcrs1 srcrs1 ;
420     translate_move fresh_srcrs2 srcrs2 ;
421     translate_cst (AST.Cst_int 0) destrs] in
422  let f = translate_muli dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl in
423  let insts_mul = MiscPottier.foldi f [] srcrs2 in
424  add_translates (insts_init @ insts_mul) start_lbl dest_lbl def
425
426
427let translate_divumodu8 order destrs srcr1 srcr2 start_lbl dest_lbl def =
428  match destrs with
429    | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
430    | destr :: destrs ->
431      let (def, dummy) = fresh_reg def in
432      let (destr1, destr2) = if order then (destr, dummy) else (dummy, destr) in
433      let inst_div =
434        adds_graph [RTL.St_opaccs (I8051.DivuModu, destr1, destr2,
435                                   srcr1, srcr2, start_lbl)] in
436      let insts_rest = translate_cst (AST.Cst_int 0) destrs in
437      add_translates [inst_div ; insts_rest] start_lbl dest_lbl def
438
439let translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def =
440  match destrs with
441    | [] -> adds_graph [] start_lbl dest_lbl def
442    | destr :: destrs ->
443      let (def, tmpr) = fresh_reg def in
444      let ((common1, rest1), (common2, rest2)) =
445        MiscPottier.reduce srcrs1 srcrs2 in
446      let rest = choose_rest rest1 rest2 in
447      let firsts = match common1, common2 with
448        | c1hd :: c1tl, c2hd :: c2tl ->
449          let init =
450            RTL.St_op2 (I8051.Xor, destr, c1hd, RTL.Reg c2hd, start_lbl) in
451          let f_common tmp_srcr1 tmp_srcr2 =
452            [RTL.St_op2 (I8051.Xor, tmpr, tmp_srcr1,
453                         RTL.Reg tmp_srcr2, start_lbl) ;
454             RTL.St_op2 (I8051.Or, destr, destr, RTL.Reg tmpr, start_lbl)] in
455          let insts_common = List.flatten (List.map2 f_common c1tl c2tl) in
456          init :: insts_common
457        | [], [] ->
458          [RTL.St_move (destr, RTL.Imm 0, start_lbl)]
459        (* common1 and common2 have the same length *)
460        | _ -> assert false in
461      let f_rest tmp_srcr =
462        RTL.St_op2 (I8051.Xor, destr, destr, RTL.Reg tmp_srcr, start_lbl) in
463      let insts_rest = List.map f_rest rest in
464      let insts = firsts @ insts_rest in
465      let epilogue = translate_cst (AST.Cst_int 0) destrs in
466      add_translates [ adds_graph insts ; epilogue] start_lbl dest_lbl def
467
468(* this requires destrs to be either 0 or 1 to be truly correct
469   to be used after translations that ensure this *)
470let translate_toggle_bool destrs start_lbl =
471  match destrs with
472    | [] -> adds_graph [] start_lbl
473    | destr :: _ ->
474      adds_graph [RTL.St_op1 (I8051.Cmpl, destr, destr, start_lbl)] start_lbl
475
476
477
478(* let translate_eq_reg tmp_zero tmpr destr dummy_lbl *)
479(*     (srcr1, srcr2) = *)
480(*   [RTL.St_op2 (I8051.Xor, tmpr, srcr1, srcr2, dummy_lbl) ; *)
481(*    (\* now tmpr = 0 iff srcr1 = srcr2 *\) *)
482(*    RTL.St_clear_carry dummy_lbl ; *)
483(*    RTL.St_op2 (I8051.Sub, tmpr, tmp_zero, tmpr, dummy_lbl) ; *)
484(*    (\* now carry bit = (old tmpr is not zero) = (srcr1 != srcr2) *\) *)
485(*    RTL.St_op2 (I8051.Addc, tmpr, tmp_zero, tmp_zero, dummy_lbl) ; *)
486(*    (\* now tmpr = old carry bit = (srcr1 != srcr2) *\) *)
487(*    RTL.St_op1 (I8051.Cpl, tmpr, tmpr, dummy_lbl)] *)
488
489(* let translate_eq_list tmp_zero tmpr destr leq dummy_lbl = match leq with *)
490(*   | leqhd :: leqtl -> *)
491(*     let init = translate_eq_reg tmp_zero destr dummy_lbl leqhd in *)
492(*     let f p = translate_eq_reg tmp_zero tmpr destr dummy_lbl p @ *)
493(*       [RTL.St_op2 (I8051.And, destr, destr, tmpr1, dummy_lbl)] in *)
494(*     init @ List.flatten (List.map f leqtl) *)
495(*   | _ -> [RTL.St_move (destr, RTL.Imm 1, dummy_lbl)] *)
496
497(* let translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq *)
498(*     srcr1 srcr2 = *)
499(*   (translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl) @ *)
500(*   [RTL.St_clear_carry dummy_lbl ; *)
501(*    RTL.St_op2 (I8051.Sub, tmpr1, srcr1, srcr2, dummy_lbl) ; *)
502(*    RTL.St_op2 (I8051.Addc, tmpr1, tmp_zero, tmp_zero, dummy_lbl) ; *)
503(*    RTL.St_op2 (I8051.And, tmpr3, tmpr3, tmpr1, dummy_lbl) ; *)
504(*    RTL.St_op2 (I8051.Or, destr, destr, tmpr3, dummy_lbl)] *)
505
506(* let translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl *)
507(*     srcrs1 srcrs2 = *)
508(*   let f (insts, leq) srcr1 srcr2 = *)
509(*     let added_insts = *)
510(*       translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq *)
511(*      srcr1 srcr2 in *)
512(*     (insts @ added_insts, leq @ [(srcr1, srcr2)]) in *)
513(*   fst (List.fold_left2 f ([], []) srcrs1 srcrs2) *)
514
515(* let translate_lt destrs srcrs1 srcrs2 start_lbl dest_lbl def = *)
516(*   match destrs with *)
517(*     | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def *)
518(*     | _ -> *)
519(*       let (def, tmp_destrs) = fresh_regs def (List.length destrs) in *)
520(*       let tmp_destr = List.hd tmp_destrs in *)
521(*       let (def, tmp_zero) = fresh_reg def in *)
522(*       let (def, tmp_one) = fresh_reg def in *)
523(*       let (def, tmpr1) = fresh_reg def in *)
524(*       let (def, tmpr2) = fresh_reg def in *)
525(*       let (def, tmpr3) = fresh_reg def in *)
526(*       let (srcrs1, srcrs2, added) = complete_regs def srcrs1 srcrs2 in *)
527(*       let srcrs1 = List.rev srcrs1 in *)
528(*       let srcrs2 = List.rev srcrs2 in *)
529(*       let insts_init = *)
530(*      [translate_cst (AST.Cst_int 0) tmp_destrs ; *)
531(*       translate_cst (AST.Cst_int 0) added ; *)
532(*       adds_graph [RTL.St_int (tmp_zero, 0, start_lbl) ; *)
533(*                   RTL.St_int (tmp_one, 1, start_lbl)]] in *)
534(*       let insts_main = *)
535(*      translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl *)
536(*        srcrs1 srcrs2 in *)
537(*       let insts_main = [adds_graph insts_main] in *)
538(*       let insts_exit = [translate_move destrs tmp_destrs] in *)
539(*       add_translates (insts_init @ insts_main @ insts_exit ) *)
540(*      start_lbl dest_lbl def *)
541
542let rec pad_with p l1 l2 = match l1, l2 with
543  | [], [] -> ([], [])
544  | x :: xs, y :: ys ->
545    let (xs', ys') = pad_with p xs ys in
546    (x :: xs', y :: ys')
547  | [], _ -> (MiscPottier.make p (List.length l2), l2)
548  | _, [] -> (l1, MiscPottier.make p (List.length l1))
549
550let translate_ltu desrtrs srcrs1 srcrs2 start_lbl dest_lbl def =
551  match desrtrs with
552    | [] -> adds_graph [] start_lbl dest_lbl def
553    | destr :: destrs ->
554      let (def, tmpr_zero) = fresh_reg def in
555      let (srcrs1, srcrs2) = pad_with tmpr_zero srcrs1 srcrs2 in
556      let init =
557        [RTL.St_move (tmpr_zero, RTL.Imm 0, start_lbl) ;
558         RTL.St_clear_carry start_lbl] in
559      let f srcr1 srcr2 =
560        RTL.St_op2 (I8051.Sub, destr, srcr1, RTL.Reg srcr2, start_lbl) in
561      (* not interested in result, just the carry bit
562         the following is safe even if destrs = srcrsi *)
563      let iter_sub = List.map2 f srcrs1 srcrs2 in
564      let extract_carry =
565        [RTL.St_op2 (I8051.Addc, destr, tmpr_zero,
566                     RTL.Reg tmpr_zero, start_lbl)] in
567      let epilogue = translate_cst (AST.Cst_int 0) destrs in
568      add_translates [adds_graph (init @ iter_sub @ extract_carry);
569                      epilogue] start_lbl dest_lbl def
570
571let rec add_128_to_last
572    (tmp_128 : Register.t)
573    (last_subst : Register.t)
574    (rs : Register.t list)
575    (dummy_lbl : Label.t) = match rs with
576  | [] -> ([], adds_graph [])
577  | [last] ->
578    let insts =
579      [RTL.St_move (last_subst, RTL.Reg last, dummy_lbl) ;
580       RTL.St_op2 (I8051.Add, last_subst, last_subst,
581                   RTL.Reg tmp_128, dummy_lbl)] in
582    ([last_subst], adds_graph insts)
583  | hd :: tail ->
584    let (tail', trans) = add_128_to_last tmp_128 last_subst tail dummy_lbl in
585    (hd :: tail', trans)
586
587(* what happens if srcrs1 and srcrs2 have different length? seems to me
588   128 is added at the wrong place then *)
589let translate_lts destrs srcrs1 srcrs2 start_lbl dest_lbl def =
590  let (def, tmp_last_srcr1) = fresh_reg def in
591  let (def, tmp_last_srcr2) = fresh_reg def in
592  let (def, tmp_128) = fresh_reg def in
593  (* I save just the last registers *)
594  let (srcrs1, add_128_to_srcrs1) =
595    add_128_to_last tmp_128 tmp_last_srcr1 srcrs1 start_lbl in
596  let (srcrs2, add_128_to_srcrs2) =
597    add_128_to_last tmp_128 tmp_last_srcr2 srcrs2 start_lbl in
598  add_translates
599    [adds_graph [RTL.St_move (tmp_128, RTL.Imm 128, start_lbl)] ;
600     add_128_to_srcrs1;
601     add_128_to_srcrs2;
602     translate_ltu destrs srcrs1 srcrs2]
603    start_lbl dest_lbl def
604
605
606let translate_op2 op2 destrs srcrs1 srcrs2 start_lbl dest_lbl def =
607  match op2 with
608
609    | AST.Op_add | AST.Op_addp ->
610      translate_op I8051.Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
611
612    | AST.Op_sub | AST.Op_subp | AST.Op_subpp ->
613      translate_op I8051.Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
614
615    | AST.Op_mul ->
616      translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def
617
618    | AST.Op_divu when List.length srcrs1 = 1 && List.length srcrs2 = 1 ->
619      translate_divumodu8 true destrs (List.hd srcrs1) (List.hd srcrs2)
620        start_lbl dest_lbl def
621
622    | AST.Op_modu when List.length srcrs1 = 1 && List.length srcrs2 = 1 ->
623      translate_divumodu8 false destrs (List.hd srcrs1) (List.hd srcrs2)
624        start_lbl dest_lbl def
625
626    | AST.Op_and ->
627      translate_op I8051.And destrs srcrs1 srcrs2 start_lbl dest_lbl def
628
629    | AST.Op_or ->
630      translate_op I8051.Or destrs srcrs1 srcrs2 start_lbl dest_lbl def
631
632    | AST.Op_xor ->
633      translate_op I8051.Xor destrs srcrs1 srcrs2 start_lbl dest_lbl def
634
635    | AST.Op_cmp AST.Cmp_eq
636    | AST.Op_cmpu AST.Cmp_eq
637    | AST.Op_cmpp AST.Cmp_eq ->
638      add_translates
639        [translate_ne destrs srcrs1 srcrs2 ;
640         translate_toggle_bool destrs] start_lbl dest_lbl def
641
642    | AST.Op_cmp AST.Cmp_ne
643    | AST.Op_cmpu AST.Cmp_ne
644    | AST.Op_cmpp AST.Cmp_ne ->
645      translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
646
647    | AST.Op_cmp AST.Cmp_lt ->
648      translate_lts destrs srcrs1 srcrs2 start_lbl dest_lbl def
649
650    | AST.Op_cmpu AST.Cmp_lt | AST.Op_cmpp AST.Cmp_lt ->
651      translate_ltu destrs srcrs1 srcrs2 start_lbl dest_lbl def
652
653    | AST.Op_cmp AST.Cmp_le ->
654      add_translates
655        [translate_lts destrs srcrs2 srcrs1 ;
656         translate_toggle_bool destrs] start_lbl dest_lbl def
657
658    | AST.Op_cmpu AST.Cmp_le | AST.Op_cmpp AST.Cmp_le ->
659      add_translates
660        [translate_ltu destrs srcrs2 srcrs1 ;
661         translate_toggle_bool destrs] start_lbl dest_lbl def
662
663    | AST.Op_cmp AST.Cmp_gt ->
664      translate_lts destrs srcrs2 srcrs1 start_lbl dest_lbl def
665
666    | AST.Op_cmpu AST.Cmp_gt | AST.Op_cmpp AST.Cmp_gt ->
667      translate_ltu destrs srcrs2 srcrs1 start_lbl dest_lbl def
668
669    | AST.Op_cmp AST.Cmp_ge ->
670      add_translates
671        [translate_lts destrs srcrs1 srcrs2 ;
672         translate_toggle_bool destrs] start_lbl dest_lbl def
673
674    | AST.Op_cmpu AST.Cmp_ge | AST.Op_cmpp AST.Cmp_ge ->
675      add_translates
676        [translate_ltu destrs srcrs1 srcrs2 ;
677         translate_toggle_bool destrs] start_lbl dest_lbl def
678
679    | AST.Op_div | AST.Op_divu | AST.Op_modu | AST.Op_mod | AST.Op_shl
680    | AST.Op_shr | AST.Op_shru ->
681      (* Unsupported, should have been replaced by a runtime function. *)
682      assert false
683
684
685let translate_cond srcrs start_lbl lbl_true lbl_false def =
686  match srcrs with
687    | [] -> add_graph start_lbl (RTL.St_skip lbl_false) def
688    | srcr :: srcrs ->
689      let (def, tmpr) = fresh_reg def in
690      let tmp_lbl = fresh_label def in
691      let init = RTL.St_move (tmpr, RTL.Reg srcr, start_lbl) in
692      let f srcr = RTL.St_op2 (I8051.Or, tmpr, tmpr, RTL.Reg srcr, start_lbl) in
693      let def = adds_graph (init :: (List.map f srcrs)) start_lbl tmp_lbl def in
694      add_graph tmp_lbl (RTL.St_cond (tmpr, lbl_true, lbl_false)) def
695
696
697let translate_load addr destrs start_lbl dest_lbl def =
698  let (def, save_addr) = fresh_regs def (List.length addr) in
699  let (def, tmp_addr) = fresh_regs def (List.length addr) in
700  let (tmp_addr1, tmp_addr2) = make_addr tmp_addr in
701  let (def, tmpr) = fresh_reg def in
702  let insts_save_addr = translate_move save_addr addr in
703  let f (translates, off) r =
704    let translates =
705      translates @
706        [adds_graph [RTL.St_move (tmpr, RTL.Imm off, start_lbl)] ;
707         translate_op2 AST.Op_addp tmp_addr save_addr [tmpr] ;
708         adds_graph [RTL.St_load (r, tmp_addr1, tmp_addr2, dest_lbl)]] in
709    (translates, off + Driver.TargetArch.int_size) in
710  let (translates, _) = List.fold_left f ([], 0) destrs in
711  add_translates (insts_save_addr :: translates) start_lbl dest_lbl def
712
713
714let translate_store addr srcrs start_lbl dest_lbl def =
715  let (def, tmp_addr) = fresh_regs def (List.length addr) in
716  let (tmp_addr1, tmp_addr2) = make_addr tmp_addr in
717  let (def, tmpr) = fresh_reg def in
718  let f (translates, off) srcr =
719    let translates =
720      translates @
721        [adds_graph [RTL.St_move (tmpr, RTL.Imm off, start_lbl)] ;
722         translate_op2 AST.Op_addp tmp_addr addr [tmpr] ;
723         adds_graph [RTL.St_store (tmp_addr1, tmp_addr2, srcr, dest_lbl)]] in
724    (translates, off + Driver.TargetArch.int_size) in
725  let (translates, _) = List.fold_left f ([], 0) srcrs in
726  add_translates translates start_lbl dest_lbl def
727
728
729let translate_stmt lenv lbl stmt def = match stmt with
730
731  | RTLabs.St_skip lbl' ->
732    add_graph lbl (RTL.St_skip lbl') def
733
734  | RTLabs.St_cost (cost_lbl, lbl') ->
735    add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def
736
737  | RTLabs.St_ind_0 (i, lbl') ->
738    add_graph lbl (RTL.St_ind_0 (i, lbl')) def
739
740  | RTLabs.St_ind_inc (i, lbl') ->
741    add_graph lbl (RTL.St_ind_inc (i, lbl')) def
742
743  | RTLabs.St_cst (destr, cst, lbl') ->
744    translate_cst cst (find_local_env destr lenv) lbl lbl' def
745
746  | RTLabs.St_op1 (op1, destr, srcr, lbl') ->
747    translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv)
748      lbl lbl' def
749
750  | RTLabs.St_op2 (op2, destr, RTLabs.Reg srcr1, RTLabs.Reg srcr2, lbl') ->
751    translate_op2 op2 (find_local_env destr lenv)
752      (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) lbl lbl' def
753
754  | RTLabs.St_load (_, RTLabs.Reg addr, destr, lbl') ->
755    translate_load (find_local_env addr lenv) (find_local_env destr lenv)
756      lbl lbl' def
757
758  | RTLabs.St_store (_, RTLabs.Reg addr, RTLabs.Reg srcr, lbl') ->
759    translate_store (find_local_env addr lenv) (find_local_env srcr lenv)
760      lbl lbl' def
761
762  | RTLabs.St_call_id (f, args, None, _, lbl') ->
763    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv, [], lbl')) def
764
765  | RTLabs.St_call_id (f, args, Some retr, _, lbl') ->
766    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv,
767                                   find_local_env retr lenv, lbl')) def
768
769  | RTLabs.St_call_ptr (f, args, None, _, lbl') ->
770    let (f1, f2) = find_and_addr f lenv in
771    add_graph lbl (RTL.St_call_ptr (f1, f2, rtl_args args lenv, [], lbl')) def
772
773  | RTLabs.St_call_ptr (f, args, Some retr, _, lbl') ->
774    let (f1, f2) = find_and_addr f lenv in
775    add_graph lbl
776      (RTL.St_call_ptr
777         (f1, f2, rtl_args args lenv, find_local_env retr lenv, lbl')) def
778
779  | RTLabs.St_tailcall_id (f, args, _) ->
780    add_graph lbl (RTL.St_tailcall_id (f, rtl_args args lenv)) def
781
782  | RTLabs.St_tailcall_ptr (f, args, _) ->
783    let (f1, f2) = find_and_addr f lenv in
784    add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args lenv)) def
785
786  | RTLabs.St_cond (r, lbl_true, lbl_false) ->
787    translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def
788
789  | RTLabs.St_jumptable _ ->
790    error "Jump tables not supported yet."
791
792  | RTLabs.St_return None ->
793    add_graph lbl (RTL.St_return []) def
794
795  | RTLabs.St_return (Some r) ->
796    add_graph lbl (RTL.St_return (find_local_env r lenv)) def
797
798  | _ -> assert false (*not possible because of previous removal of immediates*)
799
800let remove_immediates def =
801  let load_arg a lbl g rs = match a with
802    | RTLabs.Reg r -> (lbl, g, rs, r)
803    | RTLabs.Imm (c, t) ->
804      let new_l = Label.Gen.fresh def.RTLabs.f_luniverse in
805      let new_r = Register.fresh def.RTLabs.f_runiverse in
806      let g = Label.Map.add lbl (RTLabs.St_cst (new_r, c, new_l)) g in
807      (new_l, g, (new_r, t) :: rs, new_r) in 
808  let f lbl stmt (g, rs) =
809    match stmt with
810      | RTLabs.St_op2(op, r, a1, a2, l) ->
811        let (lbl', g, rs, r1) = load_arg a1 lbl g rs in
812        let (lbl', g, rs, r2) = load_arg a2 lbl' g rs in
813        let s = RTLabs.St_op2 (op, r, RTLabs.Reg r1, RTLabs.Reg r2, l) in
814        let g = Label.Map.add lbl' s g in
815        (g, rs)
816      | RTLabs.St_store(q, a1, a2, l) ->
817        let (lbl', g, rs, r1) = load_arg a1 lbl g rs in
818        let (lbl', g, rs, r2) = load_arg a2 lbl' g rs in
819        let s = RTLabs.St_store (q, RTLabs.Reg r1, RTLabs.Reg r2, l) in
820        let g = Label.Map.add lbl' s g in
821        (g, rs)
822      | RTLabs.St_load (q, a, r, l) ->
823        let (lbl', g, rs, r1) = load_arg a lbl g rs in
824        let s = RTLabs.St_load (q, RTLabs.Reg r1, r, l) in
825        let g = Label.Map.add lbl' s g in
826        (g, rs)
827      | _ -> (g, rs) in
828  let g = def.RTLabs.f_graph in
829  let (g, rs) = Label.Map.fold f g (g, []) in
830  let locals = List.rev_append rs def.RTLabs.f_locals in
831  { def with RTLabs.f_graph = g; RTLabs.f_locals = locals }
832 
833let translate_internal def =
834  let def = remove_immediates def in
835  let runiverse = def.RTLabs.f_runiverse in
836  let lenv =
837    initialize_local_env runiverse
838      (def.RTLabs.f_params @ def.RTLabs.f_locals) def.RTLabs.f_result in
839  let set_of_list l = List.fold_right Register.Set.add l Register.Set.empty in
840  let params = map_list_local_env lenv (List.map fst def.RTLabs.f_params) in
841  let locals = map_list_local_env lenv (List.map fst def.RTLabs.f_locals) in
842  let locals = set_of_list locals in
843  let result = match def.RTLabs.f_result with
844    | None -> []
845    | Some (r, _) -> find_local_env r lenv in
846  let res =
847    { RTL.f_luniverse = def.RTLabs.f_luniverse ;
848      RTL.f_runiverse = runiverse ;
849      RTL.f_result    = result ;
850      RTL.f_params    = params ;
851      RTL.f_locals    = locals ;
852      RTL.f_stacksize = concrete_size def.RTLabs.f_stacksize ;
853      RTL.f_graph     = Label.Map.empty ;
854      RTL.f_entry     = def.RTLabs.f_entry ;
855      RTL.f_exit      = def.RTLabs.f_exit } in
856  Label.Map.fold (translate_stmt lenv) def.RTLabs.f_graph res
857
858
859let translate_fun_def = function
860  | RTLabs.F_int def -> RTL.F_int (translate_internal def)
861  | RTLabs.F_ext def -> RTL.F_ext def
862
863
864let translate p =
865  let f_global (id, size) = (id, concrete_size size) in
866  let f_funct (id, fun_def) = (id, translate_fun_def fun_def) in
867  { RTL.vars   = List.map f_global p.RTLabs.vars ;
868    RTL.functs = List.map f_funct p.RTLabs.functs ;
869    RTL.main   = p.RTLabs.main }
Note: See TracBrowser for help on using the repository browser.