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

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

merge of indexed labels branch

File size: 23.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 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 ind_0 i stmt = match i with
498  | None -> stmt
499  | Some x -> Cminor.St_ind_0(x, stmt)
500
501let ind_inc i stmt = match i with
502  | None -> stmt
503  | Some x -> Cminor.St_ind_inc(x, stmt)
504
505let trans_for =
506  let f_expr e _ = e in
507  let f_stmt stmt expr_res stmt_res = match expr_res, stmt_res, stmt with
508    | e::_, s1::s2::s3::_, Clight.Sfor(i,_,_,_,_) ->
509      Clight.Ssequence(s1,Clight.Swhile(i,e,
510                                        Clight.Ssequence(s3, s2)))
511    | exprs, sub_sts, stm ->
512      ClightFold.statement_fill_subs stm exprs sub_sts in
513  ClightFold.statement2 f_expr f_stmt
514
515let cmp_complement = function
516  | AST.Cmp_eq -> AST.Cmp_ne
517  | AST.Cmp_ne -> AST.Cmp_eq
518  | AST.Cmp_gt -> AST.Cmp_le
519  | AST.Cmp_ge -> AST.Cmp_lt
520  | AST.Cmp_lt -> AST.Cmp_ge
521  | AST.Cmp_le -> AST.Cmp_gt
522
523let negate_expr (Cminor.Expr (_, et) as e) =
524  let ed' = Cminor.Op1 (AST.Op_notbool, e) in
525  Cminor.Expr(ed', et)
526
527let rec translate_stmt fresh var_locs cnt_lbl br_lbl = function
528
529    | Clight.Sskip -> ([], Cminor.St_skip)
530
531    | Clight.Sassign (e1, e2) ->
532      let e2 = translate_expr var_locs e2 in
533      ([], assign var_locs e1 e2)
534
535    | Clight.Scall (None, f, args) ->
536      let f = translate_expr var_locs f in
537      let args = List.map (translate_expr var_locs) args in
538      ([], Cminor.St_call (None, f, args, call_sig AST.Type_void args))
539
540    | Clight.Scall (Some e, f, args) ->
541      let f = translate_expr var_locs f in
542      let args = List.map (translate_expr var_locs) args in
543      let t = sig_type_of_ctype (clight_type_of e) in
544      let tmp = fresh () in
545      let tmpe = Cminor.Expr (Cminor.Id tmp, t) in
546      let stmt_call =
547        Cminor.St_call (Some tmp, f, args, call_sig (AST.Type_ret t) args) in
548      let stmt_assign = assign var_locs e tmpe in
549      ([(tmp, t)], Cminor.St_seq (stmt_call, stmt_assign))
550
551    | Clight.Swhile (i,e,stmt) ->
552      let loop_lbl = fresh () in
553      let llbl_opt = Some loop_lbl in
554      let exit_lbl = fresh () in
555      let elbl_opt = Some exit_lbl in
556      let (tmps, stmt) = translate_stmt fresh var_locs llbl_opt elbl_opt stmt in
557      let e = translate_expr var_locs e in
558      let jmp lbl = Cminor.St_goto lbl in
559      (* let econd = negate_expr e in *)
560      let scond =
561        Cminor.St_ifthenelse (e, Cminor.St_skip, jmp exit_lbl) in
562      let loop =
563        Cminor.St_seq(scond,Cminor.St_seq (stmt, ind_inc i (jmp loop_lbl))) in
564      let loop = ind_0 i (Cminor.St_label(loop_lbl,loop)) in
565      (tmps, Cminor.St_seq (loop, Cminor.St_label(exit_lbl,Cminor.St_skip)))
566       
567    | Clight.Sdowhile (i,e,stmt) ->
568      let loop_lbl = fresh () in
569      let llbl_opt = Some loop_lbl in
570      let exit_lbl = fresh () in
571      let elbl_opt = Some exit_lbl in
572      let (tmps, stmt) = translate_stmt fresh var_locs llbl_opt elbl_opt stmt in
573      let e = translate_expr var_locs e in
574      let jmp lbl = Cminor.St_goto lbl in
575      let scond =
576        Cminor.St_ifthenelse (e, ind_inc i (jmp loop_lbl), Cminor.St_skip) in
577      let loop =
578        Cminor.St_seq (stmt, scond) in
579      let loop = ind_0 i (Cminor.St_label(loop_lbl,loop)) in
580      (tmps, Cminor.St_seq (loop, Cminor.St_label(exit_lbl,Cminor.St_skip)))
581       
582    | Clight.Sfor _ -> assert false (* transformed *)
583
584    | Clight.Sifthenelse (e, stmt1, stmt2) ->
585      let (tmps1, stmt1) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt1 in
586      let (tmps2, stmt2) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt2 in
587      let e = translate_expr var_locs e in
588      (tmps1 @ tmps2, Cminor.St_ifthenelse (e, stmt1, stmt2))
589
590    | Clight.Ssequence(stmt1,stmt2) ->
591      let (tmps1, stmt1) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt1 in
592      let (tmps2, stmt2) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt2 in
593      (tmps1 @ tmps2, Cminor.St_seq (stmt1, stmt2))
594
595    | Clight.Sbreak -> 
596      let br_lbl = match br_lbl with
597        | Some x -> x
598        | None -> invalid_arg("break without enclosing scope") in
599      ([], Cminor.St_goto br_lbl)
600
601    | Clight.Scontinue ->
602      let cnt_lbl = match cnt_lbl with
603        | Some x -> x
604        | None -> invalid_arg("continue without enclosing scope") in
605      ([], Cminor.St_goto cnt_lbl)
606    | Clight.Sswitch _ ->
607      (* Should not appear because of switch transformation performed
608         beforehand. *)
609      assert false
610
611    | Clight.Sreturn None -> ([], Cminor.St_return None)
612
613    | Clight.Sreturn (Some e) ->
614      let e = translate_expr var_locs e in
615      ([], Cminor.St_return (Some e))
616
617    | Clight.Slabel (lbl, stmt) ->
618      let (tmps, stmt) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt in
619      (tmps, Cminor.St_label (lbl, stmt))
620
621    | Clight.Sgoto lbl -> ([], Cminor.St_goto lbl)
622
623    | Clight.Scost (lbl, stmt) ->
624      let (tmps, stmt) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt in
625      (tmps, Cminor.St_cost (lbl, stmt))
626
627(*    | _ -> assert false (* type error *) *)
628
629
630(* Translate functions and programs *)
631
632let add_stack_parameter_initialization x t off body =
633  let addr = Cminor.Expr (add_stack off, AST.Sig_ptr) in
634  let e = Cminor.Expr (Cminor.Id x, sig_type_of_ctype t) in
635  let stmt = Cminor.St_store (quantity_of_ctype t, addr, e) in
636  Cminor.St_seq (stmt, body)
637
638let add_stack_parameters_initialization var_locs body =
639  let f x (location, t) body = match location with
640    | ParamStack offset -> add_stack_parameter_initialization x t offset body
641    | _ -> body in
642  fold_var_locs f var_locs body
643
644let translate_internal fresh globals functs cfun =
645  let var_locs = sort_variables globals functs cfun in
646  let params =
647    List.map (fun (x, t) -> (x, sig_type_of_ctype t)) cfun.Clight.fn_params in
648  let body = cfun.Clight.fn_body in
649  let body = trans_for body in
650  let (tmps, body) = translate_stmt fresh var_locs None None body in
651  let body = add_stack_parameters_initialization var_locs body in
652  { Cminor.f_return = type_return_of_ctype cfun.Clight.fn_return ;
653    Cminor.f_params = params ;
654    Cminor.f_vars = (get_locals var_locs) @ tmps ;
655    Cminor.f_stacksize = get_stacksize var_locs ;
656    Cminor.f_body = body }
657
658let translate_external id params return = 
659  { AST.ef_tag = id ;
660    AST.ef_sig = { AST.args = translate_args_types params ;
661                   AST.res = type_return_of_ctype return } }
662
663let translate_funct fresh globals functs (id, def) =
664  let def = match def with
665    | Clight.Internal ff ->
666      Cminor.F_int (translate_internal fresh globals functs ff)
667    | Clight.External (i,p,r) -> Cminor.F_ext (translate_external i p r) in
668  (id, def)
669
670let translate p =
671  let fresh = ClightAnnotator.make_fresh "_tmp" p in
672  let translate_funct =
673    translate_funct fresh p.Clight.prog_vars p.Clight.prog_funct in
674  { Cminor.vars = List.map translate_global p.Clight.prog_vars ;
675    Cminor.functs = List.map translate_funct p.Clight.prog_funct ;
676    Cminor.main = p.Clight.prog_main }
Note: See TracBrowser for help on using the repository browser.