Ignore:
Timestamp:
Feb 11, 2011, 4:45:38 PM (9 years ago)
Author:
campbell
Message:

Use dependent pointer type to ensure that the representation is always
compatible with the memory region used.
Add a couple of missing checks as a result...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Mem.ma

    r499 r500  
    588588qed.
    589589*)
    590 (* pointer_compat block_region pointer_region *)
    591 
    592 inductive pointer_compat : block → region → Prop ≝
    593 |        same_compat : ∀s,id. pointer_compat (mk_block s id) s
    594 |      pxdata_compat : ∀id. pointer_compat (mk_block PData id) XData
    595 |   universal_compat : ∀r,id. pointer_compat (mk_block r id) Any.
    596 
    597 lemma pointer_compat_dec : ∀b,p. pointer_compat b p + ¬pointer_compat b p.
    598 * * #id *
    599 try ( %1 // )
    600 %2 % #H inversion H #e1 #e2 try #e3 try #e4 destruct
    601 qed.
    602 
    603 definition is_pointer_compat : block → region → bool ≝
    604 λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true | inr _ ⇒ false ].
    605590
    606591(* [valid_access m chunk r b ofs] holds if a memory access (load or store)
     
    695680let rec loadv (chunk:memory_chunk) (m:mem) (addr:val) on addr : option val ≝
    696681  match addr with
    697   [ Vptr r b ofs ⇒ load chunk m r b (signed ofs)
     682  [ Vptr r b p ofs ⇒ load chunk m r b (signed ofs)
    698683  | _ ⇒ None ? ].
    699684
     
    742727λchunk,m,addr,v.
    743728  match addr with
    744   [ Vptr r b ofs ⇒ store chunk m r b (signed ofs) v
     729  [ Vptr r b p ofs ⇒ store chunk m r b (signed ofs) v
    745730  | _ ⇒ None ? ].
    746731
     
    35303515  ∀m,a,v.
    35313516  storev Mint8signed m a v = storev Mint8unsigned m a v.
    3532 #m #a #v whd in ⊢ (??%%); elim a; //;
    3533 #r #b #ofs whd in ⊢ (??%%);
    3534 >(in_bounds_equiv Mint8signed Mint8unsigned … (option mem) ???) //;
     3517#m #a #v whd in ⊢ (??%%) elim a //
     3518#r #b #p #ofs whd in ⊢ (??%%)
     3519>(in_bounds_equiv Mint8signed Mint8unsigned … (option mem) ???) //
    35353520qed.
    35363521
     
    35383523  ∀m,a,v.
    35393524  storev Mint16signed m a v = storev Mint16unsigned m a v.
    3540 #m #a #v whd in ⊢ (??%%); elim a; //;
    3541 #r #b #ofs whd in ⊢ (??%%);
    3542 >(in_bounds_equiv Mint16signed Mint16unsigned … (option mem) ???) //;
     3525#m #a #v whd in ⊢ (??%%) elim a //
     3526#r #b #p #ofs whd in ⊢ (??%%)
     3527>(in_bounds_equiv Mint16signed Mint16unsigned … (option mem) ???) //
    35433528qed.
    35443529
Note: See TracChangeset for help on using the changeset viewer.