Changeset 1988 for src/common/GenMem.ma


Ignore:
Timestamp:
May 24, 2012, 11:39:27 AM (6 years ago)
Author:
campbell
Message:

Abstraction of the memory contents in the memory models is no longer
necessary.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/GenMem.ma

    r1516 r1988  
    1616
    1717(* * This file describes the part of the memory model that is in common
    18      between the front-end and the back-end. Actually, it is so tiny that
    19      the functions defined here could be put elsewhere.
     18     between the front-end and the back-end.
    2019*)
    2120
    2221include "utilities/extralib.ma".
    2322include "common/Pointers.ma".
     23include "common/ByteValues.ma".
    2424
    2525definition update : ∀A: Type[0]. ∀x: Z. ∀v: A. ∀f: Z → A. Z → A ≝
     
    7272(***************************************)
    7373
    74 record contentT: Type[1] ≝
    75  { contentcarr:> Type[0]
    76  ; undef: contentcarr
    77  }.
    78 
    79 definition contentmap: contentT → Type[0] ≝ λcontent. Z → content.
     74definition contentmap: Type[0] ≝ Z → beval.
    8075
    8176(* A memory block comprises the dimensions of the block (low and high bounds)
    8277  plus a mapping from byte offsets to contents.  *)
    8378
    84 record block_contents (content:contentT) : Type[0] ≝ {
     79record block_contents : Type[0] ≝ {
    8580  low: Z;
    8681  high: Z;
    87   contents: contentmap content
     82  contents: contentmap
    8883}.
    8984
     
    9287  unallocated block, and a proof that this address is positive. *)
    9388
    94 record mem (content:contentT): Type[0] ≝ {
    95   blocks: block -> block_contents content;
     89record mem : Type[0] ≝ {
     90  blocks: block -> block_contents;
    9691  nextblock: Z;
    9792  nextblock_pos: OZ < nextblock
     
    106101qed.
    107102
    108 definition empty_block : ∀content. Z → Z → block_contents content
    109   λcontent,lo,hi.mk_block_contents content lo hi (λy. undef content).
     103definition empty_block : Z → Z → block_contents
     104  λlo,hi.mk_block_contents lo hi (λy. BVundef).
    110105
    111 definition empty: ∀content. mem content
    112  λcontent.mk_mem content (λx.empty_block content OZ OZ) (pos one) one_pos.
     106definition empty: mem
     107 mk_mem (λx.empty_block OZ OZ) (pos one) one_pos.
    113108
    114109definition nullptr: block ≝ mk_block Any OZ.
     
    120115
    121116lemma succ_nextblock_pos:
    122   ∀content.∀m. OZ < Zsucc (nextblock content m).
    123 #content #m lapply (nextblock_pos … m);normalize;
     117  ∀m. OZ < Zsucc (nextblock m).
     118#m lapply (nextblock_pos … m);normalize;
    124119cases (nextblock … m);//;
    125120#n cases n;//;
    126121qed.
    127122
    128 definition alloc : ∀content. mem content → Z → Z → ∀r:region. mem content × Σb:block. block_region b = r ≝
    129   λcontent,m,lo,hi,r.
     123definition alloc : mem → Z → Z → ∀r:region. mem × Σb:block. block_region b = r ≝
     124  λm,lo,hi,r.
    130125  let b ≝ mk_block r (nextblock … m) in
    131   〈mk_mem content
     126  〈mk_mem
    132127    (update_block … b
    133128      (empty_block … lo hi)
     
    145140
    146141definition free ≝
    147   λcontent,m,b.mk_mem content (update_block … b
    148                 (empty_block … OZ OZ)
    149                 (blocks … m))
     142  λm,b.mk_mem (update_block … b
     143              (empty_block … OZ OZ)
     144              (blocks … m))
    150145        (nextblock … m)
    151146        (nextblock_pos … m).
     
    154149
    155150definition free_list ≝
    156   λcontent,m,l.foldr ?? (λb,m.free content m b) m l.
     151  λm,l.foldr ?? (λb,m.free m b) m l.
    157152
    158153(* XXX hack for lack of reduction with restricted unfolding *)
    159154lemma unfold_free_list :
    160  ∀content,m,h,t. free_list content m (h::t) = free … (free_list … m t) h.
     155 ∀m,h,t. free_list m (h::t) = free … (free_list … m t) h.
    161156normalize; //; qed.
    162157
     
    164159   Those bounds are 0 for freed or not yet allocated address. *)
    165160
    166 definition low_bound : ∀content. mem content → block → Z ≝
    167   λcontent,m,b.low … (blocks … m b).
    168 definition high_bound : ∀content. mem content → block → Z ≝
    169   λcontent,m,b.high … (blocks … m b).
    170 definition block_region: ∀content. mem content → block → region ≝
    171   λcontent,m,b.block_region b. (* TODO: should I keep the mem argument for uniformity, or get rid of it? *)
     161definition low_bound : mem → block → Z ≝
     162  λm,b.low … (blocks … m b).
     163definition high_bound : mem → block → Z ≝
     164  λm,b.high … (blocks … m b).
     165definition block_region: mem → block → region ≝
     166  λm,b.block_region b. (* TODO: should I keep the mem argument for uniformity, or get rid of it? *)
    172167
    173168(* A block address is valid if it was previously allocated. It remains valid
     
    175170
    176171(* TODO: should this check for region? *)
    177 definition valid_block : ∀content. mem content → block → Prop ≝
    178   λcontent,m,b.block_id b < nextblock … m.
     172definition valid_block : mem → block → Prop ≝
     173  λm,b.block_id b < nextblock … m.
    179174
    180175(* FIXME: hacks to get around lack of nunfold *)
    181 lemma unfold_low_bound : ∀content,m,b. low_bound content m b = low … (blocks … m b).
     176lemma unfold_low_bound : ∀m,b. low_bound m b = low … (blocks … m b).
    182177//; qed.
    183 lemma unfold_high_bound : ∀content,m,b. high_bound content m b = high … (blocks … m b).
     178lemma unfold_high_bound : ∀m,b. high_bound m b = high … (blocks … m b).
    184179//; qed.
    185 lemma unfold_valid_block : ∀content,m,b. (valid_block content m b) = (block_id b < nextblock … m).
     180lemma unfold_valid_block : ∀m,b. (valid_block m b) = (block_id b < nextblock … m).
    186181//; qed.
Note: See TracChangeset for help on using the changeset viewer.