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

Last change on this file since 1580 was 1580, checked in by tranquil, 8 years ago

implemented constant propagation in LTL
cleaned up translations in optimizations, a new module for translations is available

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