Changeset 1988 for src/common


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

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

Location:
src/common
Files:
3 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.
  • src/common/Globalenvs.ma

    r1986 r1988  
    7979     addresses of the memory region in question - here there are no real
    8080     pointers, so use the real region. *)
    81   let ptr ≝ mk_pointer (block_region ? m b) b ? (mk_offset p) in
     81  let ptr ≝ mk_pointer (block_region m b) b ? (mk_offset p) in
    8282  match id with
    8383  [ Init_int8 n ⇒ store (ASTint I8 Unsigned) m ptr (Vint I8 n)
     
    151151definition alloc_init_data : mem → list init_data → region → mem × block ≝
    152152  λm,i_data,r.
    153   let b ≝ mk_block r (nextblock ? m) in
    154   〈mk_mem ? (update_block ? b
    155                  (mk_block_contents becontentT OZ (size_init_data_list i_data) (λ_.BVundef))
    156                  (blocks ? m))
    157          (Zsucc (nextblock ? m))
    158          (succ_nextblock_pos ? m),
     153  let b ≝ mk_block r (nextblock m) in
     154  〈mk_mem (update_block ? b
     155                 (mk_block_contents OZ (size_init_data_list i_data) (λ_.BVundef))
     156                 (blocks m))
     157         (Zsucc (nextblock m))
     158         (succ_nextblock_pos m),
    159159   b〉.
    160160
     
    198198λF,V,init_info,p.
    199199  add_globals … init_info
    200    〈add_functs ? (empty …) (prog_funct F ? p), empty_mem ?
     200   〈add_functs ? (empty …) (prog_funct F ? p), empty_mem
    201201   (prog_vars ?? p).
    202202
  • src/common/Mem.ma

    r1874 r1988  
    22include "common/FrontEndVal.ma".
    33
    4 definition mem ≝ bemem.
    5 
    6 let rec loadn (m:bemem) (ptr:pointer) (n:nat) on n : option (list beval) ≝
     4let rec loadn (m:mem) (ptr:pointer) (n:nat) on n : option (list beval) ≝
    75match n with
    86[ O ⇒ Some ? ([ ])
     
    2321  ].
    2422
    25 let rec loadv (t:typ) (m:bemem) (addr:val) on addr : option val ≝
     23let rec loadv (t:typ) (m:mem) (addr:val) on addr : option val ≝
    2624match addr with
    2725[ Vptr ptr ⇒ load t m ptr
     
    2927].
    3028
    31 let rec storen (m:bemem) (ptr:pointer) (vs:list beval) on vs : option bemem ≝
     29let rec storen (m:bemem) (ptr:pointer) (vs:list beval) on vs : option mem ≝
    3230match vs with
    3331[ nil ⇒ Some ? m
     
    3937].
    4038
    41 definition store : typ → bemem → pointer → val → option bemem ≝
     39definition store : typ → bemem → pointer → val → option mem ≝
    4240λt,m,ptr,v. storen m ptr (fe_to_be_values t v).
    4341
    44 definition storev : typ → bemem → val → val → option bemem ≝
     42definition storev : typ → bemem → val → val → option mem ≝
    4543λt,m,addr,v.
    4644  match addr with
     
    5250
    5351definition valid_pointer : mem → pointer → bool ≝
    54 λm,ptr. Zltb (block_id (pblock ptr)) (nextblock ? m) ∧
    55   Zleb (low_bound ? m (pblock ptr)) (offv (poff ptr)) ∧
    56   Zleb (offv (poff ptr)) (high_bound ? m (pblock ptr)).
     52λm,ptr. Zltb (block_id (pblock ptr)) (nextblock m) ∧
     53  Zleb (low_bound m (pblock ptr)) (offv (poff ptr)) ∧
     54  Zleb (offv (poff ptr)) (high_bound m (pblock ptr)).
    5755
    5856
Note: See TracChangeset for help on using the changeset viewer.