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

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

32 and 16 bits operations support in D2.2/8051

File size: 29.0 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_addr (r1, r2, id, _) -> RTL.St_addr (r1, r2, id, lbl)
96  | RTL.St_stackaddr (r1, r2, _) -> RTL.St_stackaddr (r1, r2, lbl)
97  | RTL.St_int (r, i, _) -> RTL.St_int (r, i, lbl)
98  | RTL.St_move (r1, r2, _) -> RTL.St_move (r1, r2, lbl)
99  | RTL.St_opaccs (opaccs, dstr1, dstr2, srcr1, srcr2, _) ->
100    RTL.St_opaccs (opaccs, dstr1, dstr2, srcr1, srcr2, lbl)
101  | RTL.St_op1 (op1, dstr, srcr, _) -> RTL.St_op1 (op1, dstr, srcr, lbl)
102  | RTL.St_op2 (op2, dstr, srcr1, srcr2, _) ->
103    RTL.St_op2 (op2, dstr, srcr1, srcr2, lbl)
104  | RTL.St_clear_carry _ -> RTL.St_clear_carry lbl
105  | RTL.St_set_carry _ -> RTL.St_set_carry lbl
106  | RTL.St_load (dstrs, addr1, addr2, _) ->
107    RTL.St_load (dstrs, addr1, addr2, lbl)
108  | RTL.St_store (addr1, addr2, srcrs, _) ->
109    RTL.St_store (addr1, addr2, srcrs, lbl)
110  | RTL.St_call_id (f, args, retrs, _) -> RTL.St_call_id (f, args, retrs, lbl)
111  | RTL.St_call_ptr (f1, f2, args, retrs, _) ->
112    RTL.St_call_ptr (f1, f2, args, retrs, lbl)
113  | RTL.St_tailcall_id (f, args) -> RTL.St_tailcall_id (f, args)
114  | RTL.St_tailcall_ptr (f1, f2, args) -> RTL.St_tailcall_ptr (f1, f2, args)
115  | RTL.St_cond _ as inst -> inst
116  | RTL.St_return regs -> RTL.St_return regs
117
118(* Add a list of instruction in a graph, from one label to another, by creating
119   fresh labels inbetween. *)
120
121let rec adds_graph stmt_list start_lbl dest_lbl def = match stmt_list with
122  | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
123  | [stmt] ->
124    add_graph start_lbl (change_label dest_lbl stmt) def
125  | stmt :: stmt_list ->
126    let tmp_lbl = fresh_label def in
127    let stmt = change_label tmp_lbl stmt in
128    let def = add_graph start_lbl stmt def in
129    adds_graph stmt_list tmp_lbl dest_lbl def
130
131(* Process a list of function that adds a list of instructions to a graph, from
132   one label to another, and by creating fresh labels inbetween. *)
133
134let rec add_translates translate_list start_lbl dest_lbl def =
135  match translate_list with
136    | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
137    | [trans] -> trans start_lbl dest_lbl def
138    | trans :: translate_list ->
139      let tmp_lbl = fresh_label def in
140      let def = trans start_lbl tmp_lbl def in
141      add_translates translate_list tmp_lbl dest_lbl def
142
143
144(*
145
146let rec translate_op2 op2 destrs srcrs1 srcrs2 start_lbl dest_lbl def =
147  match op2, destrs, srcrs1, srcrs2 with
148
149    | AST.Op_mul (1, _), [destr], [srcr1], [srcr2] ->
150      adds_graph
151        [RTL.St_opaccs (I8051.Mul, destr, srcr1, srcr2, start_lbl)]
152        start_lbl dest_lbl def
153
154    | AST.Op_shr _, _, _, _ ->
155      error_shift ()
156
157    | AST.Op_cmp (AST.Cmp_lt, (1, AST.Unsigned)), [destr], [srcr1], [srcr2] ->
158      let (def, tmpr) = fresh_reg def in
159      adds_graph
160        [RTL.St_clear_carry start_lbl ;
161         RTL.St_op2 (I8051.Sub, destr, srcr1, srcr2, start_lbl) ;
162         RTL.St_int (destr, 0, start_lbl) ;
163         RTL.St_op2 (I8051.Addc, destr, destr, destr, start_lbl)]
164        start_lbl dest_lbl def
165
166    | AST.Op_cmp (cmp, ((size, AST.Signed) as int_type)), _, _, _ ->
167      let (def, tmprs1) = fresh_regs def (List.length srcrs1) in
168      let (def, tmprs2) = fresh_regs def (List.length srcrs2) in
169      add_translates
170        [translate_cst (AST.Cst_int 128) tmprs1 ;
171         translate_cst (AST.Cst_int 128) tmprs2 ;
172         translate_op2 (AST.Op_add int_type) tmprs1 srcrs1 tmprs1 ;
173         translate_op2 (AST.Op_add int_type) tmprs2 srcrs2 tmprs2 ;
174         translate_op2 (AST.Op_cmp (cmp, (size, AST.Unsigned)))
175           destrs tmprs1 tmprs2]
176        start_lbl dest_lbl def
177
178    | AST.Op_cmpp AST.Cmp_lt, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] ->
179      let (def, tmpr1) = fresh_reg def in
180      let (def, tmpr2) = fresh_reg def in
181      add_translates
182        [translate_op2 (AST.Op_cmp (AST.Cmp_lt, uint))
183            [tmpr1] [srcr12] [srcr22] ;
184         translate_op2 (AST.Op_cmp (AST.Cmp_eq, uint))
185            [tmpr2] [srcr12] [srcr22] ;
186         translate_op2 (AST.Op_cmp (AST.Cmp_lt, uint))
187            [destr] [srcr11] [srcr21] ;
188         translate_op2 AST.Op_and [tmpr2] [tmpr2] [destr] ;
189         translate_op2 AST.Op_or [destr] [tmpr1] [tmpr2]]
190        start_lbl dest_lbl def
191
192    | _ -> error_int ()
193*)
194
195let rec translate_cst cst destrs start_lbl dest_lbl def = match cst with
196
197  | AST.Cst_int _ when destrs = [] ->
198    add_graph start_lbl (RTL.St_skip dest_lbl) def
199
200  | AST.Cst_int i ->
201    let size = List.length destrs in
202    let module M = IntValue.Make (struct let size = size end) in
203    let is = List.map M.to_int (M.break (M.of_int i) size) in
204    let f r i = RTL.St_int (r, i, dest_lbl) in
205    let l = List.map2 f destrs is in
206    adds_graph l start_lbl dest_lbl def
207
208  | AST.Cst_float _ -> error_float ()
209
210  | AST.Cst_addrsymbol id ->
211    let (r1, r2) = make_addr destrs in
212    add_graph start_lbl (RTL.St_addr (r1, r2, id, dest_lbl)) def
213
214  | AST.Cst_stack ->
215    let (r1, r2) = make_addr destrs in
216    add_graph start_lbl (RTL.St_stackaddr (r1, r2, dest_lbl)) def
217
218  | AST.Cst_offset off ->
219    let i = concrete_offset off in
220    translate_cst (AST.Cst_int i) destrs start_lbl dest_lbl def
221
222  | AST.Cst_sizeof size ->
223    let i = concrete_size size in
224    translate_cst (AST.Cst_int i) destrs start_lbl dest_lbl def
225
226
227let rec translate_move destrs srcrs start_lbl =
228  let ((common1, rest1), (common2, rest2)) = MiscPottier.reduce destrs srcrs in
229  let f_common destr srcr = RTL.St_move (destr, srcr, start_lbl) in
230  let translates1 = adds_graph (List.map2 f_common common1 common2) in
231  let translates2 = translate_cst (AST.Cst_int 0) rest1 in
232  add_translates [translates1 ; translates2] start_lbl
233
234
235let translate_cast_unsigned destrs start_lbl dest_lbl def =
236  let (def, tmp_zero) = fresh_reg def in
237  let zeros = MiscPottier.make tmp_zero (List.length destrs) in
238  add_translates
239    [adds_graph [RTL.St_int (tmp_zero, 0, start_lbl)] ;
240     translate_move destrs zeros]
241    start_lbl dest_lbl def
242
243let translate_cast_signed destrs srcr start_lbl dest_lbl def =
244  let (def, tmp_128) = fresh_reg def in
245  let (def, tmp_255) = fresh_reg def in
246  let (def, tmpr) = fresh_reg def in
247  let (def, dummy) = fresh_reg def in
248  let insts =
249    [RTL.St_int (tmp_128, 128, start_lbl) ;
250     RTL.St_op2 (I8051.And, tmpr, tmp_128, srcr, start_lbl) ;
251     RTL.St_opaccs (I8051.DivuModu, tmpr, dummy, tmpr, tmp_128, start_lbl) ;
252     RTL.St_int (tmp_255, 255, start_lbl) ;
253     RTL.St_opaccs (I8051.Mul, tmpr, dummy, tmpr, tmp_255, start_lbl)] in
254  let srcrs = MiscPottier.make tmpr (List.length destrs) in
255  add_translates [adds_graph insts ; translate_move destrs srcrs]
256    start_lbl dest_lbl def
257
258let translate_cast src_size src_sign dest_size destrs srcrs =
259  if List.length srcrs = 0 then adds_graph []
260  else
261    if dest_size < src_size then translate_move destrs srcrs
262    else
263      let ((common1, rest1), (common2, _)) = MiscPottier.reduce destrs srcrs in
264      let insts_common = translate_move common1 common2 in
265      let sign_reg = MiscPottier.last srcrs in
266      let insts_sign = match src_sign with
267        | AST.Unsigned -> translate_cast_unsigned rest1
268        | AST.Signed -> translate_cast_signed rest1 sign_reg in
269      add_translates [insts_common ; insts_sign]
270
271
272let translate_negint destrs srcrs start_lbl dest_lbl def =
273  assert (List.length destrs = List.length srcrs) ;
274  let (def, tmpr) = fresh_reg def in
275  let f_cmpl destr srcr = RTL.St_op1 (I8051.Cmpl, destr, srcr, start_lbl) in
276  let insts_cmpl = List.map2 f_cmpl destrs srcrs in
277  let insts_init =
278    [RTL.St_set_carry start_lbl ;
279     RTL.St_int (tmpr, 0, start_lbl)] in
280  let f_add destr = RTL.St_op2 (I8051.Addc, destr, destr, tmpr, start_lbl) in
281  let insts_add = List.map f_add destrs in
282  adds_graph (insts_cmpl @ insts_init @ insts_add)
283    start_lbl dest_lbl def
284
285
286let translate_notbool destrs srcrs start_lbl dest_lbl def = match destrs with
287  | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
288  | destr :: destrs ->
289    let (def, tmpr) = fresh_reg def in
290    let (def, tmp_srcrs) = fresh_regs def (List.length srcrs) in
291    let save_srcrs = translate_move tmp_srcrs srcrs in
292    let init_destr = RTL.St_int (destr, 1, start_lbl) in
293    let f tmp_srcr =
294      [RTL.St_clear_carry start_lbl ;
295       RTL.St_int (tmpr, 0, start_lbl) ;
296       RTL.St_op2 (I8051.Sub, tmpr, tmpr, tmp_srcr, start_lbl) ;
297       RTL.St_int (tmpr, 0, start_lbl) ;
298       RTL.St_op2 (I8051.Addc, tmpr, tmpr, tmpr, start_lbl) ;
299       RTL.St_op2 (I8051.Xor, destr, destr, tmpr, start_lbl)] in
300    let insts = init_destr :: (List.flatten (List.map f tmp_srcrs)) in
301    let epilogue = translate_cst (AST.Cst_int 0) destrs in
302    add_translates [save_srcrs ; adds_graph insts ; epilogue]
303      start_lbl dest_lbl def
304
305
306let translate_op1 op1 destrs srcrs start_lbl dest_lbl def = match op1 with
307
308  | AST.Op_cast ((src_size, src_sign), dest_size) ->
309    translate_cast src_size src_sign dest_size destrs srcrs start_lbl dest_lbl
310      def
311
312  | AST.Op_negint ->
313    translate_negint destrs srcrs start_lbl dest_lbl def
314
315  | AST.Op_notbool ->
316    translate_notbool destrs srcrs start_lbl dest_lbl def
317
318  | AST.Op_notint ->
319    let f destr srcr = RTL.St_op1 (I8051.Cmpl, destr, srcr, start_lbl) in
320    let l = List.map2 f destrs srcrs in
321    adds_graph l start_lbl dest_lbl def
322
323  | AST.Op_ptrofint | AST.Op_intofptr | AST.Op_id ->
324    translate_move destrs srcrs start_lbl dest_lbl def
325
326
327let translate_op op destrs srcrs1 srcrs2 start_lbl dest_lbl def =
328  let ((srcrs1_common, srcrs1_rest), (srcrs2_common, srcrs2_rest)) =
329    MiscPottier.reduce srcrs1 srcrs2 in
330  let srcrs_rest = choose_rest srcrs1_rest srcrs2_rest in
331  let ((destrs_common, destrs_rest), _) =
332    MiscPottier.reduce destrs srcrs1_common in
333  let ((destrs_cted, destrs_rest), (srcrs_cted, _)) =
334    MiscPottier.reduce destrs_rest srcrs_rest in
335  let (def, tmpr) = fresh_reg def in
336  let insts_init =
337    [RTL.St_clear_carry start_lbl ;
338     RTL.St_int (tmpr, 0, start_lbl)] in
339  let f_add destr srcr1 srcr2 =
340    RTL.St_op2 (op, destr, srcr1, srcr2, start_lbl) in
341  let insts_add =
342    MiscPottier.map3 f_add destrs_common srcrs1_common srcrs2_common in
343  let f_add_cted destr srcr =
344    RTL.St_op2 (op, destr, srcr, tmpr, start_lbl) in
345  let insts_add_cted = List.map2 f_add_cted destrs_cted srcrs_cted in
346  let f_rest destr =
347    RTL.St_op2 (op, destr, tmpr, tmpr, start_lbl) in
348  let insts_rest = List.map f_rest destrs_rest in
349  adds_graph (insts_init @ insts_add @ insts_add_cted @ insts_rest)
350    start_lbl dest_lbl def
351
352
353let rec translate_mul1 dummy tmpr destrs srcrs1 srcr2 start_lbl =
354  match destrs, srcrs1 with
355    | [], _ -> adds_graph [RTL.St_skip start_lbl] start_lbl
356    | [destr], [] ->
357      adds_graph [RTL.St_int (tmpr, 0, start_lbl) ;
358                  RTL.St_op2 (I8051.Addc, destr, destr, tmpr, start_lbl)]
359        start_lbl
360    | destr1 :: destr2 :: destrs, [] ->
361      add_translates
362        [adds_graph [RTL.St_int (tmpr, 0, start_lbl) ;
363                     RTL.St_op2 (I8051.Addc, destr1, destr1, tmpr, start_lbl) ;
364                     RTL.St_op2 (I8051.Addc, destr2, tmpr, tmpr, start_lbl)] ;
365         translate_cst (AST.Cst_int 0) destrs]
366        start_lbl
367    | [destr], srcr1 :: _ ->
368      adds_graph
369        [RTL.St_opaccs (I8051.Mul, tmpr, dummy, srcr2, srcr1, start_lbl) ;
370         RTL.St_op2 (I8051.Addc, destr, destr, tmpr, start_lbl)]
371        start_lbl
372    | destr1 :: destr2 :: destrs, srcr1 :: srcrs1 ->
373      add_translates
374        [adds_graph
375            [RTL.St_opaccs
376                (I8051.Mul, tmpr, destr2, srcr2, srcr1, start_lbl) ;
377             RTL.St_op2 (I8051.Addc, destr1, destr1, tmpr, start_lbl)] ;
378         translate_mul1 dummy tmpr (destr2 :: destrs) srcrs1 srcr2]
379        start_lbl
380
381let translate_muli dummy tmpr destrs tmp_destrs srcrs1 dummy_lbl i translates
382    srcr2i =
383  let (tmp_destrs1, tmp_destrs2) = MiscPottier.split tmp_destrs i in
384  translates @
385    (match tmp_destrs2 with
386      | [] -> []
387      | tmp_destr2 :: tmp_destrs2 ->
388        [adds_graph [RTL.St_clear_carry dummy_lbl ;
389                     RTL.St_int (tmp_destr2, 0, dummy_lbl)] ;
390         translate_mul1 dummy tmpr (tmp_destr2 :: tmp_destrs2) srcrs1 srcr2i ;
391         translate_cst (AST.Cst_int 0) tmp_destrs1 ;
392         adds_graph [RTL.St_clear_carry dummy_lbl] ;
393         translate_op I8051.Addc destrs destrs tmp_destrs])
394
395let translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def =
396  let (def, dummy) = fresh_reg def in
397  let (def, tmpr) = fresh_reg def in
398  let (def, tmp_destrs) = fresh_regs def (List.length destrs) in
399  let (def, fresh_srcrs1) = fresh_regs def (List.length srcrs1) in
400  let (def, fresh_srcrs2) = fresh_regs def (List.length srcrs2) in
401  let insts_init =
402    [translate_move fresh_srcrs1 srcrs1 ;
403     translate_move fresh_srcrs2 srcrs2 ;
404     translate_cst (AST.Cst_int 0) destrs] in
405  let f = translate_muli dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl in
406  let insts_mul = MiscPottier.foldi f [] srcrs2 in
407  add_translates (insts_init @ insts_mul) start_lbl dest_lbl def
408
409
410let translate_divumodu8 order destrs srcr1 srcr2 start_lbl dest_lbl def =
411  match destrs with
412    | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
413    | destr :: destrs ->
414      let (def, dummy) = fresh_reg def in
415      let (destr1, destr2) = if order then (destr, dummy) else (dummy, destr) in
416      let inst_div =
417        adds_graph [RTL.St_opaccs (I8051.DivuModu, destr1, destr2,
418                                   srcr1, srcr2, start_lbl)] in
419      let insts_rest = translate_cst (AST.Cst_int 0) destrs in
420      add_translates [inst_div ; insts_rest] start_lbl dest_lbl def
421
422
423let translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def =
424  match destrs with
425    | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
426    | destr :: destrs ->
427      let (def, tmpr) = fresh_reg def in
428      let (def, tmp_zero) = fresh_reg def in
429      let (def, tmp_srcrs1) = fresh_regs def (List.length srcrs1) in
430      let save_srcrs1 = translate_move tmp_srcrs1 srcrs1 in
431      let (def, tmp_srcrs2) = fresh_regs def (List.length srcrs2) in
432      let save_srcrs2 = translate_move tmp_srcrs2 srcrs2 in
433      let ((common1, rest1), (common2, rest2)) =
434        MiscPottier.reduce tmp_srcrs1 tmp_srcrs2 in
435      let rest = choose_rest rest1 rest2 in
436      let inits =
437        [RTL.St_int (destr, 0, start_lbl) ;
438         RTL.St_int (tmp_zero, 0, start_lbl)] in
439      let f_common tmp_srcr1 tmp_srcr2 =
440        [RTL.St_clear_carry start_lbl ;
441         RTL.St_op2 (I8051.Sub, tmpr, tmp_srcr1, tmp_srcr2, start_lbl) ;
442         RTL.St_op2 (I8051.Or, destr, destr, tmpr, start_lbl)] in
443      let insts_common = List.flatten (List.map2 f_common common1 common2) in
444      let f_rest tmp_srcr =
445        [RTL.St_clear_carry start_lbl ;
446         RTL.St_op2 (I8051.Sub, tmpr, tmp_zero, tmp_srcr, start_lbl) ;
447         RTL.St_op2 (I8051.Or, destr, destr, tmpr, start_lbl)] in
448      let insts_rest = List.flatten (List.map f_rest rest) in
449      let insts = inits @ insts_common @ insts_rest in
450      let epilogue = translate_cst (AST.Cst_int 0) destrs in
451      add_translates [save_srcrs1 ; save_srcrs2 ; adds_graph insts ; epilogue]
452        start_lbl dest_lbl def
453
454
455let translate_eq_reg tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl
456    (srcr1, srcr2) =
457  [RTL.St_clear_carry dummy_lbl ;
458   RTL.St_op2 (I8051.Sub, tmpr1, srcr1, srcr2, dummy_lbl) ;
459   RTL.St_op2 (I8051.Addc, tmpr1, tmp_zero, tmp_zero, dummy_lbl) ;
460   RTL.St_op2 (I8051.Sub, tmpr2, srcr2, srcr1, dummy_lbl) ;
461   RTL.St_op2 (I8051.Addc, tmpr2, tmp_zero, tmp_zero, dummy_lbl) ;
462   RTL.St_op2 (I8051.Or, tmpr1, tmpr1, tmpr2, dummy_lbl) ;
463   RTL.St_op2 (I8051.Xor, tmpr1, tmpr1, tmp_one, dummy_lbl) ;
464   RTL.St_op2 (I8051.And, destr, destr, tmpr1, dummy_lbl)]
465
466let translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 destr leq dummy_lbl =
467  let f = translate_eq_reg tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl in
468  (RTL.St_int (destr, 1, dummy_lbl)) :: (List.flatten (List.map f leq))
469
470let translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq
471    srcr1 srcr2 =
472  (translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl) @
473  [RTL.St_clear_carry dummy_lbl ;
474   RTL.St_op2 (I8051.Sub, tmpr1, srcr1, srcr2, dummy_lbl) ;
475   RTL.St_op2 (I8051.Addc, tmpr1, tmp_zero, tmp_zero, dummy_lbl) ;
476   RTL.St_op2 (I8051.And, tmpr3, tmpr3, tmpr1, dummy_lbl) ;
477   RTL.St_op2 (I8051.Or, destr, destr, tmpr3, dummy_lbl)]
478
479let translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl
480    srcrs1 srcrs2 =
481  let f (insts, leq) srcr1 srcr2 =
482    let added_insts =
483      translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq
484        srcr1 srcr2 in
485    (insts @ added_insts, leq @ [(srcr1, srcr2)]) in
486  fst (List.fold_left2 f ([], []) srcrs1 srcrs2)
487
488let translate_lt destrs srcrs1 srcrs2 start_lbl dest_lbl def =
489  match destrs with
490    | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
491    | _ ->
492      let (def, tmp_destrs) = fresh_regs def (List.length destrs) in
493      let tmp_destr = List.hd tmp_destrs in
494      let (def, tmp_zero) = fresh_reg def in
495      let (def, tmp_one) = fresh_reg def in
496      let (def, tmpr1) = fresh_reg def in
497      let (def, tmpr2) = fresh_reg def in
498      let (def, tmpr3) = fresh_reg def in
499      let (srcrs1, srcrs2, added) = complete_regs def srcrs1 srcrs2 in
500      let srcrs1 = List.rev srcrs1 in
501      let srcrs2 = List.rev srcrs2 in
502      let insts_init =
503        [translate_cst (AST.Cst_int 0) tmp_destrs ;
504         translate_cst (AST.Cst_int 0) added ;
505         adds_graph [RTL.St_int (tmp_zero, 0, start_lbl) ;
506                     RTL.St_int (tmp_one, 1, start_lbl)]] in
507      let insts_main =
508        translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl
509          srcrs1 srcrs2 in
510      let insts_main = [adds_graph insts_main] in
511      let insts_exit = [translate_move destrs tmp_destrs] in
512      add_translates (insts_init @ insts_main @ insts_exit )
513        start_lbl dest_lbl def
514
515
516let add_128_to_last tmp_128 rs start_lbl = match rs with
517  | [] -> adds_graph [] start_lbl
518  | _ ->
519    let r = MiscPottier.last rs in
520    adds_graph [RTL.St_op2 (I8051.Add, r, r, tmp_128, start_lbl)] start_lbl
521
522let translate_lts destrs srcrs1 srcrs2 start_lbl dest_lbl def =
523  let (def, tmp_srcrs1) = fresh_regs def (List.length srcrs1) in
524  let (def, tmp_srcrs2) = fresh_regs def (List.length srcrs2) in
525  let (def, tmp_128) = fresh_reg def in
526  add_translates
527    [translate_move tmp_srcrs1 srcrs1 ;
528     translate_move tmp_srcrs2 srcrs2 ;
529     adds_graph [RTL.St_int (tmp_128, 128, start_lbl)] ;
530     add_128_to_last tmp_128 tmp_srcrs1 ;
531     add_128_to_last tmp_128 tmp_srcrs2 ;
532     translate_lt destrs tmp_srcrs1 tmp_srcrs2]
533    start_lbl dest_lbl def
534
535
536let rec translate_op2 op2 destrs srcrs1 srcrs2 start_lbl dest_lbl def =
537  match op2 with
538
539    | AST.Op_add | AST.Op_addp ->
540      translate_op I8051.Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
541
542    | AST.Op_sub | AST.Op_subp | AST.Op_subpp ->
543      translate_op I8051.Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
544
545    | AST.Op_mul ->
546      translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def
547
548    | AST.Op_divu when List.length srcrs1 = 1 && List.length srcrs2 = 1 ->
549      translate_divumodu8 true destrs (List.hd srcrs1) (List.hd srcrs2)
550        start_lbl dest_lbl def
551
552    | AST.Op_modu when List.length srcrs1 = 1 && List.length srcrs2 = 1 ->
553      translate_divumodu8 false destrs (List.hd srcrs1) (List.hd srcrs2)
554        start_lbl dest_lbl def
555
556    | AST.Op_and ->
557      translate_op I8051.And destrs srcrs1 srcrs2 start_lbl dest_lbl def
558
559    | AST.Op_or ->
560      translate_op I8051.Or destrs srcrs1 srcrs2 start_lbl dest_lbl def
561
562    | AST.Op_xor ->
563      translate_op I8051.Xor destrs srcrs1 srcrs2 start_lbl dest_lbl def
564
565    | AST.Op_cmp AST.Cmp_eq
566    | AST.Op_cmpu AST.Cmp_eq
567    | AST.Op_cmpp AST.Cmp_eq ->
568      add_translates
569        [translate_op2 (AST.Op_cmpu AST.Cmp_ne) destrs srcrs1 srcrs2 ;
570         translate_op1 AST.Op_notbool destrs destrs]
571        start_lbl dest_lbl def
572
573    | AST.Op_cmp AST.Cmp_ne
574    | AST.Op_cmpu AST.Cmp_ne
575    | AST.Op_cmpp AST.Cmp_ne ->
576      translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
577
578    | AST.Op_cmp AST.Cmp_lt ->
579      translate_lts destrs srcrs1 srcrs2 start_lbl dest_lbl def
580
581    | AST.Op_cmpu AST.Cmp_lt | AST.Op_cmpp AST.Cmp_lt ->
582      translate_lt destrs srcrs1 srcrs2 start_lbl dest_lbl def
583
584    | AST.Op_cmp AST.Cmp_le ->
585      add_translates
586        [translate_op2 (AST.Op_cmp AST.Cmp_lt) destrs srcrs2 srcrs1 ;
587         translate_op1 AST.Op_notbool destrs destrs]
588        start_lbl dest_lbl def
589
590    | AST.Op_cmpu AST.Cmp_le ->
591      add_translates
592        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs2 srcrs1 ;
593         translate_op1 AST.Op_notbool destrs destrs]
594        start_lbl dest_lbl def
595
596    | AST.Op_cmpp AST.Cmp_le ->
597      add_translates
598        [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs2 srcrs1 ;
599         translate_op1 AST.Op_notbool destrs destrs]
600        start_lbl dest_lbl def
601
602    | AST.Op_cmp AST.Cmp_gt ->
603      translate_op2 (AST.Op_cmp AST.Cmp_lt)
604        destrs srcrs2 srcrs1 start_lbl dest_lbl def
605
606    | AST.Op_cmpu AST.Cmp_gt ->
607      translate_op2 (AST.Op_cmpu AST.Cmp_lt)
608        destrs srcrs2 srcrs1 start_lbl dest_lbl def
609
610    | AST.Op_cmpp AST.Cmp_gt ->
611      translate_op2 (AST.Op_cmpp AST.Cmp_lt)
612        destrs srcrs2 srcrs1 start_lbl dest_lbl def
613
614    | AST.Op_cmp AST.Cmp_ge ->
615      add_translates
616        [translate_op2 (AST.Op_cmp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
617         translate_op1 AST.Op_notbool destrs destrs]
618        start_lbl dest_lbl def
619
620    | AST.Op_cmpu AST.Cmp_ge ->
621      add_translates
622        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs1 srcrs2 ;
623         translate_op1 AST.Op_notbool destrs destrs]
624        start_lbl dest_lbl def
625
626    | AST.Op_cmpp AST.Cmp_ge ->
627      add_translates
628        [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
629         translate_op1 AST.Op_notbool destrs destrs]
630        start_lbl dest_lbl def
631
632    | AST.Op_div | AST.Op_divu | AST.Op_modu | AST.Op_mod | AST.Op_shl
633    | AST.Op_shr | AST.Op_shru ->
634      (* Unsupported, should have been replaced by a runtime function. *)
635      assert false
636
637
638let translate_cond srcrs start_lbl lbl_true lbl_false def =
639  let (def, tmpr) = fresh_reg def in
640  let tmp_lbl = fresh_label def in
641  let init = RTL.St_int (tmpr, 0, start_lbl) in
642  let f srcr = RTL.St_op2 (I8051.Or, tmpr, tmpr, srcr, start_lbl) in
643  let def = adds_graph (init :: (List.map f srcrs)) start_lbl tmp_lbl def in
644  add_graph tmp_lbl (RTL.St_cond (tmpr, lbl_true, lbl_false)) def
645
646
647let translate_load addr destrs start_lbl dest_lbl def =
648  let (def, save_addr) = fresh_regs def (List.length addr) in
649  let (def, tmp_addr) = fresh_regs def (List.length addr) in
650  let (tmp_addr1, tmp_addr2) = make_addr tmp_addr in
651  let (def, tmpr) = fresh_reg def in
652  let insts_save_addr = translate_move save_addr addr in
653  let f (translates, off) r =
654    let translates =
655      translates @
656        [adds_graph [RTL.St_int (tmpr, off, start_lbl)] ;
657         translate_op2 AST.Op_addp tmp_addr save_addr [tmpr] ;
658         adds_graph [RTL.St_load (r, tmp_addr1, tmp_addr2, dest_lbl)]] in
659    (translates, off + Driver.TargetArch.int_size) in
660  let (translates, _) = List.fold_left f ([], 0) destrs in
661  add_translates (insts_save_addr :: translates) start_lbl dest_lbl def
662
663
664let translate_store addr srcrs start_lbl dest_lbl def =
665  let (def, tmp_addr) = fresh_regs def (List.length addr) in
666  let (tmp_addr1, tmp_addr2) = make_addr tmp_addr in
667  let (def, tmpr) = fresh_reg def in
668  let f (translates, off) srcr =
669    let translates =
670      translates @
671        [adds_graph [RTL.St_int (tmpr, off, start_lbl)] ;
672         translate_op2 AST.Op_addp tmp_addr addr [tmpr] ;
673         adds_graph [RTL.St_store (tmp_addr1, tmp_addr2, srcr, dest_lbl)]] in
674    (translates, off + Driver.TargetArch.int_size) in
675  let (translates, _) = List.fold_left f ([], 0) srcrs in
676  add_translates translates start_lbl dest_lbl def
677
678
679let translate_stmt lenv lbl stmt def = match stmt with
680
681  | RTLabs.St_skip lbl' ->
682    add_graph lbl (RTL.St_skip lbl') def
683
684  | RTLabs.St_cost (cost_lbl, lbl') ->
685    add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def
686
687  | RTLabs.St_cst (destr, cst, lbl') ->
688    translate_cst cst (find_local_env destr lenv) lbl lbl' def
689
690  | RTLabs.St_op1 (op1, destr, srcr, lbl') ->
691    translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv)
692      lbl lbl' def
693
694  | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') ->
695    translate_op2 op2 (find_local_env destr lenv)
696      (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) lbl lbl' def
697
698  | RTLabs.St_load (_, addr, destr, lbl') ->
699    translate_load (find_local_env addr lenv) (find_local_env destr lenv)
700      lbl lbl' def
701
702  | RTLabs.St_store (_, addr, srcr, lbl') ->
703    translate_store (find_local_env addr lenv) (find_local_env srcr lenv)
704      lbl lbl' def
705
706  | RTLabs.St_call_id (f, args, None, _, lbl') ->
707    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv, [], lbl')) def
708
709  | RTLabs.St_call_id (f, args, Some retr, _, lbl') ->
710    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv,
711                                   find_local_env retr lenv, lbl')) def
712
713  | RTLabs.St_call_ptr (f, args, None, _, lbl') ->
714    let (f1, f2) = find_and_addr f lenv in
715    add_graph lbl (RTL.St_call_ptr (f1, f2, rtl_args args lenv, [], lbl')) def
716
717  | RTLabs.St_call_ptr (f, args, Some retr, _, lbl') ->
718    let (f1, f2) = find_and_addr f lenv in
719    add_graph lbl
720      (RTL.St_call_ptr
721         (f1, f2, rtl_args args lenv, find_local_env retr lenv, lbl')) def
722
723  | RTLabs.St_tailcall_id (f, args, _) ->
724    add_graph lbl (RTL.St_tailcall_id (f, rtl_args args lenv)) def
725
726  | RTLabs.St_tailcall_ptr (f, args, _) ->
727    let (f1, f2) = find_and_addr f lenv in
728    add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args lenv)) def
729
730  | RTLabs.St_cond (r, lbl_true, lbl_false) ->
731    translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def
732
733  | RTLabs.St_jumptable _ ->
734    error "Jump tables not supported yet."
735
736  | RTLabs.St_return None ->
737    add_graph lbl (RTL.St_return []) def
738
739  | RTLabs.St_return (Some r) ->
740    add_graph lbl (RTL.St_return (find_local_env r lenv)) def
741
742
743let translate_internal def =
744  let runiverse = def.RTLabs.f_runiverse in
745  let lenv =
746    initialize_local_env runiverse
747      (def.RTLabs.f_params @ def.RTLabs.f_locals) def.RTLabs.f_result in
748  let set_of_list l = List.fold_right Register.Set.add l Register.Set.empty in
749  let params = map_list_local_env lenv (List.map fst def.RTLabs.f_params) in
750  let locals = map_list_local_env lenv (List.map fst def.RTLabs.f_locals) in
751  let locals = set_of_list locals in
752  let result = match def.RTLabs.f_result with
753    | None -> []
754    | Some (r, _) -> find_local_env r lenv in
755  let res =
756    { RTL.f_luniverse = def.RTLabs.f_luniverse ;
757      RTL.f_runiverse = runiverse ;
758      RTL.f_result    = result ;
759      RTL.f_params    = params ;
760      RTL.f_locals    = locals ;
761      RTL.f_stacksize = concrete_size def.RTLabs.f_stacksize ;
762      RTL.f_graph     = Label.Map.empty ;
763      RTL.f_entry     = def.RTLabs.f_entry ;
764      RTL.f_exit      = def.RTLabs.f_exit } in
765  Label.Map.fold (translate_stmt lenv) def.RTLabs.f_graph res
766
767
768let translate_fun_def = function
769  | RTLabs.F_int def -> RTL.F_int (translate_internal def)
770  | RTLabs.F_ext def -> RTL.F_ext def
771
772
773let translate p =
774  let f_global (id, size) = (id, concrete_size size) in
775  let f_funct (id, fun_def) = (id, translate_fun_def fun_def) in
776  { RTL.vars   = List.map f_global p.RTLabs.vars ;
777    RTL.functs = List.map f_funct p.RTLabs.functs ;
778    RTL.main   = p.RTLabs.main }
Note: See TracBrowser for help on using the repository browser.