source: Deliverables/D2.2/8051/src/cminor/cminorToRTLabs.ml @ 486

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

Deliverable D2.2

File size: 21.8 KB
Line 
1
2(** This module translates a [Cminor] program into a [RTLabs] program. *)
3
4open Driver
5
6
7let error_prefix = "Cminor to RTLabs"
8let error = Error.global_error error_prefix
9
10
11(* Helper functions *)
12
13let ptr_nb_ints = Driver.TargetArch.ptr_size / Driver.TargetArch.int_size
14
15let rec freshs runiverse n =
16  if n = 0 then []
17  else (Register.fresh runiverse) :: (freshs runiverse (n-1))
18
19let int_size_of_type = function
20  | AST.Type_void -> 0
21  | AST.Type_ret AST.Sig_int -> 1
22  | AST.Type_ret AST.Sig_ptr -> ptr_nb_ints
23  | AST.Type_ret AST.Sig_float -> error "floats not handled."
24
25let fresh_type runiverse ty = freshs runiverse (int_size_of_type ty)
26
27let fresh_result runiverse def = fresh_type runiverse def.Cminor.f_sig.AST.res
28
29let type_of_local def x =
30  if List.mem x def.Cminor.f_ptrs then AST.Type_ret AST.Sig_ptr
31  else
32    if List.mem x def.Cminor.f_vars then AST.Type_ret AST.Sig_int
33    else
34      let n = MiscPottier.index_of x def.Cminor.f_params in
35      AST.Type_ret (List.nth def.Cminor.f_sig.AST.args n)
36
37let type_of_cst = function
38  | AST.Cst_int _ -> AST.Sig_int
39  | AST.Cst_float _ -> error "floats not handled."
40  | AST.Cst_addrsymbol _ | AST.Cst_stackoffset _ -> AST.Sig_ptr
41
42let type_of_op1 = function
43  | AST.Op_cast8unsigned | AST.Op_cast8signed | AST.Op_cast16unsigned
44  | AST.Op_cast16signed | AST.Op_negint | AST.Op_notbool | AST.Op_notint
45  | AST.Op_intoffloat | AST.Op_intuoffloat | AST.Op_intofptr ->
46      AST.Sig_int
47  | AST.Op_negf | AST.Op_absf | AST.Op_singleoffloat | AST.Op_floatofint
48  | AST.Op_floatofintu ->
49      AST.Sig_float
50  | AST.Op_ptrofint ->
51      AST.Sig_ptr
52  | AST.Op_id ->
53      assert false (* Dependent on argument. Treated in type_of_expr *)
54
55let type_of_op2 = function
56  | AST.Op_add | AST.Op_sub | AST.Op_mul | AST.Op_div | AST.Op_divu | AST.Op_mod
57  | AST.Op_modu | AST.Op_and | AST.Op_or | AST.Op_xor | AST.Op_shl | AST.Op_shr
58  | AST.Op_shru ->
59      AST.Sig_int
60  | AST.Op_addf | AST.Op_subf | AST.Op_mulf | AST.Op_divf ->
61      AST.Sig_float
62  | AST.Op_cmp _ | AST.Op_cmpu _ | AST.Op_cmpf _ | AST.Op_cmpp _ ->
63      AST.Sig_int
64  | AST.Op_addp | AST.Op_subp ->
65      AST.Sig_ptr
66
67let rec type_of_expr def = function
68  | Cminor.Id x -> type_of_local def x
69  | Cminor.Cst cst -> AST.Type_ret (type_of_cst cst)
70  | Cminor.Op1 (AST.Op_id, e) -> type_of_expr def e
71  | Cminor.Op1 (op1, _) -> AST.Type_ret (type_of_op1 op1)
72  | Cminor.Op2 (op2, _, _) -> AST.Type_ret (type_of_op2 op2)
73  | Cminor.Mem (mq, _) -> AST.Type_ret (Memory.type_of_memory_q mq)
74  | Cminor.Cond _ -> AST.Type_ret AST.Sig_int
75  | Cminor.Exp_cost (_, e) -> type_of_expr def e
76
77let fresh_local runiverse def x =
78  fresh_type runiverse (type_of_local def x)
79
80let allocate (rtlabs_fun : RTLabs.internal_function) (n : int)
81    : RTLabs.internal_function * Register.t list =
82  let rs = freshs rtlabs_fun.RTLabs.f_runiverse n in
83  let rtlabs_fun =
84    { rtlabs_fun with RTLabs.f_locals = rtlabs_fun.RTLabs.f_locals @ [rs] } in
85  (rtlabs_fun, rs)
86
87let allocate_expr
88    (def        : Cminor.internal_function)
89    (rtlabs_fun : RTLabs.internal_function)
90    (e          : Cminor.expression)
91    : (RTLabs.internal_function * Register.t list) =
92  allocate rtlabs_fun (int_size_of_type (type_of_expr def e))
93
94type local_env = Register.t list StringTools.Map.t
95
96let find_local (lenv : local_env) (x : AST.ident) : Register.t list =
97  if StringTools.Map.mem x lenv then StringTools.Map.find x lenv
98  else error ("Unknown local \"" ^ x ^ "\".")
99
100let find_olocal (lenv : local_env) (ox : AST.ident option) : Register.t list =
101  match ox with
102    | None -> []
103    | Some x -> find_local lenv x
104
105let choose_destination
106    (def        : Cminor.internal_function)
107    (rtlabs_fun : RTLabs.internal_function)
108    (lenv       : local_env)
109    (e          : Cminor.expression)
110    : RTLabs.internal_function * Register.t list =
111  match e with
112    | Cminor.Id x -> (rtlabs_fun, find_local lenv x)
113    | _ -> allocate_expr def rtlabs_fun e
114
115let choose_destinations
116    (def        : Cminor.internal_function)
117    (rtlabs_fun : RTLabs.internal_function)
118    (lenv       : local_env)
119    (args       : Cminor.expression list)
120    : RTLabs.internal_function * Register.t list list =
121  let f (rtlabs_fun, regs) e =
122    let (rtlabs_fun, rs) = choose_destination def rtlabs_fun lenv e in
123    (rtlabs_fun, regs @ [rs]) in
124  List.fold_left f (rtlabs_fun, []) args
125
126let fresh_label (rtlabs_fun : RTLabs.internal_function) : Label.t =
127  Label.Gen.fresh rtlabs_fun.RTLabs.f_luniverse
128
129let change_entry
130    (rtlabs_fun : RTLabs.internal_function)
131    (new_entry : Label.t)
132    : RTLabs.internal_function =
133  { rtlabs_fun with RTLabs.f_entry = new_entry }
134
135
136(* Add a label and its associated instruction at the beginning of a function's
137   graph *)
138let add_graph
139    (rtlabs_fun : RTLabs.internal_function)
140    (lbl        : Label.t)
141    (stmt       : RTLabs.statement)
142    : RTLabs.internal_function =
143  let graph = Label.Map.add lbl stmt rtlabs_fun.RTLabs.f_graph in
144  let rtlabs_fun = { rtlabs_fun with RTLabs.f_graph = graph } in
145  change_entry rtlabs_fun lbl
146
147
148let generate
149    (rtlabs_fun : RTLabs.internal_function)
150    (stmt       : RTLabs.statement)
151    : RTLabs.internal_function =
152  let lbl = fresh_label rtlabs_fun in
153  add_graph rtlabs_fun lbl stmt
154
155
156(* [addressing e] returns the type of address represented by [e],
157   along with its arguments *)
158
159let addressing (e : Cminor.expression)
160    : (RTLabs.addressing * Cminor.expression list)  =
161  match e with
162    | Cminor.Cst (AST.Cst_addrsymbol id) -> (RTLabs.Aglobal (id, 0), [])
163    | Cminor.Cst (AST.Cst_stackoffset n) -> (RTLabs.Ainstack n, [])
164    | Cminor.Op2 (AST.Op_add,
165                  Cminor.Cst (AST.Cst_addrsymbol id),
166                  Cminor.Cst (AST.Cst_int n)) ->
167        (RTLabs.Aglobal (id, n), [])
168    | Cminor.Op2 (AST.Op_add, e1, Cminor.Cst (AST.Cst_int n)) ->
169        (RTLabs.Aindexed n, [e1])
170    | Cminor.Op2 (AST.Op_add,
171                  Cminor.Cst (AST.Cst_addrsymbol id),
172                  e2) ->
173        (RTLabs.Abased (id, 0), [e2])
174    | Cminor.Op2 (AST.Op_add, e1, e2) -> (RTLabs.Aindexed2, [e1 ; e2])
175    | _ -> (RTLabs.Aindexed 0, [e])
176
177
178(* Translating conditions
179
180   The Cminor definition [def] is used for typing purposes (differencing from
181   integers and pointers). [rtlabs_fun] is the function being
182   constructed. [lenv] is the environment associating a pseudo-register to the
183   variables of the program being translated. *)
184
185let rec translate_branch
186    (def        : Cminor.internal_function)
187    (rtlabs_fun : RTLabs.internal_function)
188    (lenv       : local_env)
189    (e          : Cminor.expression)
190    (lbl_true   : Label.t)
191    (lbl_false  : Label.t)
192    : RTLabs.internal_function =
193  match e with
194
195    | Cminor.Id x ->
196        let stmt =
197          RTLabs.St_cond1 (AST.Op_id, find_local lenv x, lbl_true, lbl_false) in
198        generate rtlabs_fun stmt
199
200    | Cminor.Cst cst ->
201        generate rtlabs_fun (RTLabs.St_condcst (cst, lbl_true, lbl_false))
202
203    | Cminor.Op1 (op1, e) ->
204        let (rtlabs_fun, rs) = choose_destination def rtlabs_fun lenv e in
205        let stmt = RTLabs.St_cond1 (op1, rs, lbl_true, lbl_false) in
206        let rtlabs_fun = generate rtlabs_fun stmt in
207        translate_expr def rtlabs_fun lenv rs e
208
209    | Cminor.Op2 (op2, e1, e2) ->
210        let (rtlabs_fun, rs1) = choose_destination def rtlabs_fun lenv e1 in
211        let (rtlabs_fun, rs2) = choose_destination def rtlabs_fun lenv e2 in
212        let stmt = RTLabs.St_cond2 (op2, rs1, rs2, lbl_true, lbl_false) in
213        let rtlabs_fun = generate rtlabs_fun stmt in
214        translate_exprs def rtlabs_fun lenv [rs1 ; rs2] [e1 ; e2]
215
216    | _ ->
217        let (rtlabs_fun, rs) = choose_destination def rtlabs_fun lenv e in
218        let stmt = RTLabs.St_cond1 (AST.Op_id, rs, lbl_true, lbl_false) in
219        let rtlabs_fun = generate rtlabs_fun stmt in
220        translate_expr def rtlabs_fun lenv rs e
221
222(* Translating expressions
223
224   The Cminor definition [def] is used for typing purposes (differencing from
225   integers and pointers). [rtlabs_fun] is the function being
226   constructed. [lenv] is the environment associating a pseudo-register to the
227   variables of the program being translated. [destrs] are the destination
228   registers. There may be more than one in the case of pointers, and when the
229   size of addresses is bigger than a machine word. *)
230
231and translate_expr
232    (def        : Cminor.internal_function)
233    (rtlabs_fun : RTLabs.internal_function)
234    (lenv       : local_env)
235    (destrs     : Register.t list)
236    (e          : Cminor.expression)
237    : RTLabs.internal_function =
238  match e with
239
240    | Cminor.Id x ->
241      let xrs = find_local lenv x in
242      let rec eq_reg_list rl1 rl2 = match rl1, rl2 with
243        | [], [] -> true
244        | r1 :: rl1, r2 :: rl2 ->
245          (Register.equal r1 r2) && (eq_reg_list rl1 rl2)
246        | _ -> false in
247      (* If the destinations and sources are the same, just do nothing. *)
248      if eq_reg_list destrs xrs then rtlabs_fun
249      else
250        let old_entry = rtlabs_fun.RTLabs.f_entry in
251        let stmt = RTLabs.St_op1 (AST.Op_id, destrs, xrs, old_entry) in
252        generate rtlabs_fun stmt
253
254    | Cminor.Cst cst ->
255      let old_entry = rtlabs_fun.RTLabs.f_entry in
256      let stmt = RTLabs.St_cst (destrs, cst, old_entry) in
257      generate rtlabs_fun stmt
258
259    | Cminor.Op1 (op1, e) ->
260      let (rtlabs_fun, rs) = choose_destination def rtlabs_fun lenv e in
261      let old_entry = rtlabs_fun.RTLabs.f_entry in
262      let stmt = RTLabs.St_op1 (op1, destrs, rs, old_entry) in
263      let rtlabs_fun = generate rtlabs_fun stmt in
264      translate_expr def rtlabs_fun lenv rs e
265
266    | Cminor.Op2 (op2, e1, e2) ->
267      let (rtlabs_fun, rs1) = choose_destination def rtlabs_fun lenv e1 in
268      let (rtlabs_fun, rs2) = choose_destination def rtlabs_fun lenv e2 in
269      let old_entry = rtlabs_fun.RTLabs.f_entry in
270      let stmt = RTLabs.St_op2 (op2, destrs, rs1, rs2, old_entry) in
271      let rtlabs_fun = generate rtlabs_fun stmt in
272      translate_exprs def rtlabs_fun lenv [rs1 ; rs2] [e1 ; e2]
273
274    | Cminor.Mem (chunk, e) ->
275      let (mode, args) = addressing e in
276      let (rtlabs_fun, regs) = choose_destinations def rtlabs_fun lenv args in
277      let old_entry = rtlabs_fun.RTLabs.f_entry in
278      let stmt = RTLabs.St_load (chunk, mode, regs, destrs, old_entry) in
279      let rtlabs_fun = generate rtlabs_fun stmt in
280      translate_exprs def rtlabs_fun lenv regs args
281
282    | Cminor.Cond (e1, e2, e3) ->
283      let old_entry = rtlabs_fun.RTLabs.f_entry in
284      let (rtlabs_fun, rs2) = choose_destination def rtlabs_fun lenv e2 in
285      let (rtlabs_fun, rs3) = choose_destination def rtlabs_fun lenv e3 in
286      let rtlabs_fun = translate_expr def rtlabs_fun lenv rs3 e3 in
287      let lbl_false = rtlabs_fun.RTLabs.f_entry in
288      let rtlabs_fun = change_entry rtlabs_fun old_entry in
289      let rtlabs_fun = translate_expr def rtlabs_fun lenv rs2 e2 in
290      let lbl_true = rtlabs_fun.RTLabs.f_entry in
291      translate_branch def rtlabs_fun lenv e1 lbl_true lbl_false
292
293    | Cminor.Exp_cost (lbl, e) ->
294      let (rtlabs_fun, rs) = choose_destination def rtlabs_fun lenv e in
295      let rtlabs_fun = translate_expr def rtlabs_fun lenv rs e in
296      let old_entry = rtlabs_fun.RTLabs.f_entry in
297      generate rtlabs_fun (RTLabs.St_cost (lbl, old_entry))
298
299and translate_exprs
300    (def        : Cminor.internal_function)
301    (rtlabs_fun : RTLabs.internal_function)
302    (lenv       : local_env)
303    (regs       : Register.t list list)
304    (args       : Cminor.expression list)
305    : RTLabs.internal_function =
306  let f destrs e rtlabs_fun = translate_expr def rtlabs_fun lenv destrs e in
307  List.fold_right2 f regs args rtlabs_fun
308
309
310(* Switch transformation
311
312   switch (e) {
313   case c0: exit i0;
314   case c1: exit i1;
315   ...
316   default: exit idfl; }
317
318   is translated to
319
320   if (e == c0) exit i0;
321   if (e == c1) exit i1;
322   ...
323   exit idfl; *)
324
325let transform_switch
326    (e : Cminor.expression)
327    (cases : (int * int) list)
328    (dfl : int)
329    : Cminor.statement =
330  let rec aux = function
331    | [] -> Cminor.St_skip
332    | (case, exit) :: cases ->
333        let c =
334          Cminor.Op2 (AST.Op_cmp AST.Cmp_eq,
335                      e, Cminor.Cst (AST.Cst_int case)) in
336        let stmt =
337          Cminor.St_ifthenelse (c, Cminor.St_exit exit, Cminor.St_skip) in
338        Cminor.St_seq (stmt, aux cases)
339  in
340  Cminor.St_seq (aux cases, Cminor.St_exit dfl)
341
342
343(* Translating statements
344
345   The Cminor definition [def] is used for typing purposes (differencing from
346   integers and pointers). [rtlabs_fun] is the function being
347   constructed. [lenv] is the environment associating a pseudo-register to the
348   variables of the program being translated. [exists] is the list of label to
349   exit to. The leftmost label in the list is used to exit the closest block. *)
350
351let rec translate_stmt
352    (def        : Cminor.internal_function)
353    (rtlabs_fun : RTLabs.internal_function)
354    (lenv       : local_env)
355    (exits      : Label.t list)
356    (stmt       : Cminor.statement)
357    : RTLabs.internal_function =
358  match stmt with
359
360    | Cminor.St_skip -> rtlabs_fun
361
362    | Cminor.St_assign (x, e) ->
363      translate_expr def rtlabs_fun lenv (find_local lenv x) e
364
365    | Cminor.St_store (chunk, e1, e2) ->
366      let (mode, args) = addressing e1 in
367      let (rtlabs_fun, regs) = choose_destinations def rtlabs_fun lenv args in
368      let (rtlabs_fun, rs) = choose_destination def rtlabs_fun lenv e2 in
369      let old_entry = rtlabs_fun.RTLabs.f_entry in
370      let stmt = RTLabs.St_store (chunk, mode, regs, rs, old_entry) in
371      let rtlabs_fun = generate rtlabs_fun stmt in
372      let rtlabs_fun = translate_expr def rtlabs_fun lenv rs e2 in
373      translate_exprs def rtlabs_fun lenv regs args
374
375    | Cminor.St_call (oret, Cminor.Cst (AST.Cst_addrsymbol f), args, sg) ->
376      let (rtlabs_fun, regs) = choose_destinations def rtlabs_fun lenv args in
377      let retrs = find_olocal lenv oret in
378      let old_entry = rtlabs_fun.RTLabs.f_entry in
379      let stmt = RTLabs.St_call_id (f, regs, retrs, sg, old_entry) in
380      let rtlabs_fun = generate rtlabs_fun stmt in
381      translate_exprs def rtlabs_fun lenv regs args
382
383    | Cminor.St_call (oret, f, args, sg) ->
384      let (rtlabs_fun, frs) = choose_destination def rtlabs_fun lenv f in
385      let (rtlabs_fun, regs) = choose_destinations def rtlabs_fun lenv args in
386      let retrs = find_olocal lenv oret in
387      let old_entry = rtlabs_fun.RTLabs.f_entry in
388      let stmt = RTLabs.St_call_ptr (frs, regs, retrs, sg, old_entry) in
389      let rtlabs_fun = generate rtlabs_fun stmt in
390      let rtlabs_fun = translate_exprs def rtlabs_fun lenv regs args in
391      translate_expr def rtlabs_fun lenv frs f
392
393    | Cminor.St_tailcall (Cminor.Cst (AST.Cst_addrsymbol f), args, sg) ->
394      let (rtlabs_fun, regs) = choose_destinations def rtlabs_fun lenv args in
395      let stmt = RTLabs.St_tailcall_id (f, regs, sg) in
396      let rtlabs_fun = generate rtlabs_fun stmt in
397      translate_exprs def rtlabs_fun lenv regs args
398
399    | Cminor.St_tailcall (f, args, sg) ->
400      let (rtlabs_fun, frs) = choose_destination def rtlabs_fun lenv f in
401      let (rtlabs_fun, regs) = choose_destinations def rtlabs_fun lenv args in
402      let stmt = RTLabs.St_tailcall_ptr (frs, regs, sg) in
403      let rtlabs_fun = generate rtlabs_fun stmt in
404      let rtlabs_fun = translate_exprs def rtlabs_fun lenv regs args in
405      translate_expr def rtlabs_fun lenv frs f
406
407    | Cminor.St_seq (s1, s2) ->
408      let rtlabs_fun = translate_stmt def rtlabs_fun lenv exits s2 in
409      translate_stmt def rtlabs_fun lenv exits s1
410
411    | Cminor.St_ifthenelse (e, s1, s2) ->
412      let old_entry = rtlabs_fun.RTLabs.f_entry in
413      let rtlabs_fun = translate_stmt def rtlabs_fun lenv exits s2 in
414      let lbl_false = rtlabs_fun.RTLabs.f_entry in
415      let rtlabs_fun = change_entry rtlabs_fun old_entry in
416      let rtlabs_fun = translate_stmt def rtlabs_fun lenv exits s1 in
417      let lbl_true = rtlabs_fun.RTLabs.f_entry in
418      translate_branch def rtlabs_fun lenv e lbl_true lbl_false
419
420    | Cminor.St_loop s ->
421      let loop_start = fresh_label rtlabs_fun in
422      let rtlabs_fun = change_entry rtlabs_fun loop_start in
423      let rtlabs_fun = translate_stmt def rtlabs_fun lenv exits s in
424      let old_entry = rtlabs_fun.RTLabs.f_entry in
425      add_graph rtlabs_fun loop_start (RTLabs.St_skip old_entry)
426
427    | Cminor.St_block s ->
428      let old_entry = rtlabs_fun.RTLabs.f_entry in
429      translate_stmt def rtlabs_fun lenv (old_entry :: exits) s
430
431    | Cminor.St_exit n ->
432      change_entry rtlabs_fun (List.nth exits n)
433
434    | Cminor.St_return eopt ->
435      let rtlabs_fun = change_entry rtlabs_fun rtlabs_fun.RTLabs.f_exit in
436      (match eopt, rtlabs_fun.RTLabs.f_result with
437        | None, _ -> rtlabs_fun
438        | Some e, retrs -> translate_expr def rtlabs_fun lenv retrs e)
439
440    | Cminor.St_switch (e, cases, dfl) ->
441      let stmt = transform_switch e cases dfl in
442      translate_stmt def rtlabs_fun lenv exits stmt
443
444    | Cminor.St_label (lbl, s) ->
445      let rtlabs_fun = translate_stmt def rtlabs_fun lenv exits s in
446      let old_entry = rtlabs_fun.RTLabs.f_entry in
447      add_graph rtlabs_fun lbl (RTLabs.St_skip old_entry)
448
449    | Cminor.St_cost (lbl, s) ->
450      let rtlabs_fun = translate_stmt def rtlabs_fun lenv exits s in
451      let old_entry = rtlabs_fun.RTLabs.f_entry in
452      generate rtlabs_fun (RTLabs.St_cost (lbl, old_entry))
453
454    | Cminor.St_goto lbl ->
455      change_entry rtlabs_fun lbl
456
457
458(* Translating function definitions *)
459
460(* The translation consists in the following:
461   - Create a universe of pseudo-register names
462   - Create a universe of label names
463   - Create a local environment; that is, a mapping from local
464     variables to pseudo-registers
465   - Extract the registers representing the formal variables
466   - Extract the registers representing the local variables
467   - Allocate a fresh label representing the exit point
468   - Allocate fresh registers holding the result of the function
469   - Initialize the graph with a return instruction at the end
470   - Complete the graph according to the function's body.
471     Instructions will be added from end to start following the flow of the
472     function. *)
473
474let translate_internal lbl_prefix f_def =
475
476  (* Register names *)
477  let runiverse = Register.new_universe "%" in
478
479  (* Labels of statements *)
480  let luniverse = Label.Gen.new_universe lbl_prefix in
481
482  (* Local environment *)
483  let add_local lenv x =
484    let rs = fresh_local runiverse f_def x in
485    StringTools.Map.add x rs lenv in
486  let lenv = StringTools.Map.empty in
487  let lenv = List.fold_left add_local lenv f_def.Cminor.f_params in
488  let lenv = List.fold_left add_local lenv f_def.Cminor.f_vars in
489  let lenv = List.fold_left add_local lenv f_def.Cminor.f_ptrs in
490
491  let extract vars =
492    List.fold_left (fun l x -> l @ [StringTools.Map.find x lenv]) [] vars in
493
494  (* Parameter registers *)
495  let params = extract f_def.Cminor.f_params in
496 
497 (* Local registers *)
498  let locals = extract (f_def.Cminor.f_vars @ f_def.Cminor.f_ptrs) in
499
500  (* Exit label of the graph *)
501  let exit = Label.Gen.fresh luniverse in
502
503  (* [retrs] are the registers that holds the return value of the body, if
504     any. *)
505  let retrs = fresh_result runiverse f_def in
506
507  let locals = locals @ [retrs] in
508
509  (* The control flow graph: for now, it is only a return instruction at the
510     end. *)
511  let graph = Label.Map.add exit (RTLabs.St_return retrs) Label.Map.empty in
512
513  let rtlabs_fun =
514    { RTLabs.f_luniverse = luniverse ;
515      RTLabs.f_runiverse = runiverse ;
516      RTLabs.f_sig       = f_def.Cminor.f_sig ;
517      RTLabs.f_result    = retrs ;
518      RTLabs.f_params    = params ;
519      RTLabs.f_locals    = locals ;
520      RTLabs.f_stacksize = f_def.Cminor.f_stacksize ;
521      RTLabs.f_graph     = graph ;
522      RTLabs.f_entry     = exit ;
523      RTLabs.f_exit      = exit } in
524
525  (* Complete the graph *)
526  translate_stmt f_def rtlabs_fun lenv [] f_def.Cminor.f_body
527
528
529let translate_functions lbls (f_id, f_def) = match f_def with
530  | Cminor.F_int int_def ->
531      let lbl_prefix = StringTools.Gen.fresh_prefix lbls f_id in
532      let def = translate_internal lbl_prefix int_def in
533      (f_id, RTLabs.F_int def)
534  | Cminor.F_ext def -> (f_id, RTLabs.F_ext def)
535
536
537(* Initialization of globals *)
538
539let assign_data x stmt (data, off) =
540  let e = Cminor.Op2 (AST.Op_add,
541                      Cminor.Cst (AST.Cst_addrsymbol x),
542                      Cminor.Cst (AST.Cst_int off)) in
543  let chunk () = Memory.mq_of_data data in
544  let stmt' = match data with
545    | AST.Data_reserve _ -> Cminor.St_skip
546    | AST.Data_int8 i | AST.Data_int16 i | AST.Data_int32 i ->
547        Cminor.St_store (chunk (), e, Cminor.Cst (AST.Cst_int i))
548    | AST.Data_float32 f | AST.Data_float64 f ->
549        Cminor.St_store (chunk (), e, Cminor.Cst (AST.Cst_float f)) in
550  Cminor.St_seq (stmt, stmt')
551
552let add_global_initializations_body vars body =
553  let f stmt (x, datas) =
554    let offs_of_datas = RTLabsMemory.offsets_of_datas datas in
555    List.fold_left (assign_data x) stmt offs_of_datas in
556  Cminor.St_seq (List.fold_left f Cminor.St_skip vars, body)
557
558let add_global_initializations_funct vars = function
559  | Cminor.F_int def ->
560      let f_body = add_global_initializations_body vars def.Cminor.f_body in
561      Cminor.F_int { def with Cminor.f_body = f_body }
562  | def -> def
563
564(* [add_global_initializations p] moves the initializations of the globals of
565   [p] to the beginning of the main function, if any. *)
566
567let add_global_initializations p = match p.Cminor.main with
568  | None -> p.Cminor.functs
569  | Some main ->
570    let main_def = List.assoc main p.Cminor.functs in
571    let main_def = add_global_initializations_funct p.Cminor.vars main_def in
572    MiscPottier.update_list_assoc main main_def p.Cminor.functs
573
574
575(* Translation of a Cminor program to a RTLabs program. *)
576
577let translate p =
578
579  (* Fetch the variables in the program that are pointers (whose value is an
580     address). Some architectures have different sizes for pointers and
581     integers. *)
582  let p = CminorPointers.fill p in
583
584  (* Fetch the labels already used in the program to create new ones. *)
585  let lbls = CminorAnnotator.all_labels p in
586
587  (* The initialization of globals are moved at the beginning of the main. *)
588  let functs = add_global_initializations p in
589
590  (* The globals are associated their size. *)
591  let f (id, datas) = (id, RTLabsMemory.size_of_datas datas) in
592
593  (* Put all this together and translate each function. *)
594  { RTLabs.vars = List.map f p.Cminor.vars ;
595    RTLabs.functs = List.map (translate_functions lbls) functs ;
596    RTLabs.main = p.Cminor.main }
Note: See TracBrowser for help on using the repository browser.