Changeset 1056 for src/Cminor/toRTLabs.ma
 Timestamp:
 Jul 5, 2011, 4:25:41 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Cminor/toRTLabs.ma
r961 r1056 6 6 definition env ≝ identifier_map SymbolTag register. 7 7 definition label_env ≝ identifier_map SymbolTag label. 8 definition populate_env : env → universe RegisterTag → list (ident × typ) → res (list (register×typ) × env × (universe RegisterTag)) ≝8 definition populate_env : env → universe RegisterTag → list (ident × typ) → list (register×typ) × env × (universe RegisterTag) ≝ 9 9 λen,gen. foldr ?? 10 10 (λidt,rsengen. 11 11 let 〈id,ty〉 ≝ idt in 12 do 〈rs,en,gen〉 ← rsengen;13 do 〈r,gen'〉 ← fresh … gen;14 OK ? 〈〈r,ty〉::rs, add ?? en id r, gen'〉) (OK ? 〈[ ], en, gen〉).15 16 definition populate_label_env : label_env → universe LabelTag → list ident → res (label_env × (universe LabelTag)) ≝12 let 〈rs,en,gen〉 ≝ rsengen in 13 let 〈r,gen'〉 ≝ fresh … gen in 14 〈〈r,ty〉::rs, add ?? en id r, gen'〉) 〈[ ], en, gen〉. 15 16 definition populate_label_env : label_env → universe LabelTag → list ident → label_env × (universe LabelTag) ≝ 17 17 λen,gen. foldr ?? 18 18 (λid,engen. 19 do 〈en,gen〉 ← engen;20 do 〈r,gen'〉 ← fresh … gen;21 OK ? 〈add ?? en id r, gen'〉) (OK ? 〈en, gen〉).19 let 〈en,gen〉 ≝ engen in 20 let 〈r,gen'〉 ≝ fresh … gen in 21 〈add ?? en id r, gen'〉) 〈en, gen〉. 22 22 23 23 (* Add a statement to the graph, *without* updating the entry label. *) … … 37 37 (* Add a statement with a fresh label to the start of the function. The 38 38 statement is parametrised by the *next* instruction's label. *) 39 definition add_fresh_to_graph : (label → statement) → internal_function → resinternal_function ≝39 definition add_fresh_to_graph : (label → statement) → internal_function → internal_function ≝ 40 40 λs,f. 41 do 〈l,g〉 ← fresh … (f_labgen f);41 let 〈l,g〉 ≝ fresh … (f_labgen f) in 42 42 let s' ≝ s (f_entry f) in 43 OK ?(mk_internal_function g (f_reggen f)43 (mk_internal_function g (f_reggen f) 44 44 (f_result f) (f_params f) (f_locals f) 45 45 (f_stacksize f) (add ?? (f_graph f) l s') l (f_exit f)). … … 47 47 (* Generate a fresh label and use it as a dangling entry point, to be filled in 48 48 later with the loop head. *) 49 definition add_loop_label_to_graph : internal_function → resinternal_function ≝49 definition add_loop_label_to_graph : internal_function → internal_function ≝ 50 50 λf. 51 do 〈l,g〉 ← fresh … (f_labgen f);52 OK ?(mk_internal_function g (f_reggen f)51 let 〈l,g〉 ≝ fresh … (f_labgen f) in 52 (mk_internal_function g (f_reggen f) 53 53 (f_result f) (f_params f) (f_locals f) 54 54 (f_stacksize f) (f_graph f) l (f_exit f)). 55 55 56 definition fresh_reg : internal_function → typ → re s (register × internal_function)≝56 definition fresh_reg : internal_function → typ → register × internal_function ≝ 57 57 λf,ty. 58 do 〈r,g〉 ← fresh … (f_reggen f);59 OK ?〈r, mk_internal_function (f_labgen f) g58 let 〈r,g〉 ≝ fresh … (f_reggen f) in 59 〈r, mk_internal_function (f_labgen f) g 60 60 (f_result f) (f_params f) (〈r,ty〉::(f_locals f)) 61 61 (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉. … … 70 70 OK ? 〈r, f〉 71 71  _ ⇒ 72 fresh_reg f ty72 OK ? (fresh_reg f ty) 73 73 ]. 74 74 … … 88 88 match register_eq r dst with 89 89 [ inl _ ⇒ OK ? f 90  inr _ ⇒ add_fresh_to_graph (St_op1 Oid dst r) f90  inr _ ⇒ OK ? (add_fresh_to_graph (St_op1 Oid dst r) f) 91 91 ] 92  Cst _ c ⇒ add_fresh_to_graph (St_const dst c) f92  Cst _ c ⇒ OK ? (add_fresh_to_graph (St_const dst c) f) 93 93  Op1 _ _ op e' ⇒ 94 94 do 〈r,f〉 ← choose_reg env ? e' f; 95 do f ← add_fresh_to_graph (St_op1 op dst r) f;95 let f ≝ add_fresh_to_graph (St_op1 op dst r) f in 96 96 add_expr env ? e' r f 97 97  Op2 _ _ _ op e1 e2 ⇒ 98 98 do 〈r1,f〉 ← choose_reg env ? e1 f; 99 99 do 〈r2,f〉 ← choose_reg env ? e2 f; 100 do f ← add_fresh_to_graph (St_op2 op dst r1 r2) f;100 let f ≝ add_fresh_to_graph (St_op2 op dst r1 r2) f in 101 101 do f ← add_expr env ? e2 r2 f; 102 102 add_expr env ? e1 r1 f 103 103  Mem _ _ q e' ⇒ 104 104 do 〈r,f〉 ← choose_reg env ? e' f; 105 do f ← add_fresh_to_graph (St_load q r dst) f;105 let f ≝ add_fresh_to_graph (St_load q r dst) f in 106 106 add_expr env ? e' r f 107 107  Cond _ _ _ e' e1 e2 ⇒ … … 109 109 do f ← add_expr env ? e2 dst f; 110 110 let lfalse ≝ f_entry f in 111 do f ← add_fresh_to_graph (λ_.St_skip resume_at) f;111 let f ≝ add_fresh_to_graph (λ_.St_skip resume_at) f in 112 112 do f ← add_expr env ? e1 dst f; 113 113 do 〈r,f〉 ← choose_reg env ? e' f; 114 do f ← add_fresh_to_graph (λltrue. St_cond r ltrue lfalse) f;114 let f ≝ add_fresh_to_graph (λltrue. St_cond r ltrue lfalse) f in 115 115 add_expr env ? e' r f 116 116  Ecost _ l e' ⇒ 117 117 do f ← add_expr env ? e' dst f; 118 add_fresh_to_graph (St_cost l) f118 OK ? (add_fresh_to_graph (St_cost l) f) 119 119 ]. 120 120 … … 146 146 do 〈val_reg, f〉 ← choose_reg env ? e2 f; 147 147 do 〈addr_reg, f〉 ← choose_reg env ? e1 f; 148 do f ← add_fresh_to_graph (St_store q addr_reg val_reg) f;148 let f ≝ add_fresh_to_graph (St_store q addr_reg val_reg) f in 149 149 do f ← add_expr env ? e1 addr_reg f; 150 150 add_expr env ? e2 val_reg f … … 158 158 do f ← 159 159 match e with 160 [ Id _ id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f160 [ Id _ id ⇒ OK ? (add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f) 161 161  _ ⇒ 162 162 do 〈fnr, f〉 ← choose_reg env ? e f; 163 do f ← add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg) f;163 let f ≝ add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg) f in 164 164 add_expr env ? e fnr f 165 165 ]; … … 169 169 do f ← 170 170 match e with 171 [ Id _ id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f171 [ Id _ id ⇒ OK ? (add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f) 172 172  _ ⇒ 173 173 do 〈fnr, f〉 ← choose_reg env ? e f; 174 do f ← add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs) f;174 let f ≝ add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs) f in 175 175 add_expr env ? e fnr f 176 176 ]; … … 183 183 do f ← add_stmt env label_env s2 exits f; 184 184 let l2 ≝ f_entry f in 185 do f ← add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f;185 let f ≝ add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f in 186 186 do f ← add_stmt env label_env s1 exits f; 187 187 do 〈r,f〉 ← choose_reg env ? e f; 188 do f ← add_fresh_to_graph (λl1. St_cond r l1 l2) f;188 let f ≝ add_fresh_to_graph (λl1. St_cond r l1 l2) f in 189 189 add_expr env ? e r f 190 190  St_loop s ⇒ 191 do f ← add_loop_label_to_graph f;191 let f ≝ add_loop_label_to_graph f in 192 192 let l_loop ≝ f_entry f in 193 193 do f ← add_stmt env label_env s exits f; … … 197 197  St_exit n ⇒ 198 198 do l ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits); 199 add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f199 OK ? (add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f) 200 200  St_switch sz sg e tab n ⇒ 201 201 do 〈r,f〉 ← choose_reg env ? e f; 202 202 do l_default ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits); 203 do f ← add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f;203 let f ≝ add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f in 204 204 do f ← foldr ?? (λcs,f. 205 205 do f ← f; 206 206 let 〈i,n〉 ≝ cs in 207 do 〈cr,f〉 ← fresh_reg … f (ASTint sz sg);208 do 〈br,f〉 ← fresh_reg … f (ASTint I8 Unsigned);207 let 〈cr,f〉 ≝ fresh_reg … f (ASTint sz sg) in 208 let 〈br,f〉 ≝ fresh_reg … f (ASTint I8 Unsigned) in 209 209 do l_case ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits); 210 do f ← add_fresh_to_graph (St_cond br l_case) f;211 do f ← add_fresh_to_graph (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f;212 add_fresh_to_graph (St_const cr (Ointconst ? i)) f) (OK ? f) tab;210 let f ≝ add_fresh_to_graph (St_cond br l_case) f in 211 let f ≝ add_fresh_to_graph (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f in 212 OK ? (add_fresh_to_graph (St_const cr (Ointconst ? i)) f)) (OK ? f) tab; 213 213 add_expr env ? e r f 214 214  St_return opt_e ⇒ 215 do f ← add_fresh_to_graph (λ_. St_return) f;215 let f ≝ add_fresh_to_graph (λ_. St_return) f in 216 216 match opt_e with 217 217 [ None ⇒ OK ? f … … 228 228  St_goto l ⇒ 229 229 do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l); 230 add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f230 OK ? (add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f) 231 231  St_cost l s' ⇒ 232 232 do f ← add_stmt env label_env s' exits f; 233 add_fresh_to_graph (St_cost l) f233 OK ? (add_fresh_to_graph (St_cost l) f) 234 234 ]. 235 235 [ @(λ_. St_skip l_next) … … 258 258 let reggen0 ≝ new_universe RegisterTag in 259 259 let cminor_labels ≝ labels_of (f_body f) in 260 do 〈params, env1, reggen1〉 ← populate_env (empty_map …) reggen0 (f_params f); 261 do 〈locals0, env, reggen2〉 ← populate_env env1 reggen1 (f_vars f); 262 do 〈result, locals, reggen〉 ← 260 let 〈params, env1, reggen1〉 ≝ populate_env (empty_map …) reggen0 (f_params f) in 261 let 〈locals0, env, reggen2〉 ≝ populate_env env1 reggen1 (f_vars f) in 262 let 〈result, locals, reggen〉 ≝ 263 263 match f_return f with 264 [ None ⇒ OK ?〈None ?, locals0, reggen2〉264 [ None ⇒ 〈None ?, locals0, reggen2〉 265 265  Some ty ⇒ 266 do 〈r,gen〉 ← fresh … reggen2;267 OK ? 〈Some ? 〈r,ty〉, 〈r,ty〉::locals0, gen〉 ];268 do 〈label_env, labgen1〉 ← populate_label_env (empty_map …) labgen0 cminor_labels; 269 do 〈l,labgen〉 ← fresh … labgen1; 266 let 〈r,gen〉 ≝ fresh … reggen2 in 267 〈Some ? 〈r,ty〉, 〈r,ty〉::locals0, gen〉 ] in 268 let 〈label_env, labgen1〉 ≝ populate_label_env (empty_map …) labgen0 cminor_labels in 269 let 〈l,labgen〉 ≝ fresh … labgen1 in 270 270 let emptyfn ≝ 271 271 mk_internal_function … … 279 279 l 280 280 l in 281 add_stmt env label_env (f_body f) [ ] emptyfn 281 do f ← add_stmt env label_env (f_body f) [ ] emptyfn; 282 do u1 ← check_universe_ok ? (f_labgen f); 283 do u2 ← check_universe_ok ? (f_reggen f); 284 OK ? f 282 285 . 283 286
Note: See TracChangeset
for help on using the changeset viewer.