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

Last change on this file since 740 was 740, checked in by ayache, 9 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.