source: Deliverables/D2.2/8051/src/RTL/RTLToERTL.ml @ 1568

Last change on this file since 1568 was 1568, checked in by tranquil, 8 years ago
  • Immediates introduced (but not fully used yet in RTLabs to RTL pass)
  • translation streamlined
  • BUGGY: interpretation fails in LTL, trying to fetch a function with incorrect address
File size: 18.1 KB
Line 
1
2(** This module provides a translation of [RTL] programs to [ERTL]
3    programs. *)
4
5
6let error_prefix = "RTL to ERTL"
7let error = Error.global_error error_prefix
8
9
10(* Helper functions *)
11
12let change_exit_label lbl def =
13  { def with ERTL.f_exit = lbl }
14
15let add_graph lbl stmt def =
16  { def with ERTL.f_graph = Label.Map.add lbl stmt def.ERTL.f_graph }
17
18let fresh_label def = Label.Gen.fresh def.ERTL.f_luniverse
19
20let change_label lbl = function
21  | ERTL.St_skip _ -> ERTL.St_skip lbl
22  | ERTL.St_comment (s, _) -> ERTL.St_comment (s, lbl)
23  | ERTL.St_cost (cost_lbl, _) -> ERTL.St_cost (cost_lbl, lbl)
24  | ERTL.St_ind_0 (i, _) -> ERTL.St_ind_0 (i, lbl)
25  | ERTL.St_ind_inc (i, _) -> ERTL.St_ind_inc (i, lbl)
26  | ERTL.St_get_hdw (r1, r2, _) -> ERTL.St_get_hdw (r1, r2, lbl)
27  | ERTL.St_set_hdw (r1, r2, _) -> ERTL.St_set_hdw (r1, r2, lbl)
28  | ERTL.St_hdw_to_hdw (r1, r2, _) -> ERTL.St_hdw_to_hdw (r1, r2, lbl)
29  | ERTL.St_newframe _ -> ERTL.St_newframe lbl
30  | ERTL.St_delframe _ -> ERTL.St_delframe lbl
31  | ERTL.St_framesize (r, _) -> ERTL.St_framesize (r, lbl)
32  | ERTL.St_pop (r, _) -> ERTL.St_pop (r, lbl)
33  | ERTL.St_push (r, _) -> ERTL.St_push (r, lbl)
34  | ERTL.St_addrH (r, id, _) -> ERTL.St_addrH (r, id, lbl)
35  | ERTL.St_addrL (r, id, _) -> ERTL.St_addrL (r, id, lbl)
36  | ERTL.St_move (r1, a, _) -> ERTL.St_move (r1, a, lbl)
37  | ERTL.St_opaccsA (opaccs, dstr, srcr1, srcr2, _) ->
38    ERTL.St_opaccsA (opaccs, dstr, srcr1, srcr2, lbl)
39  | ERTL.St_opaccsB (opaccs, dstr, srcr1, srcr2, _) ->
40    ERTL.St_opaccsB (opaccs, dstr, srcr1, srcr2, lbl)
41  | ERTL.St_op1 (op1, dstr, srcr, _) -> ERTL.St_op1 (op1, dstr, srcr, lbl)
42  | ERTL.St_op2 (op2, dstr, srcr1, srcr2, _) ->
43    ERTL.St_op2 (op2, dstr, srcr1, srcr2, lbl)
44  | ERTL.St_clear_carry _ -> ERTL.St_clear_carry lbl
45  | ERTL.St_set_carry _ -> ERTL.St_set_carry lbl
46  | ERTL.St_load (dstrs, addr1, addr2, _) ->
47    ERTL.St_load (dstrs, addr1, addr2, lbl)
48  | ERTL.St_store (addr1, addr2, srcrs, _) ->
49    ERTL.St_store (addr1, addr2, srcrs, lbl)
50  | ERTL.St_call_id (f, nb_args, _) -> ERTL.St_call_id (f, nb_args, lbl)
51  | ERTL.St_call_ptr (f1, f2, nb_args, _) ->
52    ERTL.St_call_ptr (f1, f2, nb_args, lbl)
53  | ERTL.St_cond _ as inst -> inst
54  | ERTL.St_return _ as inst -> inst
55
56(* Add a list of instruction in a graph, from one label to another, by creating
57   fresh labels inbetween. *)
58
59let rec adds_graph stmt_list start_lbl dest_lbl def = match stmt_list with
60  | [] -> add_graph start_lbl (ERTL.St_skip dest_lbl) def
61  | [stmt] ->
62    add_graph start_lbl (change_label dest_lbl stmt) def
63  | stmt :: stmt_list ->
64    let tmp_lbl = fresh_label def in
65    let stmt = change_label tmp_lbl stmt in
66    let def = add_graph start_lbl stmt def in
67    adds_graph stmt_list tmp_lbl dest_lbl def
68
69(* Process a list of function that adds a list of instructions to a graph, from
70   one label to another, and by creating fresh labels inbetween. *)
71
72let rec add_translates translate_list start_lbl dest_lbl def =
73  match translate_list with
74    | [] -> add_graph start_lbl (ERTL.St_skip dest_lbl) def
75    | [trans] -> trans start_lbl dest_lbl def
76    | trans :: translate_list ->
77      let tmp_lbl = fresh_label def in
78      let def = trans start_lbl tmp_lbl def in
79      add_translates translate_list tmp_lbl dest_lbl def
80
81let fresh_reg def =
82  let r = Register.fresh def.ERTL.f_runiverse in
83  let locals = Register.Set.add r def.ERTL.f_locals in
84  ({ def with ERTL.f_locals = locals }, r)
85
86let rec fresh_regs def n =
87  if n = 0 then (def, [])
88  else
89    let (def, res) = fresh_regs def (n-1) in
90    let (def, r) = fresh_reg def in
91    (def, r :: res)
92
93
94(* Translation *)
95
96let save_hdws l =
97  let f (destr, srcr) start_lbl =
98    adds_graph [ERTL.St_get_hdw (destr, srcr, start_lbl)] start_lbl in
99  List.map f l
100
101let restore_hdws l =
102  let f (destr, srcr) start_lbl =
103    adds_graph [ERTL.St_set_hdw (destr, RTL.Reg srcr, start_lbl)] start_lbl in
104  List.map f (List.map (fun (x, y) -> (y, x)) l)
105
106let get_params_hdw params =
107  if List.length params = 0 then
108    [fun start_lbl -> adds_graph [ERTL.St_skip start_lbl] start_lbl]
109  else
110    let l = MiscPottier.combine params I8051.parameters in
111    save_hdws l
112
113let get_param_stack off destr start_lbl dest_lbl def =
114  let (def, addr1) = fresh_reg def in
115  let (def, addr2) = fresh_reg def in
116  let (def, tmpr) = fresh_reg def in
117  adds_graph
118    [ERTL.St_framesize (addr1, start_lbl) ;
119     ERTL.St_op2 (I8051.Sub, addr1, addr1, RTL.Imm (off+I8051.int_size),
120                  start_lbl) ;
121     ERTL.St_get_hdw (tmpr, I8051.spl, start_lbl) ;
122     ERTL.St_op2 (I8051.Add, addr1, addr1, RTL.Reg tmpr, start_lbl) ;
123     ERTL.St_get_hdw (tmpr, I8051.sph, start_lbl) ;
124     ERTL.St_op2 (I8051.Addc, addr2, tmpr, RTL.Imm 0, start_lbl) ;
125     ERTL.St_load (destr, addr1, addr2, start_lbl)]
126    start_lbl dest_lbl def
127
128let get_params_stack params =
129  if List.length params = 0 then
130    [fun start_lbl -> adds_graph [ERTL.St_skip start_lbl] start_lbl]
131  else
132    let f i r = get_param_stack i r in
133    MiscPottier.mapi f params
134
135(* Parameters are taken from the physical parameter registers first. If there
136   are not enough such of these, then the remaining parameters are taken from
137   the stack. *)
138
139let get_params params =
140  let n = min (List.length params) (List.length I8051.parameters) in
141  let (hdw_params, stack_params) = MiscPottier.split params n in
142  (get_params_hdw hdw_params) @ (get_params_stack stack_params)
143
144let add_prologue params sral srah sregs def =
145  let start_lbl = def.ERTL.f_entry in
146  let tmp_lbl = fresh_label def in
147  let last_stmt = Label.Map.find start_lbl def.ERTL.f_graph in
148  let def =
149    add_translates
150      ([adds_graph [ERTL.St_comment ("Prologue", start_lbl)]] @
151       (* new frame *)
152       (adds_graph [ERTL.St_comment ("New frame", start_lbl) ;
153                    ERTL.St_newframe start_lbl]) ::
154       (* save the return address *)
155       (adds_graph [ERTL.St_comment ("Save return address", start_lbl) ;
156                    ERTL.St_pop (sral, start_lbl) ;
157                    ERTL.St_pop (srah, start_lbl)]) ::
158       (* save callee-saved registers *)
159       [adds_graph [ERTL.St_comment ("Save callee-saved registers",
160                                     start_lbl)]] @
161       (save_hdws sregs) @
162       (* fetch parameters *)
163       [adds_graph [ERTL.St_comment ("Fetch parameters", start_lbl)]] @
164       (get_params params) @
165       [adds_graph [ERTL.St_comment ("End Prologue", start_lbl)]])
166      start_lbl tmp_lbl def in
167  add_graph tmp_lbl last_stmt def
168
169
170(* Save the result of a function in a place that cannot be written, even after
171   register allocation. This way, the cleaning sequence of returning from a
172   function will not interfere with the result value, that can be restored right
173   before jumping out of the function. *)
174
175let save_return ret_regs start_lbl dest_lbl def =
176  let ((common1, rest1), (common2, _)) =
177    MiscPottier.reduce I8051.sts ret_regs in
178  let f_save st r = ERTL.St_set_hdw (st, RTL.Reg r, start_lbl) in
179  let saves = List.map2 f_save common1 common2 in
180  let f_default st = ERTL.St_set_hdw (st, RTL.Imm 0, start_lbl) in
181  let defaults = List.map f_default rest1 in
182  adds_graph (saves @ defaults) start_lbl dest_lbl def
183
184let assign_result start_lbl =
185  let ((common1, _), (common2, _)) = MiscPottier.reduce I8051.rets I8051.sts in
186  let f ret st = ERTL.St_hdw_to_hdw (ret, st, start_lbl) in
187  let insts = List.map2 f common1 common2 in
188  adds_graph insts start_lbl
189
190let add_epilogue ret_regs sral srah sregs def =
191  let start_lbl = def.ERTL.f_exit in
192  let tmp_lbl = fresh_label def in
193  let last_stmt = Label.Map.find start_lbl def.ERTL.f_graph in
194  let def =
195    add_translates
196      ([adds_graph [ERTL.St_comment ("Epilogue", start_lbl)]] @
197       (* save return value *)
198       [save_return ret_regs] @
199       (* restore callee-saved registers *)
200       [adds_graph [ERTL.St_comment ("Restore callee-saved registers",
201                                     start_lbl)]] @
202       (restore_hdws sregs) @
203       (* restore the return address *)
204       [adds_graph [ERTL.St_comment ("Restore return address", start_lbl) ;
205                    ERTL.St_push (srah, start_lbl) ;
206                    ERTL.St_push (sral, start_lbl)]] @
207       (* delete frame *)
208       [adds_graph [ERTL.St_comment ("Delete frame", start_lbl) ;
209                    ERTL.St_delframe start_lbl]] @
210       (* assign the result to actual return registers *)
211       [adds_graph [ERTL.St_comment ("Set result", start_lbl)]] @
212       [assign_result] @
213       [adds_graph [ERTL.St_comment ("End Epilogue", start_lbl)]])
214      start_lbl tmp_lbl def in
215  let def = add_graph tmp_lbl last_stmt def in
216  change_exit_label tmp_lbl def
217
218
219let allocate_regs saved def =
220  let f r (def, sregs) =
221    let (def, r') = fresh_reg def in
222    (def, (r', r) :: sregs) in
223  I8051.RegisterSet.fold f saved (def, [])
224
225let add_pro_and_epilogue params ret_regs def =
226  (* Allocate registers to hold the return address. *)
227  let (def, sra) = fresh_regs def 2 in
228  let sral = List.nth sra 0 in
229  let srah = List.nth sra 1 in
230  (* Allocate registers to save callee-saved registers. *)
231  let (def, sregs) = allocate_regs I8051.callee_saved def in
232  (* Add a prologue and a epilogue. *)
233  let def = add_prologue params sral srah sregs def in
234  let def = add_epilogue ret_regs sral srah sregs def in
235  def
236
237
238let set_params_hdw params =
239  if List.length params = 0 then
240    [fun start_lbl -> adds_graph [ERTL.St_skip start_lbl] start_lbl]
241  else
242    let l = MiscPottier.combine params I8051.parameters in
243    restore_hdws l
244
245let set_param_stack off srcr start_lbl dest_lbl def =
246  let (def, addr1) = fresh_reg def in
247  let (def, addr2) = fresh_reg def in
248  let (def, tmpr) = fresh_reg def in
249  adds_graph
250    [ERTL.St_get_hdw (tmpr, I8051.spl, start_lbl) ;
251     ERTL.St_clear_carry start_lbl ;
252     ERTL.St_op2 (I8051.Sub, addr1, tmpr, RTL.Imm (off+I8051.int_size),
253                  start_lbl) ;
254     ERTL.St_get_hdw (tmpr, I8051.sph, start_lbl) ;
255     ERTL.St_op2 (I8051.Sub, addr2, tmpr, RTL.Imm 0, start_lbl) ;
256     ERTL.St_store (addr1, addr2, srcr, start_lbl)]
257    start_lbl dest_lbl def
258
259let set_params_stack params =
260  if List.length params = 0 then
261    [fun start_lbl -> adds_graph [ERTL.St_skip start_lbl] start_lbl]
262  else
263    let f i r = set_param_stack i r in
264    MiscPottier.mapi f params
265
266(* Parameters are put in the physical parameter registers first. If there are
267   not enough such of these, then the remaining parameters are passed on the
268   stack. *)
269
270let set_params params =
271  let n = min (List.length params) (List.length I8051.parameters) in
272  let (hdw_params, stack_params) = MiscPottier.split params n in
273  (set_params_hdw hdw_params) @ (set_params_stack stack_params)
274
275(* Fetching the result depends on the type of the function, or say, the number
276   of registers that are waiting for a value. Temporary non allocatable
277   registers are used. Indeed, moving directly from DPL to a pseudo-register may
278   cause a bug: DPL might be used to compute the address of the
279   pseudo-register. *)
280
281let fetch_result ret_regs start_lbl =
282  let ((common1, _), (common2, _)) = MiscPottier.reduce I8051.sts I8051.rets in
283  let f_save st ret = ERTL.St_hdw_to_hdw (st, ret, start_lbl) in
284  let saves = List.map2 f_save common1 common2 in
285  let ((common1, _), (common2, _)) = MiscPottier.reduce ret_regs I8051.sts in
286  let f_restore r st = ERTL.St_get_hdw (r, st, start_lbl) in
287  let restores = List.map2 f_restore common1 common2 in
288  adds_graph (saves @ restores) start_lbl
289
290(* When calling a function, we need to set its parameters in specific locations:
291   the physical parameter registers as much as possible, and then the stack
292   below. When the called function returns, we put the result where the calling
293   function expect it to be. *)
294let translate_call stmt args ret_regs start_lbl dest_lbl def =
295  let nb_args = List.length args in
296  add_translates
297    ([adds_graph [ERTL.St_comment ("Starting a call", start_lbl)] ;
298      adds_graph [ERTL.St_comment ("Setting up parameters", start_lbl)]] @
299     set_params args @
300     [adds_graph [stmt nb_args] ;
301      adds_graph [ERTL.St_comment ("Fetching result", start_lbl)] ;
302      fetch_result ret_regs ;
303      adds_graph [ERTL.St_comment ("End of call sequence", start_lbl)]])
304    start_lbl dest_lbl def
305
306(*
307  let translate_tailcall_id f args start_lbl def = def (* TODO *)
308*)
309
310let translate_stmt lbl stmt def = match stmt with
311
312  | RTL.St_skip lbl' ->
313    add_graph lbl (ERTL.St_skip lbl') def
314
315  | RTL.St_cost (cost_lbl, lbl') ->
316    add_graph lbl (ERTL.St_cost (cost_lbl, lbl')) def
317
318  | RTL.St_ind_0 (i, lbl') ->
319    add_graph lbl (ERTL.St_ind_0 (i, lbl')) def
320
321  | RTL.St_ind_inc (i, lbl') ->
322    add_graph lbl (ERTL.St_ind_inc (i, lbl')) def
323
324  | RTL.St_addr (r1, r2, x, lbl') ->
325    adds_graph
326      [ERTL.St_addrL (r1, x, lbl) ; ERTL.St_addrH (r2, x, lbl) ;]
327      lbl lbl' def
328
329  | RTL.St_stackaddr (r1, r2, lbl') ->
330    adds_graph
331      [ERTL.St_get_hdw (r1, I8051.spl, lbl) ;
332       ERTL.St_get_hdw (r2, I8051.sph, lbl)]
333      lbl lbl' def
334
335  (* | RTL.St_int (r, i, lbl') -> *)
336  (*   add_graph lbl (ERTL.St_int (r, i, lbl')) def *)
337
338  | RTL.St_move (r1, r2, lbl') ->
339    add_graph lbl (ERTL.St_move (r1, r2, lbl')) def
340
341  | RTL.St_opaccs (op, destr1, destr2, srcr1, srcr2, lbl') ->
342    adds_graph [ERTL.St_opaccsA (op, destr1, srcr1, srcr2, lbl) ;
343                ERTL.St_opaccsB (op, destr2, srcr1, srcr2, lbl) ;]
344      lbl lbl' def
345
346  | RTL.St_op1 (op1, destr, srcr, lbl') ->
347    add_graph lbl (ERTL.St_op1 (op1, destr, srcr, lbl')) def
348
349  | RTL.St_op2 (op2, destr, srcr1, srcr2, lbl') ->
350    add_graph lbl (ERTL.St_op2 (op2, destr, srcr1, srcr2, lbl')) def
351
352  | RTL.St_clear_carry lbl' ->
353    add_graph lbl (ERTL.St_clear_carry lbl') def
354
355  | RTL.St_set_carry lbl' ->
356    add_graph lbl (ERTL.St_set_carry lbl') def
357
358  | RTL.St_load (destr, addr1, addr2, lbl') ->
359    add_graph lbl (ERTL.St_load (destr, addr1, addr2, lbl')) def
360
361  | RTL.St_store (addr1, addr2, srcr, lbl') ->
362    add_graph lbl (ERTL.St_store (addr1, addr2, srcr, lbl')) def
363
364  | RTL.St_call_id (f, args, ret_regs, lbl') ->
365    let stmt nb_args = ERTL.St_call_id (f, nb_args, lbl) in
366    translate_call stmt args ret_regs lbl lbl' def
367
368  | RTL.St_call_ptr (f1, f2, args, ret_regs, lbl') ->
369    let stmt nb_args = ERTL.St_call_ptr (f1, f2, nb_args, lbl) in
370    translate_call stmt args ret_regs lbl lbl' def
371
372  (*
373    | RTL.St_tailcall_id (f, args) ->
374    translate_tailcall_id f args lbl def
375
376    | RTL.St_tailcall_ptr _ ->
377    def (* TODO *)
378  *)
379
380  | RTL.St_cond (srcr, lbl_true, lbl_false) ->
381    add_graph lbl (ERTL.St_cond (srcr, lbl_true, lbl_false)) def
382
383  | RTL.St_return ret_regs ->
384    add_graph lbl (ERTL.St_return ret_regs) def
385
386  | RTL.St_tailcall_id _ | RTL.St_tailcall_ptr _ ->
387    assert false (* impossible: the RTL program is supposed to be simplified:
388                    no tailcalls. *)
389
390
391let translate_internal def =
392  let nb_params = List.length (def.RTL.f_params) in
393  (* The stack size is augmented by the number of parameters that cannot fit
394     into physical registers. *)
395  let added_stacksize = max 0 (nb_params - (List.length I8051.parameters)) in
396  let def' =
397    { ERTL.f_luniverse = def.RTL.f_luniverse ;
398      ERTL.f_runiverse = def.RTL.f_runiverse ;
399      ERTL.f_params    = nb_params ;
400      (* ERTL does not know about parameter registers. We need to add them to
401         the locals. *)
402      ERTL.f_locals    = Register.Set.union def.RTL.f_locals
403                         (Register.Set.of_list def.RTL.f_params) ;
404      ERTL.f_stacksize = def.RTL.f_stacksize + added_stacksize ;
405      ERTL.f_graph     = Label.Map.empty ;
406      ERTL.f_entry     = def.RTL.f_entry ;
407      ERTL.f_exit      = def.RTL.f_exit } in
408  let def' = Label.Map.fold translate_stmt def.RTL.f_graph def' in
409  let def' = add_pro_and_epilogue def.RTL.f_params def.RTL.f_result def' in
410  def'
411
412
413let translate_funct (id, def) =
414  let def' = match def with
415    | RTL.F_int def -> ERTL.F_int (translate_internal def)
416    | RTL.F_ext def -> ERTL.F_ext def
417  in
418  (id, def')
419
420
421(* Move the first cost label of each function at the beginning of the
422   function. Indeed, the instructions for calling conventions (stack allocation
423   for example) are added at the very beginning of the function, thus before the
424   first cost label. *)
425
426let generate stmt def =
427  let entry = Label.Gen.fresh def.ERTL.f_luniverse in
428  let def =
429    { def with ERTL.f_graph = Label.Map.add entry stmt def.ERTL.f_graph } in
430  { def with ERTL.f_entry = entry }
431
432let find_and_remove_first_cost_label def =
433  let rec aux lbl = match Label.Map.find lbl def.ERTL.f_graph with
434    | ERTL.St_cost (cost_label, next_lbl) ->
435      let graph = Label.Map.add lbl (ERTL.St_skip next_lbl) def.ERTL.f_graph in
436      (Some cost_label, { def with ERTL.f_graph = graph })
437    | ERTL.St_ind_0 (_, lbl) | ERTL.St_ind_inc (_, lbl)
438    | ERTL.St_skip lbl | ERTL.St_comment (_, lbl) | ERTL.St_get_hdw (_, _, lbl)
439    | ERTL.St_set_hdw (_, _, lbl) | ERTL.St_hdw_to_hdw (_, _, lbl)
440    | ERTL.St_pop (_, lbl) | ERTL.St_push (_, lbl) | ERTL.St_addrH (_, _, lbl)
441    | ERTL.St_addrL (_, _, lbl) (* | ERTL.St_int (_, _, lbl) *)
442    | ERTL.St_move (_, _, lbl) | ERTL.St_opaccsA (_, _, _, _, lbl)
443    | ERTL.St_opaccsB (_, _, _, _, lbl)
444    | ERTL.St_op1 (_, _, _, lbl) | ERTL.St_op2 (_, _, _, _, lbl)
445    | ERTL.St_clear_carry lbl | ERTL.St_set_carry lbl
446    | ERTL.St_load (_, _, _, lbl)
447    | ERTL.St_store (_, _, _, lbl) | ERTL.St_call_id (_, _, lbl)
448    | ERTL.St_call_ptr (_, _, _, lbl)
449    | ERTL.St_newframe lbl | ERTL.St_delframe lbl | ERTL.St_framesize (_, lbl)
450      ->
451      aux lbl
452    | ERTL.St_cond _ | ERTL.St_return _ ->
453      (* No cost label found (no labelling performed). Indeed, the first cost
454         label must after some linear instructions. *)
455      (None, def) in
456  aux def.ERTL.f_entry
457
458let move_first_cost_label_up_internal def =
459  let (cost_label, def) = find_and_remove_first_cost_label def in
460  match cost_label with
461    | None -> def
462    | Some cost_label ->
463      generate (ERTL.St_cost (cost_label, def.ERTL.f_entry)) def
464
465let move_first_cost_label_up (id, def) =
466  let def' = match def with
467    | ERTL.F_int int_fun ->
468      ERTL.F_int (move_first_cost_label_up_internal int_fun)
469    | _ -> def in
470  (id, def')
471
472
473let translate p =
474  (* We simplify tail calls as regular calls for now. *)
475  let p = RTLtailcall.simplify p in
476  (* The tranformation on each RTL function: create an ERTL function and move
477     its first cost label at the very beginning. *)
478  let f funct = move_first_cost_label_up (translate_funct funct) in
479  { ERTL.vars   = p.RTL.vars ;
480    ERTL.functs = List.map f p.RTL.functs ;
481    ERTL.main   = p.RTL.main }
Note: See TracBrowser for help on using the repository browser.