Changeset 2946 for src/joint/semanticsUtils.ma
 Timestamp:
 Mar 24, 2013, 11:29:01 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/semanticsUtils.ma
r2843 r2946 7 7 include "common/extraGlobalenvs.ma". 8 8 9 definition reg_store ≝ λreg,v,locals.add RegisterTag beval locals reg v. 10 11 definition reg_retrieve : register_env beval → register → res beval ≝ 12 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg). 13 9 14 record hw_register_env : Type[0] ≝ 10 15 { reg_env : BitVectorTrie beval 6 11 16 ; other_bit : bebit 12 17 }. 13 14 definition empty_hw_register_env: hw_register_env ≝15 mk_hw_register_env (Stub …) BBundef.16 18 17 19 include alias "ASM/BitVectorTrie.ma". … … 42 44 hwreg_store RegisterSPH sph (hwreg_store RegisterSPL spl env). 43 45 46 definition init_hw_register_env: xpointer → hw_register_env ≝ 47 hwreg_store_sp (mk_hw_register_env (Stub …) BBundef). 48 44 49 (*** Store/retrieve on pseudoregisters ***) 45 50 include alias "common/Identifiers.ma". 46 51 47 record reg_sp : Type[0] ≝48 { reg_sp_env :> identifier_map RegisterTag beval49 ; stackp : xpointer50 }.51 52 definition reg_store ≝ λreg,v,locals.add RegisterTag beval locals reg v.53 54 definition reg_retrieve : register_env beval → register → res beval ≝55 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).56 57 definition reg_sp_store ≝ λreg,v,locals.58 let locals' ≝ reg_store reg v (reg_sp_env locals) in59 mk_reg_sp locals' (stackp locals).60 61 52 unification hint 0 ≔ X ⊢ register_env X ≡ identifier_map RegisterTag X. 62 63 definition reg_sp_retrieve ≝ λlocals : reg_sp.reg_retrieve locals.64 65 definition reg_sp_init ≝ mk_reg_sp (empty_map …).66 (*** Store/retrieve on hardware registers ***)67 68 definition init_hw_register_env: xpointer → hw_register_env ≝69 λsp.hwreg_store_sp empty_hw_register_env sp.70 53 71 54 (******************************** GRAPHS **************************************) … … 74 57 { sgp_pars : uns_params 75 58 ; sgp_sup : ∀F.sem_unserialized_params sgp_pars F 59 ; graph_pre_main_generator : 60 ∀p : joint_program (mk_graph_params sgp_pars). 61 joint_closed_internal_function (mk_graph_params sgp_pars) (prog_var_names … p) 76 62 }. 77 63 … … 91 77 λpars. 92 78 mk_sem_params 93 (pars : graph_params) 94 (sgp_sup pars ?) 95 (word_of_identifier ?) 96 (an_identifier ?) 97 ? (refl …). 79 (mk_serialized_params 80 (pars : graph_params) 81 (sgp_sup pars ?) 82 (word_of_identifier ?) 83 (an_identifier ?) 84 ? (refl …)) 85 (graph_pre_main_generator pars). 98 86 * #p % qed. 99 87 … … 113 101 { slp_pars : uns_params 114 102 ; slp_sup : ∀F.sem_unserialized_params slp_pars F 103 ; lin_pre_main_generator : 104 ∀p : joint_program (mk_lin_params slp_pars). 105 joint_closed_internal_function (mk_lin_params slp_pars) (prog_var_names … p) 115 106 }. 116 107 … … 129 120 λpars. 130 121 mk_sem_params 131 (pars : lin_params) 132 (slp_sup pars ?) 133 succ_pos_of_nat 134 (λp.pred (nat_of_pos p)) 135 ??. 136 [ #n >nat_succ_pos % 137  @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos 122 (mk_serialized_params 123 (pars : lin_params) 124 (slp_sup pars ?) 125 succ_pos_of_nat 126 (λp.pred (nat_of_pos p)) 127 ??) 128 (lin_pre_main_generator pars). 129 [ @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos 130  #n >nat_succ_pos % 138 131 ] qed. 139 132 … … 143 136 on _pars : sem_lin_params to sem_params. 144 137 138 (* watch out, implementation dependent: 139 an_identifier SymbolTag one must be unused (used for premain) 140 *) 141 definition pre_main_id : ident ≝ an_identifier … one. 142 143 lemma lookup_opt_pm_set_elim : ∀A.∀P : option A → Prop.∀p,q,o,m. 144 (p = q → P o) → 145 (p ≠ q → P (lookup_opt A p m)) → 146 P (lookup_opt A p (pm_set A q o m)). 147 #A #P #p #q 148 @(eqb_elim p q) #H #o #m #H1 #H2 149 [ >H >lookup_opt_pm_set_hit @H1 @H 150  >lookup_opt_pm_set_miss [ @H2 ] @H 151 ] 152 qed. 153 154 lemma lookup_add_elim : ∀tag,A.∀P : option A → Prop.∀m,i,j,x. 155 (i = j → P (Some ? x)) → 156 (i ≠ j → P (lookup tag A m j)) → 157 P (lookup tag A (add tag A m i x) j). 158 #tag #A #P * #m * #p * #q #x 159 #H1 #H2 whd in ⊢ (?%); normalize nodelta whd in match insert; normalize nodelta 160 @lookup_opt_pm_set_elim #H destruct 161 [ @H1 %  @H2 % #EQ destruct cases H #H @H % ] 162 qed. 163 164 (* we just manually overwrite genv_t tables with the pre_main. 165 the RTLabs → RTL pass will need to ensure no pre_main_id is actually present *) 166 definition joint_globalenv : 167 ∀pars : sem_params.joint_program pars → genv_t ? ≝ 168 λpars,prog. 169 let genv ≝ drop_fn … pre_main_id (globalenv … (λx.x) prog) in 170 mk_genv_t ? 171 (insert … one (Internal … (pre_main_generator … pars prog)) (functions … genv)) 172 (nextfunction … genv) 173 (add … (symbols … genv) pre_main_id (mk_block (1))) 174 ?. 175 @hide_prf 176 whd in match insert; normalize nodelta #b 177 @lookup_opt_pm_set_elim #H destruct 178 [ #_ %{pre_main_id} @lookup_add_hit ] 179 #G cases (functions_inv … G) #id #EQ %{id} 180 @lookup_add_elim #EQid destruct [2: assumption ] 181 @⊥ whd in match drop_fn in EQ; normalize nodelta in EQ; 182 >lookup_remove_hit in EQ; #ABS destruct 183 qed. 145 184 146 185 lemma fetch_statement_eq : ∀p:sem_params.∀g. … … 346 385 qed. 347 386 348 349 387 lemma functions_transf: 350 388 ∀A,B,V,init.∀prog_in : program A V. … … 403 441 404 442 lemma fetch_internal_function_transf : 405 ∀A,B .∀prog_in : program (λvars.fundef (A vars)) ℕ.443 ∀A,B,V,init.∀prog_in : program (λvars.fundef (A vars)) V. 406 444 ∀trans : ∀vars.A vars → B vars. 407 445 let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in 408 446 ∀bl. 409 fetch_internal_function … (globalenv _noinit …prog_out) bl =410 ! 〈i, f〉 ← fetch_internal_function … (globalenv _noinit …prog_in) bl ;447 fetch_internal_function … (globalenv … init prog_out) bl = 448 ! 〈i, f〉 ← fetch_internal_function … (globalenv … init prog_in) bl ; 411 449 return 〈i, trans … f〉. 412 #A #B # prog #trans #bl450 #A #B #V #init #prog #trans #bl 413 451 whd in match fetch_internal_function; normalize nodelta 414 452 >(fetch_function_transf … prog) … … 452 490 λf_regs : block → label → list register. 453 491 let prog_out ≝ b_graph_transform_program src dst data prog_in in 454 let src_genv ≝ globalenv_noinit ?prog_in in455 let dst_genv ≝ globalenv_noinit ?prog_out in492 let src_genv ≝ joint_globalenv src prog_in in 493 let dst_genv ≝ joint_globalenv dst prog_out in 456 494 ∀bl,def_in. 495 block_id … bl ≠ 1 → 457 496 find_funct_ptr … src_genv bl = return (Internal ? def_in) → 458 497 ∃init_data,def_out. … … 468 507 ∀prog_in : joint_program src. 469 508 let prog_out ≝ b_graph_transform_program … data prog_in in 470 let src_genv ≝ globalenv_noinit ?prog_in in471 let dst_genv ≝ globalenv_noinit ?prog_out in509 let src_genv ≝ joint_globalenv src prog_in in 510 let dst_genv ≝ joint_globalenv dst prog_out in 472 511 ∃init_regs : block → list register. 473 512 ∃f_lbls : block → label → list label. 474 513 ∃f_regs : block → label → list register. 475 514 b_graph_transform_program_props src dst data prog_in init_regs f_lbls f_regs. 515 cases daemon (* TOREDO 476 516 #src #dst #data #prog_in 477 517 whd in match b_graph_transform_program_props; normalize nodelta 518 whd in match joint_globalenv; normalize nodelta 478 519 letin prog_out ≝ (b_graph_transform_program … data prog_in) 479 letin src_genv ≝ (globalenv _noinit ?prog_in)480 letin dst_genv ≝ (globalenv _noinit ?prog_out)520 letin src_genv ≝ (globalenv … (λx.x) prog_in) 521 letin dst_genv ≝ (globalenv … (λx.x) prog_out) 481 522 cut (∀p.lookup_opt ? p (functions ? dst_genv) = 482 523 option_map ?? (transf_fundef … (λf.b_graph_translate … (data … f) f)) 483 524 (lookup_opt ? p (functions ? src_genv))) 484 525 [ @functions_transf ] 526 cut (symbols ? dst_genv = symbols ? src_genv) 527 [ @symbols_transf ] 485 528 cases dst_genv #functs2 #nextf2 #symbols2 #H2 486 cases src_genv #functs1 #nextf1 #symbols1 #H1 529 cases src_genv #functs1 #nextf1 #symbols1 #H1 #EQ destruct 487 530 lapply H2 lapply H1 lapply functs2 488 531 @(pm_map_add_ind … functs1) functs1 functs2 #functs1 … … 490 533 #functs2 #H1 #H2 #transf 491 534 [ %{(λ_.[ ])} %{(λ_.λ_.[])} %{(λ_.λ_.[])} 492 #bl #def_in #ABS @⊥ lapply ABS ABS535 #bl #def_in #ABS1 #ABS2 @⊥ lapply ABS2 ABS2 lapply ABS1 ABS1 493 536 whd in match find_funct_ptr; 537 whd in match find_symbol; 494 538 normalize nodelta 495 whd in match (block_region bl); 496 cases (block_id bl) normalize nodelta 497 [2,3: #p [2: >functs1_empty ]] 498 normalize #ABS destruct 539 cases bl; * normalize nodelta 540 [2,3: #p ] 541 [1,3: #_ whd in ⊢ (???%→?); #EQ destruct ] 542 >lookup_add_hit 543 #H >lookup_opt_insert_miss 544 [2: @(swap_neg … H) #EQ >EQ % ] 545 whd in match drop_fn; normalize nodelta 546 cases (lookup … symbols1 pre_main_id) 547 normalize nodelta 548 [ >functs1_empty  ** [2,3: #p' ] normalize nodelta 549 [1,3: >functs1_empty 550  @lookup_opt_pm_set_elim #H destruct 551 [2: >functs1_empty ] 552 ] 553 ] whd in ⊢ (???%→?); #EQ destruct 499 554 ] 500 555 cases (IH (pm_set … p (None ?) functs2) ???) 501 [2: @hide_prf #b #G @(H1 b ?) @(swap_neg … G) G @(eqb_elim b p) 502 [ #EQ destruct >lookup_opt_insert_hit #ABS destruct ] 503 #NEQ >(lookup_opt_insert_miss ? f b p … NEQ) #H @H 504 3: @hide_prf #b #G @(H2 b ?) @(swap_neg … G) G @(eqb_elim b p) 505 [ #EQ destruct >lookup_opt_pm_set_hit #_ % ] 506 #NEQ >(lookup_opt_pm_set_miss … b p … NEQ) #H @H 507 4: #b @(eqb_elim b p) 508 [ #EQ destruct >lookup_opt_pm_set_hit >p_not_in % ] 509 #NEQ >(lookup_opt_pm_set_miss … b p … NEQ) >transf 510 >(lookup_opt_insert_miss ? f b p … NEQ) % 511 ] 556 [*: @hide_prf 557 [ #b #G @(H1 b ?) @(swap_neg … G) G 558 whd in match insert; normalize nodelta 559 @lookup_opt_pm_set_elim 560 [ #EQ #ABS destruct ] 561 #NEQ #H @H 562  #b #G @(H2 b ?) @(swap_neg … G) G 563 @lookup_opt_pm_set_elim 564 [ #_ #_ % ] 565 #_ #H @H 566  #b @lookup_opt_pm_set_elim 567 [ #EQ destruct >p_not_in % ] 568 #NEQ >transf 569 >(lookup_opt_insert_miss ? f b p … NEQ) % 570 ] 571 ] 572 #init_regs * #f_lbls * #f_regs #props 512 573 IH cases f in H1 transf; f #f #H1 #transf 513 #init_regs * #f_lbls * #f_regs #props514 574 [ (* internal *) 515 575 letin upd ≝ (λA : Type[0].λf : block → A. … … 532 592 whd in match (block_region (mk_block p')); 533 593 cases p' p' [2,3,5,6: #p' ] normalize nodelta 534 [1,3,5,6: #ABS normalize in ABS; destruct] 535 @(eqb_elim p' p) #pp' destruct 536 [1,3: >lookup_opt_insert_hit whd in ⊢ (??%%→?); #EQ destruct(EQ) 537 %{loc_data} % 538 [2: % [ % ] 539 [ >transf >lookup_opt_insert_hit % 540 *: >eq_block_b_b assumption 541 ] 542 ] 594 [1,3,5,6: #_ #ABS normalize in ABS; destruct] 595 whd in match find_symbol; 596 whd in match insert; normalize nodelta 597 #bl_prf 598 @lookup_opt_pm_set_elim #pp' destruct 599 [1,3: whd in ⊢ (??%%→?); #EQ destruct(EQ) 600 [ %{loc_data} % 601 [2: % [ % ] 602 [ >lookup_opt_insert_hit % 603 *: >eq_block_b_b assumption 604 ] 605 ] 543 606 *: >(lookup_opt_insert_miss ???? functs1 … pp') 544 607 [ @eq_block_elim [ #EQ destruct cases (absurd ?? pp') % ] #_ normalize nodelta] … … 546 609 whd in match find_funct_ptr; normalize nodelta 547 610 >(lookup_opt_pm_set_miss … functs2 … pp') #H @H 548 ] 611 ] *) 549 612 qed. 550 613 … … 559 622 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs → 560 623 let prog_out ≝ b_graph_transform_program … data prog_in in 561 let src_genv ≝ globalenv_noinit ? prog_in in 562 let dst_genv ≝ globalenv_noinit ? prog_out in 563 ∀bl,id,def_in. 624 let src_genv ≝ joint_globalenv src prog_in in 625 let dst_genv ≝ joint_globalenv dst prog_out in 626 ∀bl : Σbl.block_region … bl = Code.∀id,def_in. 627 block_id … bl ≠ 1 → 564 628 fetch_internal_function … src_genv bl = return 〈id, def_in〉 → 565 629 ∃init_data,def_out. … … 570 634 #src #dst #data #prog_in 571 635 #init_regs #f_lbls #f_regs #props 572 #bl #id #def_in 636 #bl #id #def_in #NEQ 573 637 #H @('bind_inversion H) * #id' * #def_in' H 574 638 normalize nodelta #H whd in ⊢ (??%%→?); #EQ destruct … … 576 640 #H @('bind_inversion H) H #def_in' #H 577 641 whd in ⊢ (??%%→?); #EQ destruct 578 cases (props … H)642 cases (props … NEQ H) 579 643 #loc_data * #def_out ** #H1 #H2 #H3 580 644 %{loc_data} %{def_out} … … 582 646 whd in match fetch_internal_function; 583 647 whd in match fetch_function; normalize nodelta 648 cases daemon (* TOREDO 584 649 >symbol_for_block_transf >EQ1 >m_return_bind 585 >H1 % 650 >H1 % *) 586 651 qed. 587 652 … … 596 661 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs → 597 662 let prog_out ≝ b_graph_transform_program … data prog_in in 598 let src_genv ≝ globalenv_noinit ?prog_in in599 let dst_genv ≝ globalenv_noinit ?prog_out in663 let src_genv ≝ joint_globalenv src prog_in in 664 let dst_genv ≝ joint_globalenv dst prog_out in 600 665 ∀pc,id,def_in,s. 666 block_id … (pc_block … pc) ≠ 1 → 601 667 fetch_statement … src_genv pc = return 〈id, def_in, s〉 → 602 668 ∃init_data,def_out. … … 622 688 #src #dst #data #prog_in 623 689 #init_regs #f_lbls #f_regs #props 624 #pc #id #def_in #s 690 #pc #id #def_in #s #NEQ 625 691 #H @('bind_inversion H) * #id' #def_in' H 626 692 #EQfif … … 628 694 #H lapply (opt_eq_from_res ???? H) H 629 695 #EQstmt_at whd in ⊢ (??%%→?); #EQ destruct 630 cases (b_graph_transform_program_fetch_internal_function … props … EQfif)696 cases (b_graph_transform_program_fetch_internal_function … props … NEQ EQfif) 631 697 #a * #b ** #H1 #H2 #H3 %{a} %{b} % 632 698 [ %{H1 H2} … … 644 710 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs → 645 711 let prog_out ≝ b_graph_transform_program … data prog_in in 646 let src_genv ≝ globalenv_noinit ?prog_in in647 let dst_genv ≝ globalenv_noinit ?prog_out in712 let src_genv ≝ joint_globalenv src prog_in in 713 let dst_genv ≝ joint_globalenv dst prog_out in 648 714 ∀pc,id,def_in,s. 715 block_id … (pc_block … pc) ≠ 1 → 649 716 fetch_statement … src_genv pc = return 〈id, def_in, s〉 → 650 717 ∃init_data,def_out. … … 679 746 #src #dst #data #prog_in 680 747 #init_regs #f_lbls #f_regs #props 681 #pc #id #def_in #s 748 #pc #id #def_in #s #NEQ 682 749 #H @('bind_inversion H) * #id' #def_in' H 683 750 #EQfif … … 685 752 #H lapply (opt_eq_from_res ???? H) H 686 753 #EQstmt_at whd in ⊢ (??%%→?); #EQ destruct 687 cases (b_graph_transform_program_fetch_internal_function … props … EQfif)754 cases (b_graph_transform_program_fetch_internal_function … props … NEQ EQfif) 688 755 #a * #b ** #H1 #H2 #H3 %{a} %{b} % 689 756 [ %{H1 H2}
Note: See TracChangeset
for help on using the changeset viewer.