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

Last change on this file since 1462 was 1462, checked in by ayache, 8 years ago

Added D5.1: Frama-C plug-in and Lustre wrapper. D2.2 (8051) has been updated accordingly.

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_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_opaccsA (opaccs, dstr, srcr1, srcr2, _) ->
37    ERTL.St_opaccsA (opaccs, dstr, srcr1, srcr2, lbl)
38  | ERTL.St_opaccsB (opaccs, dstr, srcr1, srcr2, _) ->
39    ERTL.St_opaccsB (opaccs, dstr, srcr1, srcr2, lbl)
40  | ERTL.St_op1 (op1, dstr, srcr, _) -> ERTL.St_op1 (op1, dstr, srcr, lbl)
41  | ERTL.St_op2 (op2, dstr, srcr1, srcr2, _) ->
42    ERTL.St_op2 (op2, dstr, srcr1, srcr2, lbl)
43  | ERTL.St_clear_carry _ -> ERTL.St_clear_carry lbl
44  | ERTL.St_set_carry _ -> ERTL.St_set_carry lbl
45  | ERTL.St_load (dstrs, addr1, addr2, _) ->
46    ERTL.St_load (dstrs, addr1, addr2, lbl)
47  | ERTL.St_store (addr1, addr2, srcrs, _) ->
48    ERTL.St_store (addr1, addr2, srcrs, lbl)
49  | ERTL.St_call_id (f, nb_args, _) -> ERTL.St_call_id (f, nb_args, lbl)
50  | ERTL.St_call_ptr (f1, f2, nb_args, _) ->
51    ERTL.St_call_ptr (f1, f2, 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 stmt 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 [stmt nb_args] ;
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_addr (r1, r2, x, lbl') ->
322    adds_graph
323      [ERTL.St_addrL (r1, x, lbl) ; ERTL.St_addrH (r2, x, lbl) ;]
324      lbl lbl' def
325
326  | RTL.St_stackaddr (r1, r2, lbl') ->
327    adds_graph
328      [ERTL.St_get_hdw (r1, I8051.spl, lbl) ;
329       ERTL.St_get_hdw (r2, I8051.sph, lbl)]
330      lbl lbl' def
331
332  | RTL.St_int (r, i, lbl') ->
333    add_graph lbl (ERTL.St_int (r, i, lbl')) def
334
335  | RTL.St_move (r1, r2, lbl') ->
336    add_graph lbl (ERTL.St_move (r1, r2, lbl')) def
337
338  | RTL.St_opaccs (op, destr1, destr2, srcr1, srcr2, lbl') ->
339    adds_graph [ERTL.St_opaccsA (op, destr1, srcr1, srcr2, lbl) ;
340                ERTL.St_opaccsB (op, destr2, srcr1, srcr2, lbl) ;]
341      lbl lbl' def
342
343  | RTL.St_op1 (op1, destr, srcr, lbl') ->
344    add_graph lbl (ERTL.St_op1 (op1, destr, srcr, lbl')) def
345
346  | RTL.St_op2 (op2, destr, srcr1, srcr2, lbl') ->
347    add_graph lbl (ERTL.St_op2 (op2, destr, srcr1, srcr2, lbl')) def
348
349  | RTL.St_clear_carry lbl' ->
350    add_graph lbl (ERTL.St_clear_carry lbl') def
351
352  | RTL.St_set_carry lbl' ->
353    add_graph lbl (ERTL.St_set_carry lbl') def
354
355  | RTL.St_load (destr, addr1, addr2, lbl') ->
356    add_graph lbl (ERTL.St_load (destr, addr1, addr2, lbl')) def
357
358  | RTL.St_store (addr1, addr2, srcr, lbl') ->
359    add_graph lbl (ERTL.St_store (addr1, addr2, srcr, lbl')) def
360
361  | RTL.St_call_id (f, args, ret_regs, lbl') ->
362    let stmt nb_args = ERTL.St_call_id (f, nb_args, lbl) in
363    translate_call stmt args ret_regs lbl lbl' def
364
365  | RTL.St_call_ptr (f1, f2, args, ret_regs, lbl') ->
366    let stmt nb_args = ERTL.St_call_ptr (f1, f2, nb_args, lbl) in
367    translate_call stmt args ret_regs lbl lbl' def
368
369  (*
370    | RTL.St_tailcall_id (f, args) ->
371    translate_tailcall_id f args lbl def
372
373    | RTL.St_tailcall_ptr _ ->
374    def (* TODO *)
375  *)
376
377  | RTL.St_cond (srcr, lbl_true, lbl_false) ->
378    add_graph lbl (ERTL.St_cond (srcr, lbl_true, lbl_false)) def
379
380  | RTL.St_return ret_regs ->
381    add_graph lbl (ERTL.St_return ret_regs) def
382
383  | RTL.St_tailcall_id _ | RTL.St_tailcall_ptr _ ->
384    assert false (* impossible: the RTL program is supposed to be simplified:
385                    no tailcalls. *)
386
387
388let translate_internal def =
389  let nb_params = List.length (def.RTL.f_params) in
390  (* The stack size is augmented by the number of parameters that cannot fit
391     into physical registers. *)
392  let added_stacksize = max 0 (nb_params - (List.length I8051.parameters)) in
393  let def' =
394    { ERTL.f_luniverse = def.RTL.f_luniverse ;
395      ERTL.f_runiverse = def.RTL.f_runiverse ;
396      ERTL.f_params    = nb_params ;
397      (* ERTL does not know about parameter registers. We need to add them to
398         the locals. *)
399      ERTL.f_locals    = Register.Set.union def.RTL.f_locals
400                         (Register.Set.of_list def.RTL.f_params) ;
401      ERTL.f_stacksize = def.RTL.f_stacksize + added_stacksize ;
402      ERTL.f_graph     = Label.Map.empty ;
403      ERTL.f_entry     = def.RTL.f_entry ;
404      ERTL.f_exit      = def.RTL.f_exit } in
405  let def' = Label.Map.fold translate_stmt def.RTL.f_graph def' in
406  let def' = add_pro_and_epilogue def.RTL.f_params def.RTL.f_result def' in
407  def'
408
409
410let translate_funct (id, def) =
411  let def' = match def with
412    | RTL.F_int def -> ERTL.F_int (translate_internal def)
413    | RTL.F_ext def -> ERTL.F_ext def
414  in
415  (id, def')
416
417
418(* Move the first cost label of each function at the beginning of the
419   function. Indeed, the instructions for calling conventions (stack allocation
420   for example) are added at the very beginning of the function, thus before the
421   first cost label. *)
422
423let generate stmt def =
424  let entry = Label.Gen.fresh def.ERTL.f_luniverse in
425  let def =
426    { def with ERTL.f_graph = Label.Map.add entry stmt def.ERTL.f_graph } in
427  { def with ERTL.f_entry = entry }
428
429let find_and_remove_first_cost_label def =
430  let rec aux lbl = match Label.Map.find lbl def.ERTL.f_graph with
431    | ERTL.St_cost (cost_label, next_lbl) ->
432      let graph = Label.Map.add lbl (ERTL.St_skip next_lbl) def.ERTL.f_graph in
433      (Some cost_label, { def with ERTL.f_graph = graph })
434    | ERTL.St_skip lbl | ERTL.St_comment (_, lbl) | ERTL.St_get_hdw (_, _, lbl)
435    | ERTL.St_set_hdw (_, _, lbl) | ERTL.St_hdw_to_hdw (_, _, lbl)
436    | ERTL.St_pop (_, lbl) | ERTL.St_push (_, lbl) | ERTL.St_addrH (_, _, lbl)
437    | ERTL.St_addrL (_, _, lbl) | ERTL.St_int (_, _, lbl)
438    | ERTL.St_move (_, _, lbl) | ERTL.St_opaccsA (_, _, _, _, lbl)
439    | ERTL.St_opaccsB (_, _, _, _, lbl)
440    | ERTL.St_op1 (_, _, _, lbl) | ERTL.St_op2 (_, _, _, _, lbl)
441    | ERTL.St_clear_carry lbl | ERTL.St_set_carry lbl
442    | ERTL.St_load (_, _, _, lbl)
443    | ERTL.St_store (_, _, _, lbl) | ERTL.St_call_id (_, _, lbl)
444    | ERTL.St_call_ptr (_, _, _, lbl)
445    | ERTL.St_newframe lbl | ERTL.St_delframe lbl | ERTL.St_framesize (_, lbl)
446      ->
447      aux lbl
448    | ERTL.St_cond _ | ERTL.St_return _ ->
449      (* No cost label found (no labelling performed). Indeed, the first cost
450         label must after some linear instructions. *)
451      (None, def) in
452  aux def.ERTL.f_entry
453
454let move_first_cost_label_up_internal def =
455  let (cost_label, def) = find_and_remove_first_cost_label def in
456  match cost_label with
457    | None -> def
458    | Some cost_label ->
459      generate (ERTL.St_cost (cost_label, def.ERTL.f_entry)) def
460
461let move_first_cost_label_up (id, def) =
462  let def' = match def with
463    | ERTL.F_int int_fun ->
464      ERTL.F_int (move_first_cost_label_up_internal int_fun)
465    | _ -> def in
466  (id, def')
467
468
469let translate p =
470  (* We simplify tail calls as regular calls for now. *)
471  let p = RTLtailcall.simplify p in
472  (* The tranformation on each RTL function: create an ERTL function and move
473     its first cost label at the very beginning. *)
474  let f funct = move_first_cost_label_up (translate_funct funct) in
475  { ERTL.vars   = p.RTL.vars ;
476    ERTL.functs = List.map f p.RTL.functs ;
477    ERTL.main   = p.RTL.main }
Note: See TracBrowser for help on using the repository browser.