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

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