Changeset 2468 for src/Clight/MemProperties.ma
 Timestamp:
 Nov 15, 2012, 6:12:57 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/MemProperties.ma
r2448 r2468 144 144 #m1 #m2 #Hloadsim #ptr #ty #v 145 145 cases ty 146 [ 1:  2: #sz #sg  3: # fsz  4: #ptrty  5: #arrayty #arraysz  6: #argsty #retty147  7: #sid #fields  8: #uid #fields  9: #cptr_id ]146 [ 1:  2: #sz #sg  3: #ptrty  4: #arrayty #arraysz  5: #argsty #retty 147  6: #sid #fields  7: #uid #fields  8: #cptr_id ] 148 148 whd in match (load_value_of_type ????) in ⊢ ((??%?) → (??%?)); 149 [ 1, 7,8: #Habsurd destruct (Habsurd)150  5,6: #H @H151  2,3, 4,9:149 [ 1,6,7: #Habsurd destruct (Habsurd) 150  4,5: #H @H 151  2,3,8: 152 152 generalize in match (mk_pointer (pblock ptr) (poff ptr)); 153 153 elim (typesize ?) 154 [ 1,3,5 ,7: #p #H @H155  2,4,6,8: #n' #Hind #p154 [ 1,3,5: #p #H @H 155  *: #n' #Hind #p 156 156 lapply (load_sim_loadn … Hloadsim (S n') p) 157 157 cases (loadn m1 p (S n')) normalize nodelta … … 200 200 cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high (contents (pblock ptr)))) 201 201 normalize nodelta try // #Habsurd destruct (Habsurd) 202 qed. 203 204 lemma bestorev_to_valid_pointer_after : ∀m,ptr,v,res. bestorev m ptr v = Some ? res → valid_pointer res ptr = true. 205 * #contents #next #nextpos #ptr #v #res 206 whd in match (bestorev ???); 207 whd in match (valid_pointer ??); #Hvalid 208 cases (if_opt_inversion ???? Hvalid) #Hnextblock normalize nodelta Hvalid #Hvalid 209 cases (if_opt_inversion ???? Hvalid) #Hin_bounds #Heq destruct (Heq) normalize 210 >Hnextblock normalize nodelta cases (block_region (pblock ptr)) normalize nodelta 211 >eqZb_z_z normalize nodelta @Hin_bounds 202 212 qed. 203 213 … … 591 601 ] qed. 592 602 603 (* extension of [bestorev_to_valid_pointer] to storen *) 604 lemma storen_to_valid_pointer : 605 ∀data,xd,m,ptr,m'. storen m ptr (xd::data) = Some ? m' → 606 (∀b.low (blocks m' b) = low (blocks m b) ∧ 607 high (blocks m' b) = high (blocks m b)) ∧ 608 nextblock m' = nextblock m ∧ 609 valid_pointer m ptr = true ∧ 610 valid_pointer m' ptr = true. 611 #data elim data 612 [ 1: #xd #m #ptr #res #Hstoren whd in Hstoren:(??%?); 613 cases (some_inversion ????? Hstoren) #m' * #Hbestorev #Hstoren' 614 normalize in Hstoren'; destruct (Hstoren') 615 lapply (mem_bounds_invariant_after_bestorev … Hbestorev) * * * * #HA #HB #HC #HD #HF 616 lapply (bestorev_to_valid_pointer … Hbestorev) #Hvalid_ptr @conj try @conj try @conj try assumption 617 @(bestorev_to_valid_pointer_after … Hbestorev) 618  2: #hd #tl #Hind #xd #m #ptr #res whd in match (storen ???); #Hstoren 619 cases (some_inversion ????? Hstoren) #m' * #Hbestorev #Hstoren' Hstoren 620 whd in match (shift_pointer ???) in Hstoren'; 621 lapply (bestorev_to_valid_pointer … Hbestorev) #H @conj try @conj try @conj try // 622 lapply (Hind … Hstoren') * * * #Hbounds #Hnext #Hvalid1 #Hvalid2 623 lapply (mem_bounds_invariant_after_bestorev … Hbestorev) * * * * #HA #HB #HC #HD #HF 624 [ 1: #b @conj cases (Hbounds b) #HG #HH cases (HB b) #HI #HJ try // 625  2: >Hnext >HA @refl ] 626 @valid_pointer_of_Prop @conj try @conj try @conj 627 cases (Hbounds (pblock ptr)) #HG #HH cases (HB (pblock ptr)) #HI #HJ 628 [ 2: cases HC #Hlow #_ whd in match (low_bound ??); 629 whd in match (Z_of_offset ?) in Hlow; 630 >HG >HI @Hlow 631  3: cases HC #_ #Hhigh whd in match (high_bound ??); >HH >HJ @Hhigh ] 632 lapply (valid_pointer_to_Prop … Hvalid2) * * #Hnext #Hlow #Hhigh // 633 ] qed. 634 635 lemma fe_to_be_values_nonempty : ∀typ,v. ∃hd,tl. fe_to_be_values typ v = hd :: tl. 636 * 637 [ 2: * /3 by ex_intro/ * #i 638 [ 1: whd in match (fe_to_be_values ??); normalize nodelta normalize 639 lapply (vsplit_eq … 7 0 … i) * #v1 * #v2 #Heq 640 <(vsplit_prod … Heq) normalize nodelta /3 by ex_intro/ 641  2: whd in match (fe_to_be_values ??); normalize nodelta normalize 642 lapply (vsplit_eq … 7 8 … i) * #va * #vb #Heq 643 <(vsplit_prod … Heq) normalize nodelta 644 lapply (vsplit_eq … 7 0 … vb) * #vba * #vbb #Heq' 645 /3 by ex_intro/ 646  3: whd in match (fe_to_be_values ??); normalize nodelta normalize 647 lapply (vsplit_eq … 7 24 … i) * #va * #vb #Heq 648 <(vsplit_prod … Heq) normalize nodelta 649 lapply (vsplit_eq … 7 16 … vb) * #vba * #vbb #Heq' 650 <(vsplit_prod … Heq') normalize nodelta 651 lapply (vsplit_eq … 7 8 … vbb) * #vbba * #vbbb #Heq'' 652 <(vsplit_prod … Heq'') normalize nodelta 653 lapply (vsplit_eq … 7 0 … vbbb) * #vbx * #vby #Heq''' 654 /3 by ex_intro/ ] 655  1: #sz #sg * /3 by ex_intro/ * #i 656 [ 1: whd in match (fe_to_be_values ??); normalize nodelta normalize 657 lapply (vsplit_eq … 7 0 … i) * #v1 * #v2 #Heq 658 <(vsplit_prod … Heq) normalize nodelta /3 by ex_intro/ 659  2: whd in match (fe_to_be_values ??); normalize nodelta normalize 660 lapply (vsplit_eq … 7 8 … i) * #va * #vb #Heq 661 <(vsplit_prod … Heq) normalize nodelta 662 lapply (vsplit_eq … 7 0 … vb) * #vba * #vbb #Heq' 663 /3 by ex_intro/ 664  3: whd in match (fe_to_be_values ??); normalize nodelta normalize 665 lapply (vsplit_eq … 7 24 … i) * #va * #vb #Heq 666 <(vsplit_prod … Heq) normalize nodelta 667 lapply (vsplit_eq … 7 16 … vb) * #vba * #vbb #Heq' 668 <(vsplit_prod … Heq') normalize nodelta 669 lapply (vsplit_eq … 7 8 … vbb) * #vbba * #vbbb #Heq'' 670 <(vsplit_prod … Heq'') normalize nodelta 671 lapply (vsplit_eq … 7 0 … vbbb) * #vbx * #vby #Heq''' 672 /3 by ex_intro/ ] 673 ] qed. 674 675 lemma storen_to_valid_pointer_fe_to_be : 676 ∀typ,v,m,ptr,m'. storen m ptr (fe_to_be_values typ v) = Some ? m' → 677 (∀b.low (blocks m' b) = low (blocks m b) ∧ 678 high (blocks m' b) = high (blocks m b)) ∧ 679 nextblock m' = nextblock m ∧ 680 valid_pointer m ptr = true ∧ 681 valid_pointer m' ptr = true. 682 #typ #v cases (fe_to_be_values_nonempty … typ v) #hd * #tl #Heq >Heq 683 @storen_to_valid_pointer 684 qed. 685 593 686 lemma storen_beloadv_ok : 594 687 ∀m,m',b,ofs,hd,tl. … … 709 802 we need to prove the fact that we store stuff of "reasonable" size, i.e. at most 8. *) 710 803 lemma typesize_bounded : ∀ty. typesize ty ≤ 8. 711 * try // 712 [ 1: * try // 713  2: * try // 714 ] qed. 804 * try // * try // qed. 715 805 716 806 (* Lifting bound on make_list *) … … 746 836 ∀ty,v. fe_to_be_values ty v ≤ 8. 747 837 #ty cases ty 748 [ 3: #fsz #v whd in match (fe_to_be_values ??); 838 [ 1: #sz #sg ] 839 #v whd in match (fe_to_be_values ??); 749 840 cases v normalize nodelta 750 [ 1 : @makelist_bounded @typesize_bounded751  2 : * normalize nodelta #bv841 [ 1,5: @makelist_bounded @typesize_bounded 842  2,6: * normalize nodelta #bv 752 843 >map_bounded >bytes_of_bitvector_bounded // 753  3: #fl @makelist_bounded @typesize_bounded 754  4: // 755  5: #ptr // ] 756  2: #v whd in match (fe_to_be_values ??); 757 cases v normalize nodelta 758 [ 1: @makelist_bounded @typesize_bounded 759  2: * normalize nodelta #bv 760 >map_bounded >bytes_of_bitvector_bounded // 761  3: #fl @makelist_bounded @typesize_bounded 762  4: // 763  5: #ptr // ] 764  1: #sz #sg #v whd in match (fe_to_be_values ??); 765 cases v normalize nodelta 766 [ 1: @makelist_bounded @typesize_bounded 767  2: * normalize nodelta #bv 768 >map_bounded >bytes_of_bitvector_bounded // 769  3: #fl @makelist_bounded @typesize_bounded 770  4: // 771  5: #ptr // ] 772 ] qed. 773 844  3,7: // 845  4,8: #ptr // ] 846 qed. 774 847 775 848 lemma mem_bounds_after_store_value_of_type : … … 782 855 lapply (fe_to_be_values_bounded (typ_of_type ty) v) 783 856 cases ty 784 [ 1:  2: #sz #sg  3: # fsz  4: #ptr_ty  5: #array_ty #array_sz  6: #domain #codomain785  7: #structname #fieldspec  8: #unionname #fieldspec  9: #id ]857 [ 1:  2: #sz #sg  3: #ptrty  4: #arrayty #arraysz  5: #argsty #retty 858  6: #sid #fields  7: #uid #fields  8: #cptr_id ] 786 859 whd in match (typ_of_type ?); #Hbounded 787 860 whd in match (store_value_of_type ?????); 788 [ 1, 5,6,7,8: #Habsurd destruct (Habsurd)861 [ 1,4,5,6,7: #Habsurd destruct (Habsurd) 789 862  *: #Hstoren lapply (mem_bounds_invariant_after_storen … Hbounded Hstoren) 790 863 * * * * * #Hnextblock #Hbounds_eq #Hnonempty … … 814 887 [ Vptr p ⇒ True 815 888  _ ⇒ False ] 816  ASTfloat fsz ⇒817 match v with818 [ Vfloat _ ⇒ True819  _ ⇒ False ]820 889 ]. 821 890 … … 835 904 whd in match (fe_to_be_values ??); cases v 836 905 normalize in ⊢ (% → ?); 837 [ 1, 4: @False_ind906 [ 1,3: @False_ind 838 907  2: #sz' #i normalize in ⊢ (% → ?); #Heq destruct normalize nodelta 839 908 >map_bounded >bytes_of_bitvector_bounded cases sz' // 840  3: #f normalize in ⊢ (% → ?); @False_ind 841  5: #p normalize in ⊢ (% → ?); @False_ind ] 909  4: #p normalize in ⊢ (% → ?); @False_ind ] 842 910  2: #v cases v 843 911 normalize in ⊢ (% → ?); 844 [ 1, 4: @False_ind912 [ 1,3: @False_ind 845 913  2: #sz' #i normalize in ⊢ (% → ?); @False_ind 846  3: #f normalize in ⊢ (% → ?); @False_ind 847  5: #p #_ // ] 848  3: #fsz #v cases v 849 normalize in ⊢ (% → ?); 850 [ 1: @False_ind 851  2: #sz' #i normalize in ⊢ (% → ?); @False_ind 852  3: #f #_ cases fsz // 853  4: @False_ind 854  5: #p normalize in ⊢ (% → ?); @False_ind ] 855 ] qed. 856 914  4: #p #_ // ] 915 ] qed. 857 916 858 917 (* Not verified for floats atm. Restricting to integers. *) … … 863 922 whd in match (fe_to_be_values ??); 864 923 cases v normalize in ⊢ (% → ?); 865 [ 1,4: @False_ind 866  3: #f @False_ind 867  5: #p @False_ind 924 [ 1,3: @False_ind 925  4: #p @False_ind 868 926  2: #sz' #i' #Heq normalize in Heq; destruct (Heq) normalize nodelta 869 927 cases sz' in i'; #i normalize nodelta … … 924 982 #sz #sg #m #b #ofs #v #m' #H lapply H whd in ⊢ (% → ?); 925 983 cases v in H; normalize nodelta 926 [ 1: #_ @False_ind  2: #vsz #vi #H  3: # vf #_ @False_ind  4: #_ @False_ind  5: #vp #_ @False_ind ]984 [ 1: #_ @False_ind  2: #vsz #vi #H  3: #_ @False_ind  4: #vp #_ @False_ind ] 927 985 #Heq >Heq in H; #H 928 986 (* The lack of control on unfolds is extremely annoying. *)
Note: See TracChangeset
for help on using the changeset viewer.