Changeset 1545 for src/common/Mem.ma


Ignore:
Timestamp:
Nov 23, 2011, 6:03:07 PM (9 years ago)
Author:
campbell
Message:

Use pointer record in front-end.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Mem.ma

    r1523 r1545  
    643643  given offset falls within the bounds of the corresponding block. *)
    644644
    645 definition valid_pointer : mem → region → block → offset → bool ≝
    646 λm,r,b,ofs. Zltb (block_id b) (nextblock m) ∧
    647   Zleb (low_bound m b) (offv ofs) ∧
    648   Zltb (offv ofs) (high_bound m b) ∧
    649   is_pointer_compat b r.
     645definition valid_pointer : mem → pointer → bool ≝
     646λm,ptr. Zltb (block_id (pblock ptr)) (nextblock m) ∧
     647  Zleb (low_bound m (pblock ptr)) (offv (poff ptr)) ∧
     648  Zltb (offv (poff ptr)) (high_bound m (pblock ptr)).
    650649
    651650(* [load chunk m r b ofs] perform a read in memory state [m], at address
     
    679678let rec loadv (chunk:memory_chunk) (m:mem) (addr:val) on addr : option val ≝
    680679  match addr with
    681   [ Vptr r b p ofs ⇒ load chunk m r b (offv ofs)
     680  [ Vptr ptr ⇒ load chunk m (ptype ptr) (pblock ptr) (offv (poff ptr))
    682681  | _ ⇒ None ? ].
    683682
     
    726725λchunk,m,addr,v.
    727726  match addr with
    728   [ Vptr r b p ofs ⇒ store chunk m r b (offv ofs) v
     727  [ Vptr ptr ⇒ store chunk m (ptype ptr) (pblock ptr) (offv (poff ptr)) v
    729728  | _ ⇒ None ? ].
    730729
     
    35153514  storev Mint8signed m a v = storev Mint8unsigned m a v.
    35163515#m #a #v whd in ⊢ (??%%); elim a //
    3517 #r #b #p #ofs whd in ⊢ (??%%);
     3516#ptr whd in ⊢ (??%%);
    35183517>(in_bounds_equiv Mint8signed Mint8unsigned … (option mem) ???) //
    35193518qed.
     
    35233522  storev Mint16signed m a v = storev Mint16unsigned m a v.
    35243523#m #a #v whd in ⊢ (??%%); elim a //
    3525 #r #b #p #ofs whd in ⊢ (??%%);
     3524#ptr whd in ⊢ (??%%);
    35263525>(in_bounds_equiv Mint16signed Mint16unsigned … (option mem) ???) //
    35273526qed.
Note: See TracChangeset for help on using the changeset viewer.