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

Last change on this file since 740 was 740, checked in by ayache, 10 years ago

New memory model and bug fixes in 8051 branch. Added primitive operations in interpreters from Clight to LIN.

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