Changeset 1101
 Timestamp:
 Aug 3, 2011, 5:18:17 PM (10 years ago)
 Location:
 Deliverables/D3.3/idlookupbranch/Cminor
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.3/idlookupbranch/Cminor/initialisation.ma
r1087 r1101 19 19 ]. 20 20 21 (* None of the additional code introduces locals or labels. *) 22 definition stmt_inv : stmt → Prop ≝ 23 stmt_P (λs. stmt_vars (λ_.False) s ∧ stmt_labels (λ_.False) s). 24 21 25 (* Produces a few extra skips  hopefully the compiler will optimise these 22 26 away. *) 23 27 24 definition init_datum : ident → region → init_data → nat (*offset*) → Σs:stmt. stmt_ vars s (λ_.False)≝28 definition init_datum : ident → region → init_data → nat (*offset*) → Σs:stmt. stmt_inv s ≝ 25 29 λid,r,init,off. 26 30 match init_expr init with … … 31 35 ] 32 36 ]. 33 //37 % // 34 38 cases init in p; [ 8: #a #b ] #c #p normalize in p; destruct; /2/ 35 39 qed. … … 44 48 qed. 45 49 46 lemma sig_stmt_ vars : ∀P:ident → Prop. ∀s:Σs:stmt.stmt_vars s P.47 stmt_ vars s P.48 #P * #s #p whd in ⊢ (?%?) // 50 lemma sig_stmt_inv : ∀s:Σs:stmt.stmt_inv s. 51 stmt_inv s. 52 * #s #p @p 49 53 qed. 50 54 51 definition init_var : ident → region → list init_data → Σs:stmt. stmt_ vars s (λ_.False)≝55 definition init_var : ident → region → list init_data → Σs:stmt. stmt_inv s ≝ 52 56 λid,r,init. 53 57 \snd (foldr ?? … … 55 59 let 〈off,s〉 ≝ os in 56 60 〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉) 57 〈0, dp ? (λx.stmt_vars x (λ_.False)) St_skip ?〉 init). 58 [ whd // 59  elim init whd // 60 #h #t #IH whd in ⊢ (?(???%)?) @sndredex whd % [ @sig_stmt_vars  @IH ] 61 〈0, dp ? (λx.stmt_inv x) St_skip ?〉 init). 62 [ % // 63  elim init 64 [ % // 65  #h #t #IH whd in ⊢ (?(???%)) @sndredex % [ % [ % //  @sig_stmt_inv ]  @IH ] 61 66 ] qed. 62 67 63 definition init_vars : list (ident × (list init_data) × region × unit) → Σs:stmt. stmt_ vars s (λ_.False)≝64 λvars. foldr ? (Σs:stmt. stmt_ vars s (λ_.False))65 (λvar,s. dp ? (λx.stmt_ vars x (λ_.False)) (St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst var)) (\snd (\fst (\fst var))))) ?) (dp ? (λx.stmt_vars x (λ_.False)) St_skip I) vars.66 whd % @sig_stmt_vars 68 definition init_vars : list (ident × (list init_data) × region × unit) → Σs:stmt. stmt_inv s ≝ 69 λvars. foldr ? (Σs:stmt. stmt_inv s) 70 (λvar,s. dp ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst var)) (\snd (\fst (\fst var))))) ?) (dp ? (λx.stmt_inv x ) St_skip (conj ?? I I)) vars. 71 % [ % [ % //  @sig_stmt_inv ]  @sig_stmt_inv ] 67 72 qed. 68 73 69 definition add_statement : ident → (Σs:stmt. stmt_vars s (λ_.False)) → 74 lemma no_labels : ∀s. stmt_inv s → labels_of s = [ ]. 75 #s elim s // 76 [ #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?) 77 >(IH1 H1) >(IH2 H2) @refl 78  #sz #sg #e #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?) 79 >(IH1 H1) >(IH2 H2) @refl 80  #s #IH * * #_ #_ #H @(IH H) 81  #s #IH * * #_ #_ #H @(IH H) 82  #l #s #IH * * #_ * 83  #l #s #IH * * #_ #_ #H @(IH H) 84 ] qed. 85 86 definition add_statement : ident → (Σs:stmt. stmt_inv s) → 70 87 list (ident × (fundef internal_function)) → 71 88 list (ident × (fundef internal_function)) ≝ … … 87 104 ] 88 105  inr _ ⇒ 〈id',f'〉 ]) ]. 89 whd % 90 [ @(stmt_vars_mp … H) #i * 91  // 106 % 107 [ % [ % //  108 @(stmt_P_mp … H) #s * #V #L % 109 [ @(stmt_vars_mp … V) #i * 110  @(stmt_labels_mp … L) #l * 111 ] 112 ] 113  whd in ⊢ (?(λ_.??(?(λ_.???%)?))?) >(no_labels … H) @(f_inv f) 92 114 ] qed. 93 115 
Deliverables/D3.3/idlookupbranch/Cminor/toRTLabs.ma
r1095 r1101 5 5 6 6 definition env ≝ identifier_map SymbolTag register. 7 definition label_env ≝ identifier_map SymbolTaglabel.7 definition label_env ≝ identifier_map Label label. 8 8 definition populate_env : env → universe RegisterTag → list (ident × typ) → list (register×typ) × env × (universe RegisterTag) ≝ 9 9 λen,gen. foldr ?? … … 52 52 #i #H @lookup_add_oblivious @(IH … E0) @H 53 53 ] qed. 54 55 definition populate_label_env : label_env → universe LabelTag → list ident→ label_env × (universe LabelTag) ≝54 55 definition populate_label_env : label_env → universe LabelTag → list (identifier Label) → label_env × (universe LabelTag) ≝ 56 56 λen,gen. foldr ?? 57 57 (λid,engen. … … 60 60 〈add ?? en id r, gen'〉) 〈en, gen〉. 61 61 62 lemma populates_label_env : ∀ls,lbls,u,lbls',u'. 63 populate_label_env lbls u ls = 〈lbls',u'〉 → 64 ∀l. Exists ? (λl'.l' = l) ls → present ?? lbls' l. 65 #ls elim ls 66 [ #lbls #u #lbls' #u' #E #l * 67  #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?) 68 change in ⊢ (??match % with [ _ ⇒ ? ]? → ?) with (populate_label_env ???) 69 lapply (refl ? (populate_label_env lbls u t)) 70 cases (populate_label_env lbls u t) in ⊢ (???% → %) 71 #lbls1 #u1 #E1 whd in ⊢ (??%? → ?) cases (fresh ? u1) #r #gen' whd in ⊢ (??%? → ?) 72 #E >(?:lbls' = add ?? lbls1 h r) [ 2: destruct (E) @refl ] 73 #l * 74 [ #El <El whd >lookup_add_hit % #Er destruct 75  #H @lookup_add_oblivious @(IH … E1 ? H) 76 ] 77 ] qed. 78 62 79 lemma lookup_sigma : ∀tag,A,m. ∀i:(Σl:identifier tag. lookup tag A m l ≠ None ?). 63 80 lookup tag A m i ≠ None ?. … … 66 83 67 84 definition lookup' : ∀e:env. ∀id. present ?? e id → register ≝ 85 λe,id. match lookup ?? e id return λx. x ≠ None ? → ? with [ Some r ⇒ λ_. r  None ⇒ λH.⊥ ]. 86 cases H #H' cases (H' (refl ??)) qed. 87 88 definition lookup_label : ∀e:label_env. ∀id. present ?? e id → label ≝ 68 89 λe,id. match lookup ?? e id return λx. x ≠ None ? → ? with [ Some r ⇒ λ_. r  None ⇒ λH.⊥ ]. 69 90 cases H #H' cases (H' (refl ??)) qed. … … 219 240 λ${ident E}.$s ] (refl ? $t) }. 220 241 221 let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_vars s (present ?? env)) (exits:list label) (f:internal_function) on s : res internal_function ≝ 222 match s return λs.stmt_vars s (present ?? env) → res internal_function with 242 definition stmt_inv : env → label_env → stmt → Prop ≝ 243 λenv,lenv. stmt_P (λs. stmt_vars (present ?? env) s ∧ stmt_labels (present ?? lenv) s). 244 245 notation "π1" with precedence 10 for @{ (proj1 ??) }. 246 notation "π2" with precedence 10 for @{ (proj2 ??) }. 247 248 let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (exits:list label) (f:internal_function) on s : res internal_function ≝ 249 match s return λs.stmt_inv env label_env s → res internal_function with 223 250 [ St_skip ⇒ λ_. OK ? f 224 251  St_assign _ x e ⇒ λEnv. 225 let dst ≝ lookup' env x ( proj1 … Env) in226 OK ? (add_expr env ? e ( proj2 … Env) dst f)252 let dst ≝ lookup' env x (π1 (π1 Env)) in 253 OK ? (add_expr env ? e (π2 (π1 Env)) dst f) 227 254  St_store _ _ q e1 e2 ⇒ λEnv. 228 let 〈val_reg, f〉 ≝ choose_reg env ? e2 f ( proj2 … Env) in229 let 〈addr_reg, f〉 ≝ choose_reg env ? e1 f ( proj1 … Env) in255 let 〈val_reg, f〉 ≝ choose_reg env ? e2 f (π2 (π1 Env)) in 256 let 〈addr_reg, f〉 ≝ choose_reg env ? e1 f (π1 (π1 Env)) in 230 257 let f ≝ add_fresh_to_graph (St_store q addr_reg val_reg) f in 231 let f ≝ add_expr env ? e1 ( proj1 … Env) addr_reg f in232 OK ? (add_expr env ? e2 ( proj2 … Env) val_reg f)258 let f ≝ add_expr env ? e1 (π1 (π1 Env)) addr_reg f in 259 OK ? (add_expr env ? e2 (π2 (π1 Env)) val_reg f) 233 260  St_call return_opt_id e args ⇒ λEnv. 234 261 let return_opt_reg ≝ … … 237 264  Some id ⇒ λEnv. Some ? (lookup' env id ?) 238 265 ] Env in 239 let 〈args_regs, f〉 as Eregs ≝ choose_regs env args f ( proj2 … Env) in266 let 〈args_regs, f〉 as Eregs ≝ choose_regs env args f (π2 (π1 Env)) in 240 267 let f ≝ 241 268 match e with 242 269 [ Id _ id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f 243 270  _ ⇒ 244 let 〈fnr, f〉 ≝ choose_reg env ? e f ( proj2 … (proj1 … Env)) in271 let 〈fnr, f〉 ≝ choose_reg env ? e f (π2 (π1 (π1 Env))) in 245 272 let f ≝ add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg) f in 246 add_expr env ? e ( proj2 … (proj1 … Env)) fnr f273 add_expr env ? e (π2 (π1 (π1 Env))) fnr f 247 274 ] in 248 OK ? (add_exprs env args ( proj2 … Env) args_regs ? f)275 OK ? (add_exprs env args (π2 (π1 Env)) args_regs ? f) 249 276  St_tailcall e args ⇒ λEnv. 250 let 〈args_regs, f〉 as Eregs ≝ choose_regs env args f ( proj2 … Env) in277 let 〈args_regs, f〉 as Eregs ≝ choose_regs env args f (π2 (π1 Env)) in 251 278 let f ≝ 252 279 match e with 253 280 [ Id _ id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f 254 281  _ ⇒ 255 let 〈fnr, f〉 ≝ choose_reg env ? e f ( proj1 … Env) in282 let 〈fnr, f〉 ≝ choose_reg env ? e f (π1 (π1 Env)) in 256 283 let f ≝ add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs) f in 257 add_expr env ? e ( proj1 … Env) fnr f284 add_expr env ? e (π1 (π1 Env)) fnr f 258 285 ] in 259 OK ? (add_exprs env args ( proj2 … Env) args_regs ? f)286 OK ? (add_exprs env args (π2 (π1 Env)) args_regs ? f) 260 287  St_seq s1 s2 ⇒ λEnv. 261 do f ← add_stmt env label_env s2 (proj2 … Env)exits f;262 add_stmt env label_env s1 (proj1 … Env)exits f288 do f ← add_stmt env label_env s2 ? exits f; 289 add_stmt env label_env s1 ? exits f 263 290  St_ifthenelse _ _ e s1 s2 ⇒ λEnv. 264 291 let l_next ≝ f_entry f in 265 do f ← add_stmt env label_env s2 ( proj2 …Env) exits f;292 do f ← add_stmt env label_env s2 (π2 Env) exits f; 266 293 let l2 ≝ f_entry f in 267 294 let f ≝ add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f in 268 do f ← add_stmt env label_env s1 ( proj2 … (proj1 …Env)) exits f;269 let 〈r,f〉 ≝ choose_reg env ? e f ( proj1 … (proj1 … Env)) in295 do f ← add_stmt env label_env s1 (π2 (π1 Env)) exits f; 296 let 〈r,f〉 ≝ choose_reg env ? e f (π1 (π1 (π1 Env))) in 270 297 let f ≝ add_fresh_to_graph (λl1. St_cond r l1 l2) f in 271 OK ? (add_expr env ? e ( proj1 … (proj1 … Env)) r f)298 OK ? (add_expr env ? e (π1 (π1 (π1 Env))) r f) 272 299  St_loop s ⇒ λEnv. 273 300 let f ≝ add_fresh_to_graph ? f in (* dummy statement, fill in afterwards *) 274 301 let l_loop ≝ f_entry f in 275 do f ← add_stmt env label_env s Envexits f;302 do f ← add_stmt env label_env s (π2 Env) exits f; 276 303 OK ? (fill_in_statement l_loop (* XXX another odd failure: St_skip (f_entry f)*)? f) 277 304  St_block s ⇒ λEnv. 278 add_stmt env label_env s Env((f_entry f)::exits) f305 add_stmt env label_env s (π2 Env) ((f_entry f)::exits) f 279 306  St_exit n ⇒ λEnv. 280 307 do l ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits); 281 308 OK ? (add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f) 282 309  St_switch sz sg e tab n ⇒ λEnv. 283 let 〈r,f〉 ≝ choose_reg env ? e f Envin310 let 〈r,f〉 ≝ choose_reg env ? e f ? in 284 311 do l_default ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits); 285 312 let f ≝ add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f in … … 293 320 let f ≝ add_fresh_to_graph (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f in 294 321 OK ? (add_fresh_to_graph (St_const cr (Ointconst ? i)) f)) (OK ? f) tab; 295 OK ? (add_expr env ? e Envr f)322 OK ? (add_expr env ? e (π1 Env) r f) 296 323  St_return opt_e ⇒ 297 324 let f ≝ add_fresh_to_graph (λ_. St_return) f in … … 305 332 ] 306 333  St_label l s' ⇒ λEnv. 307 do f ← add_stmt env label_env s' Envexits f;308 do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l);334 do f ← add_stmt env label_env s' (π2 Env) exits f; 335 let l' ≝ lookup_label label_env l ? in 309 336 OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f)*)? f) 310 337  St_goto l ⇒ λEnv. 311 do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l);338 let l' ≝ lookup_label label_env l ? in 312 339 OK ? (add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f) 313 340  St_cost l s' ⇒ λEnv. 314 do f ← add_stmt env label_env s' Envexits f;341 do f ← add_stmt env label_env s' (π2 Env) exits f; 315 342 OK ? (add_fresh_to_graph (St_cost l) f) 316 343 ] Env. 344 try @(π1 Env) 345 try @(π2 Env) 346 try @(π1 (π1 Env)) 347 try @(π2 (π1 Env)) 317 348 [ f @(choose_regs_length … (sym_eq … Eregs)) 318  whd in Env @( proj1 … (proj1 … Env))349  whd in Env @(π1 (π1 (π1 Env))) 319 350  f @(choose_regs_length … (sym_eq … Eregs)) 320 351  @(λ_. St_skip l_next) … … 323 354  @(λ_. St_skip l) 324 355  @(λ_. St_skip l_default) 325  whd in Env @Env326 356  @(St_skip (f_entry f)) 327 357  @(λ_.St_skip l') 328 358 ] qed. 329 330 (* Get labels from a Cminor statement. *)331 let rec labels_of (s:stmt) : list ident ≝332 match s with333 [ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2)334  St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2)335  St_loop s ⇒ labels_of s336  St_block s ⇒ labels_of s337  St_label l s ⇒ l::(labels_of s)338  St_cost _ s ⇒ labels_of s339  _ ⇒ [ ]340 ].341 359 342 360 notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)" … … 360 378 let 〈r,gen〉 ≝ fresh … reggen2 in 361 379 〈Some ? 〈r,ty〉, 〈r,ty〉::locals0, gen〉 ] in 362 let 〈label_env, labgen1〉 ≝ populate_label_env (empty_map …) labgen0 cminor_labels in380 let 〈label_env, labgen1〉 as El ≝ populate_label_env (empty_map …) labgen0 cminor_labels in 363 381 let 〈l,labgen〉 ≝ fresh … labgen1 in 364 382 let emptyfn ≝ … … 378 396 OK ? f 379 397 . 380 [ @(stmt_vars_mp … (f_bound f)) 381 #i #H cases (Exists_append … H) 382 [ #H1 @(populate_extends ?????? (sym_eq … E2)) 383 @(populates_env … (sym_eq … E1)) @H1 384  #H1 @(populates_env … (sym_eq … E2)) @H1 398 [ @(stmt_P_mp … (f_inv f)) 399 #s * #V #L % 400 [ @(stmt_vars_mp … V) 401 #i #H cases (Exists_append … H) 402 [ #H1 @(populate_extends ?????? (sym_eq … E2)) 403 @(populates_env … (sym_eq … E1)) @H1 404  #H1 @(populates_env … (sym_eq … E2)) @H1 405 ] 406  @(stmt_labels_mp … L) 407 #l #H @(populates_label_env … (sym_eq … El)) @H 385 408 ] 386 409  *: >lookup_add_hit % #E destruct
Note: See TracChangeset
for help on using the changeset viewer.