Changeset 2942
 Timestamp:
 Mar 23, 2013, 1:37:22 AM (7 years ago)
 Location:
 src
 Files:

 5 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLtoERTLptrOK.ma
r2940 r2942 862 862 (inr ident … 〈c_ptr1,c_ptr2〉) 863 863 (sigma_state_pc prog f_lbls f_regs st2)) 864 [ 865 866 generalize in match (block_of_call ?????); 867 868 % 864 865 [ whd in ⊢ (??%%); normalize nodelta 866 XXX 867 % 869 868 *: whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta 870 869 @if_elim change with (pc_block(pc … st2)) in match (pc_block ?); 
src/ERTLptr/ERTLptrToLTL.ma
r2888 r2942 320 320 321 321 definition translate_step: 322 ∀globals .nat → ∀after : valuation register_lattice.323 coloured_graph after→322 ∀globals,fn.nat → ∀after : valuation register_lattice. 323 coloured_graph (livebefore globals fn after) → 324 324 ℕ → label → joint_step ERTLptr globals → bind_step_block LTL globals ≝ 325 λglobals, localss,after,grph,stack_sz,lbl,s.325 λglobals,fn,localss,after,grph,stack_sz,lbl,s. 326 326 bret … ( 327 327 let lookup ≝ λr.colouring … grph (inl … r) in … … 440 440 (* added_prologue ≝ *) [ ] 441 441 (* new_regs ≝ *) [ ] 442 (* f_step ≝ *) (translate_step ? (joint_if_local_stacksize ?? int_fun) … coloured_graph stack_sz)442 (* f_step ≝ *) (translate_step ? int_fun (joint_if_local_stacksize ?? int_fun) … coloured_graph stack_sz) 443 443 (* f_fin ≝ *) (translate_fin_step globals) 444 444 ????). 
src/ERTLptr/ERTLptrToLTLProof.ma
r2940 r2942 6 6 include "common/AssocList.ma". 7 7 8 9 10 8 (* Inefficient, replace with Trie lookup *) 11 9 definition lookup_stack_cost ≝ … … 26 24 27 25 axiom to_be_cleared_sb : 28 ∀ after : valuation register_lattice. coloured_graph after→ clear_sb_type.26 ∀live_before : valuation register_lattice. coloured_graph live_before → clear_sb_type. 29 27 30 28 definition local_clear_fb_type ≝ vertex → bool. … … 32 30 33 31 axiom to_be_cleared_fb : 34 ∀ after: valuation register_lattice.clear_fb_type.32 ∀live_before : valuation register_lattice.clear_fb_type. 35 33 36 34 axiom sigma_fb_state: … … 39 37 40 38 axiom acc_is_dead : ∀fix_comp.∀prog : ertlptr_program. 41 ∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog). 42 ∀l. 43 let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in 44 ¬ lives (inr ? ? RegisterA) (livebefore … fn l after). 39 ∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog). ∀l. 40 let after ≝ analyse_liveness fix_comp (prog_var_names … prog) fn in 41 ¬ lives (inr ? ? RegisterA) (livebefore … fn after l). 45 42 46 43 axiom dead_registers_in_dead : … … 49 46 ∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog). 50 47 ∀l. 51 let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn)in48 let after ≝ analyse_liveness fix_comp (prog_var_names … prog) fn in 52 49 let coloured_graph ≝ build … fn after in 53 50 ∀R : Register. 54 ¬ lives (inr ? ? R) (livebefore … fn l after) →55 to_be_cleared_sb aftercoloured_graph l R.51 ¬ lives (inr ? ? R) (livebefore … fn after l) → 52 to_be_cleared_sb … coloured_graph l R. 56 53 57 54 axiom sigma_sb_state: … … 69 66 fixpoint_computer → ertlptr_program → 70 67 state_pc ERTLptr_semantics → state_pc ERTLptr_semantics ≝ 71 λfix_comp,prog,st. 68 λfix_comp,prog,st. 72 69 let ge ≝ globalenv_noinit … prog in 73 70 let globals ≝ prog_var_names … prog in … … 75 72 [ OK y ⇒ 76 73 let pt ≝ point_of_pc ERTLptr_semantics (pc ? st) in 77 let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) (\snd y)) in 78 mk_state_pc ? (sigma_fb_state prog (to_be_cleared_fb after pt) st) (pc … st) 74 let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) (\snd y)) in 75 let before ≝ livebefore … (\snd y) after in 76 mk_state_pc ? (sigma_fb_state prog (to_be_cleared_fb before pt) st) (pc … st) 79 77 (last_pop … st) 80 78  Error e ⇒ dummy_state_pc … … 95 93 let coloured_graph ≝ build … (\snd y) after in 96 94 mk_state_pc ? (sigma_sb_state prog 97 (to_be_cleared_sb aftercoloured_graph pt) st) (pc … st)95 (to_be_cleared_sb … coloured_graph pt) st) (pc … st) 98 96 (sigma_stored_pc ERTLptr_semantics LTL_semantics 99 97 prog f_lbls (last_pop … st)) … … 107 105 ∃f,fn.fetch_internal_function ? (globalenv_noinit … prog) bl = return 〈f,fn〉 ∧ 108 106 let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in 107 let before ≝ livebefore … fn after in 109 108 let coloured_graph ≝ build … fn after in 110 (sigma_fb_state prog (to_be_cleared_fb afterpc) st1) =111 (sigma_sb_state prog (to_be_cleared_sb aftercoloured_graph pc) st2).109 (sigma_fb_state prog (to_be_cleared_fb before pc) st1) = 110 (sigma_sb_state prog (to_be_cleared_sb … coloured_graph pc) st2). 112 111 113 112 axiom write_decision : … … 250 249 ∀bv. 251 250 ∀r : register.R st1 st2 → 252 lives (inl ? ? r) (livebefore … fn (point_of_pc ERTLptr_semantics (pc … st1)) after) →251 lives (inl ? ? r) (livebefore … fn after (point_of_pc ERTLptr_semantics (pc … st1))) → 253 252 ps_reg_retrieve (regs … st1) r = return bv → 254 253 ∃bv'.bv = sigma_beval prog f_lbls bv' ∧ 255 read_arg_decision (colouring after (colour (prog_var_names … prog) fn after) 256 (inl register Register r)) 257 st2 = bv'. 254 read_arg_decision 255 (colouring … (colour (prog_var_names … prog) fn after) 256 (inl register Register r)) 257 st2 = bv'. 258 258 259 259 axiom set_member_empty :∀A.∀DEC.∀a.¬set_member A DEC a (set_empty …). … … 276 276 let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in 277 277 eliminable ? (after l) stmt = false → 278 lives (inl ? ? r) (livebefore … fn l after).278 lives (inl ? ? r) (livebefore … fn after l). 279 279 #fix_comp #prog #fn #l * 280 280 [ * [#c* [#c_id  #c_ptr] #args #dest  #a #lbl  * … … 317 317 %{(refl …)} %{(refl …)} % 318 318 qed. 319 (*320 axiom dead_is_to_be_clear :321 *)322 319 323 320 (* Cut&paste da un altro file con nome split_on_last_append, unificare*) … … 347 344 348 345 axiom sigma_fb_state_insensitive_to_dead_reg: 349 ∀fix_comp,prog,fn,bv. ∀st: state ERTLptr_semantics. ∀l:label. 350 ∀r: register. 351 let live ≝ 352 analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn 353 in 354 set_member (identifier RegisterTag) (eq_identifier RegisterTag) r 355 (\fst (livebefore … fn l live)) = false → 346 ∀prog,bv. ∀st: state ERTLptr_semantics. ∀l:label. 347 ∀r: register. ∀before. 348 set_member … (eq_identifier RegisterTag) r (\fst (before l)) = false → 356 349 sigma_fb_state prog 357 (to_be_cleared_fb live l)350 (to_be_cleared_fb before l) 358 351 (set_regs ERTLptr_semantics 359 352 〈reg_store r bv (\fst (regs ERTLptr_semantics st)), 360 353 \snd (regs ERTLptr_semantics st)〉 st) 361 = sigma_fb_state prog (to_be_cleared_fb live l) st.354 = sigma_fb_state prog (to_be_cleared_fb before l) st. 362 355 363 356 axiom sigma_fb_state_insensitive_to_dead_Reg: 364 ∀fix_comp,prog,fn,bv. ∀st: state ERTLptr_semantics. ∀l:label. 365 ∀r: Register. 366 let live ≝ 367 analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn 368 in 369 set_member Register eq_Register r (\snd (livebefore … fn l live)) = false → 357 ∀prog,bv. ∀st: state ERTLptr_semantics. ∀l:label. 358 ∀r: Register. ∀before. 359 set_member … eq_Register r (\snd (before l)) = false → 370 360 sigma_fb_state prog 371 (to_be_cleared_fb live l)361 (to_be_cleared_fb before l) 372 362 (set_regs ERTLptr_semantics 373 363 〈\fst (regs ERTLptr_semantics st), 374 364 hwreg_store r bv (\snd (regs ERTLptr_semantics st))〉 375 365 st) 376 = sigma_fb_state prog (to_be_cleared_fb live l) st.366 = sigma_fb_state prog (to_be_cleared_fb before l) st. 377 367 378 368 axiom sigma_fb_state_insensitive_to_dead_carry: 379 ∀fix_comp,prog,fn,bv. ∀st: state ERTLptr_semantics. ∀l:label. 380 let live ≝ 381 analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn 382 in 383 set_member Register eq_Register RegisterCarry (\snd (livebefore … fn l live)) = false → 384 sigma_fb_state prog (to_be_cleared_fb live l) (set_carry ERTLptr_semantics bv st) = 385 sigma_fb_state prog (to_be_cleared_fb live l) st. 369 ∀prog,bv. ∀st: state ERTLptr_semantics. ∀l:label. ∀before. 370 set_member Register eq_Register RegisterCarry (\snd (before l)) = false → 371 sigma_fb_state prog (to_be_cleared_fb before l) (set_carry ERTLptr_semantics bv st) = 372 sigma_fb_state prog (to_be_cleared_fb before l) st. 386 373 387 374 lemma split_orb_false: ∀a,b:bool. orb a b = false → a = false ∧ b = false. … … 400 387 401 388 lemma eliminable_step_to_eq_livebefore_liveafter: 402 ∀fix_comp,colour,prog,fn. 403 let p_in ≝ 404 mk_prog_params ERTLptr_semantics prog 405 (lookup_stack_cost (\snd (\fst (ertlptr_to_ltl fix_comp colour prog)))) in 389 ∀prog,stackcost,fn. 390 let p_in ≝ mk_prog_params ERTLptr_semantics prog stackcost in 406 391 ∀st1: joint_abstract_status p_in. 407 392 ∀stms: joint_seq ERTLptr_semantics (prog_var_names … prog). ∀next. 408 393 let pt ≝ point_of_pc ERTLptr_semantics (pc ? st1) in 409 394 stmt_at p_in ? (joint_if_code p_in … fn) pt = return (sequential … stms next) → 410 let liveafter ≝ analyse_liveness fix_comp (globals p_in) fn in395 ∀liveafter. 411 396 eliminable_step (globals p_in) (liveafter (point_of_pc ERTLptr_semantics (pc … st1))) stms = true → 412 livebefore … fn pt liveafter= liveafter pt.413 # fix_comp #colour #prog #fn #st1 #stms #next #stmt_at#Helim397 livebefore … fn liveafter pt = liveafter pt. 398 #prog #stackcost #fn #st1 #stms #next #stmt_at #liveafter #Helim 414 399 whd in ⊢ (??%?); whd in stmt_at:(??%?); cases (lookup ????) in stmt_at; 415 400 normalize nodelta try (#abs whd in abs:(??%%); destruct (abs) @I) … … 420 405 lemma sigma_fb_state_insensitive_to_eliminable: 421 406 ∀fix_comp: fixpoint_computer. 422 ∀colour: coloured_graph_computer.423 407 ∀prog: ertlptr_program. 424 let p_in ≝ 425 mk_prog_params ERTLptr_semantics prog 426 (lookup_stack_cost (\snd (\fst (ertlptr_to_ltl fix_comp colour prog)))) in 408 ∀stackcost. 409 let p_in ≝ mk_prog_params ERTLptr_semantics prog stackcost in 427 410 ∀f,fn. 411 ∀after: valuation ?. 412 let before ≝ livebefore … fn after in 428 413 ∀st1 : joint_abstract_status p_in. 429 414 let pt ≝ point_of_pc ERTLptr_semantics (pc ? st1) in … … 434 419 (prog_var_names (joint_function ERTLptr_semantics) ℕ prog) 435 420 (ev_genv 436 (mk_prog_params ERTLptr_semantics prog 437 (lookup_stack_cost (\snd (\fst (ertlptr_to_ltl fix_comp colour prog)))))) 421 (mk_prog_params ERTLptr_semantics prog stackcost)) 438 422 f stms (st_no_pc … st1) 439 423 =return st1_no_pc. 440 424 ∀Heliminable: 441 425 eliminable_step (globals p_in) 442 (analyse_liveness fix_comp (globals p_in) fn 443 (point_of_pc ERTLptr_semantics (pc p_in st1))) stms 444 =true. 445 (sigma_fb_state prog 446 (to_be_cleared_fb 447 (analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) 448 fn) pt) 449 st1_no_pc 450 =sigma_fb_state prog 451 (to_be_cleared_fb 452 (analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) 453 fn) pt) 454 (st_no_pc … st1)). 455 #fix_comp #colour #prog letin p_in ≝ (mk_prog_params ???) #f #fn 426 (after (point_of_pc ERTLptr_semantics (pc p_in st1))) stms =true. 427 sigma_fb_state prog (to_be_cleared_fb before pt) st1_no_pc = 428 sigma_fb_state prog (to_be_cleared_fb before pt) (st_no_pc … st1). 429 #fix_comp #prog #stackcost letin p_in ≝ (mk_prog_params ???) #f #fn #after 456 430 #st1 #st1' #stms #next #stmt_at #Heval #Helim 457 lapply (eliminable_step_to_eq_livebefore_liveafter … stmt_at Helim)431 lapply (eliminable_step_to_eq_livebefore_liveafter … stmt_at … Helim) 458 432 #EQ_livebefore_after next 459 433 cases stms in Heval Helim; … … 596 570 (read_arg_decision 597 571 (colouring 598 (analyse_liveness fix_comp (globals prog_pars_in) fn)572 … 599 573 (colour (globals prog_pars_in) fn 600 574 (analyse_liveness fix_comp (globals prog_pars_in) fn)) … … 614 588 [2,4: @dead_registers_in_dead @acc_is_dead ] 615 589 whd >point_of_pc_of_point 590 letin after ≝ (analyse_liveness fix_comp … fn) 591 letin before ≝ (livebefore … fn after) 616 592 [ cut 617 (analyse_liveness fix_comp … fn ltrue = 618 analyse_liveness fix_comp … fn 619 (point_of_pc ERTLptr_semantics (pc … st1))) 593 (before ltrue = 594 before (point_of_pc ERTLptr_semantics (pc … st1))) 620 595 [ cases daemon (*CSC: Genuine proof obligation! *) 621 596  #Hext ] 622 597  cut 623 (analyse_liveness fix_comp … fn lfalse = 624 analyse_liveness fix_comp … fn 625 (point_of_pc ERTLptr_semantics (pc … st1))) 598 (before lfalse = 599 before (point_of_pc ERTLptr_semantics (pc … st1))) 626 600 [ cases daemon (*CSC: Genuine proof obligation! *) 627 601  #Hext ]] … … 675 649 #EQst1st2 #_ #_ 676 650 (* CSC: END *) 677 <EQst1st2 whd in EQst1_no_pc:(??%%); whd in match (st_no_pc ??); 651 lapply (sigma_fb_state_insensitive_to_eliminable fix_comp … EQstmt … Heval_seq_no_pc Heliminable) 652 XXXX 653 <EQst1st2 654 655 lapply Heval_seq_no_pc; whd in match eval_seq_no_pc; normalize nodelta 656 657 whd in Heval_seq_no_pc:(??%%); whd in match (st_no_pc ??); 678 658 679 659 
src/ERTLptr/Interference.ma
r2845 r2942 8 8 prop_colouring 2 and 3 together say that spilled_no is the number of spilled 9 9 registers *) 10 (* Wilmer: the generation of the destruct principle diverges; 11 CtrC make the file pass *) 12 record coloured_graph (after: valuation register_lattice): Type[1] ≝ 10 record coloured_graph (before: valuation register_lattice): Type[1] ≝ 13 11 { colouring: vertex → decision 14 12 ; spilled_no: nat 15 13 ; prop_colouring: ∀l. ∀v1, v2: vertex.v1 ≠v2 → 16 lives v1 ( after l) → lives v2 (afterl) → colouring v1 ≠ colouring v214 lives v1 (before l) → lives v2 (before l) → colouring v1 ≠ colouring v2 17 15 ; prop_spilled_no: (*CSC: the existguarded premise is just to make the proof more general *) 18 ∀v1:vertex. (∃l. bool_to_Prop (lives v1 ( afterl))) → ∀i. colouring v1 = decision_spill i → i < spilled_no16 ∀v1:vertex. (∃l. bool_to_Prop (lives v1 (before l))) → ∀i. colouring v1 = decision_spill i → i < spilled_no 19 17 }. 20 18 21 19 definition coloured_graph_computer ≝ 22 20 ∀globals. 23 joint_internal_function ERTLptr globals →24 ∀ valuation.25 coloured_graph valuation.21 ∀fn:joint_internal_function ERTLptr globals. 22 ∀liveafter. 23 coloured_graph (livebefore globals fn liveafter). 
src/ERTLptr/liveness.ma
r2887 r2942 232 232 rl_join (rl_diff liveafter (defined globals stmt)) (used globals stmt). 233 233 234 definition livebefore ≝ 234 definition livebefore: 235 ∀globals: list ident. 236 joint_internal_function ERTLptr globals → 237 valuation register_lattice → valuation register_lattice 238 ≝ 235 239 λglobals: list ident. 236 240 λint_fun: joint_internal_function ERTLptr globals. 241 λliveafter: valuation register_lattice. 237 242 λlabel. 238 λliveafter: valuation register_lattice.239 243 match lookup ?? (joint_if_code … int_fun) label with 240 244 [ None ⇒ rl_bottom … … 251 255  Some stmt ⇒ 252 256 \fold[rl_join,rl_bottom]_{successor ∈ stmt_labels … stmt} 253 (livebefore globals int_fun successor liveafter)257 (livebefore globals int_fun liveafter successor) 254 258 ]. 255 259
Note: See TracChangeset
for help on using the changeset viewer.