source: Deliverables/D2.2/8051-indexed-labels-branch/src/RTL/RTLToERTL.ml @ 1345

Last change on this file since 1345 was 1345, checked in by tranquil, 9 years ago

work on ERTL and LTL completed

File size: 18.0 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_int (r, i, _) -> ERTL.St_int (r, i, lbl)
37  | ERTL.St_move (r1, r2, _) -> ERTL.St_move (r1, r2, lbl)
38  | ERTL.St_opaccsA (opaccs, dstr, srcr1, srcr2, _) ->
39    ERTL.St_opaccsA (opaccs, dstr, srcr1, srcr2, lbl)
40  | ERTL.St_opaccsB (opaccs, dstr, srcr1, srcr2, _) ->
41    ERTL.St_opaccsB (opaccs, dstr, srcr1, srcr2, lbl)
42  | ERTL.St_op1 (op1, dstr, srcr, _) -> ERTL.St_op1 (op1, dstr, srcr, lbl)
43  | ERTL.St_op2 (op2, dstr, srcr1, srcr2, _) ->
44    ERTL.St_op2 (op2, dstr, srcr1, srcr2, lbl)
45  | ERTL.St_clear_carry _ -> ERTL.St_clear_carry lbl
46  | ERTL.St_set_carry _ -> ERTL.St_set_carry lbl
47  | ERTL.St_load (dstrs, addr1, addr2, _) ->
48    ERTL.St_load (dstrs, addr1, addr2, lbl)
49  | ERTL.St_store (addr1, addr2, srcrs, _) ->
50    ERTL.St_store (addr1, addr2, srcrs, lbl)
51  | ERTL.St_call_id (f, nb_args, _) -> ERTL.St_call_id (f, nb_args, lbl)
52  | ERTL.St_cond _ as inst -> inst
53  | ERTL.St_return _ as inst -> inst
54
55(* Add a list of instruction in a graph, from one label to another, by creating
56   fresh labels inbetween. *)
57
58let rec adds_graph stmt_list start_lbl dest_lbl def = match stmt_list with
59  | [] -> add_graph start_lbl (ERTL.St_skip dest_lbl) def
60  | [stmt] ->
61    add_graph start_lbl (change_label dest_lbl stmt) def
62  | stmt :: stmt_list ->
63    let tmp_lbl = fresh_label def in
64    let stmt = change_label tmp_lbl stmt in
65    let def = add_graph start_lbl stmt def in
66    adds_graph stmt_list tmp_lbl dest_lbl def
67
68(* Process a list of function that adds a list of instructions to a graph, from
69   one label to another, and by creating fresh labels inbetween. *)
70
71let rec add_translates translate_list start_lbl dest_lbl def =
72  match translate_list with
73    | [] -> add_graph start_lbl (ERTL.St_skip dest_lbl) def
74    | [trans] -> trans start_lbl dest_lbl def
75    | trans :: translate_list ->
76      let tmp_lbl = fresh_label def in
77      let def = trans start_lbl tmp_lbl def in
78      add_translates translate_list tmp_lbl dest_lbl def
79
80let fresh_reg def =
81  let r = Register.fresh def.ERTL.f_runiverse in
82  let locals = Register.Set.add r def.ERTL.f_locals in
83  ({ def with ERTL.f_locals = locals }, r)
84
85let rec fresh_regs def n =
86  if n = 0 then (def, [])
87  else
88    let (def, res) = fresh_regs def (n-1) in
89    let (def, r) = fresh_reg def in
90    (def, r :: res)
91
92
93(* Translation *)
94
95let save_hdws l =
96  let f (destr, srcr) start_lbl =
97    adds_graph [ERTL.St_get_hdw (destr, srcr, start_lbl)] start_lbl in
98  List.map f l
99
100let restore_hdws l =
101  let f (destr, srcr) start_lbl =
102    adds_graph [ERTL.St_set_hdw (destr, srcr, start_lbl)] start_lbl in
103  List.map f (List.map (fun (x, y) -> (y, x)) l)
104
105let get_params_hdw params =
106  if List.length params = 0 then
107    [fun start_lbl -> adds_graph [ERTL.St_skip start_lbl] start_lbl]
108  else
109    let l = MiscPottier.combine params I8051.parameters in
110    save_hdws l
111
112let get_param_stack off destr start_lbl dest_lbl def =
113  let (def, addr1) = fresh_reg def in
114  let (def, addr2) = fresh_reg def in
115  let (def, tmpr) = fresh_reg def in
116  adds_graph
117    [ERTL.St_framesize (addr1, start_lbl) ;
118     ERTL.St_int (tmpr, off+I8051.int_size, start_lbl) ;
119     ERTL.St_op2 (I8051.Sub, addr1, addr1, tmpr, start_lbl) ;
120     ERTL.St_get_hdw (tmpr, I8051.spl, start_lbl) ;
121     ERTL.St_op2 (I8051.Add, addr1, addr1, tmpr, start_lbl) ;
122     ERTL.St_int (addr2, 0, start_lbl) ;
123     ERTL.St_get_hdw (tmpr, I8051.sph, start_lbl) ;
124     ERTL.St_op2 (I8051.Addc, addr2, addr2, tmpr, 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 (def, tmpr) = fresh_reg def in
177  let ((common1, rest1), (common2, _)) =
178    MiscPottier.reduce I8051.sts ret_regs in
179  let init_tmpr = ERTL.St_int (tmpr, 0, start_lbl) in
180  let f_save st r = ERTL.St_set_hdw (st, r, start_lbl) in
181  let saves = List.map2 f_save common1 common2 in
182  let f_default st = ERTL.St_set_hdw (st, tmpr, start_lbl) in
183  let defaults = List.map f_default rest1 in
184  adds_graph (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
185
186let assign_result start_lbl =
187  let ((common1, _), (common2, _)) = MiscPottier.reduce I8051.rets I8051.sts in
188  let f ret st = ERTL.St_hdw_to_hdw (ret, st, start_lbl) in
189  let insts = List.map2 f common1 common2 in
190  adds_graph insts start_lbl
191
192let add_epilogue ret_regs sral srah sregs def =
193  let start_lbl = def.ERTL.f_exit in
194  let tmp_lbl = fresh_label def in
195  let last_stmt = Label.Map.find start_lbl def.ERTL.f_graph in
196  let def =
197    add_translates
198      ([adds_graph [ERTL.St_comment ("Epilogue", start_lbl)]] @
199       (* save return value *)
200       [save_return ret_regs] @
201       (* restore callee-saved registers *)
202       [adds_graph [ERTL.St_comment ("Restore callee-saved registers",
203                                     start_lbl)]] @
204       (restore_hdws sregs) @
205       (* restore the return address *)
206       [adds_graph [ERTL.St_comment ("Restore return address", start_lbl) ;
207                    ERTL.St_push (srah, start_lbl) ;
208                    ERTL.St_push (sral, start_lbl)]] @
209       (* delete frame *)
210       [adds_graph [ERTL.St_comment ("Delete frame", start_lbl) ;
211                    ERTL.St_delframe start_lbl]] @
212       (* assign the result to actual return registers *)
213       [adds_graph [ERTL.St_comment ("Set result", start_lbl)]] @
214       [assign_result] @
215       [adds_graph [ERTL.St_comment ("End Epilogue", start_lbl)]])
216      start_lbl tmp_lbl def in
217  let def = add_graph tmp_lbl last_stmt def in
218  change_exit_label tmp_lbl def
219
220
221let allocate_regs saved def =
222  let f r (def, sregs) =
223    let (def, r') = fresh_reg def in
224    (def, (r', r) :: sregs) in
225  I8051.RegisterSet.fold f saved (def, [])
226
227let add_pro_and_epilogue params ret_regs def =
228  (* Allocate registers to hold the return address. *)
229  let (def, sra) = fresh_regs def 2 in
230  let sral = List.nth sra 0 in
231  let srah = List.nth sra 1 in
232  (* Allocate registers to save callee-saved registers. *)
233  let (def, sregs) = allocate_regs I8051.callee_saved def in
234  (* Add a prologue and a epilogue. *)
235  let def = add_prologue params sral srah sregs def in
236  let def = add_epilogue ret_regs sral srah sregs def in
237  def
238
239
240let set_params_hdw params =
241  if List.length params = 0 then
242    [fun start_lbl -> adds_graph [ERTL.St_skip start_lbl] start_lbl]
243  else
244    let l = MiscPottier.combine params I8051.parameters in
245    restore_hdws l
246
247let set_param_stack off srcr start_lbl dest_lbl def =
248  let (def, addr1) = fresh_reg def in
249  let (def, addr2) = fresh_reg def in
250  let (def, tmpr) = fresh_reg def in
251  adds_graph
252    [ERTL.St_int (addr1, off+I8051.int_size, start_lbl) ;
253     ERTL.St_get_hdw (tmpr, I8051.spl, start_lbl) ;
254     ERTL.St_clear_carry start_lbl ;
255     ERTL.St_op2 (I8051.Sub, addr1, tmpr, addr1, start_lbl) ;
256     ERTL.St_get_hdw (tmpr, I8051.sph, start_lbl) ;
257     ERTL.St_int (addr2, 0, start_lbl) ;
258     ERTL.St_op2 (I8051.Sub, addr2, tmpr, addr2, start_lbl) ;
259     ERTL.St_store (addr1, addr2, srcr, start_lbl)]
260    start_lbl dest_lbl def
261
262let set_params_stack params =
263  if List.length params = 0 then
264    [fun start_lbl -> adds_graph [ERTL.St_skip start_lbl] start_lbl]
265  else
266    let f i r = set_param_stack i r in
267    MiscPottier.mapi f params
268
269(* Parameters are put in the physical parameter registers first. If there are
270   not enough such of these, then the remaining parameters are passed on the
271   stack. *)
272
273let set_params params =
274  let n = min (List.length params) (List.length I8051.parameters) in
275  let (hdw_params, stack_params) = MiscPottier.split params n in
276  (set_params_hdw hdw_params) @ (set_params_stack stack_params)
277
278(* Fetching the result depends on the type of the function, or say, the number
279   of registers that are waiting for a value. Temporary non allocatable
280   registers are used. Indeed, moving directly from DPL to a pseudo-register may
281   cause a bug: DPL might be used to compute the address of the
282   pseudo-register. *)
283
284let fetch_result ret_regs start_lbl =
285  let ((common1, _), (common2, _)) = MiscPottier.reduce I8051.sts I8051.rets in
286  let f_save st ret = ERTL.St_hdw_to_hdw (st, ret, start_lbl) in
287  let saves = List.map2 f_save common1 common2 in
288  let ((common1, _), (common2, _)) = MiscPottier.reduce ret_regs I8051.sts in
289  let f_restore r st = ERTL.St_get_hdw (r, st, start_lbl) in
290  let restores = List.map2 f_restore common1 common2 in
291  adds_graph (saves @ restores) start_lbl
292
293(* When calling a function, we need to set its parameters in specific locations:
294   the physical parameter registers as much as possible, and then the stack
295   below. When the called function returns, we put the result where the calling
296   function expect it to be. *)
297let translate_call_id f args ret_regs start_lbl dest_lbl def =
298  let nb_args = List.length args in
299  add_translates
300    ([adds_graph [ERTL.St_comment ("Starting a call", start_lbl)] ;
301      adds_graph [ERTL.St_comment ("Setting up parameters", start_lbl)]] @
302     set_params args @
303     [adds_graph [ERTL.St_call_id (f, nb_args, start_lbl)] ;
304      adds_graph [ERTL.St_comment ("Fetching result", start_lbl)] ;
305      fetch_result ret_regs ;
306      adds_graph [ERTL.St_comment ("End of call sequence", start_lbl)]])
307    start_lbl dest_lbl def
308
309(*
310  let translate_tailcall_id f args start_lbl def = def (* TODO *)
311*)
312
313let translate_stmt lbl stmt def = match stmt with
314
315  | RTL.St_skip lbl' ->
316    add_graph lbl (ERTL.St_skip lbl') def
317
318  | RTL.St_cost (cost_lbl, lbl') ->
319    add_graph lbl (ERTL.St_cost (cost_lbl, lbl')) def
320
321  | RTL.St_ind_0 (i, lbl') ->
322    add_graph lbl (ERTL.St_ind_0 (i, lbl')) def
323
324  | RTL.St_ind_inc (i, lbl') ->
325    add_graph lbl (ERTL.St_ind_inc (i, lbl')) def
326
327  | RTL.St_addr (r1, r2, x, lbl') ->
328    adds_graph
329      [ERTL.St_addrL (r1, x, lbl) ; ERTL.St_addrH (r2, x, lbl) ;]
330      lbl lbl' def
331
332  | RTL.St_stackaddr (r1, r2, lbl') ->
333    adds_graph
334      [ERTL.St_get_hdw (r1, I8051.spl, lbl) ;
335       ERTL.St_get_hdw (r2, I8051.sph, lbl)]
336      lbl lbl' def
337
338  | RTL.St_int (r, i, lbl') ->
339    add_graph lbl (ERTL.St_int (r, i, lbl')) def
340
341  | RTL.St_move (r1, r2, lbl') ->
342    add_graph lbl (ERTL.St_move (r1, r2, lbl')) def
343
344  | RTL.St_opaccs (op, destr1, destr2, srcr1, srcr2, lbl') ->
345    adds_graph [ERTL.St_opaccsA (op, destr1, srcr1, srcr2, lbl) ;
346                ERTL.St_opaccsB (op, destr2, srcr1, srcr2, lbl) ;]
347      lbl lbl' def
348
349  | RTL.St_op1 (op1, destr, srcr, lbl') ->
350    add_graph lbl (ERTL.St_op1 (op1, destr, srcr, lbl')) def
351
352  | RTL.St_op2 (op2, destr, srcr1, srcr2, lbl') ->
353    add_graph lbl (ERTL.St_op2 (op2, destr, srcr1, srcr2, lbl')) def
354
355  | RTL.St_clear_carry lbl' ->
356    add_graph lbl (ERTL.St_clear_carry lbl') def
357
358  | RTL.St_set_carry lbl' ->
359    add_graph lbl (ERTL.St_set_carry lbl') def
360
361  | RTL.St_load (destr, addr1, addr2, lbl') ->
362    add_graph lbl (ERTL.St_load (destr, addr1, addr2, lbl')) def
363
364  | RTL.St_store (addr1, addr2, srcr, lbl') ->
365    add_graph lbl (ERTL.St_store (addr1, addr2, srcr, lbl')) def
366
367  | RTL.St_call_id (f, args, ret_regs, lbl') ->
368    translate_call_id f args ret_regs lbl lbl' def
369
370  | RTL.St_call_ptr _ ->
371    assert false (* TODO *)
372
373  (*
374    | RTL.St_tailcall_id (f, args) ->
375    translate_tailcall_id f args lbl def
376
377    | RTL.St_tailcall_ptr _ ->
378    def (* TODO *)
379  *)
380
381  | RTL.St_cond (srcr, lbl_true, lbl_false) ->
382    add_graph lbl (ERTL.St_cond (srcr, lbl_true, lbl_false)) def
383
384  | RTL.St_return ret_regs ->
385    add_graph lbl (ERTL.St_return ret_regs) def
386
387  | RTL.St_tailcall_id _ | RTL.St_tailcall_ptr _ ->
388    assert false (* impossible: the RTL program is supposed to be simplified:
389                    no tailcalls. *)
390
391
392let translate_internal def =
393  let nb_params = List.length (def.RTL.f_params) in
394  (* The stack size is augmented by the number of parameters that cannot fit
395     into physical registers. *)
396  let added_stacksize = max 0 (nb_params - (List.length I8051.parameters)) in
397  let def' =
398    { ERTL.f_luniverse = def.RTL.f_luniverse ;
399      ERTL.f_runiverse = def.RTL.f_runiverse ;
400      ERTL.f_params    = nb_params ;
401      (* ERTL does not know about parameter registers. We need to add them to
402         the locals. *)
403      ERTL.f_locals    = Register.Set.union def.RTL.f_locals
404                         (Register.Set.of_list def.RTL.f_params) ;
405      ERTL.f_stacksize = def.RTL.f_stacksize + added_stacksize ;
406      ERTL.f_graph     = Label.Map.empty ;
407      ERTL.f_entry     = def.RTL.f_entry ;
408      ERTL.f_exit      = def.RTL.f_exit } in
409  let def' = Label.Map.fold translate_stmt def.RTL.f_graph def' in
410  let def' = add_pro_and_epilogue def.RTL.f_params def.RTL.f_result def' in
411  def'
412
413
414let translate_funct (id, def) =
415  let def' = match def with
416    | RTL.F_int def -> ERTL.F_int (translate_internal def)
417    | RTL.F_ext def -> ERTL.F_ext def
418  in
419  (id, def')
420
421
422(* Move the first cost label of each function at the beginning of the
423   function. Indeed, the instructions for calling conventions (stack allocation
424   for example) are added at the very beginning of the function, thus before the
425   first cost label. *)
426
427let generate stmt def =
428  let entry = Label.Gen.fresh def.ERTL.f_luniverse in
429  let def =
430    { def with ERTL.f_graph = Label.Map.add entry stmt def.ERTL.f_graph } in
431  { def with ERTL.f_entry = entry }
432
433let find_and_remove_first_cost_label def =
434  let rec aux lbl = match Label.Map.find lbl def.ERTL.f_graph with
435    | ERTL.St_cost (cost_label, next_lbl) ->
436      let graph = Label.Map.add lbl (ERTL.St_skip next_lbl) def.ERTL.f_graph in
437      (Some cost_label, { def with ERTL.f_graph = graph })
438                | ERTL.St_ind_0 (_, lbl) | ERTL.St_ind_inc (_, lbl)
439    | ERTL.St_skip lbl | ERTL.St_comment (_, lbl) | ERTL.St_get_hdw (_, _, lbl)
440    | ERTL.St_set_hdw (_, _, lbl) | ERTL.St_hdw_to_hdw (_, _, lbl)
441    | ERTL.St_pop (_, lbl) | ERTL.St_push (_, lbl) | ERTL.St_addrH (_, _, lbl)
442    | ERTL.St_addrL (_, _, lbl) | ERTL.St_int (_, _, lbl)
443    | ERTL.St_move (_, _, lbl) | ERTL.St_opaccsA (_, _, _, _, lbl)
444    | ERTL.St_opaccsB (_, _, _, _, lbl)
445    | ERTL.St_op1 (_, _, _, lbl) | ERTL.St_op2 (_, _, _, _, lbl)
446    | ERTL.St_clear_carry lbl | ERTL.St_set_carry lbl
447    | ERTL.St_load (_, _, _, lbl)
448    | ERTL.St_store (_, _, _, lbl) | ERTL.St_call_id (_, _, 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.