Changeset 1988


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.

Location:
src
Files:
11 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r1986 r1988  
    294294| cons h vars ⇒
    295295  let 〈id,ty〉 ≝ h in
    296   let 〈m1,b1〉 ≝ alloc becontentT m 0 (sizeof ty) Any in
     296  let 〈m1,b1〉 ≝ alloc m 0 (sizeof ty) Any in
    297297      exec_alloc_variables (add ?? en id b1) m1 vars
    298298].
     
    380380      | Kstop ⇒
    381381          match fn_return f with
    382           [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list becontentT m (blocks_of_env e))〉
     382          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉
    383383          | _ ⇒ Wrong ??? (msg NonsenseState)
    384384          ]
    385385      | Kcall _ _ _ _ ⇒
    386386          match fn_return f with
    387           [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list becontentT m (blocks_of_env e))〉
     387          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉
    388388          | _ ⇒ Wrong ??? (msg NonsenseState)
    389389          ]
     
    446446    match a_opt with
    447447    [ None ⇒ match fn_return f with
    448       [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list becontentT m (blocks_of_env e))〉
     448      [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉
    449449      | _ ⇒ Wrong ??? (msg ReturnMismatch)
    450450      ]
     
    454454        | inr _ ⇒
    455455          ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
    456           ret ? 〈tr, Returnstate v (call_cont k) (free_list becontentT m (blocks_of_env e))〉
     456          ret ? 〈tr, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉
    457457        ]
    458458    ]
  • src/Clight/CexecSound.ma

    r1876 r1988  
    349349[ #en #m #en' #m' #EXEC whd in EXEC:(??%?); destruct %
    350350| * #id #ty #t #IH #en #m #en' #m'
    351   lapply (refl ? (alloc ? m O (sizeof ty) Any)) #ALLOC #EXEC
     351  lapply (refl ? (alloc m O (sizeof ty) Any)) #ALLOC #EXEC
    352352  whd in EXEC:(??%?) ALLOC:(???%);
    353353 @(alloc_variables_cons … ALLOC)
  • src/Clight/Csem.ma

    r1986 r1988  
    526526  | alloc_variables_cons:
    527527      ∀e,m,id,ty,vars,m1,b1,m2,e2.
    528       alloc becontentT m 0 (sizeof ty) Any = 〈m1, b1〉 →
     528      alloc m 0 (sizeof ty) Any = 〈m1, b1〉 →
    529529      alloc_variables (add … e id (pi1 … b1)) m1 vars e2 m2 →
    530530      alloc_variables e m (〈id, ty〉 :: vars) e2 m2.
     
    11391139      fn_return f = Tvoid →
    11401140      step ge (State f (Sreturn (None ?)) k e m)
    1141            E0 (Returnstate Vundef (call_cont k) (free_list becontentT m (blocks_of_env e)))
     1141           E0 (Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e)))
    11421142  | step_return_1: ∀f,a,k,e,m,v,tr.
    11431143      fn_return f ≠ Tvoid →
    11441144      eval_expr ge e m a v tr →
    11451145      step ge (State f (Sreturn (Some ? a)) k e m)
    1146            tr (Returnstate v (call_cont k) (free_list becontentT m (blocks_of_env e)))
     1146           tr (Returnstate v (call_cont k) (free_list m (blocks_of_env e)))
    11471147  | step_skip_call: ∀f,k,e,m.
    11481148      is_call_cont k →
    11491149      fn_return f = Tvoid →
    11501150      step ge (State f Sskip k e m)
    1151            E0 (Returnstate Vundef k (free_list becontentT m (blocks_of_env e)))
     1151           E0 (Returnstate Vundef k (free_list m (blocks_of_env e)))
    11521152
    11531153  | step_switch: ∀f,a,sl,k,e,m,sz,n,tr.
  • src/Clight/test/memorymodel.ma

    r1875 r1988  
    2020   access, preventing you reading back more information than the memory can
    2121   store. *)
    22 definition store0 := empty becontentT.
    23 definition store1block : mem × Σb:block.? ≝ alloc ? store0 0 4 Any.
     22definition store0 := empty.
     23definition store1block : mem × Σb:block.? ≝ alloc store0 0 4 Any.
    2424definition store1 : mem ≝ fst ?? store1block.
    2525definition block :block := pi1 … (snd ?? store1block).
     
    5151(* NB: Double frees are allowed by the memory model (although not necessarily
    5252       by the language). *)
    53 definition store4 := free ? store3 block.
    54 definition store5 : mem. letin r ≝ (free ? store3 block); whd in r; @r qed.
     53definition store4 := free store3 block.
     54definition store5 : mem. letin r ≝ (free store3 block); whd in r; @r qed.
    5555
    5656(* No ordering is imposed on deallocation (even though alloc and free are only used for
    5757   stack memory in the semantics. *)
    58 definition storeA := empty becontentT.
    59 definition storeBblkB := alloc ? storeA 0 4 Any.
    60 definition storeCblkC := alloc ? (fst ?? storeBblkB) 0 8 Any.
    61 definition storeD := free ? (fst ?? storeCblkC) (snd ?? storeBblkB).
    62 definition storeE : mem. letin r ≝ (free ? storeD (snd ?? storeCblkC)).
     58definition storeA := empty.
     59definition storeBblkB := alloc storeA 0 4 Any.
     60definition storeCblkC := alloc (fst ?? storeBblkB) 0 8 Any.
     61definition storeD := free (fst ?? storeCblkC) (snd ?? storeBblkB).
     62definition storeE : mem. letin r ≝ (free storeD (snd ?? storeCblkC)).
    6363whd in r; @r qed.
    6464
     
    6666   but can now split up integer values into bytes.  The front-end interface
    6767   doesn't currently expose parts of pointers. *)
    68 definition storeI := empty becontentT.
    69 definition storeIIblk := alloc ? storeA 0 4 Any.
     68definition storeI := empty.
     69definition storeIIblk := alloc storeI 0 4 Any.
    7070definition storeIII : mem.
    7171 letin r ≝ (store (ASTint I32 Unsigned) (fst ?? storeIIblk) (mk_pointer Any (snd ?? storeIIblk) (same_compat …) zero_offset) (Vint I32 (repr ? 1)));
  • src/Cminor/semantics.ma

    r1986 r1988  
    300300        | Kblock k' ⇒ λkInv. return 〈E0, State f St_skip en fInv ? m sp k' ? st〉
    301301          (* cminor allows functions without an explicit return statement *)
    302         | Kend ⇒ λkInv. return 〈E0, Returnstate (None ?) (free ? m sp) st〉
     302        | Kend ⇒ λkInv. return 〈E0, Returnstate (None ?) (free m sp) st〉
    303303        ] kInv
    304304    | St_assign _ id e ⇒ λInv.
     
    345345    | St_return eo ⇒
    346346        match eo return λeo. stmt_inv f en (St_return eo) → ? with
    347         [ None ⇒ λInv. return 〈E0, Returnstate (None ?) (free ? m sp) st〉
     347        [ None ⇒ λInv. return 〈E0, Returnstate (None ?) (free m sp) st〉
    348348        | Some e ⇒
    349349            match e return λe. stmt_inv f en (St_return (Some ? e)) → ? with [ mk_DPair ty e ⇒ λInv.
    350350              ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
    351               return 〈tr, Returnstate (Some ? v) (free ? m sp) st〉
     351              return 〈tr, Returnstate (Some ? v) (free m sp) st〉
    352352            ]
    353353        ]
     
    363363    match fd with
    364364    [ Internal f ⇒ err_to_io ?? (trace × state) (
    365         let 〈m',sp〉 ≝ alloc ? m 0 (f_stacksize f) Any in
     365        let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) Any in
    366366        ! en ← bind_params args (f_params f);
    367367        return 〈E0, State f (f_body f) (init_locals en (f_vars f)) ? ? m' sp Kend ? st〉)
  • src/RTLabs/semantics.ma

    r1986 r1988  
    167167                return (Some ? v)
    168168            ];
    169       return 〈E0, Returnstate v (retdst f) fs (free ? m (sp f))〉
     169      return 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
    170170  ] (f_closed (func f) (next f) s ?)
    171171| Callstate fd params dst fs m ⇒
     
    175175        (* CSC: XXX alignment call (concrete_stacksize in OCaml) is missing
    176176           here *)
    177         let 〈m', sp〉 ≝ alloc ? m 0 (f_stacksize fn) Any in
     177        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
    178178        return 〈E0, State (mk_frame fn locals (f_entry fn) ? sp dst) fs m'〉
    179179    | External fn ⇒
     
    295295| * #fn #args #retdst #stk #m #tr #s'
    296296  whd in ⊢ (??%? → ?);
    297   [ @bind_res_value #loc #Eloc cases (alloc ? m O ??) #m' #b whd in ⊢ (??%? → ?);
     297  [ @bind_res_value #loc #Eloc cases (alloc m O ??) #m' #b whd in ⊢ (??%? → ?);
    298298    #E destruct %3
    299299  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct
  • 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
  • src/joint/BEGlobalenvs.ma

    r1599 r1988  
    428428  λm,i_data,r.
    429429  let b ≝ mk_block r (nextblock … m) in
    430   〈mk_mem ? (update_block ? b
    431                  (mk_block_contents (mk_contentT beval BVundef) OZ i_data (λ_.BVundef))
     430  〈mk_mem (update_block ? b
     431                 (mk_block_contents OZ i_data (λ_.BVundef))
    432432                 (blocks … m))
    433433         (Zsucc (nextblock … m))
  • src/joint/BEMem.ma

    r1987 r1988  
    1515include "common/GenMem.ma".
    1616
    17 definition becontentT ≝ mk_contentT beval BVundef.
    18 definition bemem ≝ mem becontentT.
     17definition bemem ≝ mem.
    1918
    2019(* This function should be moved to common/GenMem.ma and replaces in_bounds *)
    2120definition do_if_in_bounds:
    22  ∀A:Type[0]. bemem → pointer → (block → block_contents becontentT → Z → A) → option A ≝
     21 ∀A:Type[0]. bemem → pointer → (block → block_contents → Z → A) → option A ≝
    2322 λS,m,ptr,F.
    2423  let b ≝ pblock ptr in
     
    4039  (λb,content,off.
    4140    let contents ≝ update … off v (contents … content) in
    42     let content ≝ mk_block_contents (mk_contentT beval BVundef) (low … content) (high … content) contents in
     41    let content ≝ mk_block_contents (low … content) (high … content) contents in
    4342    let blocks ≝ update_block … b content (blocks … m) in
    4443     mk_mem … blocks (nextblock … m) (nextblock_pos … m)).
Note: See TracChangeset for help on using the changeset viewer.