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

Last change on this file since 624 was 624, checked in by ayache, 9 years ago

Bug fixs and signed division hack in D2.2.

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