Changeset 766 for src/Cminor
 Timestamp:
 Apr 21, 2011, 7:24:04 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Cminor/toRTLabs.ma
r764 r766 1 include "utilities/lists.ma". 1 2 include "common/Globalenvs.ma". 2 3 include "Cminor/syntax.ma". … … 4 5 5 6 definition env ≝ identifier_map SymbolTag register. 7 definition label_env ≝ identifier_map SymbolTag label. 6 8 definition populate_env : env → universe RegisterTag → list ident → res (list register × env × (universe RegisterTag)) ≝ 7 9 λen,gen. foldr ?? … … 11 13 OK ? 〈r::rs, add ?? en id r, gen'〉) (OK ? 〈[ ], en, gen〉). 12 14 13 axiom boo : ∀T:Type[0]. T. 14 15 let rec c2ra_stmt (s:stmt) : graph statement ≝ 16 ?. 17 @boo qed. 18 15 definition populate_label_env : label_env → universe LabelTag → list ident → res (label_env × (universe LabelTag)) ≝ 16 λen,gen. foldr ?? 17 (λid,engen. 18 do 〈en,gen〉 ← engen; 19 do 〈r,gen'〉 ← fresh … gen; 20 OK ? 〈add ?? en id r, gen'〉) (OK ? 〈en, gen〉). 21 22 (* Add a statement to the graph, *without* updating the entry label. *) 23 definition fill_in_statement : label → statement → internal_function → internal_function ≝ 24 λl,s,f. 25 mk_internal_function (f_labgen f) (f_reggen f) (f_sig f) 26 (f_result f) (f_params f) (f_locals f) (f_ptrs f) 27 (f_stacksize f) (add ?? (f_graph f) l s) (f_entry f) (f_exit f). 28 29 (* Add a statement to the graph, making it the entry label. *) 30 definition add_to_graph : label → statement → internal_function → internal_function ≝ 31 λl,s,f. 32 mk_internal_function (f_labgen f) (f_reggen f) (f_sig f) 33 (f_result f) (f_params f) (f_locals f) (f_ptrs f) 34 (f_stacksize f) (add ?? (f_graph f) l s) l (f_exit f). 35 36 (* Add a statement with a fresh label to the start of the function. The 37 statement is parametrised by the *next* instruction's label. *) 38 definition add_fresh_to_graph : (label → statement) → internal_function → res internal_function ≝ 39 λs,f. 40 do 〈l,g〉 ← fresh … (f_labgen f); 41 let s' ≝ s (f_entry f) in 42 OK ? (mk_internal_function g (f_reggen f) (f_sig f) 43 (f_result f) (f_params f) (f_locals f) (f_ptrs f) 44 (f_stacksize f) (add ?? (f_graph f) l s') l (f_exit f)). 45 46 (* Generate a fresh label and use it as a dangling entry point, to be filled in 47 later with the loop head. *) 48 definition add_loop_label_to_graph : internal_function → res internal_function ≝ 49 λf. 50 do 〈l,g〉 ← fresh … (f_labgen f); 51 OK ? (mk_internal_function g (f_reggen f) (f_sig f) 52 (f_result f) (f_params f) (f_locals f) (f_ptrs f) 53 (f_stacksize f) (f_graph f) l (f_exit f)). 54 55 definition fresh_reg : internal_function → res (register × internal_function) ≝ 56 λf. 57 do 〈r,g〉 ← fresh … (f_reggen f); 58 OK ? 〈r, mk_internal_function (f_labgen f) g (f_sig f) 59 (f_result f) (f_params f) (r::(f_locals f)) (f_ptrs f) 60 (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉. 61 62 definition choose_reg : env → expr → internal_function → res (register × internal_function) ≝ 63 λenv,e,f. 64 match e with 65 [ Id i ⇒ 66 do r ← opt_to_res … (lookup … env i); 67 OK ? 〈r, f〉 68  _ ⇒ fresh_reg f (* FIXME: add to pointers list if necessary *) 69 ]. 70 71 definition choose_regs : env → list expr → internal_function → res (list register × internal_function) ≝ 72 λenv,es,f. 73 foldr ?? (λe,acc. do 〈rs,f〉 ← acc; 74 do 〈r,f'〉 ← choose_reg env e f; 75 OK ? 〈r::rs,f'〉) (OK ? 〈[ ], f〉) es. 76 77 let rec add_expr (env:env) (e:expr) (dst:register) (f:internal_function) on e: res internal_function ≝ 78 match e with 79 [ Id i ⇒ 80 do r ← opt_to_res … (lookup ?? env i); 81 match register_eq r dst with 82 [ inl _ ⇒ OK ? f 83  inr _ ⇒ add_fresh_to_graph (St_op1 Oid dst r) f 84 ] 85  Cst c ⇒ add_fresh_to_graph (St_const dst c) f 86  Op1 op e' ⇒ 87 do 〈r,f1〉 ← choose_reg env e' f; 88 do f' ← add_fresh_to_graph (St_op1 op dst r) f1; 89 add_expr env e' r f' 90  Op2 op e1 e2 ⇒ 91 do 〈r1,f1〉 ← choose_reg env e1 f; 92 do 〈r2,f2〉 ← choose_reg env e2 f1; 93 do f3 ← add_fresh_to_graph (St_op2 op dst r1 r2) f2; 94 do f4 ← add_expr env e1 r1 f3; 95 add_expr env e2 r2 f4 96  Mem q e' ⇒ 97 (* FIXME: inefficient  make proper use of addressing *) 98 do 〈r, f0〉 ← choose_reg env e' f; 99 do f' ← add_fresh_to_graph (St_load q (Aindexed zero) [[ r ]] dst) f0; 100 add_expr env e' r f' 101  Cond e' e1 e2 ⇒ 102 let resume_at ≝ f_entry f in 103 do f0 ← add_expr env e2 dst f; 104 let lfalse ≝ f_entry f0 in 105 do f1 ← add_fresh_to_graph (λ_.St_skip resume_at) f0; 106 do f' ← add_expr env e1 dst f1; 107 add_branch_internal env e' (f_entry f') lfalse f' (add_expr env e') 108  Ecost l e' ⇒ 109 do f' ← add_expr env e' dst f; 110 add_fresh_to_graph (St_cost l) f' 111 112 (* Ugh, the termination checker isn't smart enough to notice that calling 113 add_expr with e is OK, so we take it partially applied and define a proper 114 add_branch afterwards. *) 115 ] and add_branch_internal (env:env) (e:expr) (ltrue:label) (lfalse:label) (f:internal_function) 116 (termination_hack_add_expr : register → internal_function → res internal_function) on e : res internal_function ≝ 117 match e with 118 [ Id i ⇒ 119 do r ← opt_to_res … (lookup ?? env i); 120 add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f 121  Cst c ⇒ 122 add_fresh_to_graph (λ_. St_condcst c ltrue lfalse) f 123  Op1 op e' ⇒ 124 do 〈r,f1〉 ← choose_reg env e' f; 125 do f' ← add_fresh_to_graph (λ_. St_cond1 op r ltrue lfalse) f1; 126 add_expr env e' r f' 127  Op2 op e1 e2 ⇒ 128 do 〈r1,f1〉 ← choose_reg env e1 f; 129 do 〈r2,f2〉 ← choose_reg env e2 f1; 130 do f3 ← add_fresh_to_graph (λ_. St_cond2 op r1 r2 ltrue lfalse) f2; 131 do f4 ← add_expr env e1 r1 f3; 132 add_expr env e2 r2 f4 133  _ ⇒ 134 do 〈r,f1〉 ← choose_reg env e f; 135 do f' ← add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f1; 136 termination_hack_add_expr r f' 137 ]. 138 139 (* See add_branch_internal above. *) 140 definition add_branch ≝ 141 λenv,e,ltrue,lfalse,f. add_branch_internal env e ltrue lfalse f (add_expr env e). 142 143 let rec add_exprs (env:env) (es:list expr) (dsts:list register) (f:internal_function) on es: res internal_function ≝ 144 match es with 145 [ nil ⇒ match dsts with [ nil ⇒ OK ? f  cons _ _ ⇒ Error ? ] 146  cons e et ⇒ 147 match dsts with 148 [ nil ⇒ Error ? 149  cons r rt ⇒ 150 do f' ← add_exprs env et rt f; 151 add_expr env e r f' 152 ] 153 ]. 154 155 let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (exits:list label) (f:internal_function) on s : res internal_function ≝ 156 match s with 157 [ St_skip ⇒ OK ? f 158  St_assign x e ⇒ 159 do dst ← opt_to_res … (lookup ?? env x); 160 add_expr env e dst f 161  St_store q e1 e2 ⇒ 162 (* FIXME: inefficient  make proper use of addressing *) 163 do 〈addr_reg, f0〉 ← choose_reg env e1 f; 164 do 〈val_reg, f1〉 ← choose_reg env e2 f0; 165 do f2 ← add_fresh_to_graph (St_store q (Aindexed zero) [[ addr_reg ]] val_reg) f1; 166 do f' ← add_expr env e1 addr_reg f2; 167 add_expr env e2 val_reg f' 168  St_call return_opt_id e args sig ⇒ 169 do return_opt_reg ← 170 match return_opt_id with 171 [ None ⇒ OK ? (None ?) 172  Some id ⇒ do r ← opt_to_res … (lookup ?? env id); OK ? (Some ? r) 173 ]; 174 do 〈args_regs, f0〉 ← choose_regs env args f; 175 do f1 ← 176 match e with 177 [ Id id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg sig) f0 178  _ ⇒ 179 do 〈fnr, fe0〉 ← choose_reg env e f0; 180 do fe1 ← add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg sig) fe0; 181 add_expr env e fnr fe1 182 ]; 183 add_exprs env args args_regs f1 184  St_tailcall e args sig ⇒ 185 do 〈args_regs, f0〉 ← choose_regs env args f; 186 do f1 ← 187 match e with 188 [ Id id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs sig) f0 189  _ ⇒ 190 do 〈fnr, fe0〉 ← choose_reg env e f0; 191 do fe1 ← add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs sig) fe0; 192 add_expr env e fnr fe1 193 ]; 194 add_exprs env args args_regs f1 195  St_seq s1 s2 ⇒ 196 do f' ← add_stmt env label_env s2 exits f; 197 add_stmt env label_env s1 exits f' 198  St_ifthenelse e s1 s2 ⇒ 199 do f2 ← add_stmt env label_env s2 exits f; 200 let l2 ≝ f_entry f in 201 do f2' ← add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l2*) f2; 202 do f1 ← add_stmt env label_env s1 exits f2'; 203 add_branch env e (f_entry f1) (f_entry f2) f1 204  St_loop s ⇒ 205 do f0 ← add_loop_label_to_graph f; 206 do f' ← add_stmt env label_env s exits f0; 207 OK ? (fill_in_statement (f_entry f0) (* XXX another odd failure: St_skip (f_entry f)*)? f') 208  St_block s ⇒ 209 add_stmt env label_env s ((f_entry f)::exits) f 210  St_exit n ⇒ 211 do l ← opt_to_res … (nth_opt ? n exits); 212 add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f 213  St_switch e tab n ⇒ Error ? (* FIXME: implement *) 214  St_return opt_e ⇒ 215 match opt_e with 216 [ None ⇒ add_fresh_to_graph (λ_. St_return) f 217  Some e ⇒ 218 match f_result f with 219 [ None ⇒ Error ? 220  Some r ⇒ add_expr env e r f 221 ] 222 ] 223  St_label l s' ⇒ 224 do f' ← add_stmt env label_env s' exits f; 225 do l' ← opt_to_res … (lookup ?? label_env l); 226 OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f')*)? f') 227  St_goto l ⇒ 228 do l' ← opt_to_res … (lookup ?? label_env l); 229 add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f 230  St_cost l s' ⇒ 231 do f' ← add_stmt env label_env s' exits f; 232 add_fresh_to_graph (St_cost l) f' 233  _ ⇒ Error ? (* XXX implement *) 234 ]. 235 [ @(λ_. St_skip l2) 236  @(St_skip (f_entry f)) 237  @(λ_. St_skip l) 238  @(St_skip (f_entry f')) 239  @(λ_.St_skip l') 240 ] qed. 241 242 (* Get labels from a Cminor statement. *) 243 let rec labels_of (s:stmt) : list ident ≝ 244 match s with 245 [ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2) 246  St_ifthenelse _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2) 247  St_loop s ⇒ labels_of s 248  St_block s ⇒ labels_of s 249  St_label l s ⇒ l::(labels_of s) 250  St_cost _ s ⇒ labels_of s 251  _ ⇒ [ ] 252 ]. 19 253 20 254 definition c2ra_function (*: internal_function → internal_function*) ≝ 21 255 λf. 22 let labgen ≝ new_universe LabelTag in256 let labgen0 ≝ new_universe LabelTag in 23 257 let reggen0 ≝ new_universe RegisterTag in 258 let cminor_labels ≝ labels_of (f_body f) in 24 259 do 〈params, env1, reggen1〉 ← populate_env (empty_map …) reggen0 (f_params f); 25 do 〈locals, env2, reggen2〉 ← populate_env env1 reggen1 (f_vars f); 26 do ptrs ← mmap ?? (λid. opt_to_res … (lookup ?? env2 id)) (f_ptrs f); 27 OK ? (mk_internal_function 260 do 〈locals0, env, reggen2〉 ← populate_env env1 reggen1 (f_vars f); 261 do 〈result, locals, reggen〉 ← 262 match sig_res (f_sig f) with 263 [ None ⇒ OK ? 〈None ?, locals0, reggen2〉 264  Some _ ⇒ 265 do 〈r,gen〉 ← fresh … reggen2; 266 OK ? 〈Some ? r, r::locals0, gen〉 ]; 267 do ptrs ← mmap ?? (λid. opt_to_res … (lookup ?? env id)) (f_ptrs f); 268 do 〈label_env, labgen1〉 ← populate_label_env (empty_map …) labgen0 cminor_labels; 269 do 〈l,labgen〉 ← fresh … labgen1; 270 let emptyfn ≝ 271 mk_internal_function 28 272 labgen 29 reggen 1273 reggen 30 274 (f_sig f) 31 ?275 result 32 276 params 33 277 locals 34 278 ptrs 35 279 (f_stacksize f) 36 (c2ra_stmt (f_body f)) 37 ? 38 ?) 39 . @boo qed. 280 (add ?? (empty_map …) l St_return) 281 l 282 l in 283 add_stmt env label_env (f_body f) [ ] emptyfn 284 . 40 285 41 286 definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝ 42 287 transform_partial_program ??? 43 288 (transf_partial_fundef ?? c2ra_function). 289 290 include "Cminor/initialisation.ma". 291 292 definition cminor_init_to_rtlabs : Cminor_program → res RTLabs_program ≝ 293 λp. let p' ≝ replace_init p in cminor_to_rtlabs p.
Note: See TracChangeset
for help on using the changeset viewer.