- Timestamp:
- Apr 28, 2011, 10:55:49 AM (10 years ago)
- Location:
- src
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Cminor/toRTLabs.ma
r772 r780 60 60 (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉. 61 61 62 definition choose_reg : env → expr → internal_function → res (register × internal_function) ≝ 63 λenv,e,f. 62 definition fresh_ptr_reg : internal_function → res (register × internal_function) ≝ 63 λf. 64 do 〈r,g〉 ← fresh … (f_reggen f); 65 OK ? 〈r, mk_internal_function (f_labgen f) g (f_sig f) 66 (f_result f) (f_params f) (r::(f_locals f)) (r::(f_ptrs f)) 67 (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉. 68 69 let rec expr_yields_pointer (e:expr) (ptrs:list ident) : bool ≝ 70 match e with 71 [ Id i ⇒ exists ? (eq_identifier ? i) ptrs 72 | Cst c ⇒ match c with [ Oaddrsymbol _ _ ⇒ true | Oaddrstack _ ⇒ true | _ ⇒ false ] 73 | Op1 op e' ⇒ 74 match op with 75 [ Oid ⇒ expr_yields_pointer e' ptrs 76 | Optrofint _ ⇒ true 77 | _ ⇒ false 78 ] 79 | Op2 op e1 e2 ⇒ 80 match op with 81 [ Oaddp ⇒ true 82 | Osubpi ⇒ true 83 | _ ⇒ false 84 ] 85 | Mem q e' ⇒ 86 match q with 87 [ Mpointer _ ⇒ true 88 | _ ⇒ false 89 ] 90 (* Both branches ought to be the same? *) 91 | Cond e' e1 e2 ⇒ (expr_yields_pointer e1 ptrs) ∨ (expr_yields_pointer e2 ptrs) 92 | Ecost _ e' ⇒ expr_yields_pointer e' ptrs 93 ]. 94 95 definition choose_reg : env → expr → list ident → internal_function → res (register × internal_function) ≝ 96 λenv,e,ptrs,f. 64 97 match e with 65 98 [ Id i ⇒ 66 99 do r ← opt_to_res … (lookup … env i); 67 100 OK ? 〈r, f〉 68 | _ ⇒ fresh_reg f (* FIXME: add to pointers list if necessary *) 101 | _ ⇒ 102 if expr_yields_pointer e ptrs then fresh_ptr_reg f else fresh_reg f 69 103 ]. 70 104 71 definition choose_regs : env → list expr → internal_function → res (list register × internal_function) ≝72 λenv,es, f.105 definition choose_regs : env → list expr → list ident → internal_function → res (list register × internal_function) ≝ 106 λenv,es,ptrs,f. 73 107 foldr ?? (λe,acc. do 〈rs,f〉 ← acc; 74 do 〈r,f'〉 ← choose_reg env e f;108 do 〈r,f'〉 ← choose_reg env e ptrs f; 75 109 OK ? 〈r::rs,f'〉) (OK ? 〈[ ], f〉) es. 76 110 77 let rec add_expr (env:env) (e:expr) (dst:register) ( f:internal_function) on e: res internal_function ≝111 let rec add_expr (env:env) (e:expr) (dst:register) (ptrs:list ident) (f:internal_function) on e: res internal_function ≝ 78 112 match e with 79 113 [ Id i ⇒ … … 85 119 | Cst c ⇒ add_fresh_to_graph (St_const dst c) f 86 120 | Op1 op e' ⇒ 87 do 〈r,f〉 ← choose_reg env e' f;121 do 〈r,f〉 ← choose_reg env e' ptrs f; 88 122 do f ← add_fresh_to_graph (St_op1 op dst r) f; 89 add_expr env e' r f123 add_expr env e' r ptrs f 90 124 | Op2 op e1 e2 ⇒ 91 do 〈r1,f〉 ← choose_reg env e1 f;92 do 〈r2,f〉 ← choose_reg env e2 f;125 do 〈r1,f〉 ← choose_reg env e1 ptrs f; 126 do 〈r2,f〉 ← choose_reg env e2 ptrs f; 93 127 do f ← add_fresh_to_graph (St_op2 op dst r1 r2) f; 94 do f ← add_expr env e2 r2 f;95 add_expr env e1 r1 f128 do f ← add_expr env e2 r2 ptrs f; 129 add_expr env e1 r1 ptrs f 96 130 | Mem q e' ⇒ 97 add_with_addressing_internal env e' (λm,rs. St_load q m rs dst) f (add_expr env e')131 add_with_addressing_internal env e' (λm,rs. St_load q m rs dst) ptrs f (add_expr env e') 98 132 | Cond e' e1 e2 ⇒ 99 133 let resume_at ≝ f_entry f in 100 do f ← add_expr env e2 dst f;134 do f ← add_expr env e2 dst ptrs f; 101 135 let lfalse ≝ f_entry f in 102 136 do f ← add_fresh_to_graph (λ_.St_skip resume_at) f; 103 do f ← add_expr env e1 dst f;104 add_branch_internal env e' (f_entry f) lfalse f (add_expr env e')137 do f ← add_expr env e1 dst ptrs f; 138 add_branch_internal env e' (f_entry f) lfalse ptrs f (add_expr env e') 105 139 | Ecost l e' ⇒ 106 do f ← add_expr env e' dst f;140 do f ← add_expr env e' dst ptrs f; 107 141 add_fresh_to_graph (St_cost l) f 108 142 … … 113 147 and add_with_addressing_internal (env:env) (e:expr) 114 148 (s:∀m:addressing. addr m → label → statement) 149 (ptrs:list ident) 115 150 (f:internal_function) 116 (termination_hack:register → internal_function → res internal_function)151 (termination_hack:register → list ident → internal_function → res internal_function) 117 152 on e : res internal_function ≝ 118 153 let add_default : unit → res internal_function ≝ λ_. 119 do 〈r, f〉 ← choose_reg env e f;154 do 〈r, f〉 ← choose_reg env e ptrs f; 120 155 do f ← add_fresh_to_graph (s (Aindexed zero) [[ r ]]) f; 121 termination_hack r f156 termination_hack r ptrs f 122 157 in 123 158 match e with … … 132 167 [ Oaddp ⇒ 133 168 let add_generic_addp : unit → res internal_function ≝ λ_. 134 do 〈r1, f〉 ← choose_reg env e1 f;135 do 〈r2, f〉 ← choose_reg env e2 f;169 do 〈r1, f〉 ← choose_reg env e1 ptrs f; 170 do 〈r2, f〉 ← choose_reg env e2 ptrs f; 136 171 do f ← add_fresh_to_graph (s Aindexed2 [[ r1 ; r2 ]]) f; 137 do f ← add_expr env e2 r2 f;138 add_expr env e1 r1 f172 do f ← add_expr env e2 r2 ptrs f; 173 add_expr env e1 r1 ptrs f 139 174 in 140 175 match e1 with … … 142 177 match c with 143 178 [ Oaddrsymbol id i ⇒ 144 do 〈r, f〉 ← choose_reg env e f;179 do 〈r, f〉 ← choose_reg env e ptrs f; 145 180 do f ← add_fresh_to_graph (s (Abased id i) [[ r ]]) f; 146 add_expr env e2 r f181 add_expr env e2 r ptrs f 147 182 | _ ⇒ add_generic_addp it 148 183 ] … … 154 189 ] 155 190 (* and again *) 156 and add_branch_internal (env:env) (e:expr) (ltrue:label) (lfalse:label) ( f:internal_function)157 (termination_hack_add_expr : register → internal_function → res internal_function) on e : res internal_function ≝191 and add_branch_internal (env:env) (e:expr) (ltrue:label) (lfalse:label) (ptrs:list ident) (f:internal_function) 192 (termination_hack_add_expr : register → list ident → internal_function → res internal_function) on e : res internal_function ≝ 158 193 match e with 159 194 [ Id i ⇒ … … 163 198 add_fresh_to_graph (λ_. St_condcst c ltrue lfalse) f 164 199 | Op1 op e' ⇒ 165 do 〈r,f〉 ← choose_reg env e' f;200 do 〈r,f〉 ← choose_reg env e' ptrs f; 166 201 do f ← add_fresh_to_graph (λ_. St_cond1 op r ltrue lfalse) f; 167 add_expr env e' r f202 add_expr env e' r ptrs f 168 203 | Op2 op e1 e2 ⇒ 169 do 〈r1,f〉 ← choose_reg env e1 f;170 do 〈r2,f〉 ← choose_reg env e2 f;204 do 〈r1,f〉 ← choose_reg env e1 ptrs f; 205 do 〈r2,f〉 ← choose_reg env e2 ptrs f; 171 206 do f ← add_fresh_to_graph (λ_. St_cond2 op r1 r2 ltrue lfalse) f; 172 do f ← add_expr env e2 r2 f;173 add_expr env e1 r1 f207 do f ← add_expr env e2 r2 ptrs f; 208 add_expr env e1 r1 ptrs f 174 209 | _ ⇒ 175 do 〈r,f〉 ← choose_reg env e f;210 do 〈r,f〉 ← choose_reg env e ptrs f; 176 211 do f ← add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f; 177 termination_hack_add_expr r f212 termination_hack_add_expr r ptrs f 178 213 ]. 179 214 180 215 (* See comment above. *) 181 216 definition add_with_addressing ≝ 182 λenv,e,s, f. add_with_addressing_internal env es f (add_expr env e).217 λenv,e,s,ptrs,f. add_with_addressing_internal env e s ptrs f (add_expr env e). 183 218 definition add_branch ≝ 184 λenv,e,ltrue,lfalse, f. add_branch_internal env e ltrue lfalsef (add_expr env e).185 186 let rec add_exprs (env:env) (es:list expr) (dsts:list register) ( f:internal_function) on es: res internal_function ≝219 λenv,e,ltrue,lfalse,ptrs,f. add_branch_internal env e ltrue lfalse ptrs f (add_expr env e). 220 221 let rec add_exprs (env:env) (es:list expr) (dsts:list register) (ptrs:list ident) (f:internal_function) on es: res internal_function ≝ 187 222 match es with 188 223 [ nil ⇒ match dsts with [ nil ⇒ OK ? f | cons _ _ ⇒ Error ? ] … … 191 226 [ nil ⇒ Error ? 192 227 | cons r rt ⇒ 193 do f ← add_exprs env et rt f;194 add_expr env e r f195 ] 196 ]. 197 198 let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (exits:list label) ( f:internal_function) on s : res internal_function ≝228 do f ← add_exprs env et rt ptrs f; 229 add_expr env e r ptrs f 230 ] 231 ]. 232 233 let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (exits:list label) (ptrs:list ident) (f:internal_function) on s : res internal_function ≝ 199 234 match s with 200 235 [ St_skip ⇒ OK ? f 201 236 | St_assign x e ⇒ 202 237 do dst ← opt_to_res … (lookup ?? env x); 203 add_expr env e dst f238 add_expr env e dst ptrs f 204 239 | St_store q e1 e2 ⇒ 205 do 〈val_reg, f〉 ← choose_reg env e2 f;206 do f ← add_with_addressing env e1 (λm,rs. St_store q m rs val_reg) f;207 add_expr env e2 val_reg f240 do 〈val_reg, f〉 ← choose_reg env e2 ptrs f; 241 do f ← add_with_addressing env e1 (λm,rs. St_store q m rs val_reg) ptrs f; 242 add_expr env e2 val_reg ptrs f 208 243 | St_call return_opt_id e args sig ⇒ 209 244 do return_opt_reg ← … … 212 247 | Some id ⇒ do r ← opt_to_res … (lookup ?? env id); OK ? (Some ? r) 213 248 ]; 214 do 〈args_regs, f〉 ← choose_regs env args f;249 do 〈args_regs, f〉 ← choose_regs env args ptrs f; 215 250 do f ← 216 251 match e with 217 252 [ Id id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg sig) f 218 253 | _ ⇒ 219 do 〈fnr, f〉 ← choose_reg env e f;254 do 〈fnr, f〉 ← choose_reg env e ptrs f; 220 255 do f ← add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg sig) f; 221 add_expr env e fnr f256 add_expr env e fnr ptrs f 222 257 ]; 223 add_exprs env args args_regs f258 add_exprs env args args_regs ptrs f 224 259 | St_tailcall e args sig ⇒ 225 do 〈args_regs, f〉 ← choose_regs env args f;260 do 〈args_regs, f〉 ← choose_regs env args ptrs f; 226 261 do f ← 227 262 match e with 228 263 [ Id id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs sig) f 229 264 | _ ⇒ 230 do 〈fnr, f〉 ← choose_reg env e f;265 do 〈fnr, f〉 ← choose_reg env e ptrs f; 231 266 do f ← add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs sig) f; 232 add_expr env e fnr f267 add_expr env e fnr ptrs f 233 268 ]; 234 add_exprs env args args_regs f269 add_exprs env args args_regs ptrs f 235 270 | St_seq s1 s2 ⇒ 236 do f ← add_stmt env label_env s2 exits f;237 add_stmt env label_env s1 exits f271 do f ← add_stmt env label_env s2 exits ptrs f; 272 add_stmt env label_env s1 exits ptrs f 238 273 | St_ifthenelse e s1 s2 ⇒ 239 274 let l_next ≝ f_entry f in 240 do f ← add_stmt env label_env s2 exits f;275 do f ← add_stmt env label_env s2 exits ptrs f; 241 276 let l2 ≝ f_entry f in 242 277 do f ← add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f; 243 do f ← add_stmt env label_env s1 exits f;244 add_branch env e (f_entry f) l2 f278 do f ← add_stmt env label_env s1 exits ptrs f; 279 add_branch env e (f_entry f) l2 ptrs f 245 280 | St_loop s ⇒ 246 281 do f ← add_loop_label_to_graph f; 247 282 let l_loop ≝ f_entry f in 248 do f ← add_stmt env label_env s exits f;283 do f ← add_stmt env label_env s exits ptrs f; 249 284 OK ? (fill_in_statement l_loop (* XXX another odd failure: St_skip (f_entry f)*)? f) 250 285 | St_block s ⇒ 251 add_stmt env label_env s ((f_entry f)::exits) f286 add_stmt env label_env s ((f_entry f)::exits) ptrs f 252 287 | St_exit n ⇒ 253 288 do l ← opt_to_res … (nth_opt ? n exits); 254 289 add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f 255 290 | St_switch e tab n ⇒ 256 do 〈r,f〉 ← choose_reg env e f;291 do 〈r,f〉 ← choose_reg env e ptrs f; 257 292 do l_default ← opt_to_res … (nth_opt ? n exits); 258 293 do f ← add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f; … … 264 299 do f ← add_fresh_to_graph (St_cond2 (Ocmpu Ceq) (* signed? *) r cr l_case) f; 265 300 add_fresh_to_graph (St_const cr (Ointconst i)) f) (OK ? f) tab; 266 add_expr env e r f301 add_expr env e r ptrs f 267 302 | St_return opt_e ⇒ 268 303 do f ← add_fresh_to_graph (λ_. St_return) f; … … 272 307 match f_result f with 273 308 [ None ⇒ Error ? 274 | Some r ⇒ add_expr env e r f309 | Some r ⇒ add_expr env e r ptrs f 275 310 ] 276 311 ] 277 312 | St_label l s' ⇒ 278 do f ← add_stmt env label_env s' exits f;313 do f ← add_stmt env label_env s' exits ptrs f; 279 314 do l' ← opt_to_res … (lookup ?? label_env l); 280 315 OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f)*)? f) … … 283 318 add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f 284 319 | St_cost l s' ⇒ 285 do f ← add_stmt env label_env s' exits f;320 do f ← add_stmt env label_env s' exits ptrs f; 286 321 add_fresh_to_graph (St_cost l) f 287 322 | _ ⇒ Error ? (* XXX implement *) … … 336 371 l 337 372 l in 338 add_stmt env label_env (f_body f) [ ] emptyfn373 add_stmt env label_env (f_body f) [ ] (f_ptrs f) emptyfn 339 374 . 340 375 -
src/utilities/lists.ma
r766 r780 6 6 | cons h t ⇒ match n with [ O ⇒ Some ? h | S m ⇒ nth_opt A m t ] 7 7 ]. 8 9 let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝ 10 match l with 11 [ nil ⇒ false 12 | cons h t ⇒ orb (p h) (exists A p t) 13 ].
Note: See TracChangeset
for help on using the changeset viewer.