Changeset 1993


Ignore:
Timestamp:
May 24, 2012, 5:10:05 PM (5 years ago)
Author:
campbell
Message:

Make front-end memory model only depend on the general definitions by
moving a few definitions from the back-end one. Give the front-end
model a more descriptive name.

Location:
src
Files:
1 added
1 deleted
6 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/test/memorymodel.ma

    r1988 r1993  
    1313(**************************************************************************)
    1414
    15 include "common/Mem.ma".
     15include "common/FrontEndMem.ma".
    1616
    1717
  • src/Cminor/semantics.ma

    r1988 r1993  
    11include "common/Events.ma".
    2 include "common/Mem.ma".
     2include "common/FrontEndMem.ma".
    33include "common/IO.ma".
    44include "common/Globalenvs.ma".
  • src/common/Animation.ma

    r1881 r1993  
    9595fw_ok : ∀r,S,t,s. finishes_with r S (OK ? (finished S t r s)).
    9696
    97 include "common/Mem.ma".
     97include "common/GenMem.ma".
    9898
    9999(* Hide the representation of memory to make displaying the results easier. *)
  • src/common/GenMem.ma

    r1988 r1993  
    180180lemma unfold_valid_block : ∀m,b. (valid_block m b) = (block_id b < nextblock … m).
    181181//; qed.
     182
     183
     184(* This function should be moved to common/GenMem.ma and replaces in_bounds *)
     185definition do_if_in_bounds:
     186 ∀A:Type[0]. mem → pointer → (block → block_contents → Z → A) → option A ≝
     187 λS,m,ptr,F.
     188  let b ≝ pblock ptr in
     189  if Zltb (block_id b) (nextblock … m) then
     190   let content ≝ blocks … m b in
     191   let off ≝ offv (poff ptr) in
     192   if andb (Zleb (low … content) off) (Zleb off (high … content)) then
     193    Some … (F b content off)
     194   else
     195    None ?
     196  else
     197   None ?.
     198
     199definition beloadv: ∀m:mem. ∀ptr:pointer. option beval ≝
     200 λm,ptr. do_if_in_bounds … m ptr (λb,content,off. contents … content off).
     201
     202definition bestorev: ∀m:mem. ∀ptr:pointer. beval → option mem ≝
     203 λm,ptr,v. do_if_in_bounds … m ptr
     204  (λb,content,off.
     205    let contents ≝ update … off v (contents … content) in
     206    let content ≝ mk_block_contents (low … content) (high … content) contents in
     207    let blocks ≝ update_block … b content (blocks … m) in
     208     mk_mem … blocks (nextblock … m) (nextblock_pos … m)).
  • src/common/Globalenvs.ma

    r1988 r1993  
    3737include "common/AST.ma".
    3838(*include "Values.ma".*)
    39 include "common/Mem.ma".
     39include "common/FrontEndMem.ma".
    4040
    4141   (* * The type of global environments.  The parameter [F] is the type
  • src/joint/BEMem.ma

    r1988 r1993  
    1616
    1717definition bemem ≝ mem.
    18 
    19 (* This function should be moved to common/GenMem.ma and replaces in_bounds *)
    20 definition do_if_in_bounds:
    21  ∀A:Type[0]. bemem → pointer → (block → block_contents → Z → A) → option A ≝
    22  λS,m,ptr,F.
    23   let b ≝ pblock ptr in
    24   if Zltb (block_id b) (nextblock … m) then
    25    let content ≝ blocks … m b in
    26    let off ≝ offv (poff ptr) in
    27    if andb (Zleb (low … content) off) (Zleb off (high … content)) then
    28     Some … (F b content off)
    29    else
    30     None ?
    31   else
    32    None ?.
    33 
    34 definition beloadv: ∀m:bemem. ∀ptr:pointer. option beval ≝
    35  λm,ptr. do_if_in_bounds … m ptr (λb,content,off. contents … content off).
    36 
    37 definition bestorev: ∀m:bemem. ∀ptr:pointer. beval → option bemem ≝
    38  λm,ptr,v. do_if_in_bounds … m ptr
    39   (λb,content,off.
    40     let contents ≝ update … off v (contents … content) in
    41     let content ≝ mk_block_contents (low … content) (high … content) contents in
    42     let blocks ≝ update_block … b content (blocks … m) in
    43      mk_mem … blocks (nextblock … m) (nextblock_pos … m)).
    4418
    4519definition is_addressable : region → bool ≝ λr.match r with
Note: See TracChangeset for help on using the changeset viewer.