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

(** This module translates a [Cminor] program into a [RTLabs] program. *)

open Driver


let error_prefix = "Cminor to RTLabs"
let error = Error.global_error error_prefix


(* Helper functions *)

let ptr_nb_ints = Driver.TargetArch.ptr_size / Driver.TargetArch.int_size

let rec freshs runiverse n =
  if n = 0 then []
  else (Register.fresh runiverse) :: (freshs runiverse (n-1))

let int_size_of_type = function
  | AST.Type_void -> 0
  | AST.Type_ret AST.Sig_int -> 1
  | AST.Type_ret AST.Sig_ptr -> ptr_nb_ints
  | AST.Type_ret AST.Sig_float -> error "floats not handled."

let fresh_type runiverse ty = freshs runiverse (int_size_of_type ty)

let fresh_result runiverse def = fresh_type runiverse def.Cminor.f_sig.AST.res

let type_of_local def x =
  if List.mem x def.Cminor.f_ptrs then AST.Type_ret AST.Sig_ptr
  else
    if List.mem x def.Cminor.f_vars then AST.Type_ret AST.Sig_int
    else
      let n = MiscPottier.index_of x def.Cminor.f_params in
      AST.Type_ret (List.nth def.Cminor.f_sig.AST.args n)

let type_of_cst = function
  | AST.Cst_int _ -> AST.Sig_int
  | AST.Cst_float _ -> error "floats not handled."
  | AST.Cst_addrsymbol _ | AST.Cst_stackoffset _ -> AST.Sig_ptr

let type_of_op1 = function
  | AST.Op_cast8unsigned | AST.Op_cast8signed | AST.Op_cast16unsigned
  | AST.Op_cast16signed | AST.Op_negint | AST.Op_notbool | AST.Op_notint
  | AST.Op_intoffloat | AST.Op_intuoffloat | AST.Op_intofptr ->
      AST.Sig_int
  | AST.Op_negf | AST.Op_absf | AST.Op_singleoffloat | AST.Op_floatofint
  | AST.Op_floatofintu ->
      AST.Sig_float
  | AST.Op_ptrofint ->
      AST.Sig_ptr
  | AST.Op_id ->
      assert false (* Dependent on argument. Treated in type_of_expr *)

let type_of_op2 = function
  | AST.Op_add | AST.Op_sub | AST.Op_mul | AST.Op_div | AST.Op_divu | AST.Op_mod
  | AST.Op_modu | AST.Op_and | AST.Op_or | AST.Op_xor | AST.Op_shl | AST.Op_shr
  | AST.Op_shru ->
      AST.Sig_int
  | AST.Op_addf | AST.Op_subf | AST.Op_mulf | AST.Op_divf ->
      AST.Sig_float
  | AST.Op_cmp _ | AST.Op_cmpu _ | AST.Op_cmpf _ | AST.Op_cmpp _ ->
      AST.Sig_int
  | AST.Op_addp | AST.Op_subp ->
      AST.Sig_ptr

let rec type_of_expr def = function
  | Cminor.Id x -> type_of_local def x
  | Cminor.Cst cst -> AST.Type_ret (type_of_cst cst)
  | Cminor.Op1 (AST.Op_id, e) -> type_of_expr def e
  | Cminor.Op1 (op1, _) -> AST.Type_ret (type_of_op1 op1)
  | Cminor.Op2 (op2, _, _) -> AST.Type_ret (type_of_op2 op2)
  | Cminor.Mem (mq, _) -> AST.Type_ret (Memory.type_of_memory_q mq)
  | Cminor.Cond _ -> AST.Type_ret AST.Sig_int
  | Cminor.Exp_cost (_, e) -> type_of_expr def e

let fresh_local runiverse def x =
  fresh_type runiverse (type_of_local def x)

let allocate (rtlabs_fun : RTLabs.internal_function) (n : int)
    : RTLabs.internal_function * Register.t list =
  let rs = freshs rtlabs_fun.RTLabs.f_runiverse n in
  let rtlabs_fun =
    { rtlabs_fun with RTLabs.f_locals = rtlabs_fun.RTLabs.f_locals @ [rs] } in
  (rtlabs_fun, rs)

let allocate_expr
    (def        : Cminor.internal_function)
    (rtlabs_fun : RTLabs.internal_function)
    (e          : Cminor.expression)
    : (RTLabs.internal_function * Register.t list) =
  allocate rtlabs_fun (int_size_of_type (type_of_expr def e))

type local_env = Register.t list StringTools.Map.t

let find_local (lenv : local_env) (x : AST.ident) : Register.t list =
  if StringTools.Map.mem x lenv then StringTools.Map.find x lenv
  else error ("Unknown local \"" ^ x ^ "\".")

let find_olocal (lenv : local_env) (ox : AST.ident option) : Register.t list =
  match ox with
    | None -> []
    | Some x -> find_local lenv x

let choose_destination
    (def        : Cminor.internal_function)
    (rtlabs_fun : RTLabs.internal_function)
    (lenv       : local_env)
    (e          : Cminor.expression)
    : RTLabs.internal_function * Register.t list =
  match e with
    | Cminor.Id x -> (rtlabs_fun, find_local lenv x)
    | _ -> allocate_expr def rtlabs_fun e

let choose_destinations
    (def        : Cminor.internal_function)
    (rtlabs_fun : RTLabs.internal_function)
    (lenv       : local_env)
    (args       : Cminor.expression list)
    : RTLabs.internal_function * Register.t list list =
  let f (rtlabs_fun, regs) e =
    let (rtlabs_fun, rs) = choose_destination def rtlabs_fun lenv e in
    (rtlabs_fun, regs @ [rs]) in
  List.fold_left f (rtlabs_fun, []) args

let fresh_label (rtlabs_fun : RTLabs.internal_function) : Label.t =
  Label.Gen.fresh rtlabs_fun.RTLabs.f_luniverse

let change_entry
    (rtlabs_fun : RTLabs.internal_function)
    (new_entry : Label.t)
    : RTLabs.internal_function =
  { rtlabs_fun with RTLabs.f_entry = new_entry }


(* Add a label and its associated instruction at the beginning of a function's
   graph *)
let add_graph
    (rtlabs_fun : RTLabs.internal_function)
    (lbl        : Label.t)
    (stmt       : RTLabs.statement)
    : RTLabs.internal_function =
  let graph = Label.Map.add lbl stmt rtlabs_fun.RTLabs.f_graph in
  let rtlabs_fun = { rtlabs_fun with RTLabs.f_graph = graph } in
  change_entry rtlabs_fun lbl


let generate
    (rtlabs_fun : RTLabs.internal_function)
    (stmt       : RTLabs.statement)
    : RTLabs.internal_function =
  let lbl = fresh_label rtlabs_fun in
  add_graph rtlabs_fun lbl stmt


(* [addressing e] returns the type of address represented by [e],
   along with its arguments *)

let addressing (e : Cminor.expression)
    : (RTLabs.addressing * Cminor.expression list)  =
  match e with
    | Cminor.Cst (AST.Cst_addrsymbol id) -> (RTLabs.Aglobal (id, 0), [])
    | Cminor.Cst (AST.Cst_stackoffset n) -> (RTLabs.Ainstack n, [])
    | Cminor.Op2 (AST.Op_add,
                  Cminor.Cst (AST.Cst_addrsymbol id),
                  Cminor.Cst (AST.Cst_int n)) ->
        (RTLabs.Aglobal (id, n), [])
    | Cminor.Op2 (AST.Op_add, e1, Cminor.Cst (AST.Cst_int n)) ->
        (RTLabs.Aindexed n, [e1])
    | Cminor.Op2 (AST.Op_add,
                  Cminor.Cst (AST.Cst_addrsymbol id),
                  e2) ->
        (RTLabs.Abased (id, 0), [e2])
    | Cminor.Op2 (AST.Op_add, e1, e2) -> (RTLabs.Aindexed2, [e1 ; e2])
    | _ -> (RTLabs.Aindexed 0, [e])


(* Translating conditions

   The Cminor definition [def] is used for typing purposes (differencing from
   integers and pointers). [rtlabs_fun] is the function being
   constructed. [lenv] is the environment associating a pseudo-register to the
   variables of the program being translated. *)

let rec translate_branch
    (def        : Cminor.internal_function)
    (rtlabs_fun : RTLabs.internal_function)
    (lenv       : local_env)
    (e          : Cminor.expression)
    (lbl_true   : Label.t)
    (lbl_false  : Label.t)
    : RTLabs.internal_function =
  match e with

    | Cminor.Id x ->
        let stmt =
          RTLabs.St_cond1 (AST.Op_id, find_local lenv x, lbl_true, lbl_false) in
        generate rtlabs_fun stmt

    | Cminor.Cst cst ->
        generate rtlabs_fun (RTLabs.St_condcst (cst, lbl_true, lbl_false))

    | Cminor.Op1 (op1, e) ->
        let (rtlabs_fun, rs) = choose_destination def rtlabs_fun lenv e in
        let stmt = RTLabs.St_cond1 (op1, rs, lbl_true, lbl_false) in
        let rtlabs_fun = generate rtlabs_fun stmt in
        translate_expr def rtlabs_fun lenv rs e

    | Cminor.Op2 (op2, e1, e2) ->
        let (rtlabs_fun, rs1) = choose_destination def rtlabs_fun lenv e1 in
        let (rtlabs_fun, rs2) = choose_destination def rtlabs_fun lenv e2 in
        let stmt = RTLabs.St_cond2 (op2, rs1, rs2, lbl_true, lbl_false) in
        let rtlabs_fun = generate rtlabs_fun stmt in
        translate_exprs def rtlabs_fun lenv [rs1 ; rs2] [e1 ; e2]

    | _ ->
        let (rtlabs_fun, rs) = choose_destination def rtlabs_fun lenv e in
        let stmt = RTLabs.St_cond1 (AST.Op_id, rs, lbl_true, lbl_false) in
        let rtlabs_fun = generate rtlabs_fun stmt in
        translate_expr def rtlabs_fun lenv rs e

(* Translating expressions

   The Cminor definition [def] is used for typing purposes (differencing from
   integers and pointers). [rtlabs_fun] is the function being
   constructed. [lenv] is the environment associating a pseudo-register to the
   variables of the program being translated. [destrs] are the destination
   registers. There may be more than one in the case of pointers, and when the
   size of addresses is bigger than a machine word. *)

and translate_expr
    (def        : Cminor.internal_function)
    (rtlabs_fun : RTLabs.internal_function)
    (lenv       : local_env)
    (destrs     : Register.t list)
    (e          : Cminor.expression)
    : RTLabs.internal_function =
  match e with

    | Cminor.Id x ->
      let xrs = find_local lenv x in
      let rec eq_reg_list rl1 rl2 = match rl1, rl2 with
        | [], [] -> true
        | r1 :: rl1, r2 :: rl2 ->
          (Register.equal r1 r2) && (eq_reg_list rl1 rl2)
        | _ -> false in
      (* If the destinations and sources are the same, just do nothing. *)
      if eq_reg_list destrs xrs then rtlabs_fun
      else
        let old_entry = rtlabs_fun.RTLabs.f_entry in
        let stmt = RTLabs.St_op1 (AST.Op_id, destrs, xrs, old_entry) in
        generate rtlabs_fun stmt

    | Cminor.Cst cst ->
      let old_entry = rtlabs_fun.RTLabs.f_entry in
      let stmt = RTLabs.St_cst (destrs, cst, old_entry) in
      generate rtlabs_fun stmt

    | Cminor.Op1 (op1, e) ->
      let (rtlabs_fun, rs) = choose_destination def rtlabs_fun lenv e in
      let old_entry = rtlabs_fun.RTLabs.f_entry in
      let stmt = RTLabs.St_op1 (op1, destrs, rs, old_entry) in
      let rtlabs_fun = generate rtlabs_fun stmt in
      translate_expr def rtlabs_fun lenv rs e

    | Cminor.Op2 (op2, e1, e2) ->
      let (rtlabs_fun, rs1) = choose_destination def rtlabs_fun lenv e1 in
      let (rtlabs_fun, rs2) = choose_destination def rtlabs_fun lenv e2 in
      let old_entry = rtlabs_fun.RTLabs.f_entry in
      let stmt = RTLabs.St_op2 (op2, destrs, rs1, rs2, old_entry) in
      let rtlabs_fun = generate rtlabs_fun stmt in
      translate_exprs def rtlabs_fun lenv [rs1 ; rs2] [e1 ; e2]

    | Cminor.Mem (chunk, e) ->
      let (mode, args) = addressing e in
      let (rtlabs_fun, regs) = choose_destinations def rtlabs_fun lenv args in
      let old_entry = rtlabs_fun.RTLabs.f_entry in
      let stmt = RTLabs.St_load (chunk, mode, regs, destrs, old_entry) in
      let rtlabs_fun = generate rtlabs_fun stmt in
      translate_exprs def rtlabs_fun lenv regs args

    | Cminor.Cond (e1, e2, e3) ->
      let old_entry = rtlabs_fun.RTLabs.f_entry in
      let (rtlabs_fun, rs2) = choose_destination def rtlabs_fun lenv e2 in
      let (rtlabs_fun, rs3) = choose_destination def rtlabs_fun lenv e3 in
      let rtlabs_fun = translate_expr def rtlabs_fun lenv rs3 e3 in
      let lbl_false = rtlabs_fun.RTLabs.f_entry in
      let rtlabs_fun = change_entry rtlabs_fun old_entry in
      let rtlabs_fun = translate_expr def rtlabs_fun lenv rs2 e2 in
      let lbl_true = rtlabs_fun.RTLabs.f_entry in
      translate_branch def rtlabs_fun lenv e1 lbl_true lbl_false

    | Cminor.Exp_cost (lbl, e) ->
      let (rtlabs_fun, rs) = choose_destination def rtlabs_fun lenv e in
      let rtlabs_fun = translate_expr def rtlabs_fun lenv rs e in
      let old_entry = rtlabs_fun.RTLabs.f_entry in
      generate rtlabs_fun (RTLabs.St_cost (lbl, old_entry))

and translate_exprs
    (def        : Cminor.internal_function)
    (rtlabs_fun : RTLabs.internal_function)
    (lenv       : local_env)
    (regs       : Register.t list list)
    (args       : Cminor.expression list)
    : RTLabs.internal_function =
  let f destrs e rtlabs_fun = translate_expr def rtlabs_fun lenv destrs e in
  List.fold_right2 f regs args rtlabs_fun


(* Switch transformation

   switch (e) {
   case c0: exit i0;
   case c1: exit i1;
   ...
   default: exit idfl; }

   is translated to

   if (e == c0) exit i0;
   if (e == c1) exit i1;
   ...
   exit idfl; *)

let transform_switch
    (e : Cminor.expression)
    (cases : (int * int) list)
    (dfl : int)
    : Cminor.statement =
  let rec aux = function
    | [] -> Cminor.St_skip
    | (case, exit) :: cases ->
        let c =
          Cminor.Op2 (AST.Op_cmp AST.Cmp_eq,
                      e, Cminor.Cst (AST.Cst_int case)) in
        let stmt =
          Cminor.St_ifthenelse (c, Cminor.St_exit exit, Cminor.St_skip) in
        Cminor.St_seq (stmt, aux cases)
  in
  Cminor.St_seq (aux cases, Cminor.St_exit dfl)


(* Translating statements

   The Cminor definition [def] is used for typing purposes (differencing from
   integers and pointers). [rtlabs_fun] is the function being
   constructed. [lenv] is the environment associating a pseudo-register to the
   variables of the program being translated. [exists] is the list of label to
   exit to. The leftmost label in the list is used to exit the closest block. *)

let rec translate_stmt
    (def        : Cminor.internal_function)
    (rtlabs_fun : RTLabs.internal_function)
    (lenv       : local_env)
    (exits      : Label.t list)
    (stmt       : Cminor.statement)
    : RTLabs.internal_function =
  match stmt with

    | Cminor.St_skip -> rtlabs_fun

    | Cminor.St_assign (x, e) ->
      translate_expr def rtlabs_fun lenv (find_local lenv x) e

    | Cminor.St_store (chunk, e1, e2) ->
      let (mode, args) = addressing e1 in
      let (rtlabs_fun, regs) = choose_destinations def rtlabs_fun lenv args in
      let (rtlabs_fun, rs) = choose_destination def rtlabs_fun lenv e2 in
      let old_entry = rtlabs_fun.RTLabs.f_entry in
      let stmt = RTLabs.St_store (chunk, mode, regs, rs, old_entry) in
      let rtlabs_fun = generate rtlabs_fun stmt in
      let rtlabs_fun = translate_expr def rtlabs_fun lenv rs e2 in
      translate_exprs def rtlabs_fun lenv regs args

    | Cminor.St_call (oret, Cminor.Cst (AST.Cst_addrsymbol f), args, sg) ->
      let (rtlabs_fun, regs) = choose_destinations def rtlabs_fun lenv args in
      let retrs = find_olocal lenv oret in
      let old_entry = rtlabs_fun.RTLabs.f_entry in
      let stmt = RTLabs.St_call_id (f, regs, retrs, sg, old_entry) in
      let rtlabs_fun = generate rtlabs_fun stmt in
      translate_exprs def rtlabs_fun lenv regs args

    | Cminor.St_call (oret, f, args, sg) ->
      let (rtlabs_fun, frs) = choose_destination def rtlabs_fun lenv f in
      let (rtlabs_fun, regs) = choose_destinations def rtlabs_fun lenv args in
      let retrs = find_olocal lenv oret in
      let old_entry = rtlabs_fun.RTLabs.f_entry in
      let stmt = RTLabs.St_call_ptr (frs, regs, retrs, sg, old_entry) in
      let rtlabs_fun = generate rtlabs_fun stmt in
      let rtlabs_fun = translate_exprs def rtlabs_fun lenv regs args in
      translate_expr def rtlabs_fun lenv frs f

    | Cminor.St_tailcall (Cminor.Cst (AST.Cst_addrsymbol f), args, sg) ->
      let (rtlabs_fun, regs) = choose_destinations def rtlabs_fun lenv args in
      let stmt = RTLabs.St_tailcall_id (f, regs, sg) in
      let rtlabs_fun = generate rtlabs_fun stmt in
      translate_exprs def rtlabs_fun lenv regs args

    | Cminor.St_tailcall (f, args, sg) ->
      let (rtlabs_fun, frs) = choose_destination def rtlabs_fun lenv f in
      let (rtlabs_fun, regs) = choose_destinations def rtlabs_fun lenv args in
      let stmt = RTLabs.St_tailcall_ptr (frs, regs, sg) in
      let rtlabs_fun = generate rtlabs_fun stmt in
      let rtlabs_fun = translate_exprs def rtlabs_fun lenv regs args in
      translate_expr def rtlabs_fun lenv frs f

    | Cminor.St_seq (s1, s2) ->
      let rtlabs_fun = translate_stmt def rtlabs_fun lenv exits s2 in
      translate_stmt def rtlabs_fun lenv exits s1

    | Cminor.St_ifthenelse (e, s1, s2) ->
      let old_entry = rtlabs_fun.RTLabs.f_entry in
      let rtlabs_fun = translate_stmt def rtlabs_fun lenv exits s2 in
      let lbl_false = rtlabs_fun.RTLabs.f_entry in
      let rtlabs_fun = change_entry rtlabs_fun old_entry in
      let rtlabs_fun = translate_stmt def rtlabs_fun lenv exits s1 in
      let lbl_true = rtlabs_fun.RTLabs.f_entry in
      translate_branch def rtlabs_fun lenv e lbl_true lbl_false

    | Cminor.St_loop s ->
      let loop_start = fresh_label rtlabs_fun in
      let rtlabs_fun = change_entry rtlabs_fun loop_start in
      let rtlabs_fun = translate_stmt def rtlabs_fun lenv exits s in
      let old_entry = rtlabs_fun.RTLabs.f_entry in
      add_graph rtlabs_fun loop_start (RTLabs.St_skip old_entry)

    | Cminor.St_block s ->
      let old_entry = rtlabs_fun.RTLabs.f_entry in
      translate_stmt def rtlabs_fun lenv (old_entry :: exits) s

    | Cminor.St_exit n ->
      change_entry rtlabs_fun (List.nth exits n)

    | Cminor.St_return eopt ->
      let rtlabs_fun = change_entry rtlabs_fun rtlabs_fun.RTLabs.f_exit in
      (match eopt, rtlabs_fun.RTLabs.f_result with
        | None, _ -> rtlabs_fun
        | Some e, retrs -> translate_expr def rtlabs_fun lenv retrs e)

    | Cminor.St_switch (e, cases, dfl) ->
      let stmt = transform_switch e cases dfl in
      translate_stmt def rtlabs_fun lenv exits stmt

    | Cminor.St_label (lbl, s) ->
      let rtlabs_fun = translate_stmt def rtlabs_fun lenv exits s in
      let old_entry = rtlabs_fun.RTLabs.f_entry in
      add_graph rtlabs_fun lbl (RTLabs.St_skip old_entry)

    | Cminor.St_cost (lbl, s) ->
      let rtlabs_fun = translate_stmt def rtlabs_fun lenv exits s in
      let old_entry = rtlabs_fun.RTLabs.f_entry in
      generate rtlabs_fun (RTLabs.St_cost (lbl, old_entry))

    | Cminor.St_goto lbl ->
      change_entry rtlabs_fun lbl


(* Translating function definitions *)

(* The translation consists in the following:
   - Create a universe of pseudo-register names
   - Create a universe of label names
   - Create a local environment; that is, a mapping from local
     variables to pseudo-registers
   - Extract the registers representing the formal variables
   - Extract the registers representing the local variables
   - Allocate a fresh label representing the exit point
   - Allocate fresh registers holding the result of the function
   - Initialize the graph with a return instruction at the end
   - Complete the graph according to the function's body.
     Instructions will be added from end to start following the flow of the
     function. *)

let translate_internal lbl_prefix f_def =

  (* Register names *)
  let runiverse = Register.new_universe "%" in

  (* Labels of statements *)
  let luniverse = Label.Gen.new_universe lbl_prefix in

  (* Local environment *)
  let add_local lenv x =
    let rs = fresh_local runiverse f_def x in
    StringTools.Map.add x rs lenv in
  let lenv = StringTools.Map.empty in
  let lenv = List.fold_left add_local lenv f_def.Cminor.f_params in
  let lenv = List.fold_left add_local lenv f_def.Cminor.f_vars in
  let lenv = List.fold_left add_local lenv f_def.Cminor.f_ptrs in

  let extract vars =
    List.fold_left (fun l x -> l @ [StringTools.Map.find x lenv]) [] vars in

  (* Parameter registers *)
  let params = extract f_def.Cminor.f_params in
 
 (* Local registers *)
  let locals = extract (f_def.Cminor.f_vars @ f_def.Cminor.f_ptrs) in

  (* Exit label of the graph *)
  let exit = Label.Gen.fresh luniverse in

  (* [retrs] are the registers that holds the return value of the body, if
     any. *)
  let retrs = fresh_result runiverse f_def in

  let locals = locals @ [retrs] in

  (* The control flow graph: for now, it is only a return instruction at the
     end. *)
  let graph = Label.Map.add exit (RTLabs.St_return retrs) Label.Map.empty in

  let rtlabs_fun =
    { RTLabs.f_luniverse = luniverse ;
      RTLabs.f_runiverse = runiverse ;
      RTLabs.f_sig       = f_def.Cminor.f_sig ;
      RTLabs.f_result    = retrs ;
      RTLabs.f_params    = params ;
      RTLabs.f_locals    = locals ;
      RTLabs.f_stacksize = f_def.Cminor.f_stacksize ;
      RTLabs.f_graph     = graph ;
      RTLabs.f_entry     = exit ;
      RTLabs.f_exit      = exit } in

  (* Complete the graph *)
  translate_stmt f_def rtlabs_fun lenv [] f_def.Cminor.f_body


let translate_functions lbls (f_id, f_def) = match f_def with
  | Cminor.F_int int_def ->
      let lbl_prefix = StringTools.Gen.fresh_prefix lbls f_id in
      let def = translate_internal lbl_prefix int_def in
      (f_id, RTLabs.F_int def)
  | Cminor.F_ext def -> (f_id, RTLabs.F_ext def)


(* Initialization of globals *)

let assign_data x stmt (data, off) =
  let e = Cminor.Op2 (AST.Op_add,
                      Cminor.Cst (AST.Cst_addrsymbol x),
                      Cminor.Cst (AST.Cst_int off)) in
  let chunk () = Memory.mq_of_data data in
  let stmt' = match data with
    | AST.Data_reserve _ -> Cminor.St_skip
    | AST.Data_int8 i | AST.Data_int16 i | AST.Data_int32 i ->
        Cminor.St_store (chunk (), e, Cminor.Cst (AST.Cst_int i))
    | AST.Data_float32 f | AST.Data_float64 f ->
        Cminor.St_store (chunk (), e, Cminor.Cst (AST.Cst_float f)) in
  Cminor.St_seq (stmt, stmt')

let add_global_initializations_body vars body =
  let f stmt (x, datas) =
    let offs_of_datas = RTLabsMemory.offsets_of_datas datas in
    List.fold_left (assign_data x) stmt offs_of_datas in
  Cminor.St_seq (List.fold_left f Cminor.St_skip vars, body)

let add_global_initializations_funct vars = function
  | Cminor.F_int def ->
      let f_body = add_global_initializations_body vars def.Cminor.f_body in
      Cminor.F_int { def with Cminor.f_body = f_body }
  | def -> def

(* [add_global_initializations p] moves the initializations of the globals of
   [p] to the beginning of the main function, if any. *)

let add_global_initializations p = match p.Cminor.main with
  | None -> p.Cminor.functs
  | Some main ->
    let main_def = List.assoc main p.Cminor.functs in
    let main_def = add_global_initializations_funct p.Cminor.vars main_def in
    MiscPottier.update_list_assoc main main_def p.Cminor.functs


(* Translation of a Cminor program to a RTLabs program. *)

let translate p =

  (* Fetch the variables in the program that are pointers (whose value is an
     address). Some architectures have different sizes for pointers and
     integers. *)
  let p = CminorPointers.fill p in

  (* Fetch the labels already used in the program to create new ones. *)
  let lbls = CminorAnnotator.all_labels p in

  (* The initialization of globals are moved at the beginning of the main. *)
  let functs = add_global_initializations p in

  (* The globals are associated their size. *)
  let f (id, datas) = (id, RTLabsMemory.size_of_datas datas) in

  (* Put all this together and translate each function. *)
  { RTLabs.vars = List.map f p.Cminor.vars ;
    RTLabs.functs = List.map (translate_functions lbls) functs ;
    RTLabs.main = p.Cminor.main }