source: Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightToCminor.ml @ 1334

Last change on this file since 1334 was 1334, checked in by tranquil, 8 years ago

work on Cminor completed

File size: 21.9 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 var_locs =
220  let globals = List.map (fun ((id, _), ctype) -> (id, ctype)) globals in
221  sort_vars Global None stack_vars globals var_locs
222
223(* The order of insertion in the sorting environment is important: it follows
224   the scope conventions of C. Local variables hide parameters that hide
225   globals. *)
226
227let sort_variables globals cfun =
228  let stack_vars = stack_vars cfun in
229  let var_locs = empty_var_locs in
230  let var_locs = sort_globals stack_vars globals var_locs in
231  let var_locs = sort_params stack_vars cfun.Clight.fn_params var_locs in
232  let var_locs = sort_locals stack_vars cfun.Clight.fn_vars var_locs in
233  var_locs
234
235
236(* Translate globals *)
237
238let init_to_data = function
239  | [Clight.Init_space _] -> None
240  | l -> Some (List.map (
241  function 
242    | Clight.Init_int8 i       -> AST.Data_int8 i
243    | Clight.Init_int16 i      -> AST.Data_int16 i
244    | Clight.Init_int32 i      -> AST.Data_int32 i
245    | Clight.Init_float32 _ 
246    | Clight.Init_float64 _    -> error_float ()
247    | Clight.Init_space n      -> error "bad global initialization style."
248    | Clight.Init_addrof (_,_) -> assert false (*TODO*)
249) l)
250
251let translate_global ((id,lst),t) = (id,global_size_of_ctype t,init_to_data lst)
252
253
254(* Translate expression *)
255
256let translate_unop = function
257  | Clight.Onotbool -> AST.Op_notbool
258  | Clight.Onotint -> AST.Op_notint
259  | Clight.Oneg -> AST.Op_negint
260
261let esizeof_ctype res_type t =
262  Cminor.Expr (Cminor.Cst (AST.Cst_sizeof (sizeof_ctype t)), res_type)
263
264let translate_add res_type ctype1 ctype2 e1 e2 = match ctype1, ctype2 with
265  | Clight.Tint _, Clight.Tint _ ->
266    Cminor.Expr (Cminor.Op2 (AST.Op_add, e1, e2), res_type)
267  | Clight.Tfloat _, Clight.Tfloat _ -> error_float ()
268  | Clight.Tpointer t, Clight.Tint _
269  | Clight.Tarray (t, _), Clight.Tint _ ->
270    let t2 = cminor_type_of e2 in
271    let size = esizeof_ctype t2 t in
272    let index = Cminor.Expr (Cminor.Op2 (AST.Op_mul, e2, size), t2) in
273    Cminor.Expr (Cminor.Op2 (AST.Op_addp, e1, index), res_type)
274  | Clight.Tint _, Clight.Tpointer t
275  | Clight.Tint _, Clight.Tarray (t, _) -> 
276    let t1 = cminor_type_of e1 in
277    let size = esizeof_ctype t1 t in
278    let index = Cminor.Expr (Cminor.Op2 (AST.Op_mul, e1, size), t1) in
279    Cminor.Expr (Cminor.Op2 (AST.Op_addp, e2, index), res_type)
280  | _ -> error "type error."
281
282let translate_sub res_type ctype1 ctype2 e1 e2 = match ctype1, ctype2 with
283  | Clight.Tint _, Clight.Tint _ ->
284    Cminor.Expr (Cminor.Op2 (AST.Op_sub, e1, e2), res_type)
285  | Clight.Tfloat _, Clight.Tfloat _ -> error_float ()
286  | Clight.Tpointer t, Clight.Tint _
287  | Clight.Tarray (t, _), Clight.Tint _ ->
288    let t2 = cminor_type_of e2 in
289    let size = esizeof_ctype t2 t in
290    let index = Cminor.Expr (Cminor.Op2 (AST.Op_mul, e2, size), t2) in
291    Cminor.Expr (Cminor.Op2 (AST.Op_subp, e1, index), res_type)
292  | Clight.Tpointer _, Clight.Tpointer _
293  | Clight.Tarray _, Clight.Tpointer _
294  | Clight.Tpointer _, Clight.Tarray _
295  | Clight.Tarray _, Clight.Tarray _ ->
296    Cminor.Expr (Cminor.Op2 (AST.Op_subpp, e1, e2), res_type)
297  | _ -> error "type error."
298
299let is_signed = function
300  | Clight.Tint (_, AST.Signed) -> true
301  | _ -> false
302
303let is_pointer = function
304  | Clight.Tpointer _ | Clight.Tarray _ -> true
305  | _ -> false
306
307let cmp_of_clight_binop = function
308  | Clight.Oeq -> AST.Cmp_eq
309  | Clight.One -> AST.Cmp_ne
310  | Clight.Olt -> AST.Cmp_lt
311  | Clight.Ole -> AST.Cmp_le
312  | Clight.Ogt -> AST.Cmp_gt
313  | Clight.Oge -> AST.Cmp_ge
314  | _ -> assert false (* do not use on these arguments *)
315
316let translate_simple_binop t = function
317  | Clight.Omul -> AST.Op_mul
318  | Clight.Odiv when is_signed t -> AST.Op_div
319  | Clight.Odiv -> AST.Op_divu
320  | Clight.Omod when is_signed t -> AST.Op_mod
321  | Clight.Omod -> AST.Op_modu
322  | Clight.Oand -> AST.Op_and
323  | Clight.Oor -> AST.Op_or
324  | Clight.Oxor -> AST.Op_xor
325  | Clight.Oshl -> AST.Op_shl
326  | Clight.Oshr when is_signed t -> AST.Op_shr
327  | Clight.Oshr -> AST.Op_shru
328  | binop when is_pointer t -> AST.Op_cmpp (cmp_of_clight_binop binop)
329  | binop when is_signed t -> AST.Op_cmp (cmp_of_clight_binop binop)
330  | binop -> AST.Op_cmpu (cmp_of_clight_binop binop)
331
332let translate_binop res_type ctype1 ctype2 e1 e2 binop =
333  match binop with
334    | Clight.Oadd -> translate_add res_type ctype1 ctype2 e1 e2
335    | Clight.Osub -> translate_sub res_type ctype1 ctype2 e1 e2
336    | _ ->
337      let cminor_binop = translate_simple_binop ctype1 binop in
338      Cminor.Expr (Cminor.Op2 (cminor_binop, e1, e2), res_type)
339
340let translate_ident var_locs res_type x =
341  let ed = match find_var_locs x var_locs with
342    | (Local, _) | (Param, _) -> Cminor.Id x
343    | (LocalStack off, t) | (ParamStack off, t) when is_scalar_ctype t ->
344      let addr = Cminor.Expr (add_stack off, AST.Sig_ptr) in
345      Cminor.Mem (quantity_of_ctype t, addr)
346    | (LocalStack off, _) | (ParamStack off, _) ->
347      add_stack off
348    | (Global, t) when is_scalar_ctype t ->
349      let addr = Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol x), AST.Sig_ptr) in
350      Cminor.Mem (quantity_of_ctype t, addr)
351    | (Global, _) -> Cminor.Cst (AST.Cst_addrsymbol x) in
352  Cminor.Expr (ed, res_type)
353
354let translate_field res_type t e field =
355  let (fields, offset) = match t with
356    | Clight.Tstruct (_, fields) -> (fields, struct_offset t field fields)
357    | Clight.Tunion (_, fields) ->
358      (fields, Cminor.Expr (Cminor.Cst (AST.Cst_int 0), AST.Sig_offset))
359    | _ -> assert false (* type error *) in
360  let addr = Cminor.Expr (Cminor.Op2 (AST.Op_addp, e, offset), AST.Sig_ptr) in
361  let quantity = quantity_of_ctype (List.assoc field fields) in
362  Cminor.Expr (Cminor.Mem (quantity, addr), res_type)
363
364let translate_cast e src_type dest_type =
365  let res_type = sig_type_of_ctype dest_type in
366  match src_type, dest_type with
367    | Clight.Tint (size1, sign1), Clight.Tint (size2, _) ->
368      let t1 = (byte_size_of_intsize size1, sign1) in
369      let t2 = byte_size_of_intsize size2 in
370      Cminor.Expr (Cminor.Op1 (AST.Op_cast (t1, t2), e), res_type)
371    | Clight.Tint _, Clight.Tpointer _
372    | Clight.Tint _, Clight.Tarray _ ->
373      Cminor.Expr (Cminor.Op1 (AST.Op_ptrofint, e), res_type)
374    | Clight.Tpointer _, Clight.Tint _
375    | Clight.Tarray _, Clight.Tint _ ->
376      Cminor.Expr (Cminor.Op1 (AST.Op_intofptr, e), res_type)
377    | _ -> e
378
379let rec f_expr var_locs (Clight.Expr (ed, t)) sub_exprs_res =
380  let t_cminor = sig_type_of_ctype t in
381  let cst_int i t = Cminor.Expr (Cminor.Cst (AST.Cst_int i), t) in
382  match ed, sub_exprs_res with
383
384  | Clight.Econst_int i, _ ->
385    Cminor.Expr (Cminor.Cst (AST.Cst_int i), t_cminor)
386
387  | Clight.Econst_float _, _ -> error_float ()
388
389  | Clight.Evar x, _ when is_function_ctype t ->
390    Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol x), t_cminor)
391
392  | Clight.Evar x, _ -> translate_ident var_locs t_cminor x
393
394  | Clight.Ederef _, e :: _ when is_scalar_ctype t ->
395    Cminor.Expr (Cminor.Mem (quantity_of_ctype t, e), t_cminor)
396
397  | Clight.Ederef _, e :: _ ->
398    (* When dereferencing something pointing to a struct for instance, the
399       result is the address of the struct. *)
400    e
401
402  | Clight.Eaddrof e, _ -> translate_addrof var_locs e
403
404  | Clight.Eunop (unop, _), e :: _ -> 
405    Cminor.Expr (Cminor.Op1 (translate_unop unop, e), t_cminor)
406
407  | Clight.Ebinop (binop, e1, e2), e1' :: e2' :: _ -> 
408    translate_binop t_cminor (clight_type_of e1) (clight_type_of e2) e1' e2'
409      binop
410
411  | Clight.Ecast (t, Clight.Expr (_, t')), e :: _ -> translate_cast e t' t
412
413  | Clight.Econdition _, e1 :: e2 :: e3 :: _ ->
414    Cminor.Expr (Cminor.Cond (e1, e2, e3), t_cminor)
415
416  | Clight.Eandbool _, e1 :: e2 :: _ -> 
417    let zero = cst_int 0 t_cminor in
418    let one = cst_int 1 t_cminor in
419    let e2_cond = Cminor.Expr (Cminor.Cond (e2, one, zero), t_cminor) in
420    Cminor.Expr (Cminor.Cond (e1, e2_cond, zero), t_cminor)
421
422  | Clight.Eorbool _, e1 :: e2 :: _ -> 
423    let zero = cst_int 0 t_cminor in
424    let one = cst_int 1 t_cminor in
425    let e2_cond = Cminor.Expr (Cminor.Cond (e2, one, zero), t_cminor) in
426    Cminor.Expr (Cminor.Cond (e1, one, e2_cond), t_cminor)
427
428  | Clight.Esizeof t, _ -> esizeof_ctype t_cminor t
429
430  | Clight.Ecost (lbl, _), e :: _ ->
431    Cminor.Expr (Cminor.Exp_cost (lbl, e), t_cminor)
432
433  | Clight.Ecall _, _ -> assert false (* only for annotations *)
434
435  | Clight.Efield (Clight.Expr (_, t), field), e :: _ ->
436    translate_field t_cminor t e field
437
438  | _ -> assert false (* wrong number of arguments *)
439
440and translate_addrof_ident res_type var_locs id =
441  match find_var_locs id var_locs with
442    | (Local, _) | (Param, _) -> assert false (* type error *)
443    | (LocalStack off, _) | (ParamStack off, _) ->
444      Cminor.Expr (add_stack off, res_type)
445    | (Global, _) ->
446      Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol id), res_type)
447
448and translate_addrof_field res_type t field e =
449  let (fields, offset) = match t with
450    | Clight.Tstruct (_, fields) -> (fields, struct_offset t field fields)
451    | Clight.Tunion (_, fields) ->
452      (fields, Cminor.Expr (Cminor.Cst (AST.Cst_int 0), AST.Sig_offset))
453    | _ -> assert false (* type error *) in
454  Cminor.Expr (Cminor.Op2 (AST.Op_addp, e, offset), res_type)
455
456and translate_addrof var_locs (Clight.Expr (ed, _)) =
457  let res_type = AST.Sig_ptr in
458  match ed with
459
460    | Clight.Evar id -> translate_addrof_ident res_type var_locs id
461
462    | Clight.Ederef e -> translate_expr var_locs e
463
464    | Clight.Efield ((Clight.Expr (_, t) as e), field) ->
465      let e = translate_expr var_locs e in
466      translate_addrof_field res_type t field e
467
468    | _ -> assert false (* not a lvalue *)
469
470and translate_expr var_locs e = ClightFold.expr2 (f_expr var_locs) e
471
472
473(* Translate statement *)
474
475let assign var_locs (Clight.Expr (ed, t) as e_res_clight) e_arg_cminor =
476  match ed with
477    | Clight.Evar id when is_local_or_param id var_locs ->
478      Cminor.St_assign (id, e_arg_cminor)
479    | _ ->
480      let quantity = quantity_of_ctype t in
481      let addr = translate_addrof var_locs e_res_clight in
482      Cminor.St_store (quantity, addr, e_arg_cminor)
483
484let call_sig ret_type args =
485  { AST.args = List.map cminor_type_of args ;
486    AST.res = ret_type }
487
488let ind_0 i stmt = match i with
489        | None -> stmt
490        | Some x -> Cminor.St_ind_0(x, stmt)
491
492let ind_inc i stmt = match i with
493        | None -> stmt
494        | Some x -> Cminor.St_ind_inc(stmt, x)
495
496let f_stmt fresh var_locs stmt sub_exprs_res sub_stmts_res =
497  let (tmps, sub_stmts_res) = List.split sub_stmts_res in
498  let tmps = List.flatten tmps in
499
500  let (added_tmps, stmt) = match stmt, sub_exprs_res, sub_stmts_res with
501
502    | Clight.Sskip, _, _ -> ([], Cminor.St_skip)
503
504    | Clight.Sassign (e1, _), _ :: e2 :: _, _ ->
505      ([], assign var_locs e1 e2)
506
507    | Clight.Scall (None, _, _), f :: args, _ ->
508      ([], Cminor.St_call (None, f, args, call_sig AST.Type_void args))
509
510    | Clight.Scall (Some e, _, _), _ :: f :: args, _ ->
511      let t = sig_type_of_ctype (clight_type_of e) in
512      let tmp = fresh () in
513      let tmpe = Cminor.Expr (Cminor.Id tmp, t) in
514      let stmt_call =
515        Cminor.St_call (Some tmp, f, args, call_sig (AST.Type_ret t) args) in
516      let stmt_assign = assign var_locs e tmpe in
517      ([(tmp, t)], Cminor.St_seq (stmt_call, stmt_assign))
518
519    | Clight.Swhile (i,_,_), e :: _, stmt :: _ ->
520      let econd =               
521        Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in
522      let scond =
523        Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in
524            let loop_body = Cminor.St_seq (scond, ind_inc i (Cminor.St_block stmt)) in
525                        let loop = ind_0 i (Cminor.St_loop loop_body) in
526      ([], Cminor.St_block loop)
527                       
528    | Clight.Sdowhile (i,_,_), e :: _, stmt :: _ ->
529      let econd =               
530        Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in
531      let scond =
532              Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in
533                        let loop_body = ind_inc i (Cminor.St_seq (Cminor.St_block stmt, scond)) in
534                        let loop = ind_0 i (Cminor.St_loop loop_body) in
535      ([], Cminor.St_block loop)
536
537    | Clight.Sfor (i,_,_,_,_), e :: _, stmt1 :: stmt2 :: stmt3 :: _ ->
538      let econd =                               
539        Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in
540      let scond =
541              Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in
542      let body = Cminor.St_seq (ind_inc i (Cminor.St_block stmt3), stmt2) in
543                        let body = Cminor.St_seq (scond, body) in
544                        let block = Cminor.St_block (ind_0 i (Cminor.St_loop body)) in 
545      ([], Cminor.St_seq (stmt1, block))
546
547    | Clight.Sifthenelse _, e :: _, stmt1 :: stmt2 :: _ ->
548      ([], Cminor.St_ifthenelse (e, stmt1, stmt2))
549
550    | Clight.Ssequence _, _, stmt1 :: stmt2 :: _ ->
551      ([], Cminor.St_seq (stmt1, stmt2))
552
553    | Clight.Sbreak, _, _ -> ([], Cminor.St_exit 1)
554
555    | Clight.Scontinue, _, _ -> ([], Cminor.St_exit 0)
556
557    | Clight.Sswitch _, _, _ ->
558      (* Should not appear because of switch transformation performed
559         beforehand. *)
560      assert false
561
562    | Clight.Sreturn None, _, _ -> ([], Cminor.St_return None)
563
564    | Clight.Sreturn (Some _), e :: _, _ -> ([], Cminor.St_return (Some e))
565
566    | Clight.Slabel (lbl, _), _, stmt :: _ -> ([], Cminor.St_label (lbl, stmt))
567
568    | Clight.Sgoto lbl, _, _ -> ([], Cminor.St_goto lbl)
569
570    | Clight.Scost (lbl, _), _, stmt :: _ -> ([], Cminor.St_cost (lbl, stmt))
571
572    | _ -> assert false (* type error *) in
573
574  (tmps @ added_tmps, stmt)
575
576let translate_statement fresh var_locs =
577  ClightFold.statement2 (f_expr var_locs) (f_stmt fresh var_locs)
578
579
580(* Translate functions and programs *)
581
582let add_stack_parameter_initialization x t off body =
583  let addr = Cminor.Expr (add_stack off, AST.Sig_ptr) in
584  let e = Cminor.Expr (Cminor.Id x, sig_type_of_ctype t) in
585  let stmt = Cminor.St_store (quantity_of_ctype t, addr, e) in
586  Cminor.St_seq (stmt, body)
587
588let add_stack_parameters_initialization var_locs body =
589  let f x (location, t) body = match location with
590    | ParamStack offset -> add_stack_parameter_initialization x t offset body
591    | _ -> body in
592  fold_var_locs f var_locs body
593
594let translate_internal fresh globals cfun =
595  let var_locs = sort_variables globals cfun in
596  let params =
597    List.map (fun (x, t) -> (x, sig_type_of_ctype t)) cfun.Clight.fn_params in
598  let (tmps, body) = translate_statement fresh var_locs cfun.Clight.fn_body in
599  let body = add_stack_parameters_initialization var_locs body in
600  { Cminor.f_return = type_return_of_ctype cfun.Clight.fn_return ;
601    Cminor.f_params = params ;
602    Cminor.f_vars = (get_locals var_locs) @ tmps ;
603    Cminor.f_stacksize = get_stacksize var_locs ;
604    Cminor.f_body = body }
605
606let translate_external id params return = 
607  { AST.ef_tag = id ;
608    AST.ef_sig = { AST.args = translate_args_types params ;
609                   AST.res = type_return_of_ctype return } }
610
611let translate_funct fresh globals (id, def) =
612  let def = match def with
613    | Clight.Internal ff -> Cminor.F_int (translate_internal fresh globals ff)
614    | Clight.External (i,p,r) -> Cminor.F_ext (translate_external i p r) in
615  (id, def)
616
617let translate p =
618  let fresh = ClightAnnotator.make_fresh "_tmp" p in
619  { Cminor.vars = List.map translate_global p.Clight.prog_vars ;
620    Cminor.functs =
621      List.map (translate_funct fresh p.Clight.prog_vars) p.Clight.prog_funct ;
622    Cminor.main = p.Clight.prog_main }
Note: See TracBrowser for help on using the repository browser.