source: Deliverables/D2.2/8051-toolstick/src/RTLabs/RTLabsToRTL.ml @ 2321

Last change on this file since 2321 was 2321, checked in by campbell, 9 years ago

Add toolstick branch of the prototype.

File size: 29.0 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      (* Set the carry flag if >0, then dump that in the destination *)
425      let squash_result =
426        [RTL.St_op2 (I8051.Add, destr, RTL.Reg destr, RTL.Imm 255, start_lbl);
427         RTL.St_op2 (I8051.Addc, destr, RTL.Imm 0, RTL.Imm 0, start_lbl)] in
428      let epilogue = translate_cst (AST.Cst_int 0) destrs in
429      add_translates [ adds_graph (insts @ squash_result); epilogue]
430        start_lbl dest_lbl def
431
432(* this requires destrs to be either 0 or 1 to be truly correct
433   to be used after translations that ensure this *)
434let translate_toggle_bool destrs start_lbl =
435  match destrs with
436    | [] -> adds_graph [] start_lbl
437    | destr :: _ ->
438      adds_graph [RTL.St_op2 (I8051.Xor, destr, RTL.Reg destr,
439                              RTL.Imm 1, start_lbl)] start_lbl
440
441let rec pad_with p l1 l2 = match l1, l2 with
442  | [], [] -> ([], [])
443  | x :: xs, y :: ys ->
444    let (xs', ys') = pad_with p xs ys in
445    (x :: xs', y :: ys')
446  | [], _ -> (MiscPottier.make p (List.length l2), l2)
447  | _, [] -> (l1, MiscPottier.make p (List.length l1))
448
449let translate_ltu desrtrs srcrs1 srcrs2 start_lbl dest_lbl def =
450  match desrtrs with
451    | [] -> adds_graph [] start_lbl dest_lbl def
452    | destr :: destrs ->
453      let (srcrs1, srcrs2) = pad_with (RTL.Imm 0) srcrs1 srcrs2 in
454      let init = RTL.St_clear_carry start_lbl in
455      let f srcr1 srcr2 =
456        RTL.St_op2 (I8051.Sub, destr, srcr1, srcr2, start_lbl) in
457      (* not interested in result, just the carry bit
458         the following is safe even if destrs = srcrsi *)
459      let iter_sub = List.map2 f srcrs1 srcrs2 in
460      let extract_carry =
461        [RTL.St_op2 (I8051.Addc, destr, RTL.Imm 0,
462                     RTL.Imm 0, start_lbl)] in
463      let epilogue = translate_cst (AST.Cst_int 0) destrs in
464      add_translates [adds_graph (init :: iter_sub @ extract_carry);
465                      epilogue] start_lbl dest_lbl def
466
467let rec add_128_to_last
468    (last_subst : Register.t)
469    (rs : RTL.argument list)
470    (dummy_lbl : Label.t) = match rs with
471  | [] -> ([], adds_graph [])
472  | [last] ->
473    let insts =
474      [RTL.St_move (last_subst, last, dummy_lbl) ;
475       RTL.St_op2 (I8051.Add, last_subst, RTL.Reg last_subst,
476                   RTL.Imm 128, dummy_lbl)] in
477    ([RTL.Reg last_subst], adds_graph insts)
478  | hd :: tail ->
479    let (tail', trans) = add_128_to_last last_subst tail dummy_lbl in
480    (hd :: tail', trans)
481
482(* Paolo: what happens if srcrs1 and srcrs2 have different length? seems to me
483   128 is added at the wrong place then *)
484let translate_lts destrs srcrs1 srcrs2 start_lbl dest_lbl def =
485  let (def, tmp_last_srcr1) = fresh_reg def in
486  let (def, tmp_last_srcr2) = fresh_reg def in
487  (* I save just the last registers *)
488  let (srcrs1, add_128_to_srcrs1) =
489    add_128_to_last tmp_last_srcr1 srcrs1 start_lbl in
490  let (srcrs2, add_128_to_srcrs2) =
491    add_128_to_last tmp_last_srcr2 srcrs2 start_lbl in
492  add_translates
493    [add_128_to_srcrs1;
494     add_128_to_srcrs2;
495     translate_ltu destrs srcrs1 srcrs2]
496    start_lbl dest_lbl def
497
498
499let translate_op2 op2 destrs srcrs1 srcrs2 start_lbl dest_lbl def =
500  match op2 with
501
502    | AST.Op_add | AST.Op_addp ->
503      translate_op I8051.Add destrs srcrs1 srcrs2 start_lbl dest_lbl def
504
505    | AST.Op_sub | AST.Op_subp | AST.Op_subpp ->
506      translate_op I8051.Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
507
508    | AST.Op_mul ->
509      translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def
510
511    | AST.Op_divu when List.length srcrs1 = 1 && List.length srcrs2 = 1 ->
512      translate_divumodu8 true destrs (List.hd srcrs1) (List.hd srcrs2)
513        start_lbl dest_lbl def
514
515    | AST.Op_modu when List.length srcrs1 = 1 && List.length srcrs2 = 1 ->
516      translate_divumodu8 false destrs (List.hd srcrs1) (List.hd srcrs2)
517        start_lbl dest_lbl def
518
519    | AST.Op_and ->
520      translate_op I8051.And destrs srcrs1 srcrs2 start_lbl dest_lbl def
521
522    | AST.Op_or ->
523      translate_op I8051.Or destrs srcrs1 srcrs2 start_lbl dest_lbl def
524
525    | AST.Op_xor ->
526      translate_op I8051.Xor destrs srcrs1 srcrs2 start_lbl dest_lbl def
527
528    | AST.Op_cmp AST.Cmp_eq
529    | AST.Op_cmpu AST.Cmp_eq
530    | AST.Op_cmpp AST.Cmp_eq ->
531      add_translates
532        [translate_ne destrs srcrs1 srcrs2 ;
533         translate_toggle_bool destrs] start_lbl dest_lbl def
534
535    | AST.Op_cmp AST.Cmp_ne
536    | AST.Op_cmpu AST.Cmp_ne
537    | AST.Op_cmpp AST.Cmp_ne ->
538      translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
539
540    | AST.Op_cmp AST.Cmp_lt ->
541      translate_lts destrs srcrs1 srcrs2 start_lbl dest_lbl def
542
543    | AST.Op_cmpu AST.Cmp_lt | AST.Op_cmpp AST.Cmp_lt ->
544      translate_ltu destrs srcrs1 srcrs2 start_lbl dest_lbl def
545
546    | AST.Op_cmp AST.Cmp_le ->
547      add_translates
548        [translate_lts destrs srcrs2 srcrs1 ;
549         translate_toggle_bool destrs] start_lbl dest_lbl def
550
551    | AST.Op_cmpu AST.Cmp_le | AST.Op_cmpp AST.Cmp_le ->
552      add_translates
553        [translate_ltu destrs srcrs2 srcrs1 ;
554         translate_toggle_bool destrs] start_lbl dest_lbl def
555
556    | AST.Op_cmp AST.Cmp_gt ->
557      translate_lts destrs srcrs2 srcrs1 start_lbl dest_lbl def
558
559    | AST.Op_cmpu AST.Cmp_gt | AST.Op_cmpp AST.Cmp_gt ->
560      translate_ltu destrs srcrs2 srcrs1 start_lbl dest_lbl def
561
562    | AST.Op_cmp AST.Cmp_ge ->
563      add_translates
564        [translate_lts destrs srcrs1 srcrs2 ;
565         translate_toggle_bool destrs] start_lbl dest_lbl def
566
567    | AST.Op_cmpu AST.Cmp_ge | AST.Op_cmpp AST.Cmp_ge ->
568      add_translates
569        [translate_ltu destrs srcrs1 srcrs2 ;
570         translate_toggle_bool destrs] start_lbl dest_lbl def
571
572    | AST.Op_div | AST.Op_divu | AST.Op_modu | AST.Op_mod | AST.Op_shl
573    | AST.Op_shr | AST.Op_shru ->
574      (* Unsupported, should have been replaced by a runtime function. *)
575      assert false
576
577
578let translate_cond srcrs start_lbl lbl_true lbl_false def =
579  match srcrs with
580    | [] -> add_graph start_lbl (RTL.St_skip lbl_false) def
581    | srcr :: srcrs ->
582      let (def, tmpr) = fresh_reg def in
583      let tmp_lbl = fresh_label def in
584      let init = RTL.St_move (tmpr, RTL.Reg srcr, start_lbl) in
585      let f srcr = RTL.St_op2 (I8051.Or, tmpr, RTL.Reg tmpr,
586                               RTL.Reg srcr, start_lbl) in
587      let def = adds_graph (init :: (List.map f srcrs)) start_lbl tmp_lbl def in
588      add_graph tmp_lbl (RTL.St_cond (tmpr, lbl_true, lbl_false)) def
589
590
591let translate_load addr destrs start_lbl dest_lbl def =
592  let (def, tmp_addr) = fresh_regs def 2 in
593  let (tmp_addr1, tmp_addr2) = make_addr tmp_addr in
594  let save_addr a (saves, def, rs) = match a with
595    | RTL.Reg r when List.exists (Register.equal r) destrs ->
596      let (def, tmp) = fresh_reg def in
597      (RTL.St_move (tmp, RTL.Reg r, start_lbl) :: saves, def, RTL.Reg tmp :: rs)
598    | _ as a -> (saves, def, a :: rs) in
599  let (saves, def, addr) = List.fold_right save_addr addr ([], def, []) in
600  let (def, tmpr) = fresh_reg def in
601  let f (translates, off) r =
602    let translates =
603      translates @
604        [translate_op2 AST.Op_addp tmp_addr addr [RTL.Imm off] ;
605         adds_graph [RTL.St_load (r, RTL.Reg tmp_addr1,
606                                  RTL.Reg tmp_addr2, dest_lbl)]] in
607    (translates, off + Driver.TargetArch.int_size) in
608  let (translates, _) = List.fold_left f ([], 0) destrs in
609  add_translates translates start_lbl dest_lbl def
610
611
612let translate_store addr srcrs start_lbl dest_lbl def =
613  let (def, tmp_addr) = fresh_regs def (List.length addr) in
614  let (tmp_addr1, tmp_addr2) = make_addr tmp_addr in
615  let (def, tmpr) = fresh_reg def in
616  let f (translates, off) srcr =
617    let translates =
618      translates @
619        [translate_op2 AST.Op_addp tmp_addr addr [RTL.Imm off] ;
620         adds_graph [RTL.St_store (RTL.Reg tmp_addr1,
621                                   RTL.Reg tmp_addr2, srcr, dest_lbl)]] in
622    (translates, off + Driver.TargetArch.int_size) in
623  let (translates, _) = List.fold_left f ([], 0) srcrs in
624  add_translates translates start_lbl dest_lbl def
625
626
627let translate_stmt lenv lbl stmt def = match stmt with
628
629  | RTLabs.St_skip lbl' ->
630    add_graph lbl (RTL.St_skip lbl') def
631
632  | RTLabs.St_cost (cost_lbl, lbl') ->
633    add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def
634
635  | RTLabs.St_ind_0 (i, lbl') ->
636    add_graph lbl (RTL.St_ind_0 (i, lbl')) def
637
638  | RTLabs.St_ind_inc (i, lbl') ->
639    add_graph lbl (RTL.St_ind_inc (i, lbl')) def
640
641  | RTLabs.St_cst (destr, cst, lbl') ->
642    translate_cst cst (find_local_env_reg destr lenv) lbl lbl' def
643
644  | RTLabs.St_op1 (op1, destr, srcr, lbl') ->
645    translate_op1 op1
646      (find_local_env_reg destr lenv)
647      (List.map (fun r -> RTL.Reg r) (find_local_env_reg srcr lenv))
648      lbl lbl' def
649
650  | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') ->
651    translate_op2 op2 (find_local_env_reg destr lenv)
652      (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) lbl lbl' def
653
654  | RTLabs.St_load (_, addr, destr, lbl') ->
655    translate_load (find_local_env addr lenv) (find_local_env_reg destr lenv)
656      lbl lbl' def
657
658  | RTLabs.St_store (_, addr,  srcr, lbl') ->
659    translate_store (find_local_env addr lenv) (find_local_env srcr lenv)
660      lbl lbl' def
661
662  | RTLabs.St_call_id (f, args, None, _, lbl') ->
663    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv, [], lbl')) def
664
665  | RTLabs.St_call_id (f, args, Some retr, _, lbl') ->
666    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv,
667                                   find_local_env_reg retr lenv, lbl')) def
668
669  | RTLabs.St_call_ptr (f, args, None, _, lbl') ->
670    let (f1, f2) = find_and_addr f lenv in
671    add_graph lbl (RTL.St_call_ptr (f1, f2, rtl_args args lenv, [], lbl')) def
672
673  | RTLabs.St_call_ptr (f, args, Some retr, _, lbl') ->
674    let (f1, f2) = find_and_addr f lenv in
675    add_graph lbl
676      (RTL.St_call_ptr
677         (f1, f2, rtl_args args lenv, find_local_env_reg retr lenv, lbl')) def
678
679  | RTLabs.St_tailcall_id (f, args, _) ->
680    add_graph lbl (RTL.St_tailcall_id (f, rtl_args args lenv)) def
681
682  | RTLabs.St_tailcall_ptr (f, args, _) ->
683    let (f1, f2) = find_and_addr f lenv in
684    add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args lenv)) def
685
686  | RTLabs.St_cond (r, lbl_true, lbl_false) ->
687    translate_cond (find_local_env_reg r lenv) lbl lbl_true lbl_false def
688
689  | RTLabs.St_jumptable _ ->
690    error "Jump tables not supported yet."
691
692  | RTLabs.St_return ->
693    add_graph lbl RTL.St_return def
694
695open BList.Notation
696
697open BList.Notation
698
699let remove_non_int_immediates def =
700  let load_arg a f = match a with
701    | RTLabs.Imm ((AST.Cst_stack _ | AST.Cst_addrsymbol _) as c, t) ->
702      fresh_t t (fun tmp ->
703      RTLabs.St_cst (tmp, c, Label.dummy) ^:: f (RTLabs.Reg tmp))
704    | _ -> f a in
705  let rec load_args args f = match args with
706    | [] -> f []
707    | a :: args ->
708      load_arg a (fun a -> load_args args (fun l -> f (a :: l))) in
709  let trans lbl = function
710    | RTLabs.St_op2(op, r, a1, a2, l) ->
711      load_arg a1 (fun a1 ->
712        load_arg a2 (fun a2 ->
713          RTLabs.St_op2 (op, r, a1, a2, l) ^:: bnil))
714    | RTLabs.St_store(q, a1, a2, l) ->
715      load_arg a1 (fun a1 ->
716        load_arg a2 (fun a2 ->
717          RTLabs.St_store (q, a1, a2, l) ^:: bnil))
718    | RTLabs.St_load (q, a, r, l) ->
719      load_arg a (fun a ->
720        RTLabs.St_load (q, a, r, l) ^:: bnil)
721    | RTLabs.St_call_id (f, args, ret, s, l) ->
722      load_args args (fun args ->
723        RTLabs.St_call_id (f, args, ret, s, l) ^:: bnil)
724    | RTLabs.St_tailcall_id (f, args, s) ->
725      load_args args (fun args ->
726        RTLabs.St_tailcall_id (f, args, s) ^:: bnil)
727    | RTLabs.St_call_ptr (f, args, ret, s, l) ->
728      load_args args (fun args ->
729        RTLabs.St_call_ptr (f, args, ret, s, l) ^:: bnil)
730    | RTLabs.St_tailcall_ptr (f, args, s) ->
731      load_args args (fun args ->
732        RTLabs.St_tailcall_ptr (f, args, s) ^:: bnil)
733    | stmt -> stmt ^:: bnil in
734  let module T = GraphUtilities.Trans(RTLabsGraph)(RTLabsGraph) in
735  let g = def.RTLabs.f_graph in
736  let fresh_reg def t =
737    let r = Register.fresh def.RTLabs.f_runiverse in
738    let locals = (r, t) :: def.RTLabs.f_locals in
739    ({ def with RTLabs.f_locals = locals }, r) in
740  let fresh_lbl () = Label.Gen.fresh def.RTLabs.f_luniverse in
741  let (def, g) = T.translate' fresh_lbl fresh_reg trans def g in
742  { def with RTLabs.f_graph = g }
743 
744let translate_internal def =
745  let def = remove_non_int_immediates def in
746  let runiverse = def.RTLabs.f_runiverse in
747  let lenv =
748    initialize_local_env runiverse
749      (def.RTLabs.f_params @ def.RTLabs.f_locals) def.RTLabs.f_result in
750  let set_of_list l = List.fold_right Register.Set.add l Register.Set.empty in
751  let params = map_list_local_env_reg lenv (List.map fst def.RTLabs.f_params) in
752  let locals = map_list_local_env_reg lenv (List.map fst def.RTLabs.f_locals) in
753  let locals = set_of_list locals in
754  let result = match def.RTLabs.f_result with
755    | None -> []
756    | Some (r, _) -> find_local_env_reg r lenv in
757  let res =
758    { RTL.f_luniverse = def.RTLabs.f_luniverse ;
759      RTL.f_runiverse = runiverse ;
760      RTL.f_result    = result ;
761      RTL.f_params    = params ;
762      RTL.f_locals    = locals ;
763      RTL.f_stacksize = concrete_size def.RTLabs.f_stacksize ;
764      RTL.f_graph     = Label.Map.empty ;
765      RTL.f_entry     = def.RTLabs.f_entry ;
766      RTL.f_exit      = def.RTLabs.f_exit } in
767  Label.Map.fold (translate_stmt lenv) def.RTLabs.f_graph res
768
769
770let translate_fun_def = function
771  | RTLabs.F_int def -> RTL.F_int (translate_internal def)
772  | RTLabs.F_ext def -> RTL.F_ext def
773
774
775let translate p =
776  let f_global (id, size) = (id, concrete_size size) in
777  let f_funct (id, fun_def) = (id, translate_fun_def fun_def) in
778  { RTL.vars   = List.map f_global p.RTLabs.vars ;
779    RTL.functs = List.map f_funct p.RTLabs.functs ;
780    RTL.main   = p.RTLabs.main }
Note: See TracBrowser for help on using the repository browser.