Ignore:
Timestamp:
Nov 9, 2012, 4:38:02 PM (7 years ago)
Author:
garnier
Message:

Comitting current state of switch removal.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/MemProperties.ma

    r2441 r2448  
    44include "Clight/frontend_misc.ma".
    55include "common/FrontEndMem.ma".
     6
     7(* for store_value_of_type' *)
     8include "Clight/Cexec.ma".
     9
    610
    711(* --------------------------------------------------------------------------- *)
     
    5761qed.
    5862
     63lemma 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
     72qed.
     73
    5974(* --------------------------------------------------------------------------- *)
    6075(* "Observational" memory equivalence. Memories use closures to represent contents,
     
    187202qed.
    188203
     204(* valid pointer implies successful bestorev *)
    189205lemma valid_pointer_to_bestorev_ok : ∀m,ptr,v. valid_pointer m ptr = true → ∃m'. bestorev m ptr v = Some ? m'.
    190206#m * #b #o #v #Hvalid cases (valid_pointer_to_Prop … Hvalid) *
     
    332348(* --------------------------------------------------------------------------- *)
    333349(* 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)                                  *)
    335351(* --------------------------------------------------------------------------- *)
    336352
     
    757773
    758774
     775lemma 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
     782lapply (fe_to_be_values_bounded (typ_of_type ty) v)
     783cases 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 ]
     786whd in match (typ_of_type ?); #Hbounded
     787whd 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
     795lemma 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
     803qed.
     804
     805
    759806definition ast_typ_consistent_with_value : typ → val → Prop ≝ λty,v.
    760807  match ty with
     
    779826| _ ⇒ True
    780827].
    781 
    782828
    783829(* 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.