Changeset 1993 for src/joint


Ignore:
Timestamp:
May 24, 2012, 5:10:05 PM (8 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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.