Changeset 2600
- Timestamp:
- Feb 1, 2013, 12:13:22 PM (8 years ago)
- Location:
- src/Clight
- Files:
-
- 3 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/memoryInjections.ma
r2598 r2600 206 206 (* --------------------------------------------------------------------------- *) 207 207 208 (* An embedding is a function from block s to (blocks × offset). *)209 definition embedding ≝ block→ option (block × offset).208 (* An embedding is a function from block ids to (blocks × offset). *) 209 definition embedding ≝ Z → option (block × offset). 210 210 211 211 definition offset_plus : offset → offset → offset ≝ … … 224 224 match p with 225 225 [ mk_pointer pblock poff ⇒ 226 match E pblockwith226 match E (block_id pblock) with 227 227 [ None ⇒ None ? 228 228 | Some loc ⇒ … … 236 236 definition embedding_compatible : embedding → embedding → Prop ≝ 237 237 λE,E'. 238 ∀b:block. E b= None ? ∨239 E b = E' b.238 ∀b:block. E (block_id b) = None ? ∨ 239 E (block_id b) = E' (block_id b). 240 240 241 241 (* We parameterise the "equivalence" relation on values with an embedding. *) … … 258 258 ∀b1,off1,b2,off2,ty,v1. 259 259 valid_block m1 b1 → (* We need this because it is not provable from [load_value_of_type ty m1 b1 off1] when loading by-ref *) 260 E b1= Some ? 〈b2,off2〉 →260 E (block_id b1) = Some ? 〈b2,off2〉 → 261 261 load_value_of_type ty m1 b1 off1 = Some ? v1 → 262 262 (∃v2. load_value_of_type ty m2 b2 (offset_plus off1 off2) = Some ? v2 ∧ value_eq E v1 v2). … … 299 299 definition block_in_bounds_if_mapped : embedding → block → mem → mem → Prop ≝ 300 300 λE.λb.λm,m'. 301 match E bwith301 match E (block_id b) with 302 302 [ None ⇒ True 303 303 | Some loc ⇒ … … 308 308 ]. 309 309 310 311 310 (* Adapted from Compcert's Memory *) 312 311 definition non_aliasing : embedding → mem → Prop ≝ 313 312 λE,m. 314 313 ∀b1,b2,b1',b2',delta1,delta2. 315 b1 ≠ b2 → 316 (* block_region b1 = block_region b2 → *) (* let's be generous with this one *) 317 E b1 = Some ? 〈b1',delta1〉 → 318 E b2 = Some ? 〈b2',delta2〉 → 319 match block_decidable_eq b1' b2' with 320 [ inl Heq ⇒ 321 (* block_is_empty m b1' ∨ *) 314 b1 ≠ b2 → (* note that two blocks can be different only becuase of this region *) 315 E (block_id b1) = Some ? 〈b1',delta1〉 → 316 E (block_id b2) = Some ? 〈b2',delta2〉 → 317 (if eqZb (block_id b1') (block_id b2') then 318 (* block_is_empty m b1' ∨ *) 322 319 high_bound m b1 + (Zoo delta1) ≤ low_bound m b2 + (Zoo delta2) ∨ 323 320 high_bound m b2 + (Zoo delta2) ≤ low_bound m b1 + (Zoo delta1) ∨ 324 321 block_is_empty m b1 ∨ 325 322 block_is_empty m b2 326 | inr Hneq ⇒ True327 ].323 else 324 True). 328 325 329 326 … … 335 332 mi_inj : load_sim_ptr E m1 m2; 336 333 (* Invalid blocks are not mapped *) 337 mi_freeblock : ∀b. ¬ (valid_block m1 b) → E b= None ?;334 mi_freeblock : ∀b. ¬ (valid_block m1 b) → E (block_id b) = None ?; 338 335 (* Valid pointers are mapped to valid pointers *) 339 336 mi_valid_pointers : ∀p,p'. … … 344 341 mi_nodangling : ∀b,b',o'. E b = Some ? 〈b',o'〉 → valid_block m2 b'; 345 342 (* Regions are preserved *) 346 mi_region : ∀b,b',o'. E b= Some ? 〈b',o'〉 → block_region b = block_region b';343 mi_region : ∀b,b',o'. E (block_id b) = Some ? 〈b',o'〉 → block_region b = block_region b'; 347 344 (* sub-blocks do not overlap (non-aliasing property) *) 348 345 mi_nonalias : non_aliasing E m1; … … 614 611 ∀m,m',z1,z2,r,new_block. 615 612 alloc m z1 z2 r=〈m',new_block〉 → 616 ∀p. (pblock p) ≠ (pi1 … new_block) → 617 block_region (pblock p) = block_region (pi1 … new_block) → 613 ∀p. block_id (pblock p) ≠ block_id (pi1 … new_block) → 618 614 valid_pointer m' p = true → 619 615 valid_pointer m p = true. … … 621 617 cases m #cont #next #Hnext 622 618 whd in ⊢ ((??%%) → ?); 623 #Heq destruct (Heq) * #b #o #Hneq #H region #Hvalid619 #Heq destruct (Heq) * #b #o #Hneq #Hvalid 624 620 @valid_pointer_of_Prop lapply (valid_pointer_to_Prop … Hvalid) 625 621 -Hvalid … … 629 625 whd in match (update_block ?????); 630 626 whd in match (update_block ?????); 631 >(not_eq_block … Hneq) normalize nodelta 627 cut (b ≠ (mk_block r next)) 628 [ @(eq_block_elim … b (mk_block r next)) #H destruct try // 629 @False_ind 630 @(absurd … (refl ??) Hneq) ] #Hneqb 631 >(not_eq_block … Hneqb) normalize nodelta 632 632 #HA #HB % [ % ] try assumption 633 cases b in Hneq Hregion Hblock_id; #r' #id * #Hnext_not_id #Hregion destruct 634 cut (next ≠ id) 635 [ % #H destruct @Hnext_not_id @refl ] 636 #Hneq #Hlt cut (id ≤ next) 633 cases b in Hneqb Hneq Hblock_id; #r' #id * #Hnext_not_id #Hneq 634 #Hlt cut (id ≤ next) 637 635 [ /3 by monotonic_Zle_Zpred, Zlt_to_Zle/ ] 638 #Hle @Zle_split try @Hle @ sym_neq @Hneq636 #Hle @Zle_split try @Hle @Hneq 639 637 qed. 640 638 … … 681 679 #bev normalize nodelta 682 680 whd in match (shift_pointer ???); >Hind try // 681 qed. 682 683 lemma alloc_load_value_of_type_conservation : 684 ∀m,m',z1,z2,r,new_block. 685 alloc m z1 z2 r = 〈m', new_block〉 → 686 ∀block,offset. 687 valid_block m block → 688 ∀ty. load_value_of_type ty m block offset = 689 load_value_of_type ty m' block offset. 690 #m #m' #z1 #z2 #r #new_block #Halloc #block #offset #Hvalid 691 #ty cases ty 692 [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain 693 | #structname #fieldspec | #unionname #fieldspec | #id ] 694 try // 695 whd in match (load_value_of_type ????) in ⊢ (??%%); 696 >(alloc_loadn_conservation … Halloc … Hvalid) @refl 683 697 qed. 684 698 … … 704 718 #Hload normalize in ⊢ ((???%) → ?); #Haccess 705 719 [ 1,6,7: normalize in Hload; destruct (Hload) 706 | 2,3,8: whd in match (load_value_of_type ????); 707 whd in match (load_value_of_type ????); 720 | 2,3,8: 708 721 lapply (load_by_value_success_valid_block … Haccess Hload) 709 722 #Hvalid_block 710 whd in match (load_value_of_type ????) in Hload; 711 <(alloc_loadn_conservation … Halloc … Hvalid_block) 712 @Hload 723 <(alloc_load_value_of_type_conservation … Halloc … Hvalid_block) 724 assumption 713 725 | 4,5: whd in match (load_value_of_type ????) in Hload ⊢ %; @Hload ] 714 726 | @(mi_freeblock … Hmemory_inj) … … 733 745 | #b lapply (mi_nowrap … Hmemory_inj b) 734 746 whd in ⊢ (% → %); 735 lapply (mi_nodangling … Hmemory_inj b)736 cases (E b) normalize nodelta try //747 lapply (mi_nodangling … Hmemory_inj (block_id b)) 748 cases (E (block_id b)) normalize nodelta try // 737 749 * #B #OFF normalize nodelta #Hguard 738 750 * * #H1 #H2 #Hinbounds @conj try @conj try assumption 739 751 @(eq_block_elim … new_block B) 740 [ #H destruct try //741 752 [ #H <H assumption 753 | #H cases m2 in Halloc H2; #contents #nextblock #notnull 742 754 whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) * 743 755 >unfold_low_bound >unfold_high_bound #HA #HB … … 749 761 ] qed. 750 762 751 752 (* TODO: these axioms are not enough for memory injections. We need the updated embedding as a byproduct753 * of the allocation. *)754 755 lemma block_neq_elim :756 ∀b1,b2. b1 ≠ b2 →757 (block_id b1 ≠ block_id b2 ∧ block_region b1 = block_region b2) ∨758 (block_id b1 = block_id b2 ∧ block_region b1 ≠ block_region b2) ∨759 (block_id b1 ≠ block_id b2 ∧ block_region b1 ≠ block_region b2).760 * #r #id * #r' #id'761 cases r cases r'762 @(eqZb_elim … id id')763 #H1 #H2764 [ 1,7: destruct @False_ind @(absurd … (refl ??) H2) ]765 try /4 by or_introl, or_intror, conj/766 destruct767 [ %1 %2 @conj // % #H destruct768 | %2 @conj try @H1 % #H destruct769 | %1 %2 @conj // % #H destruct770 | %2 @conj try @H1 % #H destruct ]771 qed.772 773 763 (* Allocating in m1 such that the resulting block has no image in m2 preserves 774 764 the injection. This is lemma 67 for Leroy&Blazy. The proof should proceed as 775 in Blazy & Leroy. Careful of using the mi_embedding hypothesis to rule out776 absurd cases. *)765 in Blazy & Leroy. Notice that we must consider blocks with different regions but 766 same id as equal. *) 777 767 lemma alloc_memory_inj_m1 : 778 768 ∀E:embedding. … … 780 770 ∀H:memory_inj E m1 m2. 781 771 alloc m1 z1 z2 r = 〈m1', new_block〉 → 782 memory_inj (λx. if eq_block x (pi1 … new_block) then None ? else E x) m1' m2 ∧ 783 embedding_compatible E (λx. if eq_block x (pi1 … new_block) then None ? else E x). 784 @cthulhu 785 qed. (* XXX finish this. *) 786 (* 772 memory_inj (λx. if eqZb (block_id (pi1 … new_block)) x then None ? else E x) m1' m2 ∧ 773 embedding_compatible E (λx. if eqZb (block_id (pi1 … new_block)) x then None ? else E x). 787 774 #E #m1 #m2 #m1' #z1 #z2 #r * #new_block #Hregion_eq #Hinj #Halloc 788 cut (E new_block= None ?)775 cut (E (block_id new_block) = None ?) 789 776 [ @(mi_freeblock … Hinj) cases m1 in Hinj Halloc; #contents #next #Hpos #Hinj whd in ⊢ ((??%%) → ?); 790 777 #Heq destruct (Heq) % #H whd in H; @(absurd … H (irreflexive_Zlt … next)) ] 791 #Hempty % 792 [ 2: whd #b @(eq_block_elim … b new_block) try // #Heq destruct (Heq) >Hempty %1 @refl ] 778 #Hempty 779 cut (embedding_compatible E 780 (λx:Z. 781 if eqZb (block_id new_block) x 782 then None (block×offset) 783 else E x )) 784 [ whd #b @(eqZb_elim … (block_id new_block) (block_id b)) normalize nodelta try // #Heq <Heq %1 @Hempty ] 785 #Hembedding_compatible @conj try assumption 793 786 % 794 787 [ whd #b1 #off1 #b2 #off2 #ty #v1 795 788 @(eq_block_elim … b1 new_block) 796 [ #Heq destruct #_ whd in ⊢ ((??%?) → ?); >eq _block_b_bnormalize nodelta789 [ #Heq destruct #_ whd in ⊢ ((??%?) → ?); >eqZb_z_z normalize nodelta 797 790 #Habsurd destruct ] 798 791 #Hneq #Hvalid 799 whd in ⊢ ((??%?) → ?); >(not_eq_block … Hneq) normalize nodelta 800 #Hembed cases (some_inversion ????? Hembed) * #b1' #off' * #Hembed 801 normalize nodelta #Heq destruct (Heq) 802 lapply (block_neq_elim … Hneq) 803 * 804 [ 2: * #Hid_neq #Hregion_neq 805 lapply (alloc_valid_pointer_conservation … Halloc (mk_pointer b1 off1) … Hneq) 806 *) 807 792 whd in ⊢ ((??%?) → ?); 793 @(eqZb_elim … (block_id new_block) (block_id b1)) 794 normalize nodelta 795 [ #Heq #Habsurd destruct (Habsurd) ] 796 #Hneq_id 797 #Hembed #Hload 798 lapply (alloc_valid_pointer_conservation … Halloc (mk_pointer b1 off1) (sym_neq ??? Hneq_id) Hvalid) 799 #Hvalid' 800 cut (valid_block m1 b1) 801 [ cases (valid_pointer_to_Prop … Hvalid') * #Hvalid_block #_ #_ @Hvalid_block ] 802 #Hvalid_block 803 lapply (alloc_load_value_of_type_conservation … Halloc … off1 … Hvalid_block ty) 804 #Heq <Heq in Hload; #Hload 805 lapply (mi_inj … Hinj … Hvalid' … Hembed … Hload) * #v2 * #Hload2 #Hveq2 806 %{v2} @conj try assumption 807 @(embedding_compatibility_value_eq … Hveq2) assumption 808 | #b #Hnot_valid @(eqZb_elim … (block_id new_block) (block_id b)) 809 normalize nodelta 810 [ #Heq @refl 811 | #Hneq @(mi_freeblock … Hinj) % #Hvalid cases Hnot_valid #H @H 812 @(alloc_valid_block_conservation … Halloc) assumption ] 813 | #p #p' lapply (mi_valid_pointers … Hinj p p') 814 cases p #b #o cases p' #b' #o' normalize nodelta #Hvalidptr #Hvalid1' 815 whd in ⊢ ((??%%) → ?); 816 @(eqZb_elim … (block_id new_block) (block_id b)) normalize nodelta 817 [ #Heq #Habsurd destruct ] 818 #Hneq #Hembed 819 lapply (alloc_valid_pointer_conservation … Halloc (mk_pointer b o) (sym_neq ??? Hneq) Hvalid1') 820 #Hvalid1 821 @(Hvalidptr Hvalid1 Hembed) 822 | #b #b' #o' @(eqZb_elim … (block_id new_block) b) 823 [ #Heq normalize nodelta #Habsurd destruct (Habsurd) ] 824 normalize nodelta #Henq 825 @(mi_nodangling … Hinj) 826 | #b #b' #o' @(eqZb_elim … (block_id new_block) (block_id b)) 827 [ #Heq normalize nodelta #Habsurd destruct (Habsurd) ] 828 #Hneq @(mi_region … Hinj) 829 | whd #b1 #b2 #b1' #b2' #delta1 #delta2 #Hneq 830 @(eqZb_elim … (block_id new_block) (block_id b1)) 831 normalize nodelta 832 [ #Heq #Habsurd destruct (Habsurd) ] 833 #Hneq1 #Hembed1 834 @(eqZb_elim … (block_id new_block) (block_id b2)) 835 normalize nodelta 836 [ #Heq #Habsurd destruct (Habsurd) ] 837 #Hneq2 #Hembed2 838 @(eqZb_elim … (block_id b1') (block_id b2')) normalize nodelta try // 839 #Heq 840 lapply (mi_nonalias … Hinj … b1 b2 b1' b2' delta1 delta2 Hneq Hembed1 Hembed2) >Heq 841 >eqZb_z_z normalize nodelta 842 cases m1 in Halloc; #contents #next #Hnext 843 >unfold_high_bound >unfold_low_bound 844 >unfold_high_bound >unfold_low_bound 845 >unfold_high_bound >unfold_low_bound 846 >unfold_high_bound >unfold_low_bound 847 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) 848 cut (eq_block b1 (mk_block r next) = false) 849 [ whd in ⊢ (??%%); 850 >(eqZb_false … (sym_neq ??? Hneq1)) 851 cases (eq_region ??) @refl ] 852 cut (eq_block b2 (mk_block r next) = false) 853 [ whd in ⊢ (??%%); 854 >(eqZb_false … (sym_neq ??? Hneq2)) 855 cases (eq_region ??) @refl ] 856 #Heq_block_2 857 #Heq_block_1 858 * [ * [ * | ] | ] 859 whd in match (update_block ?????); 860 >Heq_block_1 normalize nodelta 861 whd in match (update_block ?????); 862 >Heq_block_2 normalize nodelta 863 #H 864 try /4 by or_introl, or_intror, conj/ 865 [ %1 %2 whd whd in H; 866 >unfold_high_bound 867 whd in match (update_block ?????); 868 >unfold_low_bound 869 whd in match (update_block ?????); 870 >Heq_block_1 normalize nodelta @H 871 | %2 whd whd in H; 872 >unfold_high_bound 873 whd in match (update_block ?????); 874 >unfold_low_bound 875 whd in match (update_block ?????); 876 >Heq_block_1 >Heq_block_2 @H 877 ] 878 | #b whd @(eqZb_elim … (block_id new_block) (block_id b)) normalize nodelta try // 879 #Hneq lapply (mi_nowrap … Hinj b) whd in ⊢ (% → ?); 880 cases (E (block_id b)) normalize nodelta try // 881 * #bb #oo normalize nodelta 882 * * * #HA #HB * #HC #HD #HE @conj try @conj 883 try @conj 884 lapply HE -HE 885 lapply HD -HD 886 lapply HC -HC 887 lapply HB -HB 888 lapply HA -HA 889 >unfold_low_bound >unfold_low_bound [ >unfold_low_bound ] 890 >unfold_high_bound >unfold_high_bound [ 2,5: >unfold_high_bound ] 891 cases m1 in Halloc; #cont #next #Hnext 892 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) try // 893 whd in match (update_block ?????); 894 cut (eq_block b (mk_block r next) = false) 895 [ 1,3,5: whd in ⊢ (??%%); 896 >(eqZb_false … (sym_neq ??? Hneq)) 897 cases (eq_region ??) @refl 898 | 2,4,6: #Heq_block >Heq_block // ] 899 ] qed. 900 901 808 902 809 903 (* Embed a fresh block inside an unmapped portion of the target block. … … 820 914 z2 + Zoo delta ≤ high_bound m2 b2 → 821 915 (∀b,b',delta'. b ≠ (pi1 … new_block) → 822 E b= Some ? 〈b', delta'〉 →916 E (block_id b) = Some ? 〈b', delta'〉 → 823 917 high_bound m1 b + (Zoo delta') ≤ z1 + (Zoo delta) ∨ 824 918 z2 + (Zoo delta) ≤ low_bound m1 b + (Zoo delta')) → 825 919 memory_inj E m1 m2 → 826 memory_inj (λx. if eq _block x (pi1 … new_block)then Some ? 〈b2, delta〉 else E x) m1' m2.920 memory_inj (λx. if eqZb (block_id (pi1 … new_block)) x then Some ? 〈b2, delta〉 else E x) m1' m2. 827 921 828 922 (* -------------------------------------- *) … … 875 969 load_sim_ptr E m1 m2 → 876 970 ∀b. free m2 b = m2' → 877 (∀b1,delta. E b1= Some ? 〈b, delta〉 → ¬ (valid_block m1 b1) ∨ block_is_empty m1 b1) →971 (∀b1,delta. E (block_id b1) = Some ? 〈b, delta〉 → ¬ (valid_block m1 b1) ∨ block_is_empty m1 b1) → 878 972 load_sim_ptr E m1 m2'. 879 973 #E #m1 #m2 #m2' #Hsim #b #Hfree #Hunmapped … … 960 1054 #b1 #b2 #b1' #b2' #delta1 #delta2 #Hneq 961 1055 #Hembed1 #Hembed2 962 cases (block_decidable_eq ??) normalize nodelta1056 @(eqZb_elim … (block_id b1') (block_id b2')) normalize nodelta 963 1057 [ 2: try // ] 964 #Hblocks_eq destruct (Hblocks_eq) 1058 #Hblocks_eq 1059 lapply Hembed2 -Hembed2 965 1060 lapply Hembed1 -Hembed1 966 lapply Hembed2 -Hembed2 967 generalize in match b2'; 968 #target #Hembed2 #Hembed1 1061 lapply Hblocks_eq -Hblocks_eq 1062 cases b1' #r1' #bid1' 1063 cases b2' #r2' #bid2' 1064 #Heq destruct (Heq) 1065 generalize in match bid2'; 1066 #target #Hembed1 #Hembed2 969 1067 lapply (mi_nonalias … Hinj … Hneq Hembed1 Hembed2) 970 cases (block_decidable_eq ??) 971 [ 2: * #Habsurd @False_ind @Habsurd @refl ] #Hrefl 1068 >eqZb_z_z normalize nodelta 972 1069 normalize nodelta <Hfree 973 1070 @(eq_block_elim … b1 b) … … 1015 1112 | @(free_non_aliasing_m1 … Hinj … Hfree) 1016 1113 | #bb whd lapply (Himplementable bb) whd in ⊢ (% → ?); 1017 cases (E bb) normalize nodelta try //1114 cases (E (block_id bb)) normalize nodelta try // 1018 1115 * #BLO #DELTA normalize nodelta * * #HA #HB #HC @conj try @conj 1019 1116 try // … … 1043 1140 memory_inj E m1 m2 → 1044 1141 ∀b. free m2 b = m2' → 1045 (∀b1,delta. E b1= Some ? 〈b, delta〉 →1142 (∀b1,delta. E (block_id b1) = Some ? 〈b, delta〉 → 1046 1143 (¬ (valid_block m1 b1)) ∨ block_is_empty m1 b1) → 1047 1144 memory_inj E m1 m2'. … … 1051 1148 [ @(free_load_sim_ptr_m2 … Hload_sim … Hfree) #b1 #delta #Hembed 1052 1149 @(b_not_mapped … b1 delta Hembed) 1053 | @Hfreeblock 1150 | @Hfreeblock 1054 1151 | * #bp #op #p' #Hp_valid #Hptr_trans 1055 1152 @(eq_block_elim … (pblock p') b) … … 1074 1171 | @Hregion 1075 1172 | #bb lapply (Himpl bb) 1076 whd in ⊢ (% → %); cases (E bb) normalize nodelta try //1173 whd in ⊢ (% → %); cases (E (block_id bb)) normalize nodelta try // 1077 1174 * #BLO #OFF normalize nodelta * * destruct (Hfree) 1078 1175 #Hbb #HBLO #Hbound whd in match (free ??); @conj try @conj try @conj try assumption … … 1094 1191 memory_inj E m1 m2 → 1095 1192 ∀blocklist,b2. 1096 (∀b1,delta. E b1= Some ? 〈b2, delta〉 → meml ? b1 blocklist) →1193 (∀b1,delta. E (block_id b1) = Some ? 〈b2, delta〉 → meml ? b1 blocklist) → 1097 1194 free m2 b2 = m2' → 1098 1195 free_list m1 blocklist = m1' → … … 1135 1232 ] 1136 1233 ] 1137 ] qed. 1234 ] qed. 1138 1235 1139 1236 (* ---------------------------------------------------------- *) … … 1230 1327 memory_inj E mA mB → 1231 1328 ∀blo. storen mB (mk_pointer blo wo) l = Some ? mC → 1232 ∀b1,delta. E b1= Some ? 〈blo,delta〉 →1329 ∀b1,delta. E (block_id b1) = Some ? 〈blo,delta〉 → 1233 1330 high_bound mA b1 + Zoo delta < Zoo wo → 1234 1331 ∀ty,off. … … 1308 1405 memory_inj E mA mB → 1309 1406 ∀blo. storen mB (mk_pointer blo wo) l = Some ? mC → 1310 ∀b1,delta. E b1= Some ? 〈blo,delta〉 →1407 ∀b1,delta. E (block_id b1) = Some ? 〈blo,delta〉 → 1311 1408 Zoo wo < low_bound mA b1 + Zoo delta → 1312 1409 ∀ty,off. … … 1325 1422 ∀block2. ∀i : offset. ∀ty : type. 1326 1423 (∀block1,delta. 1327 E block1= Some ? 〈block2, delta〉 →1424 E (block_id block1) = Some ? 〈block2, delta〉 → 1328 1425 (high_bound mA block1 + (Zoo delta) < (Zoo i)) ∨ (Zoo i + (sizeof ty) ≤ (low_bound mA block1 + (Zoo delta)))) → 1329 1426 ∀v.store_value_of_type ty mB block2 i v = Some ? mC → … … 1381 1478 ∀block2. ∀i : offset. ∀ty : type. 1382 1479 (∀block1,delta. 1383 E block1= Some ? 〈block2, delta〉 →1480 E (block_id block1) = Some ? 〈block2, delta〉 → 1384 1481 (high_bound mA block1 + (Zoo delta) < (Zoo i)) ∨ (Zoo i + (sizeof ty) ≤ (low_bound mA block1 + (Zoo delta)))) → 1385 1482 ∀v.store_value_of_type ty mB block2 i v = Some ? mC → … … 1411 1508 >(Hnext_eq) try // 1412 1509 | #b lapply (mi_nowrap … Hinj b) whd in ⊢ (% → %); 1413 cases (E b) try //1510 cases (E (block_id b)) try // 1414 1511 * #BLO #OFF normalize nodelta * * 1415 1512 #Hb #HBLO #Hbound try @conj try @conj try assumption … … 1473 1570 ∀E,m1,m2. 1474 1571 memory_inj E m1 m2 → 1475 ∀b1,b2,delta. E b1= Some ? 〈b2,delta〉 →1572 ∀b1,b2,delta. E (block_id b1) = Some ? 〈b2,delta〉 → 1476 1573 ∀v1,v2. value_eq E v1 v2 → 1477 1574 ∀i,m1',ty. storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1'→ … … 1542 1639 ∀E,m1,m2. 1543 1640 memory_inj E m1 m2 → 1544 ∀b1,b2,delta. E b1= Some ? 〈b2,delta〉 →1641 ∀b1,b2,delta. E (block_id b1) = Some ? 〈b2,delta〉 → 1545 1642 ∀v1,v2. value_eq E v1 v2 → 1546 1643 ∀i,m1',ty. storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1'→ … … 1565 1662 ∀Hinj:memory_inj E m1 m2. 1566 1663 ∀v1,v2. value_eq E v1 v2 → 1567 ∀b1,b2,delta. E b1= Some ? 〈b2, delta〉 →1664 ∀b1,b2,delta. E (block_id b1) = Some ? 〈b2, delta〉 → 1568 1665 ∀ty,i,m1'. 1569 1666 ast_typ_consistent_with_value ty v1 → … … 1653 1750 ∀Hinj:memory_inj E m1 m2. 1654 1751 ∀v1,v2. value_eq E v1 v2 → 1655 ∀b1,b2,delta. E b1= Some ? 〈b2, delta〉 →1752 ∀b1,b2,delta. E (block_id b1) = Some ? 〈b2, delta〉 → 1656 1753 ∀ty,i,m1'. 1657 1754 type_consistent_with_value ty v1 → … … 1673 1770 ∀Hinj:memory_inj E m1 m2. 1674 1771 ∀ty,b,i,v. 1675 E b= None ? →1772 E (block_id b) = None ? → 1676 1773 store_value_of_type ty m1 b i v = Some ? m1' → 1677 1774 load_sim_ptr E m1' m2. … … 1723 1820 ∀Hinj:memory_inj E m1 m2. 1724 1821 ∀ty,b,i,v. 1725 E b= None ? →1822 E (block_id b) = None ? → 1726 1823 store_value_of_type ty m1 b i v = Some ? m1' → 1727 1824 memory_inj E m1' m2. … … 1752 1849 | #bb whd 1753 1850 lapply (mi_nowrap ??? Hinj bb) whd in ⊢ (% → ?); 1754 cases (E bb) normalize nodelta try // * #bb' #off1851 cases (E (block_id bb)) normalize nodelta try // * #bb' #off 1755 1852 normalize nodelta 1756 1853 whd in match (block_implementable_bv ??); … … 1763 1860 >HA >HB // 1764 1861 ] 1765 ] qed. 1862 ] qed. 1766 1863 1767 1864 (* ------------------------------------------------------------------------- *) … … 1855 1952 @(ex_intro … (conj … (refl …) ?)) 1856 1953 @vptr_eq whd in match (pointer_translation ??); 1857 cases (E b1') in Hembed;1954 cases (E (block_id b1')) in Hembed; 1858 1955 [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) 1859 1956 | 2: * #block #offset normalize nodelta #Heq destruct (Heq) … … 1897 1994 @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %; 1898 1995 elim p1 in Hembed; #b1 #o1 normalize nodelta 1899 cases (E b1)1996 cases (E (block_id b1)) 1900 1997 [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) 1901 1998 | 2: * #block #offset normalize nodelta #Heq destruct (Heq) … … 1996 2093 @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %; 1997 2094 elim p1 in Hembed; #b1 #o1 normalize nodelta 1998 cases (E b1)2095 cases (E (block_id b1)) 1999 2096 [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) 2000 2097 | 2: * #block #offset normalize nodelta #Heq destruct (Heq) … … 2012 2109 elim p1' #b1' #off1' whd in ⊢ (% → % → ?); #Hpblock1_eq destruct (Hpblock1_eq) 2013 2110 whd in ⊢ ((??%?) → (??%?) → ?); 2014 cases (E b1') normalize nodelta2111 cases (E (block_id b1')) normalize nodelta 2015 2112 [ 1: #Habsurd destruct (Habsurd) ] 2016 2113 * #dest_block #dest_off normalize nodelta … … 2418 2515 lapply (mi_nowrap … Hinj bq1) 2419 2516 whd in ⊢ (% → ?); 2420 cases (E bq1) normalize nodelta2517 cases (E (block_id bq1)) normalize nodelta 2421 2518 [ #_ #Habsurd destruct ] 2422 2519 * #BLO #OFF normalize nodelta * * … … 2437 2534 lapply (mi_nowrap … Hinj bp1) whd in ⊢ (% → ?); 2438 2535 lapply (mi_nowrap … Hinj bq1) whd in ⊢ (% → ?); 2439 cases (E bq1) [ 1: #_ #_ #_ normalize nodelta #Habsurd destruct (Habsurd) ] 2536 lapply (mi_region … Hinj bq1) 2537 lapply (mi_region … Hinj bp1) 2538 cases (E (block_id bq1)) [ 1: #_ #_ #_ #_ #_ normalize nodelta #Habsurd destruct (Habsurd) ] 2440 2539 * #BLOq #DELTAq normalize nodelta 2441 cases (E bp1) [ 1: normalize nodelta #_ #_ #_ #_ #Habsurd destruct (Habsurd) ] 2442 * #BLOp #DELTAp normalize nodelta #Hnowrap1 #Hnowrap2 #H #Heq1 #Heq2 destruct 2540 cases (E (block_id bp1)) [ 1: normalize nodelta #_ #_ #_ #_ #_ #_ #Habsurd destruct (Habsurd) ] 2541 * #BLOp #DELTAp normalize nodelta #Hregion1 #Hregion2 #Hnowrap1 #Hnowrap2 #H #Heq1 #Heq2 destruct 2542 lapply (Hregion1 … (refl ??)) lapply (Hregion2 … (refl ??)) -Hregion1 -Hregion2 2543 #Hregion2 #Hregion1 2443 2544 cases op 2444 2545 whd in ⊢ ((??%?) → ?); #H' destruct (H') … … 2455 2556 lapply (valid_pointer_to_Prop … Hvalid') 2456 2557 * * #_ #Hlowq #Hhighq * * #_ #Hlowp #Hhighp 2457 >eq _block_b_b normalize nodelta2558 >eqZb_z_z >eq_block_b_b normalize nodelta 2458 2559 * 2459 2560 [ 2,4: whd in ⊢ (% → ?); #Habsurd @False_ind -
src/Clight/toCminorCorrectnessExpr.ma
r2591 r2600 34 34 match find_symbol ? (ge_cl cminv) id with 35 35 [ None ⇒ True 36 | Some cl_blo ⇒ E cl_blo = Some ? 〈cl_blo, zero_offset〉 36 | Some cl_blo ⇒ 37 (* global symbols are mapped to themselves. Perhaps too strong. *) 38 E (block_id cl_blo) = Some ? 〈cl_blo, zero_offset〉 37 39 ] 38 40 | Some cl_blo ⇒ … … 42 44 match vtype with 43 45 [ Stack n ⇒ 44 E cl_blo= Some ? 〈sp, mk_offset (repr I16 n)〉46 E (block_id cl_blo) = Some ? 〈sp, mk_offset (repr I16 n)〉 45 47 | Local ⇒ 46 48 ∀v. load_value_of_type type m cl_blo zero_offset = Some ? v → … … 2210 2212 @conj whd in match (Eapp ??); >(append_nil ? trace) try @refl 2211 2213 %4 whd in Hptr_translate:(??%?) ⊢ (??%?); 2212 cases (E cl_blo) in Hptr_translate; normalize nodelta2214 cases (E (block_id cl_blo)) in Hptr_translate; normalize nodelta 2213 2215 [ #H destruct (H) ] 2214 2216 * #BL #OFF normalize nodelta #Heq destruct (Heq) … … 2222 2224 >(commutative_addition_n … (repr I16 field_off) (offv OFF)) 2223 2225 >(associative_addition_n ? (offv off)) 2224 @refl 2226 @refl 2225 2227 | 2: normalize in Hexec_lvalue:(???%); destruct (Hexec_lvalue) 2226 2228 cases (Hind … Hexpr_vars Htranslate_addr ??? Hyp_present Hexec_lvalue_ind) -
src/Clight/toCminorOps.ma
r2588 r2600 192 192 lapply H1 lapply H2 -H1 -H2 193 193 whd in ⊢ ((??%?) → (??%?) → ?); 194 cases (E b2) normalize nodelta194 cases (E (block_id b2)) normalize nodelta 195 195 [ #Habsurd destruct ] 196 196 * #bx #ox normalize nodelta #Heq1 #Heq2 destruct
Note: See TracChangeset
for help on using the changeset viewer.