Changeset 2448 for src/Clight/MemProperties.ma
 Timestamp:
 Nov 9, 2012, 4:38:02 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/MemProperties.ma
r2441 r2448 4 4 include "Clight/frontend_misc.ma". 5 5 include "common/FrontEndMem.ma". 6 7 (* for store_value_of_type' *) 8 include "Clight/Cexec.ma". 9 6 10 7 11 (*  *) … … 57 61 qed. 58 62 63 lemma valid_pointer_of_Prop : 64 ∀m,p. (block_id (pblock p)) < (nextblock m) ∧ 65 (low_bound m (pblock p)) ≤ (Z_of_unsigned_bitvector offset_size (offv (poff p))) ∧ 66 (Z_of_unsigned_bitvector offset_size (offv (poff p))) < (high_bound m (pblock p)) → 67 valid_pointer m p = true. 68 #m #p * * #Hnextblock #Hlowbound #Hhighbound whd in match (valid_pointer ??); 69 >(Zle_to_Zleb_true … Hlowbound) 70 >(Zlt_to_Zltb_true … Hhighbound) 71 >(Zlt_to_Zltb_true … Hnextblock) @refl 72 qed. 73 59 74 (*  *) 60 75 (* "Observational" memory equivalence. Memories use closures to represent contents, … … 187 202 qed. 188 203 204 (* valid pointer implies successful bestorev *) 189 205 lemma valid_pointer_to_bestorev_ok : ∀m,ptr,v. valid_pointer m ptr = true → ∃m'. bestorev m ptr v = Some ? m'. 190 206 #m * #b #o #v #Hvalid cases (valid_pointer_to_Prop … Hvalid) * … … 332 348 (*  *) 333 349 (* loading and storing are inverse operations for integers. (Paolo's work 334 * contain a proof of this fact for pointers 350 * contain a proof of this fact for pointers) *) 335 351 (*  *) 336 352 … … 757 773 758 774 775 lemma mem_bounds_after_store_value_of_type : 776 ∀m,m',ty,b,o,v. 777 store_value_of_type ty m b o v = Some ? m' → 778 (nextblock m' = nextblock m ∧ 779 (∀b.low (blocks m' b) = low (blocks m b) ∧ 780 high (blocks m' b) = high (blocks m b))). 781 #m #m' #ty #b #o #v 782 lapply (fe_to_be_values_bounded (typ_of_type ty) v) 783 cases ty 784 [ 1:  2: #sz #sg  3: #fsz  4: #ptr_ty  5: #array_ty #array_sz  6: #domain #codomain 785  7: #structname #fieldspec  8: #unionname #fieldspec  9: #id ] 786 whd in match (typ_of_type ?); #Hbounded 787 whd in match (store_value_of_type ?????); 788 [ 1,5,6,7,8: #Habsurd destruct (Habsurd) 789  *: #Hstoren lapply (mem_bounds_invariant_after_storen … Hbounded Hstoren) 790 * * * * * #Hnextblock #Hbounds_eq #Hnonempty 791 #Hcontents_upd #Hcontents_inv #Hvalid_ptr 792 >Hnextblock @conj // 793 ] qed. 794 795 lemma mem_bounds_after_store_value_of_type' : 796 ∀m,m',ty,p,v. 797 store_value_of_type' ty m p v = Some ? m' → 798 (nextblock m' = nextblock m ∧ 799 (∀b.low (blocks m' b) = low (blocks m b) ∧ 800 high (blocks m' b) = high (blocks m b))). 801 #m #m' #ty * #b #o #v whd in match (store_value_of_type' ????); 802 @mem_bounds_after_store_value_of_type 803 qed. 804 805 759 806 definition ast_typ_consistent_with_value : typ → val → Prop ≝ λty,v. 760 807 match ty with … … 779 826  _ ⇒ True 780 827 ]. 781 782 828 783 829 (* We also need the following property. It is not provable unless [v] and [ty] are consistent. *)
Note: See TracChangeset
for help on using the changeset viewer.