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

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

fighting with a bug of the translation from RTL to ERTL

File size: 28.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
68
69let rec int_to_args (size : int) = function
70
71  | AST.Cst_int i ->
72    let module M = IntValue.Make (struct let size = size end) in
73    let chunks = M.break (M.of_int i) size in
74    List.map (fun x -> RTL.Imm (M.to_int x)) chunks
75
76  | AST.Cst_float _ -> error_float ()
77
78  | AST.Cst_offset off ->
79    let i = concrete_offset off in
80    int_to_args size (AST.Cst_int i)
81
82  | AST.Cst_sizeof size' ->
83    let i = concrete_size size' in
84    int_to_args size (AST.Cst_int i)
85
86  | _ -> assert false (* should not be called on non-int arguments *)
87
88let find_local_env_reg = Register.Map.find
89
90let find_local_env a env = match a with
91  | RTLabs.Reg r -> List.map (fun r -> RTL.Reg r) (Register.Map.find r env)
92  | RTLabs.Imm (k, t) -> int_to_args (size_of_sig_type t) k
93
94let initialize_local_env runiverse registers result =
95  let registers =
96    registers @ (match result with None -> [] | Some (r, t) -> [(r, t)]) in
97  let f lenv (r, t) =
98    let rs = register_freshes runiverse (size_of_sig_type t) in
99    add_local_env r rs lenv in
100  List.fold_left f Register.Map.empty registers
101
102let map_list_local_env_reg lenv regs =
103  let f res r = res @ (find_local_env_reg r lenv) in
104  List.fold_left f [] regs
105
106let make_addr = function
107  | r1 :: r2 :: _ -> (r1, r2)
108  | _ -> assert false (* do not use on these arguments *)
109
110let find_and_addr r lenv = make_addr (find_local_env_reg r lenv)
111
112let rtl_args regs_list lenv =
113  List.flatten (List.map (fun r -> find_local_env r lenv) regs_list)
114
115
116let change_label lbl = function
117  | (RTL.St_cond _ | RTL.St_return _) as inst -> inst
118  | stmt -> RTLGraph.fill_succs stmt [lbl]
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
146let rec translate_move destrs srcrs start_lbl =
147  let ((common1, rest1), (common2, rest2)) = MiscPottier.reduce destrs srcrs in
148  let f_common destr srcr = RTL.St_move (destr, srcr, start_lbl) in
149  let translates1 = adds_graph (List.map2 f_common common1 common2) in
150  let translates2 = translate_cst (AST.Cst_int 0) rest1 in
151  add_translates [translates1 ; translates2] start_lbl
152
153(* translate non-int constants *)
154and translate_cst cst destrs start_lbl = match destrs, cst with
155
156  | [], _ -> adds_graph [] start_lbl
157
158  | _, AST.Cst_float _ -> error_float ()
159
160  | _, AST.Cst_addrsymbol id ->
161    let (r1, r2) = make_addr destrs in
162    adds_graph [RTL.St_addr (r1, r2, id, start_lbl)] start_lbl
163
164  | _, AST.Cst_stack ->
165    let (r1, r2) = make_addr destrs in
166    adds_graph [RTL.St_stackaddr (r1, r2, start_lbl)] start_lbl
167
168  | _ ->
169    let srcrs = int_to_args (List.length destrs) cst in
170    translate_move destrs srcrs start_lbl
171
172
173let translate_cast_unsigned destrs start_lbl dest_lbl def =
174  translate_cst (AST.Cst_int 0) destrs start_lbl dest_lbl def
175
176let translate_cast_signed destrs srcr start_lbl dest_lbl def =
177  let (def, tmpr) = fresh_reg def in
178  let insts =
179    (* this sets tmpr to 0xFF if s is neg, 0x00 o.w. Done like that:
180       byte in tmpr if srcr is: neg   |  pos
181       tmpr ← srcr | 127       11...1 | 01...1
182       tmpr ← tmpr <rot< 1     1...11 | 1...10
183       tmpr ← INC tmpr         0....0 | 1....1
184       tmpr ← CPL tmpr         1....1 | 0....0
185
186     *)
187    [RTL.St_op2 (I8051.Or, tmpr, srcr, RTL.Imm 127, start_lbl) ;
188     RTL.St_op1 (I8051.Rl, tmpr, tmpr, start_lbl) ;
189     RTL.St_op1 (I8051.Inc, tmpr, tmpr, start_lbl) ;
190     RTL.St_op1 (I8051.Cmpl, tmpr, tmpr, start_lbl) ] in
191  let srcrs = MiscPottier.make (RTL.Reg tmpr) (List.length destrs) in
192  add_translates [adds_graph insts ; translate_move destrs srcrs]
193    start_lbl dest_lbl def
194
195let translate_cast src_size src_sign dest_size destrs srcrs =
196  if List.length srcrs = 0 then adds_graph []
197  else
198    if dest_size < src_size then translate_move destrs srcrs
199    else
200      let ((common1, rest1), (common2, _)) = MiscPottier.reduce destrs srcrs in
201      let insts_common = translate_move common1 common2 in
202      let sign_reg = MiscPottier.last srcrs in
203      let insts_sign = match src_sign with
204        | AST.Unsigned -> translate_cast_unsigned rest1
205        | AST.Signed -> translate_cast_signed rest1 sign_reg in
206      add_translates [insts_common ; insts_sign]
207
208
209let translate_negint destrs srcrs start_lbl dest_lbl def =
210  let f_cmpl destr = function
211    | RTL.Reg r -> RTL.St_op1 (I8051.Cmpl, destr, r, start_lbl)
212    | RTL.Imm k -> RTL.St_move (destr, RTL.Imm (lnot k), start_lbl) in
213  let insts_cmpl = List.map2 f_cmpl destrs srcrs in
214  match destrs with
215    | destr :: destrs ->
216      let inst_init =
217        RTL.St_op2 (I8051.Add, destr, RTL.Reg destr, RTL.Imm 1, start_lbl) in
218      let f_add destr =
219        RTL.St_op2 (I8051.Addc, destr, RTL.Reg destr, RTL.Imm 0, start_lbl) in
220      let insts_add = List.map f_add destrs in
221      adds_graph (insts_cmpl @ inst_init :: insts_add)
222        start_lbl dest_lbl def
223    | [] ->
224      adds_graph [] start_lbl dest_lbl def
225
226
227let translate_notbool destrs srcrs start_lbl dest_lbl def =
228  match destrs,srcrs with
229    | [], _ -> adds_graph [] start_lbl dest_lbl def
230    | destr :: destrs, srcr :: srcrs ->
231      let (def, tmpr) = fresh_reg def in
232      let init_destr = RTL.St_move (destr, srcr, start_lbl) in
233      let f r =
234        RTL.St_op2 (I8051.Or, destr, RTL.Reg destr, r, start_lbl) in
235      let big_or = List.map f srcrs in
236      let finalize_destr =
237        [RTL.St_move (tmpr, RTL.Imm 0, start_lbl) ;
238         RTL.St_clear_carry start_lbl ;
239         RTL.St_op2 (I8051.Sub, tmpr, RTL.Reg tmpr, RTL.Reg destr, start_lbl) ;
240         (* carry bit is set iff destr is non-zero iff destrs was non-zero *)
241         RTL.St_move (tmpr, RTL.Imm 0, start_lbl) ;
242         RTL.St_op2 (I8051.Addc, destr, RTL.Reg tmpr, RTL.Reg tmpr, start_lbl) ;
243         (* destr = carry bit = bigor of old destrs *)
244         RTL.St_op2 (I8051.Xor, destr, RTL.Reg destr, RTL.Imm 1, start_lbl)] in
245      let epilogue = translate_cst (AST.Cst_int 0) destrs in
246      add_translates [adds_graph (init_destr :: big_or @ finalize_destr) ;
247                      epilogue]
248        start_lbl dest_lbl def
249    | destr :: destrs, [] ->
250      translate_cst (AST.Cst_int 1) destrs start_lbl dest_lbl def
251
252
253let translate_op1 op1 destrs srcrs start_lbl dest_lbl def = match op1 with
254
255  | AST.Op_cast ((src_size, src_sign), dest_size) ->
256    translate_cast src_size src_sign dest_size destrs srcrs start_lbl dest_lbl
257      def
258
259  | AST.Op_negint ->
260    translate_negint destrs srcrs start_lbl dest_lbl def
261
262  | AST.Op_notbool ->
263    translate_notbool destrs srcrs start_lbl dest_lbl def
264
265  | AST.Op_notint ->
266    let f destr = function
267      | RTL.Reg srcr ->  RTL.St_op1 (I8051.Cmpl, destr, srcr, start_lbl)
268      | RTL.Imm k -> RTL.St_move (destr, RTL.Imm (lnot k), start_lbl) in
269    let l = List.map2 f destrs srcrs in
270    adds_graph l start_lbl dest_lbl def
271
272  | AST.Op_ptrofint | AST.Op_intofptr | AST.Op_id ->
273    translate_move destrs srcrs start_lbl dest_lbl def
274
275
276let translate_op op destrs srcrs1 srcrs2 start_lbl dest_lbl def =
277  let ((srcrs1_common, srcrs1_rest), (srcrs2_common, srcrs2_rest)) =
278    MiscPottier.reduce srcrs1 srcrs2 in
279  let srcrs_rest = choose_rest srcrs1_rest srcrs2_rest in
280  let ((destrs_common, destrs_rest), _) =
281    MiscPottier.reduce destrs srcrs1_common in
282  let ((destrs_cted, destrs_rest), (srcrs_cted, _)) =
283    MiscPottier.reduce destrs_rest srcrs_rest in
284  let (def, tmpr) = fresh_reg def in
285  let carry_init = match op with
286    | I8051.Sub | I8051.Addc ->
287      (* depend on carry bit *)
288      [RTL.St_clear_carry start_lbl]
289    | _ -> [] in
290  let f_add op destr srcr1 srcr2 =
291    RTL.St_op2 (op, destr, srcr1, srcr2, start_lbl) in
292  let insts_add =
293    match op with
294      | I8051.Add ->
295        (* we perform a first add followed by Addc's *)
296        begin match destrs_common, srcrs1_common, srcrs2_common with
297          | destr :: destrs, srcr1 :: srcrs1, srcr2 :: srcrs2 ->
298            f_add op destr srcr1 srcr2 ::
299              MiscPottier.map3 (f_add I8051.Addc) destrs srcrs1 srcrs2
300          | [], [], [] -> []
301          | _ -> assert false
302        end
303      | _ ->
304        (* we just do the same operation on all *)
305        MiscPottier.map3 (f_add op) destrs_common srcrs1_common srcrs2_common in
306  let f_add_cted destr srcr =
307    RTL.St_op2 (op, destr, srcr, RTL.Imm 0, start_lbl) in
308  let insts_add_cted = List.map2 f_add_cted destrs_cted srcrs_cted in
309  let f_rest destr =
310    match op with
311      | I8051.Addc | I8051.Sub ->
312        (* propagate carry bit *)
313        RTL.St_op2 (op, destr, RTL.Imm 0, RTL.Imm 0, start_lbl)
314      | _ ->
315        RTL.St_move (destr, RTL.Imm 0, start_lbl) in
316  let insts_rest = List.map f_rest destrs_rest in
317  adds_graph (carry_init @ insts_add @ insts_add_cted @ insts_rest)
318    start_lbl dest_lbl def
319
320let translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def =
321  (* we save those parts of srcrs that could be overwritten *)
322  let save_srcrs a (def, srcrs, init) = match a with
323    | RTL.Reg r when List.mem r destrs ->
324      let (def, new_r) = fresh_reg def in
325      (def, RTL.Reg new_r :: srcrs,
326       adds_graph [RTL.St_move (new_r, a, start_lbl)] :: init)
327    | _ -> (def, a :: srcrs, init) in
328  let (def, fresh_srcrs1, init) =
329    List.fold_right save_srcrs srcrs1 (def, [], []) in
330  let (def, fresh_srcrs2, init) =
331    List.fold_right save_srcrs srcrs2 (def, [], init) in
332  let srcrs1_n = List.length srcrs1 in
333  let srcrs2_n = List.length srcrs2 in
334  let destrs_n = List.length destrs in
335  (* the next must be an invariant *)
336  assert (srcrs1_n = destrs_n && destrs_n = srcrs1_n);
337  (* we pad destrs with itself until we have two times as much
338     registers. The routine should thus handle overflow nicely. *)
339  let all_destrs = MiscPottier.fill destrs (2 * destrs_n) in
340  let init = translate_cst (AST.Cst_int 0) destrs :: init in
341  (* the registries to hold the temporary results of 8-bit mutliplication *)
342  let (def, a) = fresh_reg def in
343  let (def, b) = fresh_reg def in
344  (* when getting the result, this is what is used (padded as necessary) *)
345  let mul_arg k = [RTL.Reg a ; RTL.Reg b] @
346    MiscPottier.make (RTL.Imm 0) (2*destrs_n - k - 2) in
347  (* multiplication between the ith byte of srcrs1 and the jth byte of
348     srcrs2 *)
349  let mul i j =
350    let s1i, s2j = List.nth fresh_srcrs1 i, List.nth fresh_srcrs2 j in
351    (* the position in the result where the resulting bytes must be added *)
352    let k = i + j in
353    let dloc = MiscPottier.sublist all_destrs k (2*destrs_n) in
354    let dloc_arg = List.map (fun r -> RTL.Reg r) dloc in
355    (* we add until the end to propagate the carry bit.
356       At the beginning this will be useless, but we rely on
357       RTL's constant propagation and later dead register elimination
358       to amend that *)
359    [ adds_graph [RTL.St_opaccs (I8051.Mul, a, b, s1i, s2j, start_lbl)] ;
360      translate_op I8051.Add dloc dloc_arg (mul_arg k)] in
361  let insts = List.flatten (List.flatten
362    (MiscPottier.makei (fun i ->
363      MiscPottier.makei (mul i) srcrs2_n) srcrs1_n)) in
364  add_translates (init @ insts) start_lbl dest_lbl def
365
366let translate_divumodu8 order destrs srcr1 srcr2 start_lbl dest_lbl def =
367  match destrs with
368    | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
369    | destr :: destrs ->
370      let (def, dummy) = fresh_reg def in
371      let (destr1, destr2) = if order then (destr, dummy) else (dummy, destr) in
372      let inst_div =
373        adds_graph [RTL.St_opaccs (I8051.DivuModu, destr1, destr2,
374                                   srcr1, srcr2, start_lbl)] in
375      let insts_rest = translate_cst (AST.Cst_int 0) destrs in
376      add_translates [inst_div ; insts_rest] start_lbl dest_lbl def
377
378let translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def =
379  match destrs with
380    | [] -> adds_graph [] start_lbl dest_lbl def
381    | destr :: destrs ->
382      let (def, tmpr) = fresh_reg def in
383      let ((common1, rest1), (common2, rest2)) =
384        MiscPottier.reduce srcrs1 srcrs2 in
385      let rest = choose_rest rest1 rest2 in
386      let firsts = match common1, common2 with
387        | c1hd :: c1tl, c2hd :: c2tl ->
388          let init =
389            RTL.St_op2 (I8051.Xor, destr, c1hd, c2hd, start_lbl) in
390          let f_common tmp_srcr1 tmp_srcr2 =
391            [RTL.St_op2 (I8051.Xor, tmpr, tmp_srcr1, tmp_srcr2, start_lbl) ;
392             RTL.St_op2 (I8051.Or, destr, RTL.Reg destr,
393                         RTL.Reg tmpr, start_lbl)] in
394          let insts_common = List.flatten (List.map2 f_common c1tl c2tl) in
395          init :: insts_common
396        | [], [] ->
397          [RTL.St_move (destr, RTL.Imm 0, start_lbl)]
398        (* common1 and common2 have the same length *)
399        | _ -> assert false in
400      let f_rest tmp_srcr =
401        RTL.St_op2 (I8051.Xor, destr, RTL.Reg destr,
402                    tmp_srcr, start_lbl) in
403      let insts_rest = List.map f_rest rest in
404      let insts = firsts @ insts_rest in
405      let epilogue = translate_cst (AST.Cst_int 0) destrs in
406      add_translates [ adds_graph insts ; epilogue] start_lbl dest_lbl def
407
408(* this requires destrs to be either 0 or 1 to be truly correct
409   to be used after translations that ensure this *)
410let translate_toggle_bool destrs start_lbl =
411  match destrs with
412    | [] -> adds_graph [] start_lbl
413    | destr :: _ ->
414      adds_graph [RTL.St_op2 (I8051.Xor, destr, RTL.Reg destr,
415                              RTL.Imm 1, start_lbl)] start_lbl
416
417let rec pad_with p l1 l2 = match l1, l2 with
418  | [], [] -> ([], [])
419  | x :: xs, y :: ys ->
420    let (xs', ys') = pad_with p xs ys in
421    (x :: xs', y :: ys')
422  | [], _ -> (MiscPottier.make p (List.length l2), l2)
423  | _, [] -> (l1, MiscPottier.make p (List.length l1))
424
425let translate_ltu desrtrs srcrs1 srcrs2 start_lbl dest_lbl def =
426  match desrtrs with
427    | [] -> adds_graph [] start_lbl dest_lbl def
428    | destr :: destrs ->
429      let (srcrs1, srcrs2) = pad_with (RTL.Imm 0) srcrs1 srcrs2 in
430      let init = RTL.St_clear_carry start_lbl in
431      let f srcr1 srcr2 =
432        RTL.St_op2 (I8051.Sub, destr, srcr1, srcr2, start_lbl) in
433      (* not interested in result, just the carry bit
434         the following is safe even if destrs = srcrsi *)
435      let iter_sub = List.map2 f srcrs1 srcrs2 in
436      let extract_carry =
437        [RTL.St_op2 (I8051.Addc, destr, RTL.Imm 0,
438                     RTL.Imm 0, start_lbl)] in
439      let epilogue = translate_cst (AST.Cst_int 0) destrs in
440      add_translates [adds_graph (init :: iter_sub @ extract_carry);
441                      epilogue] start_lbl dest_lbl def
442
443let rec add_128_to_last
444    (last_subst : Register.t)
445    (rs : RTL.argument list)
446    (dummy_lbl : Label.t) = match rs with
447  | [] -> ([], adds_graph [])
448  | [last] ->
449    let insts =
450      [RTL.St_move (last_subst, last, dummy_lbl) ;
451       RTL.St_op2 (I8051.Add, last_subst, RTL.Reg last_subst,
452                   RTL.Imm 128, dummy_lbl)] in
453    ([RTL.Reg last_subst], adds_graph insts)
454  | hd :: tail ->
455    let (tail', trans) = add_128_to_last last_subst tail dummy_lbl in
456    (hd :: tail', trans)
457
458(* Paolo: what happens if srcrs1 and srcrs2 have different length? seems to me
459   128 is added at the wrong place then *)
460let translate_lts destrs srcrs1 srcrs2 start_lbl dest_lbl def =
461  let (def, tmp_last_srcr1) = fresh_reg def in
462  let (def, tmp_last_srcr2) = fresh_reg def in
463  (* I save just the last registers *)
464  let (srcrs1, add_128_to_srcrs1) =
465    add_128_to_last tmp_last_srcr1 srcrs1 start_lbl in
466  let (srcrs2, add_128_to_srcrs2) =
467    add_128_to_last tmp_last_srcr2 srcrs2 start_lbl in
468  add_translates
469    [add_128_to_srcrs1;
470     add_128_to_srcrs2;
471     translate_ltu destrs srcrs1 srcrs2]
472    start_lbl dest_lbl def
473
474
475let translate_op2 op2 destrs srcrs1 srcrs2 start_lbl dest_lbl def =
476  match op2 with
477
478    | AST.Op_add | AST.Op_addp ->
479      translate_op I8051.Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
480
481    | AST.Op_sub | AST.Op_subp | AST.Op_subpp ->
482      translate_op I8051.Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
483
484    | AST.Op_mul ->
485      translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def
486
487    | AST.Op_divu when List.length srcrs1 = 1 && List.length srcrs2 = 1 ->
488      translate_divumodu8 true destrs (List.hd srcrs1) (List.hd srcrs2)
489        start_lbl dest_lbl def
490
491    | AST.Op_modu when List.length srcrs1 = 1 && List.length srcrs2 = 1 ->
492      translate_divumodu8 false destrs (List.hd srcrs1) (List.hd srcrs2)
493        start_lbl dest_lbl def
494
495    | AST.Op_and ->
496      translate_op I8051.And destrs srcrs1 srcrs2 start_lbl dest_lbl def
497
498    | AST.Op_or ->
499      translate_op I8051.Or destrs srcrs1 srcrs2 start_lbl dest_lbl def
500
501    | AST.Op_xor ->
502      translate_op I8051.Xor destrs srcrs1 srcrs2 start_lbl dest_lbl def
503
504    | AST.Op_cmp AST.Cmp_eq
505    | AST.Op_cmpu AST.Cmp_eq
506    | AST.Op_cmpp AST.Cmp_eq ->
507      add_translates
508        [translate_ne destrs srcrs1 srcrs2 ;
509         translate_toggle_bool destrs] start_lbl dest_lbl def
510
511    | AST.Op_cmp AST.Cmp_ne
512    | AST.Op_cmpu AST.Cmp_ne
513    | AST.Op_cmpp AST.Cmp_ne ->
514      translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
515
516    | AST.Op_cmp AST.Cmp_lt ->
517      translate_lts destrs srcrs1 srcrs2 start_lbl dest_lbl def
518
519    | AST.Op_cmpu AST.Cmp_lt | AST.Op_cmpp AST.Cmp_lt ->
520      translate_ltu destrs srcrs1 srcrs2 start_lbl dest_lbl def
521
522    | AST.Op_cmp AST.Cmp_le ->
523      add_translates
524        [translate_lts destrs srcrs2 srcrs1 ;
525         translate_toggle_bool destrs] start_lbl dest_lbl def
526
527    | AST.Op_cmpu AST.Cmp_le | AST.Op_cmpp AST.Cmp_le ->
528      add_translates
529        [translate_ltu destrs srcrs2 srcrs1 ;
530         translate_toggle_bool destrs] start_lbl dest_lbl def
531
532    | AST.Op_cmp AST.Cmp_gt ->
533      translate_lts destrs srcrs2 srcrs1 start_lbl dest_lbl def
534
535    | AST.Op_cmpu AST.Cmp_gt | AST.Op_cmpp AST.Cmp_gt ->
536      translate_ltu destrs srcrs2 srcrs1 start_lbl dest_lbl def
537
538    | AST.Op_cmp AST.Cmp_ge ->
539      add_translates
540        [translate_lts destrs srcrs1 srcrs2 ;
541         translate_toggle_bool destrs] start_lbl dest_lbl def
542
543    | AST.Op_cmpu AST.Cmp_ge | AST.Op_cmpp AST.Cmp_ge ->
544      add_translates
545        [translate_ltu destrs srcrs1 srcrs2 ;
546         translate_toggle_bool destrs] start_lbl dest_lbl def
547
548    | AST.Op_div | AST.Op_divu | AST.Op_modu | AST.Op_mod | AST.Op_shl
549    | AST.Op_shr | AST.Op_shru ->
550      (* Unsupported, should have been replaced by a runtime function. *)
551      assert false
552
553
554let translate_cond srcrs start_lbl lbl_true lbl_false def =
555  match srcrs with
556    | [] -> add_graph start_lbl (RTL.St_skip lbl_false) def
557    | srcr :: srcrs ->
558      let (def, tmpr) = fresh_reg def in
559      let tmp_lbl = fresh_label def in
560      let init = RTL.St_move (tmpr, RTL.Reg srcr, start_lbl) in
561      let f srcr = RTL.St_op2 (I8051.Or, tmpr, RTL.Reg tmpr,
562                               RTL.Reg srcr, start_lbl) in
563      let def = adds_graph (init :: (List.map f srcrs)) start_lbl tmp_lbl def in
564      add_graph tmp_lbl (RTL.St_cond (tmpr, lbl_true, lbl_false)) def
565
566
567let translate_load addr destrs start_lbl dest_lbl def =
568  let (def, tmp_addr) = fresh_regs def 2 in
569  let (tmp_addr1, tmp_addr2) = make_addr tmp_addr in
570  let save_addr a (saves, def, rs) = match a with
571    | RTL.Reg r when List.exists (Register.equal r) destrs ->
572      let (def, tmp) = fresh_reg def in
573      (RTL.St_move (tmp, RTL.Reg r, start_lbl) :: saves, def, RTL.Reg tmp :: rs)
574    | _ as a -> (saves, def, a :: rs) in
575  let (saves, def, addr) = List.fold_right save_addr addr ([], def, []) in
576  let (def, tmpr) = fresh_reg def in
577  let f (translates, off) r =
578    let translates =
579      translates @
580        [translate_op2 AST.Op_addp tmp_addr addr [RTL.Imm off] ;
581         adds_graph [RTL.St_load (r, RTL.Reg tmp_addr1,
582                                  RTL.Reg tmp_addr2, dest_lbl)]] in
583    (translates, off + Driver.TargetArch.int_size) in
584  let (translates, _) = List.fold_left f ([], 0) destrs in
585  add_translates translates start_lbl dest_lbl def
586
587
588let translate_store addr srcrs start_lbl dest_lbl def =
589  let (def, tmp_addr) = fresh_regs def (List.length addr) in
590  let (tmp_addr1, tmp_addr2) = make_addr tmp_addr in
591  let (def, tmpr) = fresh_reg def in
592  let f (translates, off) srcr =
593    let translates =
594      translates @
595        [translate_op2 AST.Op_addp tmp_addr addr [RTL.Imm off] ;
596         adds_graph [RTL.St_store (RTL.Reg tmp_addr1,
597                                   RTL.Reg tmp_addr2, srcr, dest_lbl)]] in
598    (translates, off + Driver.TargetArch.int_size) in
599  let (translates, _) = List.fold_left f ([], 0) srcrs in
600  add_translates translates start_lbl dest_lbl def
601
602
603let translate_stmt lenv lbl stmt def = match stmt with
604
605  | RTLabs.St_skip lbl' ->
606    add_graph lbl (RTL.St_skip lbl') def
607
608  | RTLabs.St_cost (cost_lbl, lbl') ->
609    add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def
610
611  | RTLabs.St_ind_0 (i, lbl') ->
612    add_graph lbl (RTL.St_ind_0 (i, lbl')) def
613
614  | RTLabs.St_ind_inc (i, lbl') ->
615    add_graph lbl (RTL.St_ind_inc (i, lbl')) def
616
617  | RTLabs.St_cst (destr, cst, lbl') ->
618    translate_cst cst (find_local_env_reg destr lenv) lbl lbl' def
619
620  | RTLabs.St_op1 (op1, destr, srcr, lbl') ->
621    translate_op1 op1
622      (find_local_env_reg destr lenv)
623      (List.map (fun r -> RTL.Reg r) (find_local_env_reg srcr lenv))
624      lbl lbl' def
625
626  | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') ->
627    translate_op2 op2 (find_local_env_reg destr lenv)
628      (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) lbl lbl' def
629
630  | RTLabs.St_load (_, addr, destr, lbl') ->
631    translate_load (find_local_env addr lenv) (find_local_env_reg destr lenv)
632      lbl lbl' def
633
634  | RTLabs.St_store (_, addr,  srcr, lbl') ->
635    translate_store (find_local_env addr lenv) (find_local_env srcr lenv)
636      lbl lbl' def
637
638  | RTLabs.St_call_id (f, args, None, _, lbl') ->
639    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv, [], lbl')) def
640
641  | RTLabs.St_call_id (f, args, Some retr, _, lbl') ->
642    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv,
643                                   find_local_env_reg retr lenv, lbl')) def
644
645  | RTLabs.St_call_ptr (f, args, None, _, lbl') ->
646    let (f1, f2) = find_and_addr f lenv in
647    add_graph lbl (RTL.St_call_ptr (f1, f2, rtl_args args lenv, [], lbl')) def
648
649  | RTLabs.St_call_ptr (f, args, Some retr, _, lbl') ->
650    let (f1, f2) = find_and_addr f lenv in
651    add_graph lbl
652      (RTL.St_call_ptr
653         (f1, f2, rtl_args args lenv, find_local_env_reg retr lenv, lbl')) def
654
655  | RTLabs.St_tailcall_id (f, args, _) ->
656    add_graph lbl (RTL.St_tailcall_id (f, rtl_args args lenv)) def
657
658  | RTLabs.St_tailcall_ptr (f, args, _) ->
659    let (f1, f2) = find_and_addr f lenv in
660    add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args lenv)) def
661
662  | RTLabs.St_cond (r, lbl_true, lbl_false) ->
663    translate_cond (find_local_env_reg r lenv) lbl lbl_true lbl_false def
664
665  | RTLabs.St_jumptable _ ->
666    error "Jump tables not supported yet."
667
668  | RTLabs.St_return None ->
669    add_graph lbl (RTL.St_return []) def
670
671  | RTLabs.St_return (Some r) ->
672    add_graph lbl (RTL.St_return (find_local_env r lenv)) def
673
674open BList.Notation
675
676let remove_non_int_immediates def =
677  let load_arg a f = match a with
678    | RTLabs.Imm ((AST.Cst_stack _ | AST.Cst_addrsymbol _) as c, t) ->
679      fresh_t t (fun tmp ->
680      RTLabs.St_cst (tmp, c, Label.dummy) ^:: f (RTLabs.Reg tmp))
681    | _ -> f a in
682  let rec load_args args f = match args with
683    | [] -> f []
684    | a :: args ->
685      load_arg a (fun a -> load_args args (fun l -> f (a :: l))) in
686  let trans lbl = function
687    | RTLabs.St_op2(op, r, a1, a2, l) ->
688      load_arg a1 (fun a1 ->
689        load_arg a2 (fun a2 ->
690          RTLabs.St_op2 (op, r, a1, a2, l) ^:: bnil))
691    | RTLabs.St_store(q, a1, a2, l) ->
692      load_arg a1 (fun a1 ->
693        load_arg a2 (fun a2 ->
694          RTLabs.St_store (q, a1, a2, l) ^:: bnil))
695    | RTLabs.St_load (q, a, r, l) ->
696      load_arg a (fun a ->
697        RTLabs.St_load (q, a, r, l) ^:: bnil)
698    | RTLabs.St_call_id (f, args, ret, s, l) ->
699      load_args args (fun args ->
700        RTLabs.St_call_id (f, args, ret, s, l) ^:: bnil)
701    | RTLabs.St_tailcall_id (f, args, s) ->
702      load_args args (fun args ->
703        RTLabs.St_tailcall_id (f, args, s) ^:: bnil)
704    | RTLabs.St_call_ptr (f, args, ret, s, l) ->
705      load_args args (fun args ->
706        RTLabs.St_call_ptr (f, args, ret, s, l) ^:: bnil)
707    | RTLabs.St_tailcall_ptr (f, args, s) ->
708      load_args args (fun args ->
709        RTLabs.St_tailcall_ptr (f, args, s) ^:: bnil)
710    | RTLabs.St_return (Some a) ->
711      load_arg a (fun a ->
712        RTLabs.St_return (Some a) ^:: bnil)
713    | stmt -> stmt ^:: bnil in
714  let module T = GraphUtilities.Trans(RTLabsGraph)(RTLabsGraph) in
715  let g = def.RTLabs.f_graph in
716  let fresh_reg def t =
717    let r = Register.fresh def.RTLabs.f_runiverse in
718    let locals = (r, t) :: def.RTLabs.f_locals in
719    ({ def with RTLabs.f_locals = locals }, r) in
720  let fresh_lbl () = Label.Gen.fresh def.RTLabs.f_luniverse in
721  let (def, g) = T.translate' fresh_lbl fresh_reg trans def g in
722  { def with RTLabs.f_graph = g }
723 
724let translate_internal def =
725  let def = remove_non_int_immediates def in
726  let runiverse = def.RTLabs.f_runiverse in
727  let lenv =
728    initialize_local_env runiverse
729      (def.RTLabs.f_params @ def.RTLabs.f_locals) def.RTLabs.f_result in
730  let set_of_list l = List.fold_right Register.Set.add l Register.Set.empty in
731  let params = map_list_local_env_reg lenv (List.map fst def.RTLabs.f_params) in
732  let locals = map_list_local_env_reg lenv (List.map fst def.RTLabs.f_locals) in
733  let locals = set_of_list locals in
734  let result = match def.RTLabs.f_result with
735    | None -> []
736    | Some (r, _) -> find_local_env_reg r lenv in
737  let res =
738    { RTL.f_luniverse = def.RTLabs.f_luniverse ;
739      RTL.f_runiverse = runiverse ;
740      RTL.f_result    = result ;
741      RTL.f_params    = params ;
742      RTL.f_locals    = locals ;
743      RTL.f_stacksize = concrete_size def.RTLabs.f_stacksize ;
744      RTL.f_graph     = Label.Map.empty ;
745      RTL.f_entry     = def.RTLabs.f_entry ;
746      RTL.f_exit      = def.RTLabs.f_exit } in
747  Label.Map.fold (translate_stmt lenv) def.RTLabs.f_graph res
748
749
750let translate_fun_def = function
751  | RTLabs.F_int def -> RTL.F_int (translate_internal def)
752  | RTLabs.F_ext def -> RTL.F_ext def
753
754
755let translate p =
756  let f_global (id, size) = (id, concrete_size size) in
757  let f_funct (id, fun_def) = (id, translate_fun_def fun_def) in
758  { RTL.vars   = List.map f_global p.RTLabs.vars ;
759    RTL.functs = List.map f_funct p.RTLabs.functs ;
760    RTL.main   = p.RTLabs.main }
Note: See TracBrowser for help on using the repository browser.