source: Deliverables/D2.2/8051-indexed-labels-branch/src/RTLabs/RTLabsToRTL.ml @ 1340

Last change on this file since 1340 was 1340, checked in by tranquil, 8 years ago

work on RTLabs and RTL completed

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