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

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