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

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