[486] | 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 | |
---|
| 10 | |
---|
| 11 | (* Helper functions *) |
---|
| 12 | |
---|
| 13 | let ptr_nb_ints = Driver.TargetArch.ptr_size / Driver.TargetArch.int_size |
---|
| 14 | |
---|
| 15 | let rec freshs runiverse n = |
---|
| 16 | if n = 0 then [] |
---|
| 17 | else (Register.fresh runiverse) :: (freshs runiverse (n-1)) |
---|
| 18 | |
---|
| 19 | let int_size_of_type = function |
---|
| 20 | | AST.Type_void -> 0 |
---|
| 21 | | AST.Type_ret AST.Sig_int -> 1 |
---|
| 22 | | AST.Type_ret AST.Sig_ptr -> ptr_nb_ints |
---|
| 23 | | AST.Type_ret AST.Sig_float -> error "floats not handled." |
---|
| 24 | |
---|
| 25 | let fresh_type runiverse ty = freshs runiverse (int_size_of_type ty) |
---|
| 26 | |
---|
| 27 | let fresh_result runiverse def = fresh_type runiverse def.Cminor.f_sig.AST.res |
---|
| 28 | |
---|
| 29 | let type_of_local def x = |
---|
| 30 | if List.mem x def.Cminor.f_ptrs then AST.Type_ret AST.Sig_ptr |
---|
| 31 | else |
---|
| 32 | if List.mem x def.Cminor.f_vars then AST.Type_ret AST.Sig_int |
---|
| 33 | else |
---|
| 34 | let n = MiscPottier.index_of x def.Cminor.f_params in |
---|
| 35 | AST.Type_ret (List.nth def.Cminor.f_sig.AST.args n) |
---|
| 36 | |
---|
| 37 | let type_of_cst = function |
---|
| 38 | | AST.Cst_int _ -> AST.Sig_int |
---|
| 39 | | AST.Cst_float _ -> error "floats not handled." |
---|
| 40 | | AST.Cst_addrsymbol _ | AST.Cst_stackoffset _ -> AST.Sig_ptr |
---|
| 41 | |
---|
| 42 | let type_of_op1 = function |
---|
| 43 | | AST.Op_cast8unsigned | AST.Op_cast8signed | AST.Op_cast16unsigned |
---|
| 44 | | AST.Op_cast16signed | AST.Op_negint | AST.Op_notbool | AST.Op_notint |
---|
| 45 | | AST.Op_intoffloat | AST.Op_intuoffloat | AST.Op_intofptr -> |
---|
| 46 | AST.Sig_int |
---|
| 47 | | AST.Op_negf | AST.Op_absf | AST.Op_singleoffloat | AST.Op_floatofint |
---|
| 48 | | AST.Op_floatofintu -> |
---|
| 49 | AST.Sig_float |
---|
| 50 | | AST.Op_ptrofint -> |
---|
| 51 | AST.Sig_ptr |
---|
| 52 | | AST.Op_id -> |
---|
| 53 | assert false (* Dependent on argument. Treated in type_of_expr *) |
---|
| 54 | |
---|
| 55 | let type_of_op2 = function |
---|
| 56 | | AST.Op_add | AST.Op_sub | AST.Op_mul | AST.Op_div | AST.Op_divu | AST.Op_mod |
---|
| 57 | | AST.Op_modu | AST.Op_and | AST.Op_or | AST.Op_xor | AST.Op_shl | AST.Op_shr |
---|
| 58 | | AST.Op_shru -> |
---|
| 59 | AST.Sig_int |
---|
| 60 | | AST.Op_addf | AST.Op_subf | AST.Op_mulf | AST.Op_divf -> |
---|
| 61 | AST.Sig_float |
---|
| 62 | | AST.Op_cmp _ | AST.Op_cmpu _ | AST.Op_cmpf _ | AST.Op_cmpp _ -> |
---|
| 63 | AST.Sig_int |
---|
| 64 | | AST.Op_addp | AST.Op_subp -> |
---|
| 65 | AST.Sig_ptr |
---|
| 66 | |
---|
| 67 | let rec type_of_expr def = function |
---|
| 68 | | Cminor.Id x -> type_of_local def x |
---|
| 69 | | Cminor.Cst cst -> AST.Type_ret (type_of_cst cst) |
---|
| 70 | | Cminor.Op1 (AST.Op_id, e) -> type_of_expr def e |
---|
| 71 | | Cminor.Op1 (op1, _) -> AST.Type_ret (type_of_op1 op1) |
---|
| 72 | | Cminor.Op2 (op2, _, _) -> AST.Type_ret (type_of_op2 op2) |
---|
| 73 | | Cminor.Mem (mq, _) -> AST.Type_ret (Memory.type_of_memory_q mq) |
---|
| 74 | | Cminor.Cond _ -> AST.Type_ret AST.Sig_int |
---|
| 75 | | Cminor.Exp_cost (_, e) -> type_of_expr def e |
---|
| 76 | |
---|
| 77 | let fresh_local runiverse def x = |
---|
| 78 | fresh_type runiverse (type_of_local def x) |
---|
| 79 | |
---|
| 80 | let allocate (rtlabs_fun : RTLabs.internal_function) (n : int) |
---|
| 81 | : RTLabs.internal_function * Register.t list = |
---|
| 82 | let rs = freshs rtlabs_fun.RTLabs.f_runiverse n in |
---|
| 83 | let rtlabs_fun = |
---|
| 84 | { rtlabs_fun with RTLabs.f_locals = rtlabs_fun.RTLabs.f_locals @ [rs] } in |
---|
| 85 | (rtlabs_fun, rs) |
---|
| 86 | |
---|
| 87 | let allocate_expr |
---|
| 88 | (def : Cminor.internal_function) |
---|
| 89 | (rtlabs_fun : RTLabs.internal_function) |
---|
| 90 | (e : Cminor.expression) |
---|
| 91 | : (RTLabs.internal_function * Register.t list) = |
---|
| 92 | allocate rtlabs_fun (int_size_of_type (type_of_expr def e)) |
---|
| 93 | |
---|
| 94 | type local_env = Register.t list StringTools.Map.t |
---|
| 95 | |
---|
| 96 | let find_local (lenv : local_env) (x : AST.ident) : Register.t list = |
---|
| 97 | if StringTools.Map.mem x lenv then StringTools.Map.find x lenv |
---|
| 98 | else error ("Unknown local \"" ^ x ^ "\".") |
---|
| 99 | |
---|
| 100 | let find_olocal (lenv : local_env) (ox : AST.ident option) : Register.t list = |
---|
| 101 | match ox with |
---|
| 102 | | None -> [] |
---|
| 103 | | Some x -> find_local lenv x |
---|
| 104 | |
---|
| 105 | let choose_destination |
---|
| 106 | (def : Cminor.internal_function) |
---|
| 107 | (rtlabs_fun : RTLabs.internal_function) |
---|
| 108 | (lenv : local_env) |
---|
| 109 | (e : Cminor.expression) |
---|
| 110 | : RTLabs.internal_function * Register.t list = |
---|
| 111 | match e with |
---|
| 112 | | Cminor.Id x -> (rtlabs_fun, find_local lenv x) |
---|
| 113 | | _ -> allocate_expr def rtlabs_fun e |
---|
| 114 | |
---|
| 115 | let choose_destinations |
---|
| 116 | (def : Cminor.internal_function) |
---|
| 117 | (rtlabs_fun : RTLabs.internal_function) |
---|
| 118 | (lenv : local_env) |
---|
| 119 | (args : Cminor.expression list) |
---|
| 120 | : RTLabs.internal_function * Register.t list list = |
---|
| 121 | let f (rtlabs_fun, regs) e = |
---|
| 122 | let (rtlabs_fun, rs) = choose_destination def rtlabs_fun lenv e in |
---|
| 123 | (rtlabs_fun, regs @ [rs]) in |
---|
| 124 | List.fold_left f (rtlabs_fun, []) args |
---|
| 125 | |
---|
| 126 | let fresh_label (rtlabs_fun : RTLabs.internal_function) : Label.t = |
---|
| 127 | Label.Gen.fresh rtlabs_fun.RTLabs.f_luniverse |
---|
| 128 | |
---|
| 129 | let change_entry |
---|
| 130 | (rtlabs_fun : RTLabs.internal_function) |
---|
| 131 | (new_entry : Label.t) |
---|
| 132 | : RTLabs.internal_function = |
---|
| 133 | { rtlabs_fun with RTLabs.f_entry = new_entry } |
---|
| 134 | |
---|
| 135 | |
---|
| 136 | (* Add a label and its associated instruction at the beginning of a function's |
---|
| 137 | graph *) |
---|
| 138 | let add_graph |
---|
| 139 | (rtlabs_fun : RTLabs.internal_function) |
---|
| 140 | (lbl : Label.t) |
---|
| 141 | (stmt : RTLabs.statement) |
---|
| 142 | : RTLabs.internal_function = |
---|
| 143 | let graph = Label.Map.add lbl stmt rtlabs_fun.RTLabs.f_graph in |
---|
| 144 | let rtlabs_fun = { rtlabs_fun with RTLabs.f_graph = graph } in |
---|
| 145 | change_entry rtlabs_fun lbl |
---|
| 146 | |
---|
| 147 | |
---|
| 148 | let generate |
---|
| 149 | (rtlabs_fun : RTLabs.internal_function) |
---|
| 150 | (stmt : RTLabs.statement) |
---|
| 151 | : RTLabs.internal_function = |
---|
| 152 | let lbl = fresh_label rtlabs_fun in |
---|
| 153 | add_graph rtlabs_fun lbl stmt |
---|
| 154 | |
---|
| 155 | |
---|
| 156 | (* [addressing e] returns the type of address represented by [e], |
---|
| 157 | along with its arguments *) |
---|
| 158 | |
---|
| 159 | let addressing (e : Cminor.expression) |
---|
| 160 | : (RTLabs.addressing * Cminor.expression list) = |
---|
| 161 | match e with |
---|
| 162 | | Cminor.Cst (AST.Cst_addrsymbol id) -> (RTLabs.Aglobal (id, 0), []) |
---|
| 163 | | Cminor.Cst (AST.Cst_stackoffset n) -> (RTLabs.Ainstack n, []) |
---|
| 164 | | Cminor.Op2 (AST.Op_add, |
---|
| 165 | Cminor.Cst (AST.Cst_addrsymbol id), |
---|
| 166 | Cminor.Cst (AST.Cst_int n)) -> |
---|
| 167 | (RTLabs.Aglobal (id, n), []) |
---|
| 168 | | Cminor.Op2 (AST.Op_add, e1, Cminor.Cst (AST.Cst_int n)) -> |
---|
| 169 | (RTLabs.Aindexed n, [e1]) |
---|
| 170 | | Cminor.Op2 (AST.Op_add, |
---|
| 171 | Cminor.Cst (AST.Cst_addrsymbol id), |
---|
| 172 | e2) -> |
---|
| 173 | (RTLabs.Abased (id, 0), [e2]) |
---|
| 174 | | Cminor.Op2 (AST.Op_add, e1, e2) -> (RTLabs.Aindexed2, [e1 ; e2]) |
---|
| 175 | | _ -> (RTLabs.Aindexed 0, [e]) |
---|
| 176 | |
---|
| 177 | |
---|
| 178 | (* Translating conditions |
---|
| 179 | |
---|
| 180 | The Cminor definition [def] is used for typing purposes (differencing from |
---|
| 181 | integers and pointers). [rtlabs_fun] is the function being |
---|
| 182 | constructed. [lenv] is the environment associating a pseudo-register to the |
---|
| 183 | variables of the program being translated. *) |
---|
| 184 | |
---|
| 185 | let rec translate_branch |
---|
| 186 | (def : Cminor.internal_function) |
---|
| 187 | (rtlabs_fun : RTLabs.internal_function) |
---|
| 188 | (lenv : local_env) |
---|
| 189 | (e : Cminor.expression) |
---|
| 190 | (lbl_true : Label.t) |
---|
| 191 | (lbl_false : Label.t) |
---|
| 192 | : RTLabs.internal_function = |
---|
| 193 | match e with |
---|
| 194 | |
---|
| 195 | | Cminor.Id x -> |
---|
| 196 | let stmt = |
---|
| 197 | RTLabs.St_cond1 (AST.Op_id, find_local lenv x, lbl_true, lbl_false) in |
---|
| 198 | generate rtlabs_fun stmt |
---|
| 199 | |
---|
| 200 | | Cminor.Cst cst -> |
---|
| 201 | generate rtlabs_fun (RTLabs.St_condcst (cst, lbl_true, lbl_false)) |
---|
| 202 | |
---|
| 203 | | Cminor.Op1 (op1, e) -> |
---|
| 204 | let (rtlabs_fun, rs) = choose_destination def rtlabs_fun lenv e in |
---|
| 205 | let stmt = RTLabs.St_cond1 (op1, rs, lbl_true, lbl_false) in |
---|
| 206 | let rtlabs_fun = generate rtlabs_fun stmt in |
---|
| 207 | translate_expr def rtlabs_fun lenv rs e |
---|
| 208 | |
---|
| 209 | | Cminor.Op2 (op2, e1, e2) -> |
---|
| 210 | let (rtlabs_fun, rs1) = choose_destination def rtlabs_fun lenv e1 in |
---|
| 211 | let (rtlabs_fun, rs2) = choose_destination def rtlabs_fun lenv e2 in |
---|
| 212 | let stmt = RTLabs.St_cond2 (op2, rs1, rs2, lbl_true, lbl_false) in |
---|
| 213 | let rtlabs_fun = generate rtlabs_fun stmt in |
---|
| 214 | translate_exprs def rtlabs_fun lenv [rs1 ; rs2] [e1 ; e2] |
---|
| 215 | |
---|
| 216 | | _ -> |
---|
| 217 | let (rtlabs_fun, rs) = choose_destination def rtlabs_fun lenv e in |
---|
| 218 | let stmt = RTLabs.St_cond1 (AST.Op_id, rs, lbl_true, lbl_false) in |
---|
| 219 | let rtlabs_fun = generate rtlabs_fun stmt in |
---|
| 220 | translate_expr def rtlabs_fun lenv rs e |
---|
| 221 | |
---|
| 222 | (* Translating expressions |
---|
| 223 | |
---|
| 224 | The Cminor definition [def] is used for typing purposes (differencing from |
---|
| 225 | integers and pointers). [rtlabs_fun] is the function being |
---|
| 226 | constructed. [lenv] is the environment associating a pseudo-register to the |
---|
| 227 | variables of the program being translated. [destrs] are the destination |
---|
| 228 | registers. There may be more than one in the case of pointers, and when the |
---|
| 229 | size of addresses is bigger than a machine word. *) |
---|
| 230 | |
---|
| 231 | and translate_expr |
---|
| 232 | (def : Cminor.internal_function) |
---|
| 233 | (rtlabs_fun : RTLabs.internal_function) |
---|
| 234 | (lenv : local_env) |
---|
| 235 | (destrs : Register.t list) |
---|
| 236 | (e : Cminor.expression) |
---|
| 237 | : RTLabs.internal_function = |
---|
| 238 | match e with |
---|
| 239 | |
---|
| 240 | | Cminor.Id x -> |
---|
| 241 | let xrs = find_local lenv x in |
---|
| 242 | let rec eq_reg_list rl1 rl2 = match rl1, rl2 with |
---|
| 243 | | [], [] -> true |
---|
| 244 | | r1 :: rl1, r2 :: rl2 -> |
---|
| 245 | (Register.equal r1 r2) && (eq_reg_list rl1 rl2) |
---|
| 246 | | _ -> false in |
---|
| 247 | (* If the destinations and sources are the same, just do nothing. *) |
---|
| 248 | if eq_reg_list destrs xrs then rtlabs_fun |
---|
| 249 | else |
---|
| 250 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
| 251 | let stmt = RTLabs.St_op1 (AST.Op_id, destrs, xrs, old_entry) in |
---|
| 252 | generate rtlabs_fun stmt |
---|
| 253 | |
---|
| 254 | | Cminor.Cst cst -> |
---|
| 255 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
| 256 | let stmt = RTLabs.St_cst (destrs, cst, old_entry) in |
---|
| 257 | generate rtlabs_fun stmt |
---|
| 258 | |
---|
| 259 | | Cminor.Op1 (op1, e) -> |
---|
| 260 | let (rtlabs_fun, rs) = choose_destination def rtlabs_fun lenv e in |
---|
| 261 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
| 262 | let stmt = RTLabs.St_op1 (op1, destrs, rs, old_entry) in |
---|
| 263 | let rtlabs_fun = generate rtlabs_fun stmt in |
---|
| 264 | translate_expr def rtlabs_fun lenv rs e |
---|
| 265 | |
---|
| 266 | | Cminor.Op2 (op2, e1, e2) -> |
---|
| 267 | let (rtlabs_fun, rs1) = choose_destination def rtlabs_fun lenv e1 in |
---|
| 268 | let (rtlabs_fun, rs2) = choose_destination def rtlabs_fun lenv e2 in |
---|
| 269 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
| 270 | let stmt = RTLabs.St_op2 (op2, destrs, rs1, rs2, old_entry) in |
---|
| 271 | let rtlabs_fun = generate rtlabs_fun stmt in |
---|
| 272 | translate_exprs def rtlabs_fun lenv [rs1 ; rs2] [e1 ; e2] |
---|
| 273 | |
---|
| 274 | | Cminor.Mem (chunk, e) -> |
---|
| 275 | let (mode, args) = addressing e in |
---|
| 276 | let (rtlabs_fun, regs) = choose_destinations def rtlabs_fun lenv args in |
---|
| 277 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
| 278 | let stmt = RTLabs.St_load (chunk, mode, regs, destrs, old_entry) in |
---|
| 279 | let rtlabs_fun = generate rtlabs_fun stmt in |
---|
| 280 | translate_exprs def rtlabs_fun lenv regs args |
---|
| 281 | |
---|
| 282 | | Cminor.Cond (e1, e2, e3) -> |
---|
| 283 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
| 284 | let (rtlabs_fun, rs2) = choose_destination def rtlabs_fun lenv e2 in |
---|
| 285 | let (rtlabs_fun, rs3) = choose_destination def rtlabs_fun lenv e3 in |
---|
| 286 | let rtlabs_fun = translate_expr def rtlabs_fun lenv rs3 e3 in |
---|
| 287 | let lbl_false = rtlabs_fun.RTLabs.f_entry in |
---|
| 288 | let rtlabs_fun = change_entry rtlabs_fun old_entry in |
---|
| 289 | let rtlabs_fun = translate_expr def rtlabs_fun lenv rs2 e2 in |
---|
| 290 | let lbl_true = rtlabs_fun.RTLabs.f_entry in |
---|
| 291 | translate_branch def rtlabs_fun lenv e1 lbl_true lbl_false |
---|
| 292 | |
---|
| 293 | | Cminor.Exp_cost (lbl, e) -> |
---|
| 294 | let (rtlabs_fun, rs) = choose_destination def rtlabs_fun lenv e in |
---|
| 295 | let rtlabs_fun = translate_expr def rtlabs_fun lenv rs e in |
---|
| 296 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
| 297 | generate rtlabs_fun (RTLabs.St_cost (lbl, old_entry)) |
---|
| 298 | |
---|
| 299 | and translate_exprs |
---|
| 300 | (def : Cminor.internal_function) |
---|
| 301 | (rtlabs_fun : RTLabs.internal_function) |
---|
| 302 | (lenv : local_env) |
---|
| 303 | (regs : Register.t list list) |
---|
| 304 | (args : Cminor.expression list) |
---|
| 305 | : RTLabs.internal_function = |
---|
| 306 | let f destrs e rtlabs_fun = translate_expr def rtlabs_fun lenv destrs e in |
---|
| 307 | List.fold_right2 f regs args rtlabs_fun |
---|
| 308 | |
---|
| 309 | |
---|
| 310 | (* Switch transformation |
---|
| 311 | |
---|
| 312 | switch (e) { |
---|
| 313 | case c0: exit i0; |
---|
| 314 | case c1: exit i1; |
---|
| 315 | ... |
---|
| 316 | default: exit idfl; } |
---|
| 317 | |
---|
| 318 | is translated to |
---|
| 319 | |
---|
| 320 | if (e == c0) exit i0; |
---|
| 321 | if (e == c1) exit i1; |
---|
| 322 | ... |
---|
| 323 | exit idfl; *) |
---|
| 324 | |
---|
| 325 | let transform_switch |
---|
| 326 | (e : Cminor.expression) |
---|
| 327 | (cases : (int * int) list) |
---|
| 328 | (dfl : int) |
---|
| 329 | : Cminor.statement = |
---|
| 330 | let rec aux = function |
---|
| 331 | | [] -> Cminor.St_skip |
---|
| 332 | | (case, exit) :: cases -> |
---|
| 333 | let c = |
---|
| 334 | Cminor.Op2 (AST.Op_cmp AST.Cmp_eq, |
---|
| 335 | e, Cminor.Cst (AST.Cst_int case)) in |
---|
| 336 | let stmt = |
---|
| 337 | Cminor.St_ifthenelse (c, Cminor.St_exit exit, Cminor.St_skip) in |
---|
| 338 | Cminor.St_seq (stmt, aux cases) |
---|
| 339 | in |
---|
| 340 | Cminor.St_seq (aux cases, Cminor.St_exit dfl) |
---|
| 341 | |
---|
| 342 | |
---|
| 343 | (* Translating statements |
---|
| 344 | |
---|
| 345 | The Cminor definition [def] is used for typing purposes (differencing from |
---|
| 346 | integers and pointers). [rtlabs_fun] is the function being |
---|
| 347 | constructed. [lenv] is the environment associating a pseudo-register to the |
---|
| 348 | variables of the program being translated. [exists] is the list of label to |
---|
| 349 | exit to. The leftmost label in the list is used to exit the closest block. *) |
---|
| 350 | |
---|
| 351 | let rec translate_stmt |
---|
| 352 | (def : Cminor.internal_function) |
---|
| 353 | (rtlabs_fun : RTLabs.internal_function) |
---|
| 354 | (lenv : local_env) |
---|
| 355 | (exits : Label.t list) |
---|
| 356 | (stmt : Cminor.statement) |
---|
| 357 | : RTLabs.internal_function = |
---|
| 358 | match stmt with |
---|
| 359 | |
---|
| 360 | | Cminor.St_skip -> rtlabs_fun |
---|
| 361 | |
---|
| 362 | | Cminor.St_assign (x, e) -> |
---|
| 363 | translate_expr def rtlabs_fun lenv (find_local lenv x) e |
---|
| 364 | |
---|
| 365 | | Cminor.St_store (chunk, e1, e2) -> |
---|
| 366 | let (mode, args) = addressing e1 in |
---|
| 367 | let (rtlabs_fun, regs) = choose_destinations def rtlabs_fun lenv args in |
---|
| 368 | let (rtlabs_fun, rs) = choose_destination def rtlabs_fun lenv e2 in |
---|
| 369 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
| 370 | let stmt = RTLabs.St_store (chunk, mode, regs, rs, old_entry) in |
---|
| 371 | let rtlabs_fun = generate rtlabs_fun stmt in |
---|
| 372 | let rtlabs_fun = translate_expr def rtlabs_fun lenv rs e2 in |
---|
| 373 | translate_exprs def rtlabs_fun lenv regs args |
---|
| 374 | |
---|
| 375 | | Cminor.St_call (oret, Cminor.Cst (AST.Cst_addrsymbol f), args, sg) -> |
---|
| 376 | let (rtlabs_fun, regs) = choose_destinations def rtlabs_fun lenv args in |
---|
| 377 | let retrs = find_olocal lenv oret in |
---|
| 378 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
| 379 | let stmt = RTLabs.St_call_id (f, regs, retrs, sg, old_entry) in |
---|
| 380 | let rtlabs_fun = generate rtlabs_fun stmt in |
---|
| 381 | translate_exprs def rtlabs_fun lenv regs args |
---|
| 382 | |
---|
| 383 | | Cminor.St_call (oret, f, args, sg) -> |
---|
| 384 | let (rtlabs_fun, frs) = choose_destination def rtlabs_fun lenv f in |
---|
| 385 | let (rtlabs_fun, regs) = choose_destinations def rtlabs_fun lenv args in |
---|
| 386 | let retrs = find_olocal lenv oret in |
---|
| 387 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
| 388 | let stmt = RTLabs.St_call_ptr (frs, regs, retrs, sg, old_entry) in |
---|
| 389 | let rtlabs_fun = generate rtlabs_fun stmt in |
---|
| 390 | let rtlabs_fun = translate_exprs def rtlabs_fun lenv regs args in |
---|
| 391 | translate_expr def rtlabs_fun lenv frs f |
---|
| 392 | |
---|
| 393 | | Cminor.St_tailcall (Cminor.Cst (AST.Cst_addrsymbol f), args, sg) -> |
---|
| 394 | let (rtlabs_fun, regs) = choose_destinations def rtlabs_fun lenv args in |
---|
| 395 | let stmt = RTLabs.St_tailcall_id (f, regs, sg) in |
---|
| 396 | let rtlabs_fun = generate rtlabs_fun stmt in |
---|
| 397 | translate_exprs def rtlabs_fun lenv regs args |
---|
| 398 | |
---|
| 399 | | Cminor.St_tailcall (f, args, sg) -> |
---|
| 400 | let (rtlabs_fun, frs) = choose_destination def rtlabs_fun lenv f in |
---|
| 401 | let (rtlabs_fun, regs) = choose_destinations def rtlabs_fun lenv args in |
---|
| 402 | let stmt = RTLabs.St_tailcall_ptr (frs, regs, sg) in |
---|
| 403 | let rtlabs_fun = generate rtlabs_fun stmt in |
---|
| 404 | let rtlabs_fun = translate_exprs def rtlabs_fun lenv regs args in |
---|
| 405 | translate_expr def rtlabs_fun lenv frs f |
---|
| 406 | |
---|
| 407 | | Cminor.St_seq (s1, s2) -> |
---|
| 408 | let rtlabs_fun = translate_stmt def rtlabs_fun lenv exits s2 in |
---|
| 409 | translate_stmt def rtlabs_fun lenv exits s1 |
---|
| 410 | |
---|
| 411 | | Cminor.St_ifthenelse (e, s1, s2) -> |
---|
| 412 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
| 413 | let rtlabs_fun = translate_stmt def rtlabs_fun lenv exits s2 in |
---|
| 414 | let lbl_false = rtlabs_fun.RTLabs.f_entry in |
---|
| 415 | let rtlabs_fun = change_entry rtlabs_fun old_entry in |
---|
| 416 | let rtlabs_fun = translate_stmt def rtlabs_fun lenv exits s1 in |
---|
| 417 | let lbl_true = rtlabs_fun.RTLabs.f_entry in |
---|
| 418 | translate_branch def rtlabs_fun lenv e lbl_true lbl_false |
---|
| 419 | |
---|
| 420 | | Cminor.St_loop s -> |
---|
| 421 | let loop_start = fresh_label rtlabs_fun in |
---|
| 422 | let rtlabs_fun = change_entry rtlabs_fun loop_start in |
---|
| 423 | let rtlabs_fun = translate_stmt def rtlabs_fun lenv exits s in |
---|
| 424 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
| 425 | add_graph rtlabs_fun loop_start (RTLabs.St_skip old_entry) |
---|
| 426 | |
---|
| 427 | | Cminor.St_block s -> |
---|
| 428 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
| 429 | translate_stmt def rtlabs_fun lenv (old_entry :: exits) s |
---|
| 430 | |
---|
| 431 | | Cminor.St_exit n -> |
---|
| 432 | change_entry rtlabs_fun (List.nth exits n) |
---|
| 433 | |
---|
| 434 | | Cminor.St_return eopt -> |
---|
| 435 | let rtlabs_fun = change_entry rtlabs_fun rtlabs_fun.RTLabs.f_exit in |
---|
| 436 | (match eopt, rtlabs_fun.RTLabs.f_result with |
---|
| 437 | | None, _ -> rtlabs_fun |
---|
| 438 | | Some e, retrs -> translate_expr def rtlabs_fun lenv retrs e) |
---|
| 439 | |
---|
| 440 | | Cminor.St_switch (e, cases, dfl) -> |
---|
| 441 | let stmt = transform_switch e cases dfl in |
---|
| 442 | translate_stmt def rtlabs_fun lenv exits stmt |
---|
| 443 | |
---|
| 444 | | Cminor.St_label (lbl, s) -> |
---|
| 445 | let rtlabs_fun = translate_stmt def rtlabs_fun lenv exits s in |
---|
| 446 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
| 447 | add_graph rtlabs_fun lbl (RTLabs.St_skip old_entry) |
---|
| 448 | |
---|
| 449 | | Cminor.St_cost (lbl, s) -> |
---|
| 450 | let rtlabs_fun = translate_stmt def rtlabs_fun lenv exits s in |
---|
| 451 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
| 452 | generate rtlabs_fun (RTLabs.St_cost (lbl, old_entry)) |
---|
| 453 | |
---|
| 454 | | Cminor.St_goto lbl -> |
---|
| 455 | change_entry rtlabs_fun lbl |
---|
| 456 | |
---|
| 457 | |
---|
| 458 | (* Translating function definitions *) |
---|
| 459 | |
---|
| 460 | (* The translation consists in the following: |
---|
| 461 | - Create a universe of pseudo-register names |
---|
| 462 | - Create a universe of label names |
---|
| 463 | - Create a local environment; that is, a mapping from local |
---|
| 464 | variables to pseudo-registers |
---|
| 465 | - Extract the registers representing the formal variables |
---|
| 466 | - Extract the registers representing the local variables |
---|
| 467 | - Allocate a fresh label representing the exit point |
---|
| 468 | - Allocate fresh registers holding the result of the function |
---|
| 469 | - Initialize the graph with a return instruction at the end |
---|
| 470 | - Complete the graph according to the function's body. |
---|
| 471 | Instructions will be added from end to start following the flow of the |
---|
| 472 | function. *) |
---|
| 473 | |
---|
| 474 | let translate_internal lbl_prefix f_def = |
---|
| 475 | |
---|
| 476 | (* Register names *) |
---|
| 477 | let runiverse = Register.new_universe "%" in |
---|
| 478 | |
---|
| 479 | (* Labels of statements *) |
---|
| 480 | let luniverse = Label.Gen.new_universe lbl_prefix in |
---|
| 481 | |
---|
| 482 | (* Local environment *) |
---|
| 483 | let add_local lenv x = |
---|
| 484 | let rs = fresh_local runiverse f_def x in |
---|
| 485 | StringTools.Map.add x rs lenv in |
---|
| 486 | let lenv = StringTools.Map.empty in |
---|
| 487 | let lenv = List.fold_left add_local lenv f_def.Cminor.f_params in |
---|
| 488 | let lenv = List.fold_left add_local lenv f_def.Cminor.f_vars in |
---|
| 489 | let lenv = List.fold_left add_local lenv f_def.Cminor.f_ptrs in |
---|
| 490 | |
---|
| 491 | let extract vars = |
---|
| 492 | List.fold_left (fun l x -> l @ [StringTools.Map.find x lenv]) [] vars in |
---|
| 493 | |
---|
| 494 | (* Parameter registers *) |
---|
| 495 | let params = extract f_def.Cminor.f_params in |
---|
| 496 | |
---|
| 497 | (* Local registers *) |
---|
| 498 | let locals = extract (f_def.Cminor.f_vars @ f_def.Cminor.f_ptrs) in |
---|
| 499 | |
---|
| 500 | (* Exit label of the graph *) |
---|
| 501 | let exit = Label.Gen.fresh luniverse in |
---|
| 502 | |
---|
| 503 | (* [retrs] are the registers that holds the return value of the body, if |
---|
| 504 | any. *) |
---|
| 505 | let retrs = fresh_result runiverse f_def in |
---|
| 506 | |
---|
| 507 | let locals = locals @ [retrs] in |
---|
| 508 | |
---|
| 509 | (* The control flow graph: for now, it is only a return instruction at the |
---|
| 510 | end. *) |
---|
| 511 | let graph = Label.Map.add exit (RTLabs.St_return retrs) Label.Map.empty in |
---|
| 512 | |
---|
| 513 | let rtlabs_fun = |
---|
| 514 | { RTLabs.f_luniverse = luniverse ; |
---|
| 515 | RTLabs.f_runiverse = runiverse ; |
---|
| 516 | RTLabs.f_sig = f_def.Cminor.f_sig ; |
---|
| 517 | RTLabs.f_result = retrs ; |
---|
| 518 | RTLabs.f_params = params ; |
---|
| 519 | RTLabs.f_locals = locals ; |
---|
| 520 | RTLabs.f_stacksize = f_def.Cminor.f_stacksize ; |
---|
| 521 | RTLabs.f_graph = graph ; |
---|
| 522 | RTLabs.f_entry = exit ; |
---|
| 523 | RTLabs.f_exit = exit } in |
---|
| 524 | |
---|
| 525 | (* Complete the graph *) |
---|
| 526 | translate_stmt f_def rtlabs_fun lenv [] f_def.Cminor.f_body |
---|
| 527 | |
---|
| 528 | |
---|
| 529 | let translate_functions lbls (f_id, f_def) = match f_def with |
---|
| 530 | | Cminor.F_int int_def -> |
---|
| 531 | let lbl_prefix = StringTools.Gen.fresh_prefix lbls f_id in |
---|
| 532 | let def = translate_internal lbl_prefix int_def in |
---|
| 533 | (f_id, RTLabs.F_int def) |
---|
| 534 | | Cminor.F_ext def -> (f_id, RTLabs.F_ext def) |
---|
| 535 | |
---|
| 536 | |
---|
| 537 | (* Initialization of globals *) |
---|
| 538 | |
---|
| 539 | let assign_data x stmt (data, off) = |
---|
| 540 | let e = Cminor.Op2 (AST.Op_add, |
---|
| 541 | Cminor.Cst (AST.Cst_addrsymbol x), |
---|
| 542 | Cminor.Cst (AST.Cst_int off)) in |
---|
| 543 | let chunk () = Memory.mq_of_data data in |
---|
| 544 | let stmt' = match data with |
---|
| 545 | | AST.Data_reserve _ -> Cminor.St_skip |
---|
| 546 | | AST.Data_int8 i | AST.Data_int16 i | AST.Data_int32 i -> |
---|
| 547 | Cminor.St_store (chunk (), e, Cminor.Cst (AST.Cst_int i)) |
---|
| 548 | | AST.Data_float32 f | AST.Data_float64 f -> |
---|
| 549 | Cminor.St_store (chunk (), e, Cminor.Cst (AST.Cst_float f)) in |
---|
| 550 | Cminor.St_seq (stmt, stmt') |
---|
| 551 | |
---|
| 552 | let add_global_initializations_body vars body = |
---|
| 553 | let f stmt (x, datas) = |
---|
| 554 | let offs_of_datas = RTLabsMemory.offsets_of_datas datas in |
---|
| 555 | List.fold_left (assign_data x) stmt offs_of_datas in |
---|
| 556 | Cminor.St_seq (List.fold_left f Cminor.St_skip vars, body) |
---|
| 557 | |
---|
| 558 | let add_global_initializations_funct vars = function |
---|
| 559 | | Cminor.F_int def -> |
---|
| 560 | let f_body = add_global_initializations_body vars def.Cminor.f_body in |
---|
| 561 | Cminor.F_int { def with Cminor.f_body = f_body } |
---|
| 562 | | def -> def |
---|
| 563 | |
---|
| 564 | (* [add_global_initializations p] moves the initializations of the globals of |
---|
| 565 | [p] to the beginning of the main function, if any. *) |
---|
| 566 | |
---|
| 567 | let add_global_initializations p = match p.Cminor.main with |
---|
| 568 | | None -> p.Cminor.functs |
---|
| 569 | | Some main -> |
---|
| 570 | let main_def = List.assoc main p.Cminor.functs in |
---|
| 571 | let main_def = add_global_initializations_funct p.Cminor.vars main_def in |
---|
| 572 | MiscPottier.update_list_assoc main main_def p.Cminor.functs |
---|
| 573 | |
---|
| 574 | |
---|
| 575 | (* Translation of a Cminor program to a RTLabs program. *) |
---|
| 576 | |
---|
| 577 | let translate p = |
---|
| 578 | |
---|
| 579 | (* Fetch the variables in the program that are pointers (whose value is an |
---|
| 580 | address). Some architectures have different sizes for pointers and |
---|
| 581 | integers. *) |
---|
| 582 | let p = CminorPointers.fill p in |
---|
| 583 | |
---|
| 584 | (* Fetch the labels already used in the program to create new ones. *) |
---|
| 585 | let lbls = CminorAnnotator.all_labels p in |
---|
| 586 | |
---|
| 587 | (* The initialization of globals are moved at the beginning of the main. *) |
---|
| 588 | let functs = add_global_initializations p in |
---|
| 589 | |
---|
| 590 | (* The globals are associated their size. *) |
---|
| 591 | let f (id, datas) = (id, RTLabsMemory.size_of_datas datas) in |
---|
| 592 | |
---|
| 593 | (* Put all this together and translate each function. *) |
---|
| 594 | { RTLabs.vars = List.map f p.Cminor.vars ; |
---|
| 595 | RTLabs.functs = List.map (translate_functions lbls) functs ; |
---|
| 596 | RTLabs.main = p.Cminor.main } |
---|