source: Deliverables/D2.2/8051/src/clight/clightToCminor.ml @ 1462

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

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

File size: 22.0 KB
Line 
1
2
3let error_prefix = "Clight to Cminor"
4let error = Error.global_error error_prefix
5let error_float () = error "float not supported."
6
7
8(* General helpers *)
9
10let clight_type_of (Clight.Expr (_, t)) = t
11
12let cminor_type_of (Cminor.Expr (_, t)) = t
13
14
15(* Translate types *)
16
17let byte_size_of_intsize = function
18  | Clight.I8 -> 1
19  | Clight.I16 -> 2
20  | Clight.I32 -> 4
21
22let sig_type_of_ctype = function
23  | Clight.Tvoid -> assert false (* do not use on this argument *)
24  | Clight.Tint (intsize, sign) ->
25    AST.Sig_int (byte_size_of_intsize intsize, sign)
26  | Clight.Tfloat _ -> error_float ()
27  | Clight.Tfunction _ | Clight.Tstruct _ | Clight.Tunion _
28  | Clight.Tpointer _ | Clight.Tarray _ | Clight.Tcomp_ptr _ -> AST.Sig_ptr
29
30let translate_args_types = List.map sig_type_of_ctype
31
32let type_return_of_ctype = function
33  | Clight.Tvoid -> AST.Type_void
34  | t -> AST.Type_ret (sig_type_of_ctype t)
35
36let quantity_of_sig_type = function
37  | AST.Sig_int (size, _) -> AST.QInt size
38  | AST.Sig_float _ -> error_float ()
39  | AST.Sig_offset -> AST.QOffset
40  | AST.Sig_ptr -> AST.QPtr
41
42let quantity_of_ctype t = quantity_of_sig_type (sig_type_of_ctype t)
43
44let rec sizeof_ctype = function
45  | Clight.Tvoid | Clight.Tfunction _ -> AST.SQ (AST.QInt 1)
46  | Clight.Tfloat _ -> error_float ()
47  | Clight.Tint (size, _) -> AST.SQ (AST.QInt (byte_size_of_intsize size))
48  | Clight.Tpointer _
49  | Clight.Tcomp_ptr _ -> AST.SQ AST.QPtr
50  | Clight.Tarray (t, n) -> AST.SArray (n, sizeof_ctype t)
51  | Clight.Tstruct (_, fields) ->
52    AST.SProd (List.map sizeof_ctype (List.map snd fields))
53  | Clight.Tunion (_, fields) ->
54    AST.SSum (List.map sizeof_ctype (List.map snd fields))
55
56let global_size_of_ctype = sizeof_ctype
57
58
59(** Helpers on abstract sizes and offsets *)
60
61let max_stacksize size1 size2 = match size1, size2 with
62  | AST.SProd l1, AST.SProd l2 when List.length l1 > List.length l2 -> size1
63  | AST.SProd l1, AST.SProd l2 -> size2
64  | _ -> raise (Failure "ClightToCminor.max_stacksize")
65
66(** Hypothesis: [offset1] is a prefix of [offset2] or vice-versa. *)
67let max_offset offset1 offset2 =
68  if List.length offset1 > List.length offset2 then offset1
69  else offset2
70
71let next_depth = function
72  | AST.SProd l -> List.length l
73  | _ -> raise (Failure "ClightToCminor.next_offset")
74
75let add_stack offset =
76  let e1 = Cminor.Expr (Cminor.Cst AST.Cst_stack, AST.Sig_ptr) in
77  let e2 = Cminor.Expr (Cminor.Cst (AST.Cst_offset offset), AST.Sig_offset) in
78  Cminor.Op2 (AST.Op_addp, e1, e2)
79
80let add_stacksize t = function
81  | AST.SProd l -> AST.SProd (l @ [sizeof_ctype t])
82  | _ -> raise (Failure "ClightToCminor.add_stacksize")
83
84let struct_depth field fields =
85  let rec aux i = function
86    | [] -> error ("unknown field " ^ field ^ ".")
87    | (field', t) :: _ when field' = field -> i
88    | (_, t) :: fields -> aux (i+1) fields in
89  aux 0 fields
90
91let struct_offset t field fields =
92  let size = sizeof_ctype t in
93  let depth = struct_depth field fields in
94  let offset = (size, depth) in
95  let t = AST.Sig_offset in
96  Cminor.Expr (Cminor.Cst (AST.Cst_offset offset), t)
97
98
99(** Sort variables: locals, parameters, globals, in stack. *)
100
101type location = 
102  | Local
103  | LocalStack of AST.abstract_offset
104  | Param
105  | ParamStack of AST.abstract_offset
106  | Global
107
108(** Below are some helper definitions to ease the manipulation of a translation
109    environment for variables. *)
110
111type var_locations = (location * Clight.ctype) StringTools.Map.t
112
113let empty_var_locs : var_locations = StringTools.Map.empty
114
115let add_var_locs : AST.ident -> (location * Clight.ctype) -> var_locations ->
116  var_locations =
117  StringTools.Map.add
118
119let mem_var_locs : AST.ident -> var_locations -> bool = StringTools.Map.mem
120
121let find_var_locs : AST.ident -> var_locations -> (location * Clight.ctype) =
122  StringTools.Map.find
123
124let fold_var_locs : (AST.ident -> (location * Clight.ctype) -> 'a -> 'a) ->
125  var_locations -> 'a -> 'a =
126  StringTools.Map.fold
127
128
129let is_local_or_param id var_locs = match find_var_locs id var_locs with
130  | (Local, _) | (Param, _) -> true
131  | _ -> false
132
133let get_locals var_locs =
134  let f id (location, ctype) locals =
135    let added = match location with
136      | Local -> [(id, sig_type_of_ctype ctype)]
137      | _ -> [] in
138    locals @ added in
139  fold_var_locs f var_locs []
140
141let get_stacksize var_locs =
142  let f _ (location, _) res = match location with
143    | LocalStack (stacksize, _) | ParamStack (stacksize, _) ->
144      max_stacksize res stacksize
145    | _ -> res in
146  fold_var_locs f var_locs (AST.SProd [])
147
148
149(* Variables of a function that will go in stack: variables of a complex type
150   (array, structure or union) and variables whose address is evaluated. *)
151
152let is_function_ctype = function
153  | Clight.Tfunction _ -> true
154  | _ -> false
155
156let is_scalar_ctype : Clight.ctype -> bool = function
157  | Clight.Tint _ | Clight.Tfloat _ | Clight.Tpointer _ -> true
158  | _ -> false
159
160let is_complex_ctype : Clight.ctype -> bool = function
161  | Clight.Tarray _ | Clight.Tstruct _ | Clight.Tunion _ | Clight.Tfunction _ ->
162    true
163  | _ -> false
164
165let complex_ctype_vars cfun =
166  let f set (x, t) =
167    if is_complex_ctype t then StringTools.Set.add x set else set in
168  (* Because of CIL, parameters should not have a complex type, but let's add
169     them just in case. *)
170  List.fold_left f StringTools.Set.empty
171    (cfun.Clight.fn_params @ cfun.Clight.fn_vars)
172
173let union_list = List.fold_left StringTools.Set.union StringTools.Set.empty
174
175let f_expr (Clight.Expr (ed, _)) sub_exprs_res =
176  let res_ed = match ed with
177    | Clight.Eaddrof (Clight.Expr (Clight.Evar id, _)) ->
178      StringTools.Set.singleton id
179    | _ -> StringTools.Set.empty in
180  union_list (res_ed :: sub_exprs_res)
181
182let f_stmt _ sub_exprs_res sub_stmts_res =
183  union_list (sub_exprs_res @ sub_stmts_res)
184
185let addr_vars_fun cfun = ClightFold.statement2 f_expr f_stmt cfun.Clight.fn_body
186
187let stack_vars cfun =
188  StringTools.Set.union (complex_ctype_vars cfun) (addr_vars_fun cfun)
189
190
191let sort_stacks stack_location vars var_locs =
192  let stacksize = get_stacksize var_locs in
193  let f (current_stacksize, var_locs) (id, t) =
194    let depth = next_depth current_stacksize in
195    let current_stacksize = add_stacksize t current_stacksize in
196    let offset = (current_stacksize, depth) in
197    let var_locs = add_var_locs id (stack_location offset, t) var_locs in
198    (current_stacksize, var_locs) in
199  snd (List.fold_left f (stacksize, var_locs) vars)
200
201let sort_normals normal_location vars var_locs =
202  let f var_locs (id, ctype) =
203    add_var_locs id (normal_location, ctype) var_locs in
204  List.fold_left f var_locs vars
205
206let sort_vars normal_location stack_location_opt stack_vars vars var_locs =
207  let f_stack (x, _) = StringTools.Set.mem x stack_vars in
208  let (f_normal, var_locs) = match stack_location_opt with
209    | None -> ((fun _ -> true), var_locs)
210    | Some stack_location ->
211      ((fun var -> not (f_stack var)),
212       sort_stacks stack_location (List.filter f_stack vars) var_locs) in
213  sort_normals normal_location (List.filter f_normal vars) var_locs
214
215let sort_locals = sort_vars Local (Some (fun offset -> LocalStack offset))
216
217let sort_params = sort_vars Param (Some (fun offset -> ParamStack offset))
218
219let sort_globals stack_vars globals functs var_locs =
220  let globals = List.map (fun ((id, _), ctype) -> (id, ctype)) globals in
221  let f_functs (id, fundef) =
222    let (params, return) =  match fundef with
223      | Clight.Internal cfun ->
224        (List.map snd cfun.Clight.fn_params, cfun.Clight.fn_return)
225      | Clight.External (_, params, return) -> (params, return) in
226    (id, Clight.Tfunction (params, return)) in
227  let functs = List.map f_functs functs in
228  let globals = globals @ functs in
229  sort_vars Global None stack_vars globals var_locs
230
231(* The order of insertion in the sorting environment is important: it follows
232   the scope conventions of C. Local variables hide parameters that hide
233   globals. *)
234
235let sort_variables globals functs cfun =
236  let stack_vars = stack_vars cfun in
237  let var_locs = empty_var_locs in
238  let var_locs = sort_globals stack_vars globals functs var_locs in
239  let var_locs = sort_params stack_vars cfun.Clight.fn_params var_locs in
240  let var_locs = sort_locals stack_vars cfun.Clight.fn_vars var_locs in
241  var_locs
242
243
244(* Translate globals *)
245
246let init_to_data = function
247  | [Clight.Init_space _] -> None
248  | l -> Some (List.map (
249  function 
250    | Clight.Init_int8 i       -> AST.Data_int8 i
251    | Clight.Init_int16 i      -> AST.Data_int16 i
252    | Clight.Init_int32 i      -> AST.Data_int32 i
253    | Clight.Init_float32 _ 
254    | Clight.Init_float64 _    -> error_float ()
255    | Clight.Init_space n      -> error "bad global initialization style."
256    | Clight.Init_addrof (_,_) -> assert false (*TODO*)
257) l)
258
259let translate_global ((id,lst),t) = (id,global_size_of_ctype t,init_to_data lst)
260
261
262(* Translate expression *)
263
264let translate_unop = function
265  | Clight.Onotbool -> AST.Op_notbool
266  | Clight.Onotint -> AST.Op_notint
267  | Clight.Oneg -> AST.Op_negint
268
269let esizeof_ctype res_type t =
270  Cminor.Expr (Cminor.Cst (AST.Cst_sizeof (sizeof_ctype t)), res_type)
271
272let translate_add res_type ctype1 ctype2 e1 e2 = match ctype1, ctype2 with
273  | Clight.Tint _, Clight.Tint _ ->
274    Cminor.Expr (Cminor.Op2 (AST.Op_add, e1, e2), res_type)
275  | Clight.Tfloat _, Clight.Tfloat _ -> error_float ()
276  | Clight.Tpointer t, Clight.Tint _
277  | Clight.Tarray (t, _), Clight.Tint _ ->
278    let t2 = cminor_type_of e2 in
279    let size = esizeof_ctype t2 t in
280    let index = Cminor.Expr (Cminor.Op2 (AST.Op_mul, e2, size), t2) in
281    Cminor.Expr (Cminor.Op2 (AST.Op_addp, e1, index), res_type)
282  | Clight.Tint _, Clight.Tpointer t
283  | Clight.Tint _, Clight.Tarray (t, _) -> 
284    let t1 = cminor_type_of e1 in
285    let size = esizeof_ctype t1 t in
286    let index = Cminor.Expr (Cminor.Op2 (AST.Op_mul, e1, size), t1) in
287    Cminor.Expr (Cminor.Op2 (AST.Op_addp, e2, index), res_type)
288  | _ -> error "type error."
289
290let translate_sub res_type ctype1 ctype2 e1 e2 = match ctype1, ctype2 with
291  | Clight.Tint _, Clight.Tint _ ->
292    Cminor.Expr (Cminor.Op2 (AST.Op_sub, e1, e2), res_type)
293  | Clight.Tfloat _, Clight.Tfloat _ -> error_float ()
294  | Clight.Tpointer t, Clight.Tint _
295  | Clight.Tarray (t, _), Clight.Tint _ ->
296    let t2 = cminor_type_of e2 in
297    let size = esizeof_ctype t2 t in
298    let index = Cminor.Expr (Cminor.Op2 (AST.Op_mul, e2, size), t2) in
299    Cminor.Expr (Cminor.Op2 (AST.Op_subp, e1, index), res_type)
300  | Clight.Tpointer _, Clight.Tpointer _
301  | Clight.Tarray _, Clight.Tpointer _
302  | Clight.Tpointer _, Clight.Tarray _
303  | Clight.Tarray _, Clight.Tarray _ ->
304    Cminor.Expr (Cminor.Op2 (AST.Op_subpp, e1, e2), res_type)
305  | _ -> error "type error."
306
307let is_signed = function
308  | Clight.Tint (_, AST.Signed) -> true
309  | _ -> false
310
311let is_pointer = function
312  | Clight.Tpointer _ | Clight.Tarray _ -> true
313  | _ -> false
314
315let cmp_of_clight_binop = function
316  | Clight.Oeq -> AST.Cmp_eq
317  | Clight.One -> AST.Cmp_ne
318  | Clight.Olt -> AST.Cmp_lt
319  | Clight.Ole -> AST.Cmp_le
320  | Clight.Ogt -> AST.Cmp_gt
321  | Clight.Oge -> AST.Cmp_ge
322  | _ -> assert false (* do not use on these arguments *)
323
324let translate_simple_binop t = function
325  | Clight.Omul -> AST.Op_mul
326  | Clight.Odiv when is_signed t -> AST.Op_div
327  | Clight.Odiv -> AST.Op_divu
328  | Clight.Omod when is_signed t -> AST.Op_mod
329  | Clight.Omod -> AST.Op_modu
330  | Clight.Oand -> AST.Op_and
331  | Clight.Oor -> AST.Op_or
332  | Clight.Oxor -> AST.Op_xor
333  | Clight.Oshl -> AST.Op_shl
334  | Clight.Oshr when is_signed t -> AST.Op_shr
335  | Clight.Oshr -> AST.Op_shru
336  | binop when is_pointer t -> AST.Op_cmpp (cmp_of_clight_binop binop)
337  | binop when is_signed t -> AST.Op_cmp (cmp_of_clight_binop binop)
338  | binop -> AST.Op_cmpu (cmp_of_clight_binop binop)
339
340let translate_binop res_type ctype1 ctype2 e1 e2 binop =
341  match binop with
342    | Clight.Oadd -> translate_add res_type ctype1 ctype2 e1 e2
343    | Clight.Osub -> translate_sub res_type ctype1 ctype2 e1 e2
344    | _ ->
345      let cminor_binop = translate_simple_binop ctype1 binop in
346      Cminor.Expr (Cminor.Op2 (cminor_binop, e1, e2), res_type)
347
348let translate_ident var_locs res_type x =
349  let ed = match find_var_locs x var_locs with
350    | (Local, _) | (Param, _) -> Cminor.Id x
351    | (LocalStack off, t) | (ParamStack off, t) when is_scalar_ctype t ->
352      let addr = Cminor.Expr (add_stack off, AST.Sig_ptr) in
353      Cminor.Mem (quantity_of_ctype t, addr)
354    | (LocalStack off, _) | (ParamStack off, _) ->
355      add_stack off
356    | (Global, t) when is_scalar_ctype t ->
357      let addr = Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol x), AST.Sig_ptr) in
358      Cminor.Mem (quantity_of_ctype t, addr)
359    | (Global, _) -> Cminor.Cst (AST.Cst_addrsymbol x) in
360  Cminor.Expr (ed, res_type)
361
362let translate_field res_type t e field =
363  let (fields, offset) = match t with
364    | Clight.Tstruct (_, fields) -> (fields, struct_offset t field fields)
365    | Clight.Tunion (_, fields) ->
366      (fields, Cminor.Expr (Cminor.Cst (AST.Cst_int 0), AST.Sig_offset))
367    | _ -> assert false (* type error *) in
368  let addr = Cminor.Expr (Cminor.Op2 (AST.Op_addp, e, offset), AST.Sig_ptr) in
369  let quantity = quantity_of_ctype (List.assoc field fields) in
370  Cminor.Expr (Cminor.Mem (quantity, addr), res_type)
371
372let translate_cast e src_type dest_type =
373  let res_type = sig_type_of_ctype dest_type in
374  match src_type, dest_type with
375    | Clight.Tint (size1, sign1), Clight.Tint (size2, _) ->
376      let t1 = (byte_size_of_intsize size1, sign1) in
377      let t2 = byte_size_of_intsize size2 in
378      Cminor.Expr (Cminor.Op1 (AST.Op_cast (t1, t2), e), res_type)
379    | Clight.Tint _, Clight.Tpointer _
380    | Clight.Tint _, Clight.Tarray _ ->
381      Cminor.Expr (Cminor.Op1 (AST.Op_ptrofint, e), res_type)
382    | Clight.Tpointer _, Clight.Tint _
383    | Clight.Tarray _, Clight.Tint _ ->
384      Cminor.Expr (Cminor.Op1 (AST.Op_intofptr, e), res_type)
385    | _ -> e
386
387let rec f_expr var_locs (Clight.Expr (ed, t)) sub_exprs_res =
388  let t_cminor = sig_type_of_ctype t in
389  let cst_int i t = Cminor.Expr (Cminor.Cst (AST.Cst_int i), t) in
390  match ed, sub_exprs_res with
391
392  | Clight.Econst_int i, _ ->
393    Cminor.Expr (Cminor.Cst (AST.Cst_int i), t_cminor)
394
395  | Clight.Econst_float _, _ -> error_float ()
396
397  | Clight.Evar x, _ when is_function_ctype t ->
398    Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol x), t_cminor)
399
400  | Clight.Evar x, _ -> translate_ident var_locs t_cminor x
401
402  | Clight.Ederef _, e :: _ when is_scalar_ctype t ->
403    Cminor.Expr (Cminor.Mem (quantity_of_ctype t, e), t_cminor)
404
405  | Clight.Ederef _, e :: _ ->
406    (* When dereferencing something pointing to a struct for instance, the
407       result is the address of the struct. *)
408    e
409
410  | Clight.Eaddrof e, _ -> translate_addrof var_locs e
411
412  | Clight.Eunop (unop, _), e :: _ -> 
413    Cminor.Expr (Cminor.Op1 (translate_unop unop, e), t_cminor)
414
415  | Clight.Ebinop (binop, e1, e2), e1' :: e2' :: _ -> 
416    translate_binop t_cminor (clight_type_of e1) (clight_type_of e2) e1' e2'
417      binop
418
419  | Clight.Ecast (t, Clight.Expr (_, t')), e :: _ -> translate_cast e t' t
420
421  | Clight.Econdition _, e1 :: e2 :: e3 :: _ ->
422    Cminor.Expr (Cminor.Cond (e1, e2, e3), t_cminor)
423
424  | Clight.Eandbool _, e1 :: e2 :: _ -> 
425    let zero = cst_int 0 t_cminor in
426    let one = cst_int 1 t_cminor in
427    let e2_cond = Cminor.Expr (Cminor.Cond (e2, one, zero), t_cminor) in
428    Cminor.Expr (Cminor.Cond (e1, e2_cond, zero), t_cminor)
429
430  | Clight.Eorbool _, e1 :: e2 :: _ -> 
431    let zero = cst_int 0 t_cminor in
432    let one = cst_int 1 t_cminor in
433    let e2_cond = Cminor.Expr (Cminor.Cond (e2, one, zero), t_cminor) in
434    Cminor.Expr (Cminor.Cond (e1, one, e2_cond), t_cminor)
435
436  | Clight.Esizeof t, _ -> esizeof_ctype t_cminor t
437
438  | Clight.Ecost (lbl, _), e :: _ ->
439    Cminor.Expr (Cminor.Exp_cost (lbl, e), t_cminor)
440
441  | Clight.Ecall _, _ -> assert false (* only for annotations *)
442
443  | Clight.Efield (Clight.Expr (_, t), field), e :: _ ->
444    translate_field t_cminor t e field
445
446  | _ -> assert false (* wrong number of arguments *)
447
448and translate_addrof_ident res_type var_locs id =
449  assert (mem_var_locs id var_locs) ;
450  match find_var_locs id var_locs with
451    | (Local, _) | (Param, _) -> assert false (* location error *)
452    | (LocalStack off, _) | (ParamStack off, _) ->
453      Cminor.Expr (add_stack off, res_type)
454    | (Global, _) ->
455      Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol id), res_type)
456
457and translate_addrof_field res_type t field e =
458  let (fields, offset) = match t with
459    | Clight.Tstruct (_, fields) -> (fields, struct_offset t field fields)
460    | Clight.Tunion (_, fields) ->
461      (fields, Cminor.Expr (Cminor.Cst (AST.Cst_int 0), AST.Sig_offset))
462    | _ -> assert false (* type error *) in
463  Cminor.Expr (Cminor.Op2 (AST.Op_addp, e, offset), res_type)
464
465and translate_addrof var_locs (Clight.Expr (ed, _)) =
466  let res_type = AST.Sig_ptr in
467  match ed with
468
469    | Clight.Evar id -> translate_addrof_ident res_type var_locs id
470
471    | Clight.Ederef e -> translate_expr var_locs e
472
473    | Clight.Efield ((Clight.Expr (_, t) as e), field) ->
474      let e = translate_expr var_locs e in
475      translate_addrof_field res_type t field e
476
477    | _ -> assert false (* not a lvalue *)
478
479and translate_expr var_locs e = ClightFold.expr2 (f_expr var_locs) e
480
481
482(* Translate statement *)
483
484let assign var_locs (Clight.Expr (ed, t) as e_res_clight) e_arg_cminor =
485  match ed with
486    | Clight.Evar id when is_local_or_param id var_locs ->
487      Cminor.St_assign (id, e_arg_cminor)
488    | _ ->
489      let quantity = quantity_of_ctype t in
490      let addr = translate_addrof var_locs e_res_clight in
491      Cminor.St_store (quantity, addr, e_arg_cminor)
492
493let call_sig ret_type args =
494  { AST.args = List.map cminor_type_of args ;
495    AST.res = ret_type }
496
497let f_stmt fresh var_locs stmt sub_exprs_res sub_stmts_res =
498  let (tmps, sub_stmts_res) = List.split sub_stmts_res in
499  let tmps = List.flatten tmps in
500
501  let (added_tmps, stmt) = match stmt, sub_exprs_res, sub_stmts_res with
502
503    | Clight.Sskip, _, _ -> ([], Cminor.St_skip)
504
505    | Clight.Sassign (e1, _), _ :: e2 :: _, _ ->
506      ([], assign var_locs e1 e2)
507
508    | Clight.Scall (None, _, _), f :: args, _ ->
509      ([], Cminor.St_call (None, f, args, call_sig AST.Type_void args))
510
511    | Clight.Scall (Some e, _, _), _ :: f :: args, _ ->
512      let t = sig_type_of_ctype (clight_type_of e) in
513      let tmp = fresh () in
514      let tmpe = Cminor.Expr (Cminor.Id tmp, t) in
515      let stmt_call =
516        Cminor.St_call (Some tmp, f, args, call_sig (AST.Type_ret t) args) in
517      let stmt_assign = assign var_locs e tmpe in
518      ([(tmp, t)], Cminor.St_seq (stmt_call, stmt_assign))
519
520    | Clight.Swhile _, e :: _, stmt :: _ ->
521      let econd =
522        Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in
523      let scond =
524        Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in
525      ([],
526       Cminor.St_block (Cminor.St_loop (Cminor.St_seq (scond,
527                                                       Cminor.St_block stmt))))
528
529    | Clight.Sdowhile _, e :: _, stmt :: _ ->
530      let econd =
531        Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in
532      let scond =
533        Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in
534      ([],
535       Cminor.St_block (Cminor.St_loop (Cminor.St_seq (Cminor.St_block stmt,
536                                                       scond))))
537
538    | Clight.Sfor _, e :: _, stmt1 :: stmt2 :: stmt3 :: _ ->
539      let econd = 
540        Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in
541      let scond =
542        Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in
543      let body = Cminor.St_seq (Cminor.St_block stmt3, stmt2) in
544      ([],
545       Cminor.St_seq (stmt1,
546                      Cminor.St_block
547                        (Cminor.St_loop (Cminor.St_seq (scond, body)))))
548
549    | Clight.Sifthenelse _, e :: _, stmt1 :: stmt2 :: _ ->
550      ([], Cminor.St_ifthenelse (e, stmt1, stmt2))
551
552    | Clight.Ssequence _, _, stmt1 :: stmt2 :: _ ->
553      ([], Cminor.St_seq (stmt1, stmt2))
554
555    | Clight.Sbreak, _, _ -> ([], Cminor.St_exit 1)
556
557    | Clight.Scontinue, _, _ -> ([], Cminor.St_exit 0)
558
559    | Clight.Sswitch _, _, _ ->
560      (* Should not appear because of switch transformation performed
561         beforehand. *)
562      assert false
563
564    | Clight.Sreturn None, _, _ -> ([], Cminor.St_return None)
565
566    | Clight.Sreturn (Some _), e :: _, _ -> ([], Cminor.St_return (Some e))
567
568    | Clight.Slabel (lbl, _), _, stmt :: _ -> ([], Cminor.St_label (lbl, stmt))
569
570    | Clight.Sgoto lbl, _, _ -> ([], Cminor.St_goto lbl)
571
572    | Clight.Scost (lbl, _), _, stmt :: _ -> ([], Cminor.St_cost (lbl, stmt))
573
574    | _ -> assert false (* type error *) in
575
576  (tmps @ added_tmps, stmt)
577
578let translate_statement fresh var_locs =
579  ClightFold.statement2 (f_expr var_locs) (f_stmt fresh var_locs)
580
581
582(* Translate functions and programs *)
583
584let add_stack_parameter_initialization x t off body =
585  let addr = Cminor.Expr (add_stack off, AST.Sig_ptr) in
586  let e = Cminor.Expr (Cminor.Id x, sig_type_of_ctype t) in
587  let stmt = Cminor.St_store (quantity_of_ctype t, addr, e) in
588  Cminor.St_seq (stmt, body)
589
590let add_stack_parameters_initialization var_locs body =
591  let f x (location, t) body = match location with
592    | ParamStack offset -> add_stack_parameter_initialization x t offset body
593    | _ -> body in
594  fold_var_locs f var_locs body
595
596let translate_internal fresh globals functs cfun =
597  let var_locs = sort_variables globals functs cfun in
598  let params =
599    List.map (fun (x, t) -> (x, sig_type_of_ctype t)) cfun.Clight.fn_params in
600  let (tmps, body) = translate_statement fresh var_locs cfun.Clight.fn_body in
601  let body = add_stack_parameters_initialization var_locs body in
602  { Cminor.f_return = type_return_of_ctype cfun.Clight.fn_return ;
603    Cminor.f_params = params ;
604    Cminor.f_vars = (get_locals var_locs) @ tmps ;
605    Cminor.f_stacksize = get_stacksize var_locs ;
606    Cminor.f_body = body }
607
608let translate_external id params return = 
609  { AST.ef_tag = id ;
610    AST.ef_sig = { AST.args = translate_args_types params ;
611                   AST.res = type_return_of_ctype return } }
612
613let translate_funct fresh globals functs (id, def) =
614  let def = match def with
615    | Clight.Internal ff ->
616      Cminor.F_int (translate_internal fresh globals functs ff)
617    | Clight.External (i,p,r) -> Cminor.F_ext (translate_external i p r) in
618  (id, def)
619
620let translate p =
621  let fresh = ClightAnnotator.make_fresh "_tmp" p in
622  let translate_funct =
623    translate_funct fresh p.Clight.prog_vars p.Clight.prog_funct in
624  { Cminor.vars = List.map translate_global p.Clight.prog_vars ;
625    Cminor.functs = List.map translate_funct p.Clight.prog_funct ;
626    Cminor.main = p.Clight.prog_main }
Note: See TracBrowser for help on using the repository browser.