Ignore:
Timestamp:
Jan 25, 2011, 5:30:37 PM (9 years ago)
Author:
campbell
Message:

"memory_space" to "region" replacement to match ocaml code

File:
1 edited

Legend:

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

    r474 r480  
    8989  high: Z;
    9090  contents: contentmap;
    91   space: memory_space
     91  space: region
    9292}.
    9393
     
    188188nqed.
    189189
    190 ndefinition empty_block : Z → Z → memory_space → block_contents ≝
     190ndefinition empty_block : Z → Z → region → block_contents ≝
    191191  λlo,hi,bty.mk_block_contents lo hi (λy. Undef) bty.
    192192
     
    208208nqed.
    209209
    210 ndefinition alloc : mem → Z → Z → memory_space → mem × block ≝
     210ndefinition alloc : mem → Z → Z → region → mem × block ≝
    211211  λm,lo,hi,bty.〈mk_mem
    212212              (update … (nextblock m)
     
    245245ndefinition high_bound : mem → block → Z ≝
    246246  λm,b.high (blocks m b).
    247 ndefinition block_space: mem → block → memory_space
     247ndefinition block_space: mem → block → region
    248248  λm,b.space (blocks m b).
    249249
     
    559559(* pointer_compat block_space pointer_space *)
    560560
    561 ninductive pointer_compat : memory_space → memory_space → Prop ≝
     561ninductive pointer_compat : region → region → Prop ≝
    562562|  same_compat : ∀s. pointer_compat s s
    563563| pxdata_compat : pointer_compat PData XData
     
    571571##] nqed.
    572572
    573 ndefinition is_pointer_compat : memory_space → memory_space → bool ≝
     573ndefinition is_pointer_compat : region → region → bool ≝
    574574λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true | inr _ ⇒ false ].
    575575
     
    583583*)
    584584
    585 ninductive valid_access (m: mem) (chunk: memory_chunk) (psp: memory_space) (b: block) (ofs: Z)
     585ninductive valid_access (m: mem) (chunk: memory_chunk) (psp: region) (b: block) (ofs: Z)
    586586            : Prop ≝
    587587  | valid_access_intro:
     
    598598(* XXX: Using + and ¬ instead of Sum and Not causes trouble *)
    599599nlet rec in_bounds
    600   (m:mem) (chunk:memory_chunk) (psp:memory_space) (b:block) (ofs:Z) on b : 
     600  (m:mem) (chunk:memory_chunk) (psp:region) (b:block) (ofs:Z) on b : 
    601601    Sum (valid_access m chunk psp b ofs) (Not (valid_access m chunk psp b ofs)) ≝ ?.
    602602napply (Zltb_elim_Type0 b (nextblock m)); #Hnext;
     
    627627  given offset falls within the bounds of the corresponding block. *)
    628628
    629 ndefinition valid_pointer : mem → memory_space → block → Z → bool ≝
     629ndefinition valid_pointer : mem → region → block → Z → bool ≝
    630630λm,psp,b,ofs. Zltb b (nextblock m) ∧
    631631  Zleb (low_bound m b) ofs ∧
     
    637637  or the memory access is out of bounds. *)
    638638
    639 ndefinition load : memory_chunk → mem → memory_space → block → Z → option val ≝
     639ndefinition load : memory_chunk → mem → region → block → Z → option val ≝
    640640λchunk,m,psp,b,ofs.
    641641  match in_bounds m chunk psp b ofs with
     
    684684  or the memory access is out of bounds. *)
    685685
    686 ndefinition store : memory_chunk → mem → memory_space → block → Z → val → option mem ≝
     686ndefinition store : memory_chunk → mem → region → block → Z → val → option mem ≝
    687687λchunk,m,psp,b,ofs,v.
    688688  match in_bounds m chunk psp b ofs with
     
    780780*)
    781781
    782 ndefinition block_init_data : list init_data → memory_space → block_contents ≝
     782ndefinition block_init_data : list init_data → region → block_contents ≝
    783783  λi_data,bcl.mk_block_contents
    784784    OZ (size_init_data_list i_data) (contents_init_data OZ i_data) bcl.
    785785
    786 ndefinition alloc_init_data : mem → list init_data → memory_space → mem × block ≝
     786ndefinition alloc_init_data : mem → list init_data → region → mem × block ≝
    787787  λm,i_data,bcl.
    788788  〈mk_mem (update ? (nextblock m)
     
    902902nqed.
    903903
    904 nlemma memory_space_store:
     904nlemma region_store:
    905905  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
    906906  ∀b'. block_space m2 b' = block_space m1 b'.
     
    944944##|nrewrite > (low_bound_store … STORE …);//
    945945##|nrewrite > (high_bound_store … STORE …);//
    946 ##|nrewrite > (memory_space_store … STORE …);//]
     946##|nrewrite > (region_store … STORE …);//]
    947947nqed.
    948948
     
    959959##|nrewrite < (low_bound_store … STORE …);//
    960960##|nrewrite < (high_bound_store … STORE …);//
    961 ##|nrewrite < (memory_space_store … STORE …);//]
     961##|nrewrite < (region_store … STORE …);//]
    962962nqed.
    963963
     
    11991199   ##[#H1;#H2;#H3;nwhd in ⊢ (???%);nrewrite < H1;nrewrite < H2;
    12001200      napply (load_compat_pointer … psp);
    1201       ##[ nrewrite > (memory_space_store … STORE b);
     1201      ##[ nrewrite > (region_store … STORE b);
    12021202          ncases Hvalid; //;
    12031203      ##| napply (load_store_similar … STORE);//;
     
    12101210      ##|#H2;@2;//]
    12111211   ##|#H1;#H2;#H3;#H4; nlapply (load_compat_pointer … psp … Hx);
    1212      ##[ nrewrite > (memory_space_store … STORE b');
     1212     ##[ nrewrite > (region_store … STORE b');
    12131213         nrewrite > H1; nelim (store_valid_access_3 … STORE); //
    12141214     ##| nrewrite < H1 in ⊢ (% → ?);#Hx';
     
    12181218   ##|#H1;#H2;#H3;
    12191219       nlapply (load_compat_pointer … psp … Hx);
    1220        ##[ nrewrite > (memory_space_store … STORE b');
     1220       ##[ nrewrite > (region_store … STORE b');
    12211221           nrewrite > H1; nelim (store_valid_access_3 … STORE); //
    12221222       ##| nrewrite < H1 in Hx ⊢ %; nrewrite < H2; #Hx Hx';
     
    17361736ntheorem valid_pointer_store:
    17371737  ∀chunk: memory_chunk. ∀m1,m2: mem.
    1738   ∀psp,psp': memory_space. ∀b,b': block. ∀ofs,ofs': Z. ∀v: val.
     1738  ∀psp,psp': region. ∀b,b': block. ∀ofs,ofs': Z. ∀v: val.
    17391739  store chunk m1 psp' b' ofs' v = Some ? m2 →
    17401740  valid_pointer m1 psp b ofs = true → valid_pointer m2 psp b ofs = true.
Note: See TracChangeset for help on using the changeset viewer.