src/cminor/cminorToRTLabs.ml

   1
   2 (** This module translates a [Cminor] program into a [RTLabs] program. *)
   3
   4 open Driver
   5
   6
   7 let error_prefix = "Cminor to RTLabs"
   8 let error = Error.global_error error_prefix
   9 let error_float () = error "float not supported."
  10
  11
  12 (* Helper functions *)
  13
  14 let allocate (rtlabs_fun : RTLabs.internal_function) (sig_type : AST.sig_type)
  15     : RTLabs.internal_function * Register.t =
  16   let r = Register.fresh rtlabs_fun.RTLabs.f_runiverse in
  17   let locals = rtlabs_fun.RTLabs.f_locals @ [(r, sig_type)] in
  18   let rtlabs_fun =
  19     { rtlabs_fun with RTLabs.f_locals = locals } in
  20   (rtlabs_fun, r)
  21
  22 let type_of (Cminor.Expr (_, t)) = t
  23
  24 let allocate_expr
  25     (rtlabs_fun : RTLabs.internal_function)
  26     (e          : Cminor.expression)
  27     : (RTLabs.internal_function * Register.t) =
  28   allocate rtlabs_fun (type_of e)
  29
  30 type local_env = Register.t StringTools.Map.t
  31
  32 let find_local (lenv : local_env) (x : AST.ident) : Register.t =
  33   if StringTools.Map.mem x lenv then StringTools.Map.find x lenv
  34   else error ("Unknown local \"" ^ x ^ "\".")
  35
  36 let find_olocal (lenv : local_env) (ox : AST.ident option) : Register.t option =
  37   match ox with
  38     | None -> None
  39     | Some x -> Some (find_local lenv x)
  40
  41 let choose_destination
  42     (rtlabs_fun : RTLabs.internal_function)
  43     (lenv       : local_env)
  44     (e          : Cminor.expression)
  45     : RTLabs.internal_function * Register.t =
  46   match e with
  47     | Cminor.Expr (Cminor.Id x, _) -> (rtlabs_fun, find_local lenv x)
  48     | _ -> allocate_expr rtlabs_fun e
  49
  50 let choose_destinations
  51     (rtlabs_fun : RTLabs.internal_function)
  52     (lenv       : local_env)
  53     (args       : Cminor.expression list)
  54     : RTLabs.internal_function * Register.t list =
  55   let f (rtlabs_fun, regs) e =
  56     let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e in
  57     (rtlabs_fun, regs @ [r]) in
  58   List.fold_left f (rtlabs_fun, []) args
  59
  60 let fresh_label (rtlabs_fun : RTLabs.internal_function) : Label.t =
  61   Label.Gen.fresh rtlabs_fun.RTLabs.f_luniverse
  62
  63 let change_entry
  64     (rtlabs_fun : RTLabs.internal_function)
  65     (new_entry : Label.t)
  66     : RTLabs.internal_function =
  67   { rtlabs_fun with RTLabs.f_entry = new_entry }
  68
  69
  70 (* Add a label and its associated instruction at the beginning of a function's
  71    graph *)
  72 let add_graph
  73     (rtlabs_fun : RTLabs.internal_function)
  74     (lbl        : Label.t)
  75     (stmt       : RTLabs.statement)
  76     : RTLabs.internal_function =
  77   let graph = Label.Map.add lbl stmt rtlabs_fun.RTLabs.f_graph in
  78   let rtlabs_fun = { rtlabs_fun with RTLabs.f_graph = graph } in
  79   change_entry rtlabs_fun lbl
  80
  81
  82 let generate
  83     (rtlabs_fun : RTLabs.internal_function)
  84     (stmt       : RTLabs.statement)
  85     : RTLabs.internal_function =
  86   let lbl = fresh_label rtlabs_fun in
  87   add_graph rtlabs_fun lbl stmt
  88
  89
  90 (*
  91 (* [addressing e] returns the type of address represented by [e],
  92    along with its arguments *)
  93
  94 let addressing (Cminor.Expr (ed, t) : Cminor.expression)
  95     : (RTLabs.addressing * Cminor.expression list)  =
  96   match ed with
  97     | Cminor.Cst (AST.Cst_addrsymbol id) -> (RTLabs.Aglobal (id, 0), [])
  98     | Cminor.Cst (AST.Cst_stackoffset n) -> (RTLabs.Ainstack n, [])
  99     | Cminor.Op2 (AST.Op_addp _,
 100                   Cminor.Cst (AST.Cst_addrsymbol id),
 101                   Cminor.Cst (AST.Cst_int n)) ->
 102       (RTLabs.Aglobal (id, n), [])
 103     | Cminor.Op2 (AST.Op_addp _, e1, Cminor.Cst (AST.Cst_int n)) ->
 104       (RTLabs.Aindexed n, [e1])
 105     | Cminor.Op2 (AST.Op_addp _,
 106                   Cminor.Cst (AST.Cst_addrsymbol id),
 107                   e2) ->
 108       (RTLabs.Abased (id, 0), [e2])
 109     | Cminor.Op2 (AST.Op_addp _, e1, e2) -> (RTLabs.Aindexed2, [e1 ; e2])
 110     | _ -> (RTLabs.Aindexed 0, [e])
 111 *)
 112
 113
 114 (* Translating conditions *)
 115
 116 let rec translate_branch
 117     (rtlabs_fun : RTLabs.internal_function)
 118     (lenv       : local_env)
 119     (e          : Cminor.expression)
 120     (lbl_true   : Label.t)
 121     (lbl_false  : Label.t)
 122     : RTLabs.internal_function =
 123   let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e in
 124   let stmt = RTLabs.St_cond (r, lbl_true, lbl_false) in
 125   let rtlabs_fun = generate rtlabs_fun stmt in
 126   translate_expr rtlabs_fun lenv r e
 127
 128 (*
 129   let Cminor.Expr (ed, t) = e in
 130   match ed with
 131
 132     | Cminor.Id x ->
 133       let stmt =
 134         RTLabs.St_cond1 (AST.Op_id, find_local lenv x, lbl_true, lbl_false) in
 135       generate rtlabs_fun stmt
 136
 137     | Cminor.Cst cst ->
 138       generate rtlabs_fun (RTLabs.St_condcst (cst, t, lbl_true, lbl_false))
 139
 140     | Cminor.Op1 (op1, e) ->
 141       let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e in
 142       let stmt = RTLabs.St_cond1 (op1, r, lbl_true, lbl_false) in
 143       let rtlabs_fun = generate rtlabs_fun stmt in
 144       translate_expr rtlabs_fun lenv r e
 145
 146     | Cminor.Op2 (op2, e1, e2) ->
 147       let (rtlabs_fun, r1) = choose_destination rtlabs_fun lenv e1 in
 148       let (rtlabs_fun, r2) = choose_destination rtlabs_fun lenv e2 in
 149       let stmt = RTLabs.St_cond2 (op2, r1, r2, lbl_true, lbl_false) in
 150       let rtlabs_fun = generate rtlabs_fun stmt in
 151       translate_exprs rtlabs_fun lenv [r1 ; r2] [e1 ; e2]
 152
 153     | _ ->
 154       let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e in
 155       let stmt = RTLabs.St_cond1 (AST.Op_id, r, lbl_true, lbl_false) in
 156       let rtlabs_fun = generate rtlabs_fun stmt in
 157       translate_expr rtlabs_fun lenv r e
 158 *)
 159
 160 (* Translating expressions *)
 161
 162 and translate_expr
 163     (rtlabs_fun : RTLabs.internal_function)
 164     (lenv       : local_env)
 165     (destr      : Register.t)
 166     (e          : Cminor.expression)
 167     : RTLabs.internal_function =
 168   let Cminor.Expr (ed, t) = e in
 169   match ed with
 170
 171     | Cminor.Id x ->
 172       let xr = find_local lenv x in
 173       (* If the destination and source are the same, just do nothing. *)
 174       if Register.equal destr xr then rtlabs_fun
 175       else
 176         let old_entry = rtlabs_fun.RTLabs.f_entry in
 177         let stmt = RTLabs.St_op1 (AST.Op_id, destr, xr, old_entry) in
 178         generate rtlabs_fun stmt
 179
 180     | Cminor.Cst cst ->
 181       let old_entry = rtlabs_fun.RTLabs.f_entry in
 182       let stmt = RTLabs.St_cst (destr, cst, old_entry) in
 183       generate rtlabs_fun stmt
 184
 185     | Cminor.Op1 (op1, e) ->
 186       let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e in
 187       let old_entry = rtlabs_fun.RTLabs.f_entry in
 188       let stmt = RTLabs.St_op1 (op1, destr, r, old_entry) in
 189       let rtlabs_fun = generate rtlabs_fun stmt in
 190       translate_expr rtlabs_fun lenv r e
 191
 192     | Cminor.Op2 (op2, e1, e2) ->
 193       let (rtlabs_fun, r1) = choose_destination rtlabs_fun lenv e1 in
 194       let (rtlabs_fun, r2) = choose_destination rtlabs_fun lenv e2 in
 195       let old_entry = rtlabs_fun.RTLabs.f_entry in
 196       let stmt = RTLabs.St_op2 (op2, destr, r1, r2, old_entry) in
 197       let rtlabs_fun = generate rtlabs_fun stmt in
 198       translate_exprs rtlabs_fun lenv [r1 ; r2] [e1 ; e2]
 199
 200     | Cminor.Mem (chunk, e) ->
 201       let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e in
 202       let old_entry = rtlabs_fun.RTLabs.f_entry in
 203       let stmt = RTLabs.St_load (chunk, r, destr, old_entry) in
 204       let rtlabs_fun = generate rtlabs_fun stmt in
 205       translate_expr rtlabs_fun lenv r e
 206
 207     | Cminor.Cond (e1, e2, e3) ->
 208       let old_entry = rtlabs_fun.RTLabs.f_entry in
 209       let rtlabs_fun = translate_expr rtlabs_fun lenv destr e3 in
 210       let lbl_false = rtlabs_fun.RTLabs.f_entry in
 211       let rtlabs_fun = change_entry rtlabs_fun old_entry in
 212       let rtlabs_fun = translate_expr rtlabs_fun lenv destr e2 in
 213       let lbl_true = rtlabs_fun.RTLabs.f_entry in
 214       translate_branch rtlabs_fun lenv e1 lbl_true lbl_false
 215
 216     | Cminor.Exp_cost (lbl, e) ->
 217       let rtlabs_fun = translate_expr rtlabs_fun lenv destr e in
 218       let old_entry = rtlabs_fun.RTLabs.f_entry in
 219       generate rtlabs_fun (RTLabs.St_cost (lbl, old_entry))
 220
 221 and translate_exprs
 222     (rtlabs_fun : RTLabs.internal_function)
 223     (lenv       : local_env)
 224     (regs       : Register.t list)
 225     (args       : Cminor.expression list)
 226     : RTLabs.internal_function =
 227   let f destr e rtlabs_fun = translate_expr rtlabs_fun lenv destr e in
 228   List.fold_right2 f regs args rtlabs_fun
 229
 230
 231 (*
 232 (* Switch transformation
 233
 234    switch (e) {
 235    case c0: exit i0;
 236    case c1: exit i1;
 237    ...
 238    default: exit idfl; }
 239
 240    is translated to
 241
 242    if (e == c0) exit i0;
 243    if (e == c1) exit i1;
 244    ...
 245    exit idfl; *)
 246
 247 let transform_switch
 248     (e : Cminor.expression)
 249     (cases : (int * int) list)
 250     (dfl : int)
 251     : Cminor.statement =
 252   let rec aux = function
 253     | [] -> Cminor.St_skip
 254     | (case, exit) :: cases ->
 255       let c =
 256         Cminor.Op2 (AST.Op_cmp (AST.Cmp_eq, uint),
 257                     e, Cminor.Cst (AST.Cst_int case)) in
 258       let stmt =
 259         Cminor.St_ifthenelse (c, Cminor.St_exit exit, Cminor.St_skip) in
 260       Cminor.St_seq (stmt, aux cases)
 261   in
 262   Cminor.St_seq (aux cases, Cminor.St_exit dfl)
 263 *)
 264
 265
 266 (* Translating statements *)
 267
 268 let rec translate_stmt
 269     (rtlabs_fun : RTLabs.internal_function)
 270     (lenv       : local_env)
 271     (exits      : Label.t list)
 272     (stmt       : Cminor.statement)
 273     : RTLabs.internal_function =
 274   match stmt with
 275
 276     | Cminor.St_skip -> rtlabs_fun
 277
 278     | Cminor.St_assign (x, e) ->
 279       translate_expr rtlabs_fun lenv (find_local lenv x) e
 280
 281     | Cminor.St_store (chunk, e1, e2) ->
 282       let (rtlabs_fun, addr) = choose_destination rtlabs_fun lenv e1 in
 283       let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e2 in
 284       let old_entry = rtlabs_fun.RTLabs.f_entry in
 285       let stmt = RTLabs.St_store (chunk, addr, r, old_entry) in
 286       let rtlabs_fun = generate rtlabs_fun stmt in
 287       translate_exprs rtlabs_fun lenv [addr ; r] [e1 ; e2]
 288
 289     | Cminor.St_call (oret,
 290                       Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol f), _),
 291                       args, sg) ->
 292       let (rtlabs_fun, regs) = choose_destinations rtlabs_fun lenv args in
 293       let oretr = find_olocal lenv oret in
 294       let old_entry = rtlabs_fun.RTLabs.f_entry in
 295       let stmt = RTLabs.St_call_id (f, regs, oretr, sg, old_entry) in
 296       let rtlabs_fun = generate rtlabs_fun stmt in
 297       translate_exprs rtlabs_fun lenv regs args
 298
 299     | Cminor.St_call (oret, f, args, sg) ->
 300       let (rtlabs_fun, fr) = choose_destination rtlabs_fun lenv f in
 301       let (rtlabs_fun, regs) = choose_destinations rtlabs_fun lenv args in
 302       let oretr = find_olocal lenv oret in
 303       let old_entry = rtlabs_fun.RTLabs.f_entry in
 304       let stmt = RTLabs.St_call_ptr (fr, regs, oretr, sg, old_entry) in
 305       let rtlabs_fun = generate rtlabs_fun stmt in
 306       translate_exprs rtlabs_fun lenv (fr :: regs) (f :: args)
 307
 308     | Cminor.St_tailcall (Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol f), _),
 309                           args, sg) ->
 310       let (rtlabs_fun, regs) = choose_destinations rtlabs_fun lenv args in
 311       let stmt = RTLabs.St_tailcall_id (f, regs, sg) in
 312       let rtlabs_fun = generate rtlabs_fun stmt in
 313       translate_exprs rtlabs_fun lenv regs args
 314
 315     | Cminor.St_tailcall (f, args, sg) ->
 316       let (rtlabs_fun, fr) = choose_destination rtlabs_fun lenv f in
 317       let (rtlabs_fun, regs) = choose_destinations rtlabs_fun lenv args in
 318       let stmt = RTLabs.St_tailcall_ptr (fr, regs, sg) in
 319       let rtlabs_fun = generate rtlabs_fun stmt in
 320       translate_exprs rtlabs_fun lenv (fr :: regs) (f :: args)
 321
 322     | Cminor.St_seq (s1, s2) ->
 323       let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s2 in
 324       translate_stmt rtlabs_fun lenv exits s1
 325
 326     | Cminor.St_ifthenelse (e, s1, s2) ->
 327       let old_entry = rtlabs_fun.RTLabs.f_entry in
 328       let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s2 in
 329       let lbl_false = rtlabs_fun.RTLabs.f_entry in
 330       let rtlabs_fun = change_entry rtlabs_fun old_entry in
 331       let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s1 in
 332       let lbl_true = rtlabs_fun.RTLabs.f_entry in
 333       translate_branch rtlabs_fun lenv e lbl_true lbl_false
 334
 335     | Cminor.St_loop s ->
 336       let loop_start = fresh_label rtlabs_fun in
 337       let rtlabs_fun = change_entry rtlabs_fun loop_start in
 338       let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s in
 339       let old_entry = rtlabs_fun.RTLabs.f_entry in
 340       add_graph rtlabs_fun loop_start (RTLabs.St_skip old_entry)
 341
 342     | Cminor.St_block s ->
 343       let old_entry = rtlabs_fun.RTLabs.f_entry in
 344       translate_stmt rtlabs_fun lenv (old_entry :: exits) s
 345
 346     | Cminor.St_exit n ->
 347       change_entry rtlabs_fun (List.nth exits n)
 348
 349     | Cminor.St_return eopt ->
 350       let rtlabs_fun = change_entry rtlabs_fun rtlabs_fun.RTLabs.f_exit in
 351       (match eopt, rtlabs_fun.RTLabs.f_result with
 352         | None, None -> rtlabs_fun
 353         | Some e, Some (retr, _) -> translate_expr rtlabs_fun lenv retr e
 354         | _ -> assert false (* should be impossible *))
 355
 356     | Cminor.St_switch (e, cases, dfl) ->
 357       assert false (* should have been simplified before *)
 358 (*
 359       let stmt = transform_switch e cases dfl in
 360       translate_stmt rtlabs_fun lenv exits stmt
 361 *)
 362
 363     | Cminor.St_label (lbl, s) ->
 364       let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s in
 365       let old_entry = rtlabs_fun.RTLabs.f_entry in
 366       add_graph rtlabs_fun lbl (RTLabs.St_skip old_entry)
 367
 368     | Cminor.St_cost (lbl, s) ->
 369       let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s in
 370       let old_entry = rtlabs_fun.RTLabs.f_entry in
 371       generate rtlabs_fun (RTLabs.St_cost (lbl, old_entry))
 372
 373     | Cminor.St_goto lbl ->
 374       change_entry rtlabs_fun lbl
 375
 376
 377 (* Translating function definitions *)
 378
 379 (* The translation consists in the following:
 380    - Create a universe of pseudo-register names
 381    - Create a universe of label names
 382    - Create a local environment; that is, a mapping from local
 383      variables to pseudo-registers
 384    - Extract the registers representing the formal variables
 385    - Extract the registers representing the local variables
 386    - Allocate a fresh register to hold the result of the function
 387    - Allocate a fresh label representing the exit point
 388    - Initialize the graph with a return instruction at the end
 389    - Complete the graph according to the function's body.
 390      Instructions will be added from end to start following the flow of the
 391      function. *)
 392
 393 let translate_internal lbl_prefix f_def =
 394
 395   (* Register names *)
 396   let runiverse = Register.new_universe "%" in
 397
 398   (* Labels of statements *)
 399   let luniverse = Label.Gen.new_universe lbl_prefix in
 400
 401   (* Local environment *)
 402   let add_local lenv (x, _) =
 403     StringTools.Map.add x (Register.fresh runiverse) lenv in
 404   let lenv = StringTools.Map.empty in
 405   let lenv = List.fold_left add_local lenv f_def.Cminor.f_params in
 406   let lenv = List.fold_left add_local lenv f_def.Cminor.f_vars in
 407
 408   let extract vars =
 409     let f l (x, t) = l @ [(find_local lenv x, t)] in
 410     List.fold_left f [] vars in
 411
 412   (* Parameter registers *)
 413   let params = extract f_def.Cminor.f_params in
 414
 415   (* Local registers *)
 416   let locals =  extract f_def.Cminor.f_vars in
 417
 418   (* [result] is the result of the body, if any. *)
 419   let result = match f_def.Cminor.f_return with
 420     | AST.Type_void -> None
 421     | AST.Type_ret t -> Some (Register.fresh runiverse, t) in
 422
 423   let locals =
 424     locals @ (match result with None -> [] | Some (r, t) -> [(r, t)]) in
 425
 426   (* Exit label of the graph *)
 427   let exit = Label.Gen.fresh luniverse in
 428
 429   (* The control flow graph: for now, it is only a return instruction at the
 430      end. *)
 431   let return = match result with
 432     | None -> None
 433     | Some (retr, _) -> Some retr in
 434   let graph = Label.Map.add exit (RTLabs.St_return return) Label.Map.empty in
 435
 436   let rtlabs_fun =
 437     { RTLabs.f_luniverse = luniverse ;
 438       RTLabs.f_runiverse = runiverse ;
 439       RTLabs.f_result    = result ;
 440       RTLabs.f_params    = params ;
 441       RTLabs.f_locals    = locals ;
 442       RTLabs.f_stacksize = f_def.Cminor.f_stacksize ;
 443       RTLabs.f_graph     = graph ;
 444       RTLabs.f_entry     = exit ;
 445       RTLabs.f_exit      = exit } in
 446
 447   (* Complete the graph *)
 448   translate_stmt rtlabs_fun lenv [] f_def.Cminor.f_body
 449
 450
 451 let translate_functions lbls (f_id, f_def) = match f_def with
 452   | Cminor.F_int int_def ->
 453     let lbl_prefix = StringTools.Gen.fresh_prefix lbls f_id in
 454     let def = translate_internal lbl_prefix int_def in
 455     (f_id, RTLabs.F_int def)
 456   | Cminor.F_ext def -> (f_id, RTLabs.F_ext def)
 457
 458
 459 (* Initialization of globals *)
 460
 461 let sum_offsets =
 462   let f res off =
 463     let cst_off =
 464       Cminor.Expr (Cminor.Cst (AST.Cst_offset off), AST.Sig_offset) in
 465     Cminor.Expr (Cminor.Op2 (AST.Op_add, res, cst_off), AST.Sig_offset) in
 466   List.fold_left f (Cminor.Expr (Cminor.Cst (AST.Cst_int 0), AST.Sig_offset))
 467
 468 let quantity_sig_of_data data =
 469   let i = match data with
 470     | AST.Data_int8 _ -> 1
 471     | AST.Data_int16 _ -> 2
 472     | AST.Data_int32 _ -> 4
 473     | _ -> assert false (* do not use on these arguments *) in
 474   (AST.QInt i, AST.Sig_int (i, AST.Unsigned))
 475
 476 let assign_data x stmt (offsets, data) =
 477   let off = sum_offsets offsets in
 478   let addr = Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol x), AST.Sig_ptr) in
 479   let e = Cminor.Expr (Cminor.Op2 (AST.Op_addp, addr, off), AST.Sig_ptr) in
 480   let stmt' = match data with
 481 (*
 482     | AST.Data_reserve _ -> Cminor.St_skip
 483 *)
 484     | AST.Data_int8 i | AST.Data_int16 i | AST.Data_int32 i ->
 485       let (quantity, etype) = quantity_sig_of_data data in
 486       let cst = Cminor.Expr (Cminor.Cst (AST.Cst_int i), etype) in
 487       Cminor.St_store (quantity, e, cst)
 488     | AST.Data_float32 f | AST.Data_float64 f -> error_float () in
 489   Cminor.St_seq (stmt, stmt')
 490
 491 let add_global_initializations_body vars body =
 492   let f stmt (x, size, datas_opt) = match datas_opt with
 493     | None -> Cminor.St_skip
 494     | Some datas ->
 495       let offsets = Memory.all_offsets size in
 496       if List.length offsets <> List.length datas then
 497         error "bad global initialization style."
 498       else
 499         let offs_datas = List.combine offsets datas in
 500         List.fold_left (assign_data x) stmt offs_datas in
 501   Cminor.St_seq (List.fold_left f Cminor.St_skip vars, body)
 502
 503 let add_global_initializations_funct vars = function
 504   | Cminor.F_int def ->
 505     let f_body = add_global_initializations_body vars def.Cminor.f_body in
 506     Cminor.F_int { def with Cminor.f_body = f_body }
 507   | def -> def
 508
 509 (* [add_global_initializations p] moves the initializations of the globals of
 510    [p] to the beginning of the main function, if any. *)
 511
 512 let add_global_initializations p = match p.Cminor.main with
 513   | None -> p.Cminor.functs
 514   | Some main ->
 515     let main_def = List.assoc main p.Cminor.functs in
 516     let main_def = add_global_initializations_funct p.Cminor.vars main_def in
 517     MiscPottier.update_list_assoc main main_def p.Cminor.functs
 518
 519
 520 (* Translation of a Cminor program to a RTLabs program. *)
 521
 522 let translate p =
 523
 524   (* Fetch the labels already used in the program to create new ones. *)
 525   let lbls = CminorAnnotator.all_labels p in
 526
 527   (* The initialization of globals are moved at the beginning of the main. *)
 528   let functs = p.Cminor.functs (* add_global_initializations p *) in
 529
 530 (*
 531   (* The globals are associated their size. *)
 532   let f (id, size, _) = (id, size) in
 533 *)
 534
 535   (* Put all this together and translate each function. *)
 536   { RTLabs.vars = p.Cminor.vars ;
 537     RTLabs.functs = List.map (translate_functions lbls) functs ;
 538     RTLabs.main = p.Cminor.main }