src/clight/clightToCminor.ml

   1
   2
   3 let error_prefix = "Clight to Cminor"
   4 let error = Error.global_error error_prefix
   5 let error_float () = error "float not supported."
   6
   7
   8 (* General helpers *)
   9
  10 let clight_type_of (Clight.Expr (_, t)) = t
  11
  12 let cminor_type_of (Cminor.Expr (_, t)) = t
  13
  14
  15 (* Translate types *)
  16
  17 let byte_size_of_intsize = function
  18   | Clight.I8 -> 1
  19   | Clight.I16 -> 2
  20   | Clight.I32 -> 4
  21
  22 let 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
  30 let translate_args_types = List.map sig_type_of_ctype
  31
  32 let type_return_of_ctype = function
  33   | Clight.Tvoid -> AST.Type_void
  34   | t -> AST.Type_ret (sig_type_of_ctype t)
  35
  36 let 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
  42 let quantity_of_ctype t = quantity_of_sig_type (sig_type_of_ctype t)
  43
  44 let 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
  56 let global_size_of_ctype = sizeof_ctype
  57
  58
  59 (** Helpers on abstract sizes and offsets *)
  60
  61 let 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. *)
  67 let max_offset offset1 offset2 =
  68   if List.length offset1 > List.length offset2 then offset1
  69   else offset2
  70
  71 let next_depth = function
  72   | AST.SProd l -> List.length l
  73   | _ -> raise (Failure "ClightToCminor.next_offset")
  74
  75 let 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
  80 let add_stacksize t = function
  81   | AST.SProd l -> AST.SProd (l @ [sizeof_ctype t])
  82   | _ -> raise (Failure "ClightToCminor.add_stacksize")
  83
  84 let 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
  91 let 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
 101 type 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
 111 type var_locations = (location * Clight.ctype) StringTools.Map.t
 112
 113 let empty_var_locs : var_locations = StringTools.Map.empty
 114
 115 let add_var_locs : AST.ident -> (location * Clight.ctype) -> var_locations ->
 116   var_locations =
 117   StringTools.Map.add
 118
 119 let mem_var_locs : AST.ident -> var_locations -> bool = StringTools.Map.mem
 120
 121 let find_var_locs : AST.ident -> var_locations -> (location * Clight.ctype) =
 122   StringTools.Map.find
 123
 124 let fold_var_locs : (AST.ident -> (location * Clight.ctype) -> 'a -> 'a) ->
 125   var_locations -> 'a -> 'a =
 126   StringTools.Map.fold
 127
 128
 129 let is_local_or_param id var_locs = match find_var_locs id var_locs with
 130   | (Local, _) | (Param, _) -> true
 131   | _ -> false
 132
 133 let 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
 141 let 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
 152 let is_function_ctype = function
 153   | Clight.Tfunction _ -> true
 154   | _ -> false
 155
 156 let is_scalar_ctype : Clight.ctype -> bool = function
 157   | Clight.Tint _ | Clight.Tfloat _ | Clight.Tpointer _ -> true
 158   | _ -> false
 159
 160 let is_complex_ctype : Clight.ctype -> bool = function
 161   | Clight.Tarray _ | Clight.Tstruct _ | Clight.Tunion _ | Clight.Tfunction _ ->
 162     true
 163   | _ -> false
 164
 165 let 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
 173 let union_list = List.fold_left StringTools.Set.union StringTools.Set.empty
 174
 175 let 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
 182 let f_stmt _ sub_exprs_res sub_stmts_res =
 183   union_list (sub_exprs_res @ sub_stmts_res)
 184
 185 let addr_vars_fun cfun = ClightFold.statement2 f_expr f_stmt cfun.Clight.fn_body
 186
 187 let stack_vars cfun =
 188   StringTools.Set.union (complex_ctype_vars cfun) (addr_vars_fun cfun)
 189
 190
 191 let 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
 201 let 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
 206 let 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
 215 let sort_locals = sort_vars Local (Some (fun offset -> LocalStack offset))
 216
 217 let sort_params = sort_vars Param (Some (fun offset -> ParamStack offset))
 218
 219 let 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
 235 let 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
 246 let 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
 259 let translate_global ((id,lst),t) = (id,global_size_of_ctype t,init_to_data lst)
 260
 261
 262 (* Translate expression *)
 263
 264 let translate_unop = function
 265   | Clight.Onotbool -> AST.Op_notbool
 266   | Clight.Onotint -> AST.Op_notint
 267   | Clight.Oneg -> AST.Op_negint
 268
 269 let esizeof_ctype res_type t =
 270   Cminor.Expr (Cminor.Cst (AST.Cst_sizeof (sizeof_ctype t)), res_type)
 271
 272 let 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
 290 let 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
 307 let is_signed = function
 308   | Clight.Tint (_, AST.Signed) -> true
 309   | _ -> false
 310
 311 let is_pointer = function
 312   | Clight.Tpointer _ | Clight.Tarray _ -> true
 313   | _ -> false
 314
 315 let 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
 324 let 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
 340 let 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
 348 let 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
 362 let 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
 372 let 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
 387 let 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
 448 and 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
 457 and 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
 465 and 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
 479 and translate_expr var_locs e = ClightFold.expr2 (f_expr var_locs) e
 480
 481
 482 (* Translate statement *)
 483
 484 let 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
 493 let call_sig ret_type args =
 494   { AST.args = List.map cminor_type_of args ;
 495     AST.res = ret_type }
 496
 497 let 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
 578 let 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
 584 let 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
 590 let 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
 596 let 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
 608 let 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
 613 let 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
 620 let 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 }