Changeset 2930
- Timestamp:
- Mar 21, 2013, 7:14:38 PM (8 years ago)
- File:
-
- 1 edited
-
src/ERTLptr/ERTLptrToLTLProof.ma (modified) (16 diffs)
Legend:
- Unmodified
- Added
- Removed
-
src/ERTLptr/ERTLptrToLTLProof.ma
r2922 r2930 22 22 joint_abstract_status (mk_prog_params LTL_semantics prog stack_sizes). 23 23 24 definition clear_sb_type ≝ label → decision → bool. 24 definition local_clear_sb_type ≝ decision → bool. 25 definition clear_sb_type ≝ label → local_clear_sb_type. 25 26 26 27 axiom to_be_cleared_sb : 27 28 ∀after : valuation register_lattice. coloured_graph after → clear_sb_type. 28 29 29 definition clear_fb_type ≝ label → vertex → bool. 30 definition local_clear_fb_type ≝ vertex → bool. 31 definition clear_fb_type ≝ label → local_clear_fb_type. 30 32 31 33 axiom to_be_cleared_fb : 32 34 ∀after : valuation register_lattice.clear_fb_type. 33 35 34 axiom sigma_fb_state: ertlptr_program → (block → label → list label) →35 (block → label → list register) →36 clear_fb_type →state ERTLptr_semantics → state ERTLptr_semantics.36 axiom sigma_fb_state: 37 ertlptr_program → local_clear_fb_type → 38 state ERTLptr_semantics → state ERTLptr_semantics. 37 39 38 40 axiom acc_is_dead : ∀fix_comp.∀prog : ertlptr_program. … … 42 44 ¬ lives (inr ? ? RegisterA) (livebefore … fn l after). 43 45 44 axiom dead_registers_in_dead : ∀fix_comp.∀build : coloured_graph_computer. 45 ∀prog : ertlptr_program. 46 ∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog). 47 ∀l. 48 let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in 49 let coloured_graph ≝ build … fn after in 50 ∀R : Register. 51 ¬ lives (inr ? ? R) (livebefore … fn l after) → 52 to_be_cleared_sb after coloured_graph l R. 53 54 axiom sigma_sb_state: ertlptr_program → (block → label → list label) → 55 (block → label → list register) → clear_sb_type → state LTL_semantics → state ERTLptr_semantics. 46 axiom dead_registers_in_dead : 47 ∀fix_comp.∀build : coloured_graph_computer. 48 ∀prog : ertlptr_program. 49 ∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog). 50 ∀l. 51 let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in 52 let coloured_graph ≝ build … fn after in 53 ∀R : Register. 54 ¬ lives (inr ? ? R) (livebefore … fn l after) → 55 to_be_cleared_sb after coloured_graph l R. 56 57 axiom sigma_sb_state: 58 ertlptr_program → local_clear_sb_type → state LTL_semantics → state ERTLptr_semantics. 56 59 57 60 definition dummy_state : state ERTLptr_semantics ≝ … … 63 66 64 67 65 definition sigma_fb_state_pc : fixpoint_computer → ertlptr_program →66 (block → label → list label) → (block → label → list register)→67 state_pc ERTLptr_semantics → state_pc ERTLptr_semantics ≝68 λfix_comp,prog,f_lbls,f_regs,st.69 let ge ≝ globalenv_noinit … prog in70 let globals ≝ prog_var_names … prog in71 match fetch_internal_function … ge (pc_block (pc … st)) with68 definition sigma_fb_state_pc : 69 fixpoint_computer → ertlptr_program → 70 state_pc ERTLptr_semantics → state_pc ERTLptr_semantics ≝ 71 λfix_comp,prog,st. 72 let ge ≝ globalenv_noinit … prog in 73 let globals ≝ prog_var_names … prog in 74 match fetch_internal_function … ge (pc_block (pc … st)) with 72 75 [ OK y ⇒ 73 let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) (\snd y)) in 74 mk_state_pc ? (sigma_fb_state prog f_lbls f_regs (to_be_cleared_fb after) st) (pc … st) 75 (last_pop … st) 76 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) 79 (last_pop … st) 76 80 | Error e ⇒ dummy_state_pc 77 81 ]. … … 79 83 include "joint/StatusSimulationHelper.ma". 80 84 81 definition sigma_sb_state_pc :fixpoint_computer → coloured_graph_computer →82 ertlptr_program → (block → label → list label) → 83 (block → label → list register)→ state_pc LTL_semantics → state_pc ERTLptr_semantics ≝84 λfix_comp,build,prog,f_lbls,f_regs,st.85 let ge ≝ globalenv_noinit … prog in86 let globals ≝ prog_var_names … prog in87 match fetch_internal_function … ge (pc_block (pc … st)) with85 definition sigma_sb_state_pc: 86 fixpoint_computer → coloured_graph_computer → 87 ertlptr_program → lbl_funct → state_pc LTL_semantics → state_pc ERTLptr_semantics ≝ 88 λfix_comp,build,prog,f_lbls,st. 89 let ge ≝ globalenv_noinit … prog in 90 let globals ≝ prog_var_names … prog in 91 match fetch_internal_function … ge (pc_block (pc … st)) with 88 92 [ OK y ⇒ 93 let pt ≝ point_of_pc ERTLptr_semantics (pc ? st) in 89 94 let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) (\snd y)) in 90 95 let coloured_graph ≝ build … (\snd y) after in 91 mk_state_pc ? (sigma_sb_state prog f_lbls f_regs92 (to_be_cleared_sb after coloured_graph ) st) (pc … st)96 mk_state_pc ? (sigma_sb_state prog 97 (to_be_cleared_sb after coloured_graph pt) st) (pc … st) 93 98 (sigma_stored_pc ERTLptr_semantics LTL_semantics 94 99 prog f_lbls (last_pop … st)) … … 97 102 98 103 definition state_rel : fixpoint_computer → coloured_graph_computer → 99 ertlptr_program → ( block → label → list label) → (block → label → list register) →100 (Σb:block.block_region b = Code) →state ERTL_state → state LTL_LIN_state → Prop ≝101 λfix_comp,build,prog, f_lbls,f_regs,bl,st1,st2.104 ertlptr_program → (Σb:block.block_region b = Code) → label → 105 state ERTL_state → state LTL_LIN_state → Prop ≝ 106 λfix_comp,build,prog,bl,pc,st1,st2. 102 107 ∃f,fn.fetch_internal_function ? (globalenv_noinit … prog) bl = return 〈f,fn〉 ∧ 103 108 let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in 104 109 let coloured_graph ≝ build … fn after in 105 (sigma_fb_state prog f_lbls f_regs (to_be_cleared_fb after) st1) = 106 (sigma_sb_state prog f_lbls f_regs 107 (to_be_cleared_sb after coloured_graph) st2). 108 109 axiom write_decision : decision → beval → state LTL_LIN_state → 110 state LTL_LIN_state. 110 (sigma_fb_state prog (to_be_cleared_fb after pc) st1) = 111 (sigma_sb_state prog (to_be_cleared_sb after coloured_graph pc) st2). 112 113 axiom write_decision : 114 decision → beval → state LTL_LIN_state → state LTL_LIN_state. 111 115 112 116 axiom read_arg_decision : arg_decision → state LTL_LIN_state → beval. 113 117 114 axiom insensitive_to_be_cleared_sb : ∀prog. ∀f_lbls : (block → label → list label). 115 ∀f_regs : (block → label → list register).∀tb : clear_sb_type. 116 ∀st : state LTL_LIN_state.∀lab. 117 ∀d : decision.∀bv.tb lab d → 118 sigma_sb_state prog f_lbls f_regs tb st = 119 sigma_sb_state prog f_lbls f_regs tb (write_decision d bv st). 118 axiom insensitive_to_be_cleared_sb : 119 ∀prog. ∀tb : local_clear_sb_type. ∀st : state LTL_LIN_state. 120 ∀d : decision.∀bv.tb d → 121 sigma_sb_state prog tb st = 122 sigma_sb_state prog tb (write_decision d bv st). 120 123 121 124 … … 124 127 ∀colour : coloured_graph_computer. 125 128 ∀ prog : ertlptr_program. 126 ∀ f_lbls . ∀f_regs. ∀f_bl_r.129 ∀ f_lbls, f_regs. ∀f_bl_r. 127 130 b_graph_transform_program_props ERTLptr_semantics LTL_semantics 128 131 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs → … … 137 140 (λs1:ERTLptr_status ? ? 138 141 .λs2:LTL_status ? ? 139 .sigma_fb_state_pc fix_comp prog f_lbls f_regss1140 =sigma_sb_state_pc fix_comp colour prog f_lbls f_regss2)142 .sigma_fb_state_pc fix_comp prog s1 143 =sigma_sb_state_pc fix_comp colour prog f_lbls s2) 141 144 (* call_rel ≝ *) 142 145 (λs1:Σs:ERTLptr_status ??.as_classifier ? s cl_call … … 159 162 (globalenv_noinit … prog) (pc … st1) = return 〈id,fn,stmt〉 → 160 163 as_label ? st2 = as_label ? st1. 161 162 163 164 164 165 165 (* … … 177 177 *) 178 178 179 180 181 179 axiom pc_block_eq_sigma_commute : ∀fix_comp,colour. 182 180 ∀prog.∀ f_lbls,f_regs.∀f_bl_r. … … 187 185 R st1 st2 → 188 186 pc_block (pc … st1) = pc_block (pc … st2). 189 190 187 191 188 axiom pc_eq_sigma_commute : ∀fix_comp,colour. … … 237 234 return write_decision dest (read_arg_decision src s) s. 238 235 239 axiom sigma_beval : ertlptr_program → (block → label → list label) →240 236 axiom sigma_beval: 237 ertlptr_program → (block → label → list label) → beval → beval. 241 238 242 239 … … 269 266 ¬set_member A DEC a y → 270 267 set_member A DEC a (set_diff … x y). 271 272 268 273 269 lemma all_used_are_live_before : … … 351 347 352 348 axiom sigma_fb_state_insensitive_to_dead_reg: 353 ∀fix_comp,colour,prog. 354 let p_in ≝ 355 mk_prog_params ERTLptr_semantics prog 356 (lookup_stack_cost (\snd (\fst (ertlptr_to_ltl fix_comp colour prog)))) in 357 ∀fn,f_lbls,f_regs,bv. 358 ∀st: joint_abstract_status p_in. 349 ∀fix_comp,prog,fn,bv. ∀st: state ERTLptr_semantics. ∀l:label. 359 350 ∀r: register. 360 351 let live ≝ 361 analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn 362 in 352 analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn in 363 353 set_member (identifier RegisterTag) (eq_identifier RegisterTag) r 364 (\fst (live (point_of_pc ERTLptr_semantics (pc p_in st)))) = false →365 sigma_fb_state prog f_lbls f_regs366 (to_be_cleared_fb live )354 (\fst (live l)) = false → 355 sigma_fb_state prog 356 (to_be_cleared_fb live l) 367 357 (set_regs ERTLptr_semantics 368 〈reg_store r bv (\fst (regs ERTLptr_semantics (st_no_pc … st))),369 \snd (regs ERTLptr_semantics (st_no_pc … st))〉 (st_no_pc … st))370 = sigma_fb_state prog f_lbls f_regs (to_be_cleared_fb live) (st_no_pc … st).358 〈reg_store r bv (\fst (regs ERTLptr_semantics st)), 359 \snd (regs ERTLptr_semantics st)〉 st) 360 = sigma_fb_state prog (to_be_cleared_fb live l) st. 371 361 372 362 axiom sigma_fb_state_insensitive_to_dead_Reg: 373 ∀fix_comp,colour,prog. 374 let p_in ≝ 375 mk_prog_params ERTLptr_semantics prog 376 (lookup_stack_cost (\snd (\fst (ertlptr_to_ltl fix_comp colour prog)))) in 377 ∀fn,f_lbls,f_regs,bv. 378 ∀st: joint_abstract_status p_in. 363 ∀fix_comp,prog,fn,bv. ∀st: state ERTLptr_semantics. ∀l:label. 379 364 ∀r: Register. 380 365 let live ≝ 381 366 analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn 382 367 in 383 set_member Register eq_Register r 384 (\snd (live (point_of_pc ERTLptr_semantics (pc p_in st)))) = false → 385 sigma_fb_state prog f_lbls f_regs 386 (to_be_cleared_fb live) 368 set_member Register eq_Register r (\snd (live l)) = false → 369 sigma_fb_state prog 370 (to_be_cleared_fb live l) 387 371 (set_regs ERTLptr_semantics 388 〈\fst (regs ERTLptr_semantics (st_no_pc … st)), 389 hwreg_store r bv (\snd (regs ERTLptr_semantics (st_no_pc … st)))〉 390 (st_no_pc … st)) 391 = sigma_fb_state prog f_lbls f_regs 392 (to_be_cleared_fb live) (st_no_pc … st). 372 〈\fst (regs ERTLptr_semantics st), 373 hwreg_store r bv (\snd (regs ERTLptr_semantics st))〉 374 st) 375 = sigma_fb_state prog (to_be_cleared_fb live l) st. 393 376 394 377 axiom sigma_fb_state_insensitive_to_dead_carry: 395 ∀fix_comp,colour,prog. 396 let p_in ≝ 397 mk_prog_params ERTLptr_semantics prog 398 (lookup_stack_cost (\snd (\fst (ertlptr_to_ltl fix_comp colour prog)))) in 399 ∀fn,f_lbls,f_regs,bv. 400 ∀st: joint_abstract_status p_in. 378 ∀fix_comp,prog,fn,bv. ∀st: state ERTLptr_semantics. ∀l:label. 401 379 let live ≝ 402 380 analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn 403 381 in 404 set_member Register eq_Register RegisterCarry 405 (\snd (live (point_of_pc ERTLptr_semantics (pc p_in st)))) = false → 406 sigma_fb_state prog f_lbls f_regs 407 (to_be_cleared_fb live) 408 (set_carry ERTLptr_semantics bv (st_no_pc … st)) 409 = sigma_fb_state prog f_lbls f_regs (to_be_cleared_fb live) (st_no_pc … st). 382 set_member Register eq_Register RegisterCarry (\snd (live l)) = false → 383 sigma_fb_state prog (to_be_cleared_fb live l) (set_carry ERTLptr_semantics bv st) = 384 sigma_fb_state prog (to_be_cleared_fb live l) st. 410 385 411 386 lemma split_orb_false: ∀a,b:bool. orb a b = false → a = false ∧ b = false. … … 420 395 mk_prog_params ERTLptr_semantics prog 421 396 (lookup_stack_cost (\snd (\fst (ertlptr_to_ltl fix_comp colour prog)))) in 422 ∀f,fn ,f_lbls,f_regs.397 ∀f,fn. 423 398 ∀st1 : joint_abstract_status p_in. 399 let pt ≝ point_of_pc ERTLptr_semantics (pc ? st1) in 424 400 ∀st1_no_pc,stms. 425 401 ∀Heval_seq_no_pc: … … 436 412 (point_of_pc ERTLptr_semantics (pc p_in st1))) stms 437 413 =true. 438 (sigma_fb_state prog f_lbls f_regs414 (sigma_fb_state prog 439 415 (to_be_cleared_fb 440 416 (analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) 441 fn) )417 fn) pt) 442 418 st1_no_pc 443 =sigma_fb_state prog f_lbls f_regs419 =sigma_fb_state prog 444 420 (to_be_cleared_fb 445 421 (analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) 446 fn) )422 fn) pt) 447 423 (st_no_pc … st1)). 448 #fix_comp #colour #prog letin p_in ≝ (mk_prog_params ???) #f #fn #f_lbls #f_regs424 #fix_comp #colour #prog letin p_in ≝ (mk_prog_params ???) #f #fn 449 425 #st1 #st1' * 450 426 try (#arg1 #arg2 #arg3 #arg4 #arg5 #Heval #Helim) … … 493 469 try (@sigma_fb_state_insensitive_to_dead_Reg assumption) 494 470 try (@sigma_fb_state_insensitive_to_dead_carry assumption) 495 [ <(injective_OK ??? Hst1'') XXX 496 >sigma_fb_state_insensitive_to_dead_carry assumption 497 @sigma_fb_state_insensitive_to_dead_carry 471 [1,2,3,4,5,6,7: <(injective_OK ??? Hst1'') ] 472 [1,2,3: 473 >sigma_fb_state_insensitive_to_dead_carry try assumption 474 @sigma_fb_state_insensitive_to_dead_reg assumption 475 |4,5,6: (* BUG! *) 476 |7: >sigma_fb_state_insensitive_to_dead_reg try assumption 498 477 499 478 lemma make_ERTLptr_To_LTL_good_state_relation :
Note: See TracChangeset
for help on using the changeset viewer.
