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

Last change on this file since 1584 was 1584, checked in by tranquil, 8 years ago
  • new form of translation written in graphUtilites (mainly as a test before implementation in Matita)
  • rewritten multiplication in RTLasbToRTL
File size: 28.1 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        let f destr srcr1 srcr2 (op, insts) =
297          (I8051.Addc, f_add op destr srcr1 srcr2 :: insts) in
298        snd (MiscPottier.fold3_right
299          f destrs_common srcrs1_common srcrs2_common (I8051.Add, []))
300      | _ ->
301        (* we just do the same operation on all *)
302        MiscPottier.map3 (f_add op) destrs_common srcrs1_common srcrs2_common in
303  let f_add_cted destr srcr =
304    RTL.St_op2 (op, destr, srcr, RTL.Imm 0, start_lbl) in
305  let insts_add_cted = List.map2 f_add_cted destrs_cted srcrs_cted in
306  let f_rest destr =
307    match op with
308      | I8051.Addc | I8051.Sub ->
309        (* propagate carry bit *)
310        RTL.St_op2 (op, destr, RTL.Imm 0, RTL.Imm 0, start_lbl)
311      | _ ->
312        RTL.St_move (destr, RTL.Imm 0, start_lbl) in
313  let insts_rest = List.map f_rest destrs_rest in
314  adds_graph (carry_init @ insts_add @ insts_add_cted @ insts_rest)
315    start_lbl dest_lbl def
316
317let translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def =
318  (* we save those parts of srcrs that could be overwritten *)
319  let save_srcrs a (def, srcrs, init) = match a with
320    | RTL.Reg r when List.mem r destrs ->
321      let (def, new_r) = fresh_reg def in
322      (def, RTL.Reg new_r :: srcrs,
323       adds_graph [RTL.St_move (new_r, a, start_lbl)] :: init)
324    | _ -> (def, a :: srcrs, init) in
325  let (def, fresh_srcrs1, init) =
326    List.fold_right save_srcrs srcrs1 (def, [], []) in
327  let (def, fresh_srcrs2, init) =
328    List.fold_right save_srcrs srcrs2 (def, [], init) in
329  let srcrs1_n = List.length srcrs1 in
330  let srcrs2_n = List.length srcrs2 in
331  let destrs_n = List.length destrs in
332  (* the next must be an invariant *)
333  assert (srcrs1_n = destrs_n && destrs_n = srcrs1_n);
334  (* we pad destrs with a copy of itself that will be added to it at the end
335     (when the multiplication overflows) and then three more. The routine
336     should thus handle overflow nicely, but it must be checked *)
337  let all_destrs = MiscPottier.fill destrs (2 * destrs_n + 3) in
338  let init = translate_cst (AST.Cst_int 0) destrs :: init in
339  (* the registries to hold the temporary results of 8-bit mutliplication *)
340  let (def, a) = fresh_reg def in
341  let (def, b) = fresh_reg def in
342  (* when getting the result, this is what is used (padded to 3 bytes *)
343  let mul_arg = [RTL.Reg a ; RTL.Reg b ; RTL.Imm 0] in
344  let mul i j =
345    let s1i, s2j = List.nth fresh_srcrs1 i, List.nth fresh_srcrs2 i in
346    let k = i + j in
347    let dloc = MiscPottier.sublist all_destrs k (k+3) in
348    let dloc_arg = List.map (fun r -> RTL.Reg r) dloc in
349    [ adds_graph [RTL.St_opaccs (I8051.Mul, a, b, s1i, s2j, start_lbl)] ;
350      translate_op I8051.Add dloc dloc_arg mul_arg ] in
351  let insts = List.flatten (List.flatten
352    (MiscPottier.makei (fun i ->
353      MiscPottier.makei (mul i) srcrs2_n) srcrs1_n)) in
354  add_translates (init @ insts) start_lbl dest_lbl def
355
356let translate_divumodu8 order destrs srcr1 srcr2 start_lbl dest_lbl def =
357  match destrs with
358    | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
359    | destr :: destrs ->
360      let (def, dummy) = fresh_reg def in
361      let (destr1, destr2) = if order then (destr, dummy) else (dummy, destr) in
362      let inst_div =
363        adds_graph [RTL.St_opaccs (I8051.DivuModu, destr1, destr2,
364                                   srcr1, srcr2, start_lbl)] in
365      let insts_rest = translate_cst (AST.Cst_int 0) destrs in
366      add_translates [inst_div ; insts_rest] start_lbl dest_lbl def
367
368let translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def =
369  match destrs with
370    | [] -> adds_graph [] start_lbl dest_lbl def
371    | destr :: destrs ->
372      let (def, tmpr) = fresh_reg def in
373      let ((common1, rest1), (common2, rest2)) =
374        MiscPottier.reduce srcrs1 srcrs2 in
375      let rest = choose_rest rest1 rest2 in
376      let firsts = match common1, common2 with
377        | c1hd :: c1tl, c2hd :: c2tl ->
378          let init =
379            RTL.St_op2 (I8051.Xor, destr, c1hd, c2hd, start_lbl) in
380          let f_common tmp_srcr1 tmp_srcr2 =
381            [RTL.St_op2 (I8051.Xor, tmpr, tmp_srcr1, tmp_srcr2, start_lbl) ;
382             RTL.St_op2 (I8051.Or, destr, RTL.Reg destr,
383                         RTL.Reg tmpr, start_lbl)] in
384          let insts_common = List.flatten (List.map2 f_common c1tl c2tl) in
385          init :: insts_common
386        | [], [] ->
387          [RTL.St_move (destr, RTL.Imm 0, start_lbl)]
388        (* common1 and common2 have the same length *)
389        | _ -> assert false in
390      let f_rest tmp_srcr =
391        RTL.St_op2 (I8051.Xor, destr, RTL.Reg destr,
392                    tmp_srcr, start_lbl) in
393      let insts_rest = List.map f_rest rest in
394      let insts = firsts @ insts_rest in
395      let epilogue = translate_cst (AST.Cst_int 0) destrs in
396      add_translates [ adds_graph insts ; epilogue] start_lbl dest_lbl def
397
398(* this requires destrs to be either 0 or 1 to be truly correct
399   to be used after translations that ensure this *)
400let translate_toggle_bool destrs start_lbl =
401  match destrs with
402    | [] -> adds_graph [] start_lbl
403    | destr :: _ ->
404      adds_graph [RTL.St_op2 (I8051.Xor, destr, RTL.Reg destr,
405                              RTL.Imm 1, start_lbl)] start_lbl
406
407let rec pad_with p l1 l2 = match l1, l2 with
408  | [], [] -> ([], [])
409  | x :: xs, y :: ys ->
410    let (xs', ys') = pad_with p xs ys in
411    (x :: xs', y :: ys')
412  | [], _ -> (MiscPottier.make p (List.length l2), l2)
413  | _, [] -> (l1, MiscPottier.make p (List.length l1))
414
415let translate_ltu desrtrs srcrs1 srcrs2 start_lbl dest_lbl def =
416  match desrtrs with
417    | [] -> adds_graph [] start_lbl dest_lbl def
418    | destr :: destrs ->
419      let (srcrs1, srcrs2) = pad_with (RTL.Imm 0) srcrs1 srcrs2 in
420      let init = RTL.St_clear_carry start_lbl in
421      let f srcr1 srcr2 =
422        RTL.St_op2 (I8051.Sub, destr, srcr1, srcr2, start_lbl) in
423      (* not interested in result, just the carry bit
424         the following is safe even if destrs = srcrsi *)
425      let iter_sub = List.map2 f srcrs1 srcrs2 in
426      let extract_carry =
427        [RTL.St_op2 (I8051.Addc, destr, RTL.Imm 0,
428                     RTL.Imm 0, start_lbl)] in
429      let epilogue = translate_cst (AST.Cst_int 0) destrs in
430      add_translates [adds_graph (init :: iter_sub @ extract_carry);
431                      epilogue] start_lbl dest_lbl def
432
433let rec add_128_to_last
434    (last_subst : Register.t)
435    (rs : RTL.argument list)
436    (dummy_lbl : Label.t) = match rs with
437  | [] -> ([], adds_graph [])
438  | [last] ->
439    let insts =
440      [RTL.St_move (last_subst, last, dummy_lbl) ;
441       RTL.St_op2 (I8051.Add, last_subst, RTL.Reg last_subst,
442                   RTL.Imm 128, dummy_lbl)] in
443    ([RTL.Reg last_subst], adds_graph insts)
444  | hd :: tail ->
445    let (tail', trans) = add_128_to_last last_subst tail dummy_lbl in
446    (hd :: tail', trans)
447
448(* Paolo: what happens if srcrs1 and srcrs2 have different length? seems to me
449   128 is added at the wrong place then *)
450let translate_lts destrs srcrs1 srcrs2 start_lbl dest_lbl def =
451  let (def, tmp_last_srcr1) = fresh_reg def in
452  let (def, tmp_last_srcr2) = fresh_reg def in
453  (* I save just the last registers *)
454  let (srcrs1, add_128_to_srcrs1) =
455    add_128_to_last tmp_last_srcr1 srcrs1 start_lbl in
456  let (srcrs2, add_128_to_srcrs2) =
457    add_128_to_last tmp_last_srcr2 srcrs2 start_lbl in
458  add_translates
459    [add_128_to_srcrs1;
460     add_128_to_srcrs2;
461     translate_ltu destrs srcrs1 srcrs2]
462    start_lbl dest_lbl def
463
464
465let translate_op2 op2 destrs srcrs1 srcrs2 start_lbl dest_lbl def =
466  match op2 with
467
468    | AST.Op_add | AST.Op_addp ->
469      translate_op I8051.Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
470
471    | AST.Op_sub | AST.Op_subp | AST.Op_subpp ->
472      translate_op I8051.Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
473
474    | AST.Op_mul ->
475      translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def
476
477    | AST.Op_divu when List.length srcrs1 = 1 && List.length srcrs2 = 1 ->
478      translate_divumodu8 true destrs (List.hd srcrs1) (List.hd srcrs2)
479        start_lbl dest_lbl def
480
481    | AST.Op_modu when List.length srcrs1 = 1 && List.length srcrs2 = 1 ->
482      translate_divumodu8 false destrs (List.hd srcrs1) (List.hd srcrs2)
483        start_lbl dest_lbl def
484
485    | AST.Op_and ->
486      translate_op I8051.And destrs srcrs1 srcrs2 start_lbl dest_lbl def
487
488    | AST.Op_or ->
489      translate_op I8051.Or destrs srcrs1 srcrs2 start_lbl dest_lbl def
490
491    | AST.Op_xor ->
492      translate_op I8051.Xor destrs srcrs1 srcrs2 start_lbl dest_lbl def
493
494    | AST.Op_cmp AST.Cmp_eq
495    | AST.Op_cmpu AST.Cmp_eq
496    | AST.Op_cmpp AST.Cmp_eq ->
497      add_translates
498        [translate_ne destrs srcrs1 srcrs2 ;
499         translate_toggle_bool destrs] start_lbl dest_lbl def
500
501    | AST.Op_cmp AST.Cmp_ne
502    | AST.Op_cmpu AST.Cmp_ne
503    | AST.Op_cmpp AST.Cmp_ne ->
504      translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
505
506    | AST.Op_cmp AST.Cmp_lt ->
507      translate_lts destrs srcrs1 srcrs2 start_lbl dest_lbl def
508
509    | AST.Op_cmpu AST.Cmp_lt | AST.Op_cmpp AST.Cmp_lt ->
510      translate_ltu destrs srcrs1 srcrs2 start_lbl dest_lbl def
511
512    | AST.Op_cmp AST.Cmp_le ->
513      add_translates
514        [translate_lts destrs srcrs2 srcrs1 ;
515         translate_toggle_bool destrs] start_lbl dest_lbl def
516
517    | AST.Op_cmpu AST.Cmp_le | AST.Op_cmpp AST.Cmp_le ->
518      add_translates
519        [translate_ltu destrs srcrs2 srcrs1 ;
520         translate_toggle_bool destrs] start_lbl dest_lbl def
521
522    | AST.Op_cmp AST.Cmp_gt ->
523      translate_lts destrs srcrs2 srcrs1 start_lbl dest_lbl def
524
525    | AST.Op_cmpu AST.Cmp_gt | AST.Op_cmpp AST.Cmp_gt ->
526      translate_ltu destrs srcrs2 srcrs1 start_lbl dest_lbl def
527
528    | AST.Op_cmp AST.Cmp_ge ->
529      add_translates
530        [translate_lts destrs srcrs1 srcrs2 ;
531         translate_toggle_bool destrs] start_lbl dest_lbl def
532
533    | AST.Op_cmpu AST.Cmp_ge | AST.Op_cmpp AST.Cmp_ge ->
534      add_translates
535        [translate_ltu destrs srcrs1 srcrs2 ;
536         translate_toggle_bool destrs] start_lbl dest_lbl def
537
538    | AST.Op_div | AST.Op_divu | AST.Op_modu | AST.Op_mod | AST.Op_shl
539    | AST.Op_shr | AST.Op_shru ->
540      (* Unsupported, should have been replaced by a runtime function. *)
541      assert false
542
543
544let translate_cond srcrs start_lbl lbl_true lbl_false def =
545  match srcrs with
546    | [] -> add_graph start_lbl (RTL.St_skip lbl_false) def
547    | srcr :: srcrs ->
548      let (def, tmpr) = fresh_reg def in
549      let tmp_lbl = fresh_label def in
550      let init = RTL.St_move (tmpr, RTL.Reg srcr, start_lbl) in
551      let f srcr = RTL.St_op2 (I8051.Or, tmpr, RTL.Reg tmpr,
552                               RTL.Reg srcr, start_lbl) in
553      let def = adds_graph (init :: (List.map f srcrs)) start_lbl tmp_lbl def in
554      add_graph tmp_lbl (RTL.St_cond (tmpr, lbl_true, lbl_false)) def
555
556
557let translate_load addr destrs start_lbl dest_lbl def =
558  let (def, tmp_addr) = fresh_regs def 2 in
559  let (tmp_addr1, tmp_addr2) = make_addr tmp_addr in
560  let save_addr a (saves, def, rs) = match a with
561    | RTL.Reg r when List.exists (Register.equal r) destrs ->
562      let (def, tmp) = fresh_reg def in
563      (RTL.St_move (tmp, RTL.Reg r, start_lbl) :: saves, def, RTL.Reg tmp :: rs)
564    | _ as a -> (saves, def, a :: rs) in
565  let (saves, def, addr) = List.fold_right save_addr addr ([], def, []) in
566  let (def, tmpr) = fresh_reg def in
567  let f (translates, off) r =
568    let translates =
569      translates @
570        [translate_op2 AST.Op_addp tmp_addr addr [RTL.Imm off] ;
571         adds_graph [RTL.St_load (r, RTL.Reg tmp_addr1,
572                                  RTL.Reg tmp_addr2, dest_lbl)]] in
573    (translates, off + Driver.TargetArch.int_size) in
574  let (translates, _) = List.fold_left f ([], 0) destrs in
575  add_translates translates start_lbl dest_lbl def
576
577
578let translate_store addr srcrs start_lbl dest_lbl def =
579  let (def, tmp_addr) = fresh_regs def (List.length addr) in
580  let (tmp_addr1, tmp_addr2) = make_addr tmp_addr in
581  let (def, tmpr) = fresh_reg def in
582  let f (translates, off) srcr =
583    let translates =
584      translates @
585        [translate_op2 AST.Op_addp tmp_addr addr [RTL.Imm off] ;
586         adds_graph [RTL.St_store (RTL.Reg tmp_addr1,
587                                   RTL.Reg tmp_addr2, srcr, dest_lbl)]] in
588    (translates, off + Driver.TargetArch.int_size) in
589  let (translates, _) = List.fold_left f ([], 0) srcrs in
590  add_translates translates start_lbl dest_lbl def
591
592
593let translate_stmt lenv lbl stmt def = match stmt with
594
595  | RTLabs.St_skip lbl' ->
596    add_graph lbl (RTL.St_skip lbl') def
597
598  | RTLabs.St_cost (cost_lbl, lbl') ->
599    add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def
600
601  | RTLabs.St_ind_0 (i, lbl') ->
602    add_graph lbl (RTL.St_ind_0 (i, lbl')) def
603
604  | RTLabs.St_ind_inc (i, lbl') ->
605    add_graph lbl (RTL.St_ind_inc (i, lbl')) def
606
607  | RTLabs.St_cst (destr, cst, lbl') ->
608    translate_cst cst (find_local_env_reg destr lenv) lbl lbl' def
609
610  | RTLabs.St_op1 (op1, destr, srcr, lbl') ->
611    translate_op1 op1
612      (find_local_env_reg destr lenv)
613      (List.map (fun r -> RTL.Reg r) (find_local_env_reg srcr lenv))
614      lbl lbl' def
615
616  | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') ->
617    translate_op2 op2 (find_local_env_reg destr lenv)
618      (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) lbl lbl' def
619
620  | RTLabs.St_load (_, addr, destr, lbl') ->
621    translate_load (find_local_env addr lenv) (find_local_env_reg destr lenv)
622      lbl lbl' def
623
624  | RTLabs.St_store (_, addr,  srcr, lbl') ->
625    translate_store (find_local_env addr lenv) (find_local_env srcr lenv)
626      lbl lbl' def
627
628  | RTLabs.St_call_id (f, args, None, _, lbl') ->
629    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv, [], lbl')) def
630
631  | RTLabs.St_call_id (f, args, Some retr, _, lbl') ->
632    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv,
633                                   find_local_env_reg retr lenv, lbl')) def
634
635  | RTLabs.St_call_ptr (f, args, None, _, lbl') ->
636    let (f1, f2) = find_and_addr f lenv in
637    add_graph lbl (RTL.St_call_ptr (f1, f2, rtl_args args lenv, [], lbl')) def
638
639  | RTLabs.St_call_ptr (f, args, Some retr, _, lbl') ->
640    let (f1, f2) = find_and_addr f lenv in
641    add_graph lbl
642      (RTL.St_call_ptr
643         (f1, f2, rtl_args args lenv, find_local_env_reg retr lenv, lbl')) def
644
645  | RTLabs.St_tailcall_id (f, args, _) ->
646    add_graph lbl (RTL.St_tailcall_id (f, rtl_args args lenv)) def
647
648  | RTLabs.St_tailcall_ptr (f, args, _) ->
649    let (f1, f2) = find_and_addr f lenv in
650    add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args lenv)) def
651
652  | RTLabs.St_cond (r, lbl_true, lbl_false) ->
653    translate_cond (find_local_env_reg r lenv) lbl lbl_true lbl_false def
654
655  | RTLabs.St_jumptable _ ->
656    error "Jump tables not supported yet."
657
658  | RTLabs.St_return None ->
659    add_graph lbl (RTL.St_return []) def
660
661  | RTLabs.St_return (Some r) ->
662    add_graph lbl (RTL.St_return (find_local_env r lenv)) def
663
664open BList.Notation
665
666let remove_non_int_immediates def =
667  let load_arg a f = match a with
668    | RTLabs.Imm ((AST.Cst_stack _ | AST.Cst_addrsymbol _) as c, t) ->
669      fresh_t t (fun tmp ->
670      RTLabs.St_cst (tmp, c, Label.dummy) ^:: f (RTLabs.Reg tmp))
671    | _ -> f a in
672  let rec load_args args f = match args with
673    | [] -> f []
674    | a :: args ->
675      load_arg a (fun a -> load_args args (fun l -> f (a :: l))) in
676  let trans lbl = function
677    | RTLabs.St_op2(op, r, a1, a2, l) ->
678      load_arg a1 (fun a1 ->
679        load_arg a2 (fun a2 ->
680          RTLabs.St_op2 (op, r, a1, a2, l) ^:: bnil))
681    | RTLabs.St_store(q, a1, a2, l) ->
682      load_arg a1 (fun a1 ->
683        load_arg a2 (fun a2 ->
684          RTLabs.St_store (q, a1, a2, l) ^:: bnil))
685    | RTLabs.St_load (q, a, r, l) ->
686      load_arg a (fun a ->
687        RTLabs.St_load (q, a, r, l) ^:: bnil)
688    | RTLabs.St_call_id (f, args, ret, s, l) ->
689      load_args args (fun args ->
690        RTLabs.St_call_id (f, args, ret, s, l) ^:: bnil)
691    | RTLabs.St_tailcall_id (f, args, s) ->
692      load_args args (fun args ->
693        RTLabs.St_tailcall_id (f, args, s) ^:: bnil)
694    | RTLabs.St_call_ptr (f, args, ret, s, l) ->
695      load_args args (fun args ->
696        RTLabs.St_call_ptr (f, args, ret, s, l) ^:: bnil)
697    | RTLabs.St_tailcall_ptr (f, args, s) ->
698      load_args args (fun args ->
699        RTLabs.St_tailcall_ptr (f, args, s) ^:: bnil)
700    | RTLabs.St_return (Some a) ->
701      load_arg a (fun a ->
702        RTLabs.St_return (Some a) ^:: bnil)
703    | stmt -> stmt ^:: bnil in
704  let module T = GraphUtilities.Trans(RTLabsGraph)(RTLabsGraph) in
705  let g = def.RTLabs.f_graph in
706  let fresh_reg def t =
707    let r = Register.fresh def.RTLabs.f_runiverse in
708    let locals = (r, t) :: def.RTLabs.f_locals in
709    ({ def with RTLabs.f_locals = locals }, r) in
710  let fresh_lbl () = Label.Gen.fresh def.RTLabs.f_luniverse in
711  let (def, g) = T.translate' fresh_lbl fresh_reg trans def g in
712  { def with RTLabs.f_graph = g }
713 
714let translate_internal def =
715  let def = remove_non_int_immediates def in
716  let runiverse = def.RTLabs.f_runiverse in
717  let lenv =
718    initialize_local_env runiverse
719      (def.RTLabs.f_params @ def.RTLabs.f_locals) def.RTLabs.f_result in
720  let set_of_list l = List.fold_right Register.Set.add l Register.Set.empty in
721  let params = map_list_local_env_reg lenv (List.map fst def.RTLabs.f_params) in
722  let locals = map_list_local_env_reg lenv (List.map fst def.RTLabs.f_locals) in
723  let locals = set_of_list locals in
724  let result = match def.RTLabs.f_result with
725    | None -> []
726    | Some (r, _) -> find_local_env_reg r lenv in
727  let res =
728    { RTL.f_luniverse = def.RTLabs.f_luniverse ;
729      RTL.f_runiverse = runiverse ;
730      RTL.f_result    = result ;
731      RTL.f_params    = params ;
732      RTL.f_locals    = locals ;
733      RTL.f_stacksize = concrete_size def.RTLabs.f_stacksize ;
734      RTL.f_graph     = Label.Map.empty ;
735      RTL.f_entry     = def.RTLabs.f_entry ;
736      RTL.f_exit      = def.RTLabs.f_exit } in
737  Label.Map.fold (translate_stmt lenv) def.RTLabs.f_graph res
738
739
740let translate_fun_def = function
741  | RTLabs.F_int def -> RTL.F_int (translate_internal def)
742  | RTLabs.F_ext def -> RTL.F_ext def
743
744
745let translate p =
746  let f_global (id, size) = (id, concrete_size size) in
747  let f_funct (id, fun_def) = (id, translate_fun_def fun_def) in
748  { RTL.vars   = List.map f_global p.RTLabs.vars ;
749    RTL.functs = List.map f_funct p.RTLabs.functs ;
750    RTL.main   = p.RTLabs.main }
Note: See TracBrowser for help on using the repository browser.