Changeset 2973
 Timestamp:
 Mar 27, 2013, 1:11:13 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/semanticsUtils.ma
r2954 r2973 515 515 let dst_genv ≝ joint_globalenv dst prog_out stacksizes in 516 516 ∀bl,def_in. 517 block_id … bl ≠ 1 →518 517 find_funct_ptr … src_genv bl = return (Internal ? def_in) → 519 518 ∃init_data,def_out. … … 653 652 let dst_genv ≝ joint_globalenv dst prog_out stacksizes in 654 653 ∀bl : Σbl.block_region … bl = Code.∀id,def_in. 655 block_id … bl ≠ 1 → 656 fetch_internal_function … src_genv bl = return 〈id, def_in〉 → 657 ∃init_data,def_out. 658 fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧ 659 bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧ 660 b_graph_translate_props src dst ? init_data 661 def_in def_out (f_lbls bl) (f_regs bl). 654 if eqZb (block_id … bl) (1) then 655 (fetch_internal_function … dst_genv bl = 656 return 〈pre_main_id, pre_main_generator … dst prog_out〉) 657 else 658 (fetch_internal_function … src_genv bl = return 〈id, def_in〉 → 659 ∃init_data,def_out. 660 fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧ 661 bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧ 662 b_graph_translate_props src dst ? init_data 663 def_in def_out (f_lbls bl) (f_regs bl)). 662 664 #src #dst #stacksizes #data #prog_in 663 665 #init_regs #f_lbls #f_regs #props 664 #bl #id #def_in #NEQ 666 #bl #id #def_in 667 @if_elim' #Hbl 668 [ whd in match fetch_internal_function; whd in match fetch_function; 669 normalize nodelta >Hbl % ] 665 670 #H @('bind_inversion H) * #id' * #def_in' H 666 671 normalize nodelta [2: #_ whd in ⊢ (??%%→?); #ABS destruct ] 667 672 whd in match fetch_function; normalize nodelta 668 > (eqZb_false … NEQ)normalize nodelta673 >Hbl normalize nodelta 669 674 #H @('bind_inversion (opt_eq_from_res … H)) H #id'' #EQ1 670 675 #H @('bind_inversion H) H #def_in'' #H 671 676 whd in ⊢ (??%%→??%%→?); #EQ2 #EQ3 destruct 672 cases (props … NEQH)677 cases (props … H) 673 678 #loc_data * #def_out ** #H1 #H2 #H3 674 679 %{loc_data} %{def_out} … … 676 681 whd in match fetch_internal_function; 677 682 whd in match fetch_function; normalize nodelta 678 > (eqZb_false … NEQ)normalize nodelta683 >Hbl normalize nodelta 679 684 >symbol_for_block_transf >EQ1 >m_return_bind 680 685 >H1 % … … 694 699 let dst_genv ≝ joint_globalenv dst prog_out stacksizes in 695 700 ∀pc,id,def_in,s. 696 block_id … (pc_block … pc) ≠ 1 → 697 fetch_statement … src_genv pc = return 〈id, def_in, s〉 → 698 ∃init_data,def_out. 699 let bl ≝ pc_block pc in 700 fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧ 701 bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧ 702 let l ≝ point_of_pc dst pc in 703 ∃lbls,regs. 704 f_lbls bl l = lbls ∧ 705 f_regs bl l = regs ∧ 706 match s with 707 [ sequential s' nxt ⇒ 708 let block ≝ 709 if eq_identifier … (joint_if_entry … def_in) l then 710 append_seq_list … (f_step … init_data l s') (added_prologue … init_data) 711 else 712 f_step … init_data l s' in 713 l ~❨block, l::lbls, regs❩~> nxt in joint_if_code … def_out 714  final s' ⇒ 715 l ~❨f_fin … init_data l s', l::lbls, regs❩~> it in joint_if_code … def_out 716  FCOND abs _ _ _ ⇒ Ⓧabs 717 ]. 701 if eqZb (block_id … (pc_block … pc)) (1) then 702 (fetch_internal_function … dst_genv (pc_block … pc) = 703 return 〈pre_main_id, pre_main_generator … dst prog_out〉) 704 else 705 (fetch_statement … src_genv pc = return 〈id, def_in, s〉 → 706 ∃init_data,def_out. 707 let bl ≝ pc_block pc in 708 fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧ 709 bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧ 710 let l ≝ point_of_pc dst pc in 711 let lbls ≝ f_lbls bl l in let regs ≝ f_regs bl l in 712 match s with 713 [ sequential s' nxt ⇒ 714 let block ≝ 715 if not_emptyb … (added_prologue … init_data) ∧ 716 eq_identifier … (joint_if_entry … def_in) l then 717 bret … [ ] 718 else 719 f_step … init_data l s' in 720 l ~❨block, l::lbls, regs❩~> nxt in joint_if_code … def_out 721  final s' ⇒ 722 l ~❨f_fin … init_data l s', l::lbls, regs❩~> it in joint_if_code … def_out 723  FCOND abs _ _ _ ⇒ Ⓧabs 724 ]). 718 725 #src #dst #stacksizes #data #prog_in 719 726 #init_regs #f_lbls #f_regs #props 720 #pc #id #def_in #s #NEQ 727 #pc #id #def_in #s 728 lapply (b_graph_transform_program_fetch_internal_function … props 729 (pc_block … pc) id def_in) 730 @if_elim' #Hbl >Hbl normalize nodelta [ #H @H ] #G 721 731 #H @('bind_inversion H) * #id' #def_in' H 722 732 #EQfif … … 724 734 #H lapply (opt_eq_from_res ???? H) H 725 735 #EQstmt_at whd in ⊢ (??%%→?); #EQ destruct 726 cases ( b_graph_transform_program_fetch_internal_function … props … NEQEQfif)736 cases (G … EQfif) 727 737 #a * #b ** #H1 #H2 #H3 %{a} %{b} % 728 738 [ %{H1 H2} 729  % [2: % [2: % [% %]]  skip] @(multi_fetch_ok … H3 … EQstmt_at) ] 739  @(multi_fetch_ok … H3 … EQstmt_at) 740 ] 730 741 qed. 731 742 … … 743 754 let dst_genv ≝ joint_globalenv dst prog_out stacksizes in 744 755 ∀pc,id,def_in,s. 745 block_id … (pc_block … pc) ≠ 1 → 746 fetch_statement … src_genv pc = return 〈id, def_in, s〉 → 747 ∃init_data,def_out. 748 let bl ≝ pc_block pc in 749 fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧ 750 bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧ 751 let l ≝ point_of_pc dst pc in 752 ∃lbls,regs. 753 f_lbls bl l = lbls ∧ 754 f_regs bl l = regs ∧ 755 joint_if_entry … def_out = joint_if_entry … def_in ∧ 756 partial_partition … (f_lbls bl) ∧ 757 partial_partition … (f_regs bl) ∧ 758 (∀l.All … 759 (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧ 760 fresh_for_univ … lbl (joint_if_luniverse … def_out)) (f_lbls bl l)) ∧ 761 (∀l.All … 762 (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧ 763 fresh_for_univ … reg (joint_if_runiverse … def_out)) (f_regs bl l)) ∧ 764 match s with 765 [ sequential s' nxt ⇒ 766 let block ≝ 767 if eq_identifier … (joint_if_entry … def_in) l then 768 append_seq_list … (f_step … init_data l s') (added_prologue … init_data) 769 else 770 f_step … init_data l s' in 771 l ~❨block, l::lbls, regs❩~> nxt in joint_if_code … def_out 772  final s' ⇒ 773 l ~❨f_fin … init_data l s', l::lbls, regs❩~> it in joint_if_code … def_out 774  FCOND abs _ _ _ ⇒ Ⓧabs 775 ]. 756 if eqZb (block_id … (pc_block … pc)) (1) then 757 (fetch_internal_function … dst_genv (pc_block … pc) = 758 return 〈pre_main_id, pre_main_generator … dst prog_out〉) 759 else 760 (fetch_statement … src_genv pc = return 〈id, def_in, s〉 → 761 ∃init_data,def_out. 762 let bl ≝ pc_block pc in 763 fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧ 764 bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧ 765 let l ≝ point_of_pc dst pc in 766 let lbls ≝ f_lbls bl l in 767 let regs ≝ f_regs bl l in 768 partial_partition … (f_lbls bl) ∧ 769 partial_partition … (f_regs bl) ∧ 770 (∀l.All … 771 (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧ 772 fresh_for_univ … lbl (joint_if_luniverse … def_out)) (f_lbls bl l)) ∧ 773 (∀l.All … 774 (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧ 775 fresh_for_univ … reg (joint_if_runiverse … def_out)) (f_regs bl l)) ∧ 776 match s with 777 [ sequential s' nxt ⇒ 778 let block ≝ 779 if not_emptyb … (added_prologue … init_data) ∧ 780 eq_identifier … (joint_if_entry … def_in) l then 781 bret … [ ] 782 else 783 f_step … init_data l s' in 784 l ~❨block, l::lbls, regs❩~> nxt in joint_if_code … def_out 785  final s' ⇒ 786 l ~❨f_fin … init_data l s', l::lbls, regs❩~> it in joint_if_code … def_out 787  FCOND abs _ _ _ ⇒ Ⓧabs 788 ]). 776 789 #src #dst #stacksizes #data #prog_in 777 790 #init_regs #f_lbls #f_regs #props 778 #pc #id #def_in #s #NEQ 791 #pc #id #def_in #s 792 lapply (b_graph_transform_program_fetch_internal_function … props … (pc_block … pc) id def_in) 793 @if_elim' #Hbl >Hbl normalize nodelta 794 [ #H @H ] #G 779 795 #H @('bind_inversion H) * #id' #def_in' H 780 796 #EQfif … … 782 798 #H lapply (opt_eq_from_res ???? H) H 783 799 #EQstmt_at whd in ⊢ (??%%→?); #EQ destruct 784 cases ( b_graph_transform_program_fetch_internal_function … props … NEQEQfif)800 cases (G … EQfif) 785 801 #a * #b ** #H1 #H2 #H3 %{a} %{b} % 786 802 [ %{H1 H2} 787  % 788 [2: 789 % 790 [2: % 791 [% 792 [% 793 [% 794 [% 795 [% 796 [% 797 % 798  @(entry_eq … H3) 799 ] 800  @(partition_lbls … H3) 801 ] 802  @(partition_regs … H3) 803 ] 804  @(freshness_lbls … H3) 805 ] 806  @(freshness_regs … H3) 807 ] 808  @(multi_fetch_ok … H3 … EQstmt_at) 809 ] 810  811 ] 812  813 ] 803  %{(multi_fetch_ok … H3 … EQstmt_at)} 804 %{(freshness_regs … H3)} 805 %{(freshness_lbls … H3)} 806 %{(partition_regs … H3)} 807 @(partition_lbls … H3) 814 808 ] 815 809 qed.
Note: See TracChangeset
for help on using the changeset viewer.