Library Mem

This file develops the memory model that is used in the dynamic semantics of all the languages used in the compiler. It defines a type mem of memory states, the following 4 basic operations over memory states, and their properties:

load: read a memory chunk at a given address;
store: store a memory chunk at a given address;
alloc: allocate a fresh memory block;
free: invalidate a memory block.





Require Import Coqlib.

Require Import Maps.

Require Import AST.

Require Import Integers.

Require Import Floats.

Require Import Values.




Definition update (A: Type) (x: Z) (v: A) (f: Z -> A) : Z -> A :=

  fun y => if zeq y x then v else f y.




Implicit Arguments update [A].




Lemma update_s:

  forall (A: Type) (x: Z) (v: A) (f: Z -> A),

  update x v f x = v.






Lemma update_o:

  forall (A: Type) (x: Z) (v: A) (f: Z -> A) (y: Z),

  x <> y -> update x v f y = f y.

Structure of memory states

A memory state is organized in several disjoint blocks. Each block has a low and a high bound that defines its size. Each block map byte offsets to the contents of this byte.

The possible contents of a byte-sized memory cell. To give intuitions, a 4-byte value v stored at offset d will be represented by the content Datum(4, v) at offset d and Cont at offsets d+1, d+2 and d+3. The Cont contents enable detecting future writes that would partially overlap the 4-byte value.





Inductive content : Type :=

  | Undef: content

undefined contents




  | Datum: nat -> val -> content

first byte of a value




  | Cont: content.

continuation bytes for a multi-byte value







Definition contentmap : Type := Z -> content.

A memory block comprises the dimensions of the block (low and high bounds) plus a mapping from byte offsets to contents.





Record block_contents : Type := mkblock {

  low: Z;

  high: Z;

  contents: contentmap

}.

A memory state is a mapping from block addresses (represented by Z integers) to blocks. We also maintain the address of the next unallocated block, and a proof that this address is positive.





Record mem : Type := mkmem {

  blocks: Z -> block_contents;

  nextblock: block;

  nextblock_pos: nextblock > 0

}.

Operations on memory stores

Memory reads and writes are performed by quantities called memory chunks, encoding the type, size and signedness of the chunk being addressed. The following functions extract the size information from a chunk.





Definition size_chunk (chunk: memory_chunk) : Z :=

  match chunk with

  | Mint8signed => 1

  | Mint8unsigned => 1

  | Mint16signed => 2

  | Mint16unsigned => 2

  | Mint32 => 4

  | Mfloat32 => 4

  | Mfloat64 => 8

  end.




Definition pred_size_chunk (chunk: memory_chunk) : nat :=

  match chunk with

  | Mint8signed => 0%nat

  | Mint8unsigned => 0%nat

  | Mint16signed => 1%nat

  | Mint16unsigned => 1%nat

  | Mint32 => 3%nat

  | Mfloat32 => 3%nat

  | Mfloat64 => 7%nat

  end.




Lemma size_chunk_pred:

  forall chunk, size_chunk chunk = 1 + Z_of_nat (pred_size_chunk chunk).






Lemma size_chunk_pos:

  forall chunk, size_chunk chunk > 0.

Memory reads and writes must respect alignment constraints: the byte offset of the location being addressed should be an exact multiple of the natural alignment for the chunk being addressed. This natural alignment is defined by the following align_chunk function. Some target architectures (e.g. the PowerPC) have no alignment constraints, which we could reflect by taking align_chunk chunk = 1. However, other architectures have stronger alignment requirements. The following definition is appropriate for PowerPC and ARM.





Definition align_chunk (chunk: memory_chunk) : Z := 

  match chunk with

  | Mint8signed => 1

  | Mint8unsigned => 1

  | Mint16signed => 2

  | Mint16unsigned => 2

  | _ => 4

  end.




Lemma align_chunk_pos:

  forall chunk, align_chunk chunk > 0.






Lemma align_size_chunk_divides:

  forall chunk, (align_chunk chunk | size_chunk chunk).






Lemma align_chunk_compat:

  forall chunk1 chunk2,

  size_chunk chunk1 = size_chunk chunk2 -> align_chunk chunk1 = align_chunk chunk2.

The initial store.





Remark one_pos: 1 > 0.






Definition empty_block (lo hi: Z) : block_contents :=

  mkblock lo hi (fun y => Undef).




Definition empty: mem :=

  mkmem (fun x => empty_block 0 0) 1 one_pos.




Definition nullptr: block := 0.

Allocation of a fresh block with the given bounds. Return an updated memory state and the address of the fresh block, which initially contains undefined cells. Note that allocation never fails: we model an infinite memory.





Remark succ_nextblock_pos:

  forall m, Zsucc m.(nextblock) > 0.






Definition alloc (m: mem) (lo hi: Z) :=

  (mkmem (update m.(nextblock) 

                 (empty_block lo hi)

                 m.(blocks))

         (Zsucc m.(nextblock))

         (succ_nextblock_pos m),

   m.(nextblock)).

Freeing a block. Return the updated memory state where the given block address has been invalidated: future reads and writes to this address will fail. Note that we make no attempt to return the block to an allocation pool: the given block address will never be allocated later.





Definition free (m: mem) (b: block) :=

  mkmem (update b 

                (empty_block 0 0)

                m.(blocks))

        m.(nextblock)

        m.(nextblock_pos).

Freeing of a list of blocks.





Definition free_list (m:mem) (l:list block) :=

  List.fold_right (fun b m => free m b) m l.

Return the low and high bounds for the given block address. Those bounds are 0 for freed or not yet allocated address.





Definition low_bound (m: mem) (b: block) :=

  low (m.(blocks) b).

Definition high_bound (m: mem) (b: block) :=

  high (m.(blocks) b).

A block address is valid if it was previously allocated. It remains valid even after being freed.





Definition valid_block (m: mem) (b: block) :=

  b < m.(nextblock).

Reading and writing N adjacent locations in a contentmap.

We define two functions and prove some of their properties:

getN n ofs m returns the datum at offset ofs in block contents m after checking that the contents of offsets ofs+1 to ofs+n+1 are Cont.
setN n ofs v m updates the block contents m, storing the content v at offset ofs and the content Cont at offsets ofs+1 to ofs+n+1.





Fixpoint check_cont (n: nat) (p: Z) (m: contentmap) {struct n} : bool :=

  match n with

  | O => true

  | S n1 =>

      match m p with

      | Cont => check_cont n1 (p + 1) m

      | _ => false

      end

  end.




Definition eq_nat: forall (p q: nat), {p=q} + {p<>q}.






Definition getN (n: nat) (p: Z) (m: contentmap) : val :=

  match m p with

  | Datum n' v =>

      if eq_nat n n' && check_cont n (p + 1) m then v else Vundef

  | _ =>

      Vundef

  end.




Fixpoint set_cont (n: nat) (p: Z) (m: contentmap) {struct n} : contentmap :=

  match n with

  | O => m

  | S n1 => update p Cont (set_cont n1 (p + 1) m)

  end.




Definition setN (n: nat) (p: Z) (v: val) (m: contentmap) : contentmap :=

  update p (Datum n v) (set_cont n (p + 1) m).




Lemma check_cont_spec:

  forall n m p,

  if check_cont n p m

  then (forall q, p <= q < p + Z_of_nat n -> m q = Cont)

  else (exists q, p <= q < p + Z_of_nat n /\ m q <> Cont).






Lemma check_cont_true:

  forall n m p,

  (forall q, p <= q < p + Z_of_nat n -> m q = Cont) ->

  check_cont n p m = true.






Lemma check_cont_false:

  forall n m p q,

  p <= q < p + Z_of_nat n -> m q <> Cont ->

  check_cont n p m = false.






Lemma set_cont_inside:

  forall n p m q,

  p <= q < p + Z_of_nat n ->

  (set_cont n p m) q = Cont.






Lemma set_cont_outside:

  forall n p m q,

  q < p \/ p + Z_of_nat n <= q ->

  (set_cont n p m) q = m q.






Lemma getN_setN_same:

  forall n p v m,

  getN n p (setN n p v m) = v.






Lemma getN_setN_other:

  forall n1 n2 p1 p2 v m,

  p1 + Z_of_nat n1 < p2 \/ p2 + Z_of_nat n2 < p1 ->

  getN n2 p2 (setN n1 p1 v m) = getN n2 p2 m.






Lemma getN_setN_overlap:

  forall n1 n2 p1 p2 v m,

  p1 <> p2 ->

  p1 + Z_of_nat n1 >= p2 -> p2 + Z_of_nat n2 >= p1 ->

  getN n2 p2 (setN n1 p1 v m) = Vundef.






Lemma getN_setN_mismatch:

  forall n1 n2 p v m,

  n1 <> n2 ->

  getN n2 p (setN n1 p v m) = Vundef.






Lemma getN_setN_characterization:

  forall m v n1 p1 n2 p2,

  getN n2 p2 (setN n1 p1 v m) = v

  \/ getN n2 p2 (setN n1 p1 v m) = getN n2 p2 m

  \/ getN n2 p2 (setN n1 p1 v m) = Vundef.






Lemma getN_init:

  forall n p,

  getN n p (fun y => Undef) = Vundef.

valid_access m chunk b ofs holds if a memory access (load or store) of the given chunk is possible in m at address b, ofs. This means:

The block b is valid.
The range of bytes accessed is within the bounds of b.
The offset ofs is aligned.





Inductive valid_access (m: mem) (chunk: memory_chunk) (b: block) (ofs: Z) : Prop :=

  | valid_access_intro:

      valid_block m b ->

      low_bound m b <= ofs ->

      ofs + size_chunk chunk <= high_bound m b ->

      (align_chunk chunk | ofs) ->

      valid_access m chunk b ofs.

The following function checks whether accessing the given memory chunk at the given offset in the given block respects the bounds of the block.





Definition in_bounds (m: mem) (chunk: memory_chunk) (b: block) (ofs: Z) :

           {valid_access m chunk b ofs} + {~valid_access m chunk b ofs}.






Lemma in_bounds_true:

  forall m chunk b ofs (A: Type) (a1 a2: A),

  valid_access m chunk b ofs ->

  (if in_bounds m chunk b ofs then a1 else a2) = a1.

valid_pointer holds if the given block address is valid and the given offset falls within the bounds of the corresponding block.





Definition valid_pointer (m: mem) (b: block) (ofs: Z) : bool :=

  zlt b m.(nextblock) &&

  zle (low_bound m b) ofs &&

  zlt ofs (high_bound m b).

load chunk m b ofs perform a read in memory state m, at address b and offset ofs. None is returned if the address is invalid or the memory access is out of bounds.





Definition load (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z)

                : option val :=

  if in_bounds m chunk b ofs then

    Some (Val.load_result chunk

           (getN (pred_size_chunk chunk) ofs (contents (blocks m b))))

  else

    None.




Lemma load_inv:

  forall chunk m b ofs v,

  load chunk m b ofs = Some v ->

  valid_access m chunk b ofs /\

  v = Val.load_result chunk

           (getN (pred_size_chunk chunk) ofs (contents (blocks m b))).

loadv chunk m addr is similar, but the address and offset are given as a single value addr, which must be a pointer value.





Definition loadv (chunk: memory_chunk) (m: mem) (addr: val) : option val :=

  match addr with

  | Vptr b ofs => load chunk m b (Int.signed ofs)

  | _ => None

  end.




Definition unchecked_store

     (chunk: memory_chunk) (m: mem) (b: block)

     (ofs: Z) (v: val) : mem :=

  let c := m.(blocks) b in

  mkmem

    (update b

        (mkblock c.(low) c.(high)

                 (setN (pred_size_chunk chunk) ofs v c.(contents)))

        m.(blocks))

    m.(nextblock)

    m.(nextblock_pos).

store chunk m b ofs v perform a write in memory state m. Value v is stored at address b and offset ofs. Return the updated memory store, or None if the address is invalid or the memory access is out of bounds.





Definition store (chunk: memory_chunk) (m: mem) (b: block)

                 (ofs: Z) (v: val) : option mem :=

  if in_bounds m chunk b ofs

  then Some(unchecked_store chunk m b ofs v)

  else None.




Lemma store_inv:

  forall chunk m b ofs v m',

  store chunk m b ofs v = Some m' ->

  valid_access m chunk b ofs /\

  m' = unchecked_store chunk m b ofs v.

storev chunk m addr v is similar, but the address and offset are given as a single value addr, which must be a pointer value.





Definition storev (chunk: memory_chunk) (m: mem) (addr v: val) : option mem :=

  match addr with

  | Vptr b ofs => store chunk m b (Int.signed ofs) v

  | _ => None

  end.

Build a block filled with the given initialization data.





Fixpoint contents_init_data (pos: Z) (id: list init_data) {struct id}: contentmap :=

  match id with

  | nil => (fun y => Undef)

  | Init_int8 n :: id' =>

      setN 0%nat pos (Vint n) (contents_init_data (pos + 1) id')

  | Init_int16 n :: id' =>

      setN 1%nat pos (Vint n) (contents_init_data (pos + 1) id')

  | Init_int32 n :: id' =>

      setN 3%nat pos (Vint n) (contents_init_data (pos + 1) id')

  | Init_float32 f :: id' =>

      setN 3%nat pos (Vfloat f) (contents_init_data (pos + 1) id')

  | Init_float64 f :: id' =>

      setN 7%nat pos (Vfloat f) (contents_init_data (pos + 1) id')

  | Init_space n :: id' =>

      contents_init_data (pos + Zmax n 0) id'

  | Init_addrof s n :: id' =>

            contents_init_data (pos + 4) id'

  | Init_pointer x :: id' =>

            contents_init_data (pos + 4) id'

  end.




Definition size_init_data (id: init_data) : Z :=

  match id with

  | Init_int8 _ => 1

  | Init_int16 _ => 2

  | Init_int32 _ => 4

  | Init_float32 _ => 4

  | Init_float64 _ => 8

  | Init_space n => Zmax n 0

  | Init_addrof _ _ => 4

  | Init_pointer _ => 4

  end.




Definition size_init_data_list (id: list init_data): Z :=

  List.fold_right (fun id sz => size_init_data id + sz) 0 id.




Remark size_init_data_list_pos:

  forall id, size_init_data_list id >= 0.






Definition block_init_data (id: list init_data) : block_contents :=

  mkblock 0 (size_init_data_list id) (contents_init_data 0 id).




Definition alloc_init_data (m: mem) (id: list init_data) : mem * block :=

  (mkmem (update m.(nextblock)

                 (block_init_data id)

                 m.(blocks))

         (Zsucc m.(nextblock))

         (succ_nextblock_pos m),

   m.(nextblock)).




Remark block_init_data_empty:

  block_init_data nil = empty_block 0 0.

Properties of the memory operations

Properties related to block validity





Lemma valid_not_valid_diff:

  forall m b b', valid_block m b -> ~(valid_block m b') -> b <> b'.






Lemma valid_access_valid_block:

  forall m chunk b ofs,

  valid_access m chunk b ofs -> valid_block m b.






Lemma valid_access_aligned:

  forall m chunk b ofs,

  valid_access m chunk b ofs -> (align_chunk chunk | ofs).






Lemma valid_access_compat:

  forall m chunk1 chunk2 b ofs,

  size_chunk chunk1 = size_chunk chunk2 ->

  valid_access m chunk1 b ofs ->

  valid_access m chunk2 b ofs.






Hint Resolve valid_not_valid_diff valid_access_valid_block valid_access_aligned: mem.

Properties related to `load`





Theorem valid_access_load:

  forall m chunk b ofs,

  valid_access m chunk b ofs ->

  exists v, load chunk m b ofs = Some v.






Theorem load_valid_access:

  forall m chunk b ofs v,

  load chunk m b ofs = Some v ->

  valid_access m chunk b ofs.






Hint Resolve load_valid_access valid_access_load.

Properties related to `store`





Lemma valid_access_store:

  forall m1 chunk b ofs v,

  valid_access m1 chunk b ofs ->

  exists m2, store chunk m1 b ofs v = Some m2.






Hint Resolve valid_access_store: mem.




Section STORE.

Variable chunk: memory_chunk.

Variable m1: mem.

Variable b: block.

Variable ofs: Z.

Variable v: val.

Variable m2: mem.

Hypothesis STORE: store chunk m1 b ofs v = Some m2.




Lemma low_bound_store:

  forall b', low_bound m2 b' = low_bound m1 b'.






Lemma high_bound_store:

  forall b', high_bound m2 b' = high_bound m1 b'.






Lemma nextblock_store:

  nextblock m2 = nextblock m1.






Lemma store_valid_block_1:

  forall b', valid_block m1 b' -> valid_block m2 b'.






Lemma store_valid_block_2:

  forall b', valid_block m2 b' -> valid_block m1 b'.






Hint Resolve store_valid_block_1 store_valid_block_2: mem.




Lemma store_valid_access_1:

  forall chunk' b' ofs',

  valid_access m1 chunk' b' ofs' -> valid_access m2 chunk' b' ofs'.






Lemma store_valid_access_2:

  forall chunk' b' ofs',

  valid_access m2 chunk' b' ofs' -> valid_access m1 chunk' b' ofs'.






Lemma store_valid_access_3:

  valid_access m1 chunk b ofs.






Hint Resolve store_valid_access_1 store_valid_access_2

             store_valid_access_3: mem.




Theorem load_store_similar:

  forall chunk',

  size_chunk chunk' = size_chunk chunk ->

  load chunk' m2 b ofs = Some (Val.load_result chunk' v).






Theorem load_store_same:

  load chunk m2 b ofs = Some (Val.load_result chunk v).






Theorem load_store_other:

  forall chunk' b' ofs',

  b' <> b

  \/ ofs' + size_chunk chunk' <= ofs

  \/ ofs + size_chunk chunk <= ofs' ->

  load chunk' m2 b' ofs' = load chunk' m1 b' ofs'.






Theorem load_store_overlap:

  forall chunk' ofs' v',

  load chunk' m2 b ofs' = Some v' ->

  ofs' <> ofs ->

  ofs' + size_chunk chunk' > ofs ->

  ofs + size_chunk chunk > ofs' ->

  v' = Vundef.






Theorem load_store_overlap':

  forall chunk' ofs',

  valid_access m1 chunk' b ofs' ->

  ofs' <> ofs ->

  ofs' + size_chunk chunk' > ofs ->

  ofs + size_chunk chunk > ofs' ->

  load chunk' m2 b ofs' = Some Vundef.






Theorem load_store_mismatch:

  forall chunk' v',

  load chunk' m2 b ofs = Some v' ->

  size_chunk chunk' <> size_chunk chunk ->

  v' = Vundef.






Theorem load_store_mismatch':

  forall chunk',

  valid_access m1 chunk' b ofs ->

  size_chunk chunk' <> size_chunk chunk ->

  load chunk' m2 b ofs = Some Vundef.






Inductive load_store_cases 

      (chunk1: memory_chunk) (b1: block) (ofs1: Z)

      (chunk2: memory_chunk) (b2: block) (ofs2: Z) : Type :=

  | lsc_similar:

      b1 = b2 -> ofs1 = ofs2 -> size_chunk chunk1 = size_chunk chunk2 ->

      load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2

  | lsc_other:

      b1 <> b2 \/ ofs2 + size_chunk chunk2 <= ofs1 \/ ofs1 + size_chunk chunk1 <= ofs2 ->

      load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2

  | lsc_overlap:

      b1 = b2 -> ofs1 <> ofs2 -> ofs2 + size_chunk chunk2 > ofs1 -> ofs1 + size_chunk chunk1 > ofs2 ->

      load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2

  | lsc_mismatch:

      b1 = b2 -> ofs1 = ofs2 -> size_chunk chunk1 <> size_chunk chunk2 ->

      load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2.




Definition load_store_classification:

  forall (chunk1: memory_chunk) (b1: block) (ofs1: Z)

         (chunk2: memory_chunk) (b2: block) (ofs2: Z),

  load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2.






Theorem load_store_characterization:

  forall chunk' b' ofs',

  valid_access m1 chunk' b' ofs' ->

  load chunk' m2 b' ofs' =

    match load_store_classification chunk b ofs chunk' b' ofs' with

    | lsc_similar _ _ _ => Some (Val.load_result chunk' v)

    | lsc_other _ => load chunk' m1 b' ofs'

    | lsc_overlap _ _ _ _ => Some Vundef

    | lsc_mismatch _ _ _ => Some Vundef

    end.






End STORE.




Hint Resolve store_valid_block_1 store_valid_block_2: mem.

Hint Resolve store_valid_access_1 store_valid_access_2

             store_valid_access_3: mem.

Properties related to `alloc`.





Section ALLOC.




Variable m1: mem.

Variables lo hi: Z.

Variable m2: mem.

Variable b: block.

Hypothesis ALLOC: alloc m1 lo hi = (m2, b).




Lemma nextblock_alloc:

  nextblock m2 = Zsucc (nextblock m1).






Lemma alloc_result:

  b = nextblock m1.






Lemma valid_block_alloc:

  forall b', valid_block m1 b' -> valid_block m2 b'.






Lemma fresh_block_alloc:

  ~(valid_block m1 b).






Lemma valid_new_block:

  valid_block m2 b.






Hint Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem.




Lemma valid_block_alloc_inv:

  forall b', valid_block m2 b' -> b' = b \/ valid_block m1 b'.






Lemma low_bound_alloc:

  forall b', low_bound m2 b' = if zeq b' b then lo else low_bound m1 b'.






Lemma low_bound_alloc_same:

  low_bound m2 b = lo.






Lemma low_bound_alloc_other:

  forall b', valid_block m1 b' -> low_bound m2 b' = low_bound m1 b'.






Lemma high_bound_alloc:

  forall b', high_bound m2 b' = if zeq b' b then hi else high_bound m1 b'.






Lemma high_bound_alloc_same:

  high_bound m2 b = hi.






Lemma high_bound_alloc_other:

  forall b', valid_block m1 b' -> high_bound m2 b' = high_bound m1 b'.






Lemma valid_access_alloc_other:

  forall chunk b' ofs,

  valid_access m1 chunk b' ofs ->

  valid_access m2 chunk b' ofs.






Lemma valid_access_alloc_same:

  forall chunk ofs,

  lo <= ofs -> ofs + size_chunk chunk <= hi -> (align_chunk chunk | ofs) ->

  valid_access m2 chunk b ofs.






Hint Resolve valid_access_alloc_other valid_access_alloc_same: mem.




Lemma valid_access_alloc_inv:

  forall chunk b' ofs,

  valid_access m2 chunk b' ofs ->

  valid_access m1 chunk b' ofs \/

  (b' = b /\ lo <= ofs /\ ofs + size_chunk chunk <= hi /\ (align_chunk chunk | ofs)).






Theorem load_alloc_unchanged:

  forall chunk b' ofs,

  valid_block m1 b' ->

  load chunk m2 b' ofs = load chunk m1 b' ofs.






Theorem load_alloc_other:

  forall chunk b' ofs v,

  load chunk m1 b' ofs = Some v ->

  load chunk m2 b' ofs = Some v.






Theorem load_alloc_same:

  forall chunk ofs v,

  load chunk m2 b ofs = Some v ->

  v = Vundef.






Theorem load_alloc_same':

  forall chunk ofs,

  lo <= ofs -> ofs + size_chunk chunk <= hi -> (align_chunk chunk | ofs) ->

  load chunk m2 b ofs = Some Vundef.






End ALLOC.




Hint Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem.

Hint Resolve valid_access_alloc_other valid_access_alloc_same: mem.

Hint Resolve load_alloc_unchanged: mem.

Properties related to `free`.





Section FREE.




Variable m: mem.

Variable bf: block.




Lemma valid_block_free_1:

  forall b, valid_block m b -> valid_block (free m bf) b.






Lemma valid_block_free_2:

  forall b, valid_block (free m bf) b -> valid_block m b.






Hint Resolve valid_block_free_1 valid_block_free_2: mem.




Lemma low_bound_free:

  forall b, b <> bf -> low_bound (free m bf) b = low_bound m b.






Lemma high_bound_free:

  forall b, b <> bf -> high_bound (free m bf) b = high_bound m b.






Lemma low_bound_free_same:

  forall m b, low_bound (free m b) b = 0.






Lemma high_bound_free_same:

  forall m b, high_bound (free m b) b = 0.






Lemma valid_access_free_1:

  forall chunk b ofs,

  valid_access m chunk b ofs -> b <> bf ->

  valid_access (free m bf) chunk b ofs.






Lemma valid_access_free_2:

  forall chunk ofs, ~(valid_access (free m bf) chunk bf ofs).






Hint Resolve valid_access_free_1 valid_access_free_2: mem.




Lemma valid_access_free_inv:

  forall chunk b ofs,

  valid_access (free m bf) chunk b ofs ->

  valid_access m chunk b ofs /\ b <> bf.






Theorem load_free:

  forall chunk b ofs,

  b <> bf ->

  load chunk (free m bf) b ofs = load chunk m b ofs.






End FREE.

Properties related to `free_list`





Lemma valid_block_free_list_1:

  forall bl m b, valid_block m b -> valid_block (free_list m bl) b.






Lemma valid_block_free_list_2:

  forall bl m b, valid_block (free_list m bl) b -> valid_block m b.






Lemma valid_access_free_list:

  forall chunk b ofs m bl,

  valid_access m chunk b ofs -> ~In b bl ->

  valid_access (free_list m bl) chunk b ofs.






Lemma valid_access_free_list_inv:

  forall chunk b ofs m bl,

  valid_access (free_list m bl) chunk b ofs ->

  ~In b bl /\ valid_access m chunk b ofs.

Properties related to pointer validity





Lemma valid_pointer_valid_access:

  forall m b ofs,

  valid_pointer m b ofs = true <-> valid_access m Mint8unsigned b ofs.






Theorem valid_pointer_alloc:

  forall (m1 m2: mem) (lo hi: Z) (b b': block) (ofs: Z), 

  alloc m1 lo hi = (m2, b') ->

  valid_pointer m1 b ofs = true ->

  valid_pointer m2 b ofs = true.






Theorem valid_pointer_store:

  forall (chunk: memory_chunk) (m1 m2: mem) (b b': block) (ofs ofs': Z) (v: val),

  store chunk m1 b' ofs' v = Some m2 ->

  valid_pointer m1 b ofs = true -> valid_pointer m2 b ofs = true.

Generic injections between memory states.





Section GENERIC_INJECT.




Definition meminj : Type := block -> option (block * Z).




Variable val_inj: meminj -> val -> val -> Prop.




Hypothesis val_inj_undef:

  forall mi, val_inj mi Vundef Vundef.




Definition mem_inj (mi: meminj) (m1 m2: mem) :=

  forall chunk b1 ofs v1 b2 delta,

  mi b1 = Some(b2, delta) ->

  load chunk m1 b1 ofs = Some v1 ->

  exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ val_inj mi v1 v2.




Lemma valid_access_inj:

  forall mi m1 m2 chunk b1 ofs b2 delta,

  mi b1 = Some(b2, delta) ->

  mem_inj mi m1 m2 ->

  valid_access m1 chunk b1 ofs ->

  valid_access m2 chunk b2 (ofs + delta).






Hint Resolve valid_access_inj: mem.




Lemma store_unmapped_inj:

  forall mi m1 m2 b ofs v chunk m1',

  mem_inj mi m1 m2 ->

  mi b = None ->

  store chunk m1 b ofs v = Some m1' ->

  mem_inj mi m1' m2.






Lemma store_outside_inj:

  forall mi m1 m2 chunk b ofs v m2',

  mem_inj mi m1 m2 ->

  (forall b' delta,

    mi b' = Some(b, delta) ->

    high_bound m1 b' + delta <= ofs

    \/ ofs + size_chunk chunk <= low_bound m1 b' + delta) ->

  store chunk m2 b ofs v = Some m2' ->

  mem_inj mi m1 m2'.






Definition meminj_no_overlap (mi: meminj) (m: mem) : Prop :=

  forall b1 b1' delta1 b2 b2' delta2,

  b1 <> b2 ->

  mi b1 = Some (b1', delta1) ->

  mi b2 = Some (b2', delta2) ->

  b1' <> b2' 

  \/ low_bound m b1 >= high_bound m b1

  \/ low_bound m b2 >= high_bound m b2

  \/ high_bound m b1 + delta1 <= low_bound m b2 + delta2 

  \/ high_bound m b2 + delta2 <= low_bound m b1 + delta1.




Lemma store_mapped_inj:

  forall mi m1 m2 b1 ofs b2 delta v1 v2 chunk m1',

  mem_inj mi m1 m2 ->

  meminj_no_overlap mi m1 ->

  mi b1 = Some(b2, delta) ->

  store chunk m1 b1 ofs v1 = Some m1' ->

  (forall chunk', size_chunk chunk' = size_chunk chunk ->

    val_inj mi (Val.load_result chunk' v1) (Val.load_result chunk' v2)) ->

  exists m2',

  store chunk m2 b2 (ofs + delta) v2 = Some m2' /\ mem_inj mi m1' m2'.






Definition inj_offset_aligned (delta: Z) (size: Z) : Prop :=

  forall chunk, size_chunk chunk <= size -> (align_chunk chunk | delta).




Lemma alloc_parallel_inj:

  forall mi m1 m2 lo1 hi1 m1' b1 lo2 hi2 m2' b2 delta,

  mem_inj mi m1 m2 ->

  alloc m1 lo1 hi1 = (m1', b1) ->

  alloc m2 lo2 hi2 = (m2', b2) ->

  mi b1 = Some(b2, delta) ->

  lo2 <= lo1 + delta -> hi1 + delta <= hi2 ->

  inj_offset_aligned delta (hi1 - lo1) ->

  mem_inj mi m1' m2'.






Lemma alloc_right_inj:

  forall mi m1 m2 lo hi b2 m2',

  mem_inj mi m1 m2 ->

  alloc m2 lo hi = (m2', b2) ->

  mem_inj mi m1 m2'.






Hypothesis val_inj_undef_any:

  forall mi v, val_inj mi Vundef v.




Lemma alloc_left_unmapped_inj:

  forall mi m1 m2 lo hi b1 m1',

  mem_inj mi m1 m2 ->

  alloc m1 lo hi = (m1', b1) ->

  mi b1 = None ->

  mem_inj mi m1' m2.






Lemma alloc_left_mapped_inj:

  forall mi m1 m2 lo hi b1 m1' b2 delta,

  mem_inj mi m1 m2 ->

  alloc m1 lo hi = (m1', b1) ->

  mi b1 = Some(b2, delta) ->

  valid_block m2 b2 ->

  low_bound m2 b2 <= lo + delta -> hi + delta <= high_bound m2 b2 ->

  inj_offset_aligned delta (hi - lo) ->

  mem_inj mi m1' m2.






Lemma free_parallel_inj:

  forall mi m1 m2 b1 b2 delta,

  mem_inj mi m1 m2 ->

  mi b1 = Some(b2, delta) ->

  (forall b delta', mi b = Some(b2, delta') -> b = b1) ->

  mem_inj mi (free m1 b1) (free m2 b2).






Lemma free_left_inj:

  forall mi m1 m2 b1,

  mem_inj mi m1 m2 ->

  mem_inj mi (free m1 b1) m2.






Lemma free_list_left_inj:

  forall mi bl m1 m2,

  mem_inj mi m1 m2 ->

  mem_inj mi (free_list m1 bl) m2.






Lemma free_right_inj:

  forall mi m1 m2 b2,

  mem_inj mi m1 m2 ->

  (forall b1 delta chunk ofs, 

   mi b1 = Some(b2, delta) -> ~(valid_access m1 chunk b1 ofs)) ->

  mem_inj mi m1 (free m2 b2).






Lemma valid_pointer_inj:

  forall mi m1 m2 b1 ofs b2 delta,

  mi b1 = Some(b2, delta) ->

  mem_inj mi m1 m2 ->

  valid_pointer m1 b1 ofs = true ->

  valid_pointer m2 b2 (ofs + delta) = true.






End GENERIC_INJECT.

Store extensions

A store m2 extends a store m1 if m2 can be obtained from m1 by increasing the sizes of the memory blocks of m1 (decreasing the low bounds, increasing the high bounds), while still keeping the same contents for block offsets that are valid in m1.





Definition inject_id : meminj := fun b => Some(b, 0).




Definition val_inj_id (mi: meminj) (v1 v2: val) : Prop := v1 = v2.




Definition extends (m1 m2: mem) :=

  nextblock m1 = nextblock m2 /\ mem_inj val_inj_id inject_id m1 m2.




Theorem extends_refl:

  forall (m: mem), extends m m.






Theorem alloc_extends:

  forall (m1 m2 m1' m2': mem) (lo1 hi1 lo2 hi2: Z) (b1 b2: block),

  extends m1 m2 ->

  lo2 <= lo1 -> hi1 <= hi2 ->

  alloc m1 lo1 hi1 = (m1', b1) ->

  alloc m2 lo2 hi2 = (m2', b2) ->

  b1 = b2 /\ extends m1' m2'.






Theorem free_extends:

  forall (m1 m2: mem) (b: block),

  extends m1 m2 ->

  extends (free m1 b) (free m2 b).






Theorem load_extends:

  forall (chunk: memory_chunk) (m1 m2: mem) (b: block) (ofs: Z) (v: val),

  extends m1 m2 ->

  load chunk m1 b ofs = Some v ->

  load chunk m2 b ofs = Some v.






Theorem store_within_extends:

  forall (chunk: memory_chunk) (m1 m2 m1': mem) (b: block) (ofs: Z) (v: val),

  extends m1 m2 ->

  store chunk m1 b ofs v = Some m1' ->

  exists m2', store chunk m2 b ofs v = Some m2' /\ extends m1' m2'.






Theorem store_outside_extends:

  forall (chunk: memory_chunk) (m1 m2 m2': mem) (b: block) (ofs: Z) (v: val),

  extends m1 m2 ->

  ofs + size_chunk chunk <= low_bound m1 b \/ high_bound m1 b <= ofs ->

  store chunk m2 b ofs v = Some m2' ->

  extends m1 m2'.






Theorem valid_pointer_extends:

  forall m1 m2 b ofs,

  extends m1 m2 -> valid_pointer m1 b ofs = true ->

  valid_pointer m2 b ofs = true.

The ``less defined than'' relation over memory states

A memory state m1 is less defined than m2 if, for all addresses, the value v1 read in m1 at this address is less defined than the value v2 read in m2, that is, either v1 = v2 or v1 = Vundef.





Definition val_inj_lessdef (mi: meminj) (v1 v2: val) : Prop :=

  Val.lessdef v1 v2.




Definition lessdef (m1 m2: mem) : Prop :=

  nextblock m1 = nextblock m2 /\

  mem_inj val_inj_lessdef inject_id m1 m2.




Lemma lessdef_refl:

  forall m, lessdef m m.






Lemma load_lessdef:

  forall m1 m2 chunk b ofs v1,

  lessdef m1 m2 -> load chunk m1 b ofs = Some v1 ->

  exists v2, load chunk m2 b ofs = Some v2 /\ Val.lessdef v1 v2.






Lemma loadv_lessdef:

  forall m1 m2 chunk addr1 addr2 v1,

  lessdef m1 m2 -> Val.lessdef addr1 addr2 ->

  loadv chunk m1 addr1 = Some v1 ->

  exists v2, loadv chunk m2 addr2 = Some v2 /\ Val.lessdef v1 v2.






Lemma store_lessdef:

  forall m1 m2 chunk b ofs v1 v2 m1',

  lessdef m1 m2 -> Val.lessdef v1 v2 ->

  store chunk m1 b ofs v1 = Some m1' ->

  exists m2', store chunk m2 b ofs v2 = Some m2' /\ lessdef m1' m2'.






Lemma storev_lessdef:

  forall m1 m2 chunk addr1 v1 addr2 v2 m1',

  lessdef m1 m2 -> Val.lessdef addr1 addr2 -> Val.lessdef v1 v2 ->

  storev chunk m1 addr1 v1 = Some m1' ->

  exists m2', storev chunk m2 addr2 v2 = Some m2' /\ lessdef m1' m2'.






Lemma alloc_lessdef:

  forall m1 m2 lo hi b1 m1' b2 m2',

  lessdef m1 m2 -> alloc m1 lo hi = (m1', b1) -> alloc m2 lo hi = (m2', b2) ->

  b1 = b2 /\ lessdef m1' m2'.






Lemma free_lessdef:

  forall m1 m2 b, lessdef m1 m2 -> lessdef (free m1 b) (free m2 b).






Lemma free_left_lessdef:

  forall m1 m2 b,

  lessdef m1 m2 -> lessdef (free m1 b) m2.






Lemma free_right_lessdef:

  forall m1 m2 b,

  lessdef m1 m2 -> low_bound m1 b >= high_bound m1 b ->

  lessdef m1 (free m2 b).






Lemma valid_block_lessdef:

  forall m1 m2 b, lessdef m1 m2 -> valid_block m1 b -> valid_block m2 b.






Lemma valid_pointer_lessdef:

  forall m1 m2 b ofs,

  lessdef m1 m2 -> valid_pointer m1 b ofs = true -> valid_pointer m2 b ofs = true.

Memory injections

A memory injection f is a function from addresses to either None or Some of an address and an offset. It defines a correspondence between the blocks of two memory states m1 and m2:

if f b = None, the block b of m1 has no equivalent in m2;
if f b = Some(b', ofs), the block b of m2 corresponds to a sub-block at offset ofs of the block b' in m2.

A memory injection defines a relation between values that is the identity relation, except for pointer values which are shifted as prescribed by the memory injection.





Inductive val_inject (mi: meminj): val -> val -> Prop :=

  | val_inject_int:

      forall i, val_inject mi (Vint i) (Vint i)

  | val_inject_float:

      forall f, val_inject mi (Vfloat f) (Vfloat f)

  | val_inject_ptr:

      forall b1 ofs1 b2 ofs2 x,

      mi b1 = Some (b2, x) ->

      ofs2 = Int.add ofs1 (Int.repr x) ->

      val_inject mi (Vptr b1 ofs1) (Vptr b2 ofs2)

  | val_inject_undef: forall v,

      val_inject mi Vundef v.




Hint Resolve val_inject_int val_inject_float val_inject_ptr 

             val_inject_undef.




Inductive val_list_inject (mi: meminj): list val -> list val-> Prop:= 

  | val_nil_inject :

      val_list_inject mi nil nil

  | val_cons_inject : forall v v' vl vl' , 

      val_inject mi v v' -> val_list_inject mi vl vl'->

      val_list_inject mi (v :: vl) (v' :: vl').




Hint Resolve val_nil_inject val_cons_inject.

A memory state m1 injects into another memory state m2 via the memory injection f if the following conditions hold:

loads in m1 must have matching loads in m2 in the sense of the mem_inj predicate;
unallocated blocks in m1 must be mapped to None by f;
if f b = Some(b', delta), b' must be valid in m2;
distinct blocks in m1 are mapped to non-overlapping sub-blocks in m2;
the sizes of m2's blocks are representable with signed machine integers;
the offsets delta are representable with signed machine integers.





Record mem_inject (f: meminj) (m1 m2: mem) : Prop :=

  mk_mem_inject {

    mi_inj:

      mem_inj val_inject f m1 m2;

    mi_freeblocks:

      forall b, ~(valid_block m1 b) -> f b = None;

    mi_mappedblocks:

      forall b b' delta, f b = Some(b', delta) -> valid_block m2 b';

    mi_no_overlap:

      meminj_no_overlap f m1;

    mi_range_1:

      forall b b' delta,

      f b = Some(b', delta) ->

      Int.min_signed <= delta <= Int.max_signed;

    mi_range_2:

      forall b b' delta,

      f b = Some(b', delta) ->

      delta = 0 \/ (Int.min_signed <= low_bound m2 b' /\ high_bound m2 b' <= Int.max_signed)

  }.

The following lemmas establish the absence of machine integer overflow during address computations.





Lemma address_inject:

  forall f m1 m2 chunk b1 ofs1 b2 delta,

  mem_inject f m1 m2 ->

  valid_access m1 chunk b1 (Int.signed ofs1) ->

  f b1 = Some (b2, delta) ->

  Int.signed (Int.add ofs1 (Int.repr delta)) = Int.signed ofs1 + delta.






Lemma valid_pointer_inject_no_overflow:

  forall f m1 m2 b ofs b' x,

  mem_inject f m1 m2 ->

  valid_pointer m1 b (Int.signed ofs) = true ->

  f b = Some(b', x) ->

  Int.min_signed <= Int.signed ofs + Int.signed (Int.repr x) <= Int.max_signed.






Lemma valid_pointer_inject:

  forall f m1 m2 b ofs b' ofs',

  mem_inject f m1 m2 ->

  valid_pointer m1 b (Int.signed ofs) = true ->

  val_inject f (Vptr b ofs) (Vptr b' ofs') ->

  valid_pointer m2 b' (Int.signed ofs') = true.






Lemma different_pointers_inject:

  forall f m m' b1 ofs1 b2 ofs2 b1' delta1 b2' delta2,

  mem_inject f m m' ->

  b1 <> b2 ->

  valid_pointer m b1 (Int.signed ofs1) = true ->

  valid_pointer m b2 (Int.signed ofs2) = true ->

  f b1 = Some (b1', delta1) ->

  f b2 = Some (b2', delta2) ->

  b1' <> b2' \/

  Int.signed (Int.add ofs1 (Int.repr delta1)) <>

  Int.signed (Int.add ofs2 (Int.repr delta2)).

Relation between injections and loads.





Lemma load_inject:

  forall f m1 m2 chunk b1 ofs b2 delta v1,

  mem_inject f m1 m2 ->

  load chunk m1 b1 ofs = Some v1 ->

  f b1 = Some (b2, delta) ->

  exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ val_inject f v1 v2.






Lemma loadv_inject:

  forall f m1 m2 chunk a1 a2 v1,

  mem_inject f m1 m2 ->

  loadv chunk m1 a1 = Some v1 ->

  val_inject f a1 a2 ->

  exists v2, loadv chunk m2 a2 = Some v2 /\ val_inject f v1 v2.

Relation between injections and stores.





Inductive val_content_inject (f: meminj): memory_chunk -> val -> val -> Prop :=

  | val_content_inject_base:

      forall chunk v1 v2,

      val_inject f v1 v2 ->

      val_content_inject f chunk v1 v2

  | val_content_inject_8:

      forall chunk n1 n2,

      chunk = Mint8unsigned \/ chunk = Mint8signed ->

      Int.zero_ext 8 n1 = Int.zero_ext 8 n2 ->

      val_content_inject f chunk (Vint n1) (Vint n2)

  | val_content_inject_16:

      forall chunk n1 n2,

      chunk = Mint16unsigned \/ chunk = Mint16signed ->

      Int.zero_ext 16 n1 = Int.zero_ext 16 n2 ->

      val_content_inject f chunk (Vint n1) (Vint n2)

  | val_content_inject_32:

      forall f1 f2,

      Float.singleoffloat f1 = Float.singleoffloat f2 ->

      val_content_inject f Mfloat32 (Vfloat f1) (Vfloat f2).




Hint Resolve val_content_inject_base.




Lemma load_result_inject:

  forall f chunk v1 v2 chunk',

  val_content_inject f chunk v1 v2 ->

  size_chunk chunk = size_chunk chunk' ->

  val_inject f (Val.load_result chunk' v1) (Val.load_result chunk' v2).






Lemma store_mapped_inject_1 :

  forall f chunk m1 b1 ofs v1 n1 m2 b2 delta v2,

  mem_inject f m1 m2 ->

  store chunk m1 b1 ofs v1 = Some n1 ->

  f b1 = Some (b2, delta) ->

  val_content_inject f chunk v1 v2 ->

  exists n2,

    store chunk m2 b2 (ofs + delta) v2 = Some n2

    /\ mem_inject f n1 n2.






Lemma store_mapped_inject:

  forall f chunk m1 b1 ofs v1 n1 m2 b2 delta v2,

  mem_inject f m1 m2 ->

  store chunk m1 b1 ofs v1 = Some n1 ->

  f b1 = Some (b2, delta) ->

  val_inject f v1 v2 ->

  exists n2,

    store chunk m2 b2 (ofs + delta) v2 = Some n2

    /\ mem_inject f n1 n2.






Lemma store_unmapped_inject:

  forall f chunk m1 b1 ofs v1 n1 m2,

  mem_inject f m1 m2 ->

  store chunk m1 b1 ofs v1 = Some n1 ->

  f b1 = None ->

  mem_inject f n1 m2.






Lemma storev_mapped_inject_1:

  forall f chunk m1 a1 v1 n1 m2 a2 v2,

  mem_inject f m1 m2 ->

  storev chunk m1 a1 v1 = Some n1 ->

  val_inject f a1 a2 ->

  val_content_inject f chunk v1 v2 ->

  exists n2,

    storev chunk m2 a2 v2 = Some n2 /\ mem_inject f n1 n2.






Lemma storev_mapped_inject:

  forall f chunk m1 a1 v1 n1 m2 a2 v2,

  mem_inject f m1 m2 ->

  storev chunk m1 a1 v1 = Some n1 ->

  val_inject f a1 a2 ->

  val_inject f v1 v2 ->

  exists n2,

    storev chunk m2 a2 v2 = Some n2 /\ mem_inject f n1 n2.

Relation between injections and free





Lemma meminj_no_overlap_free:

  forall mi m b,

  meminj_no_overlap mi m ->

  meminj_no_overlap mi (free m b).






Lemma meminj_no_overlap_free_list:

  forall mi m bl,

  meminj_no_overlap mi m ->

  meminj_no_overlap mi (free_list m bl).






Lemma free_inject:

  forall f m1 m2 l b,

  (forall b1 delta, f b1 = Some(b, delta) -> In b1 l) ->

  mem_inject f m1 m2 ->

  mem_inject f (free_list m1 l) (free m2 b).

Monotonicity properties of memory injections.





Definition inject_incr (f1 f2: meminj) : Prop :=

  forall b, f1 b = f2 b \/ f1 b = None.




Lemma inject_incr_refl :

   forall f , inject_incr f f .






Lemma inject_incr_trans :

  forall f1 f2 f3, 

  inject_incr f1 f2 -> inject_incr f2 f3 -> inject_incr f1 f3 .






Lemma val_inject_incr:

  forall f1 f2 v v',

  inject_incr f1 f2 ->

  val_inject f1 v v' ->

  val_inject f2 v v'.






Lemma val_list_inject_incr:

  forall f1 f2 vl vl' ,

  inject_incr f1 f2 -> val_list_inject f1 vl vl' ->

  val_list_inject f2 vl vl'.






Hint Resolve inject_incr_refl val_inject_incr val_list_inject_incr.

Properties of injections and allocations.





Definition extend_inject

       (b: block) (x: option (block * Z)) (f: meminj) : meminj :=

  fun (b': block) => if zeq b' b then x else f b'.




Lemma extend_inject_incr:

  forall f b x,

  f b = None ->

  inject_incr f (extend_inject b x f).






Lemma alloc_right_inject:

  forall f m1 m2 lo hi m2' b,

  mem_inject f m1 m2 ->

  alloc m2 lo hi = (m2', b) ->

  mem_inject f m1 m2'.






Lemma alloc_unmapped_inject:

  forall f m1 m2 lo hi m1' b,

  mem_inject f m1 m2 ->

  alloc m1 lo hi = (m1', b) ->

  mem_inject (extend_inject b None f) m1' m2 /\

  inject_incr f (extend_inject b None f).






Lemma alloc_mapped_inject:

  forall f m1 m2 lo hi m1' b b' ofs,

  mem_inject f m1 m2 ->

  alloc m1 lo hi = (m1', b) ->

  valid_block m2 b' ->

  Int.min_signed <= ofs <= Int.max_signed ->

  Int.min_signed <= low_bound m2 b' ->

  high_bound m2 b' <= Int.max_signed ->

  low_bound m2 b' <= lo + ofs ->

  hi + ofs <= high_bound m2 b' ->

  inj_offset_aligned ofs (hi-lo) ->

  (forall b0 ofs0, 

   f b0 = Some (b', ofs0) -> 

   high_bound m1 b0 + ofs0 <= lo + ofs \/

   hi + ofs <= low_bound m1 b0 + ofs0) ->

  mem_inject (extend_inject b (Some (b', ofs)) f) m1' m2 /\

  inject_incr f (extend_inject b (Some (b', ofs)) f).






Lemma alloc_parallel_inject:

  forall f m1 m2 lo hi m1' m2' b1 b2,

  mem_inject f m1 m2 ->

  alloc m1 lo hi = (m1', b1) ->

  alloc m2 lo hi = (m2', b2) ->

  Int.min_signed <= lo -> hi <= Int.max_signed ->

  mem_inject (extend_inject b1 (Some(b2, 0)) f) m1' m2' /\

  inject_incr f (extend_inject b1 (Some(b2, 0)) f).






Definition meminj_init (m: mem) : meminj :=

  fun (b: block) => if zlt b m.(nextblock) then Some(b, 0) else None.




Definition mem_inject_neutral (m: mem) : Prop :=

  forall f chunk b ofs v,

  load chunk m b ofs = Some v -> val_inject f v v.




Lemma init_inject:

  forall m,

  mem_inject_neutral m ->

  mem_inject (meminj_init m) m m.






Remark getN_setN_inject:

  forall f m v n1 p1 n2 p2,

  val_inject f (getN n2 p2 m) (getN n2 p2 m) ->

  val_inject f v v ->

  val_inject f (getN n2 p2 (setN n1 p1 v m))

               (getN n2 p2 (setN n1 p1 v m)).






Remark getN_contents_init_data_inject:

  forall f n ofs id pos,

  val_inject f (getN n ofs (contents_init_data pos id))

               (getN n ofs (contents_init_data pos id)).






Lemma alloc_init_data_neutral:

  forall m id m' b,

  mem_inject_neutral m ->

  alloc_init_data m id = (m', b) ->

  mem_inject_neutral m'.

Memory shifting

A special case of memory injection where blocks are not coalesced: each source block injects in a distinct target block.





Definition memshift := block -> option Z.




Definition meminj_of_shift (mi: memshift) : meminj :=

  fun b => match mi b with None => None | Some x => Some (b, x) end.




Definition val_shift (mi: memshift) (v1 v2: val): Prop :=

  val_inject (meminj_of_shift mi) v1 v2.




Record mem_shift (f: memshift) (m1 m2: mem) : Prop :=

  mk_mem_shift {

    ms_inj:

      mem_inj val_inject (meminj_of_shift f) m1 m2;

    ms_samedomain:

      nextblock m1 = nextblock m2;

    ms_domain:

      forall b, match f b with Some _ => b < nextblock m1 | None => b >= nextblock m1 end;

    ms_range_1:

      forall b delta,

      f b = Some delta ->

      Int.min_signed <= delta <= Int.max_signed;

    ms_range_2:

      forall b delta,

      f b = Some delta ->

      Int.min_signed <= low_bound m2 b /\ high_bound m2 b <= Int.max_signed

  }.

The following lemmas establish the absence of machine integer overflow during address computations.





Lemma address_shift:

  forall f m1 m2 chunk b ofs1 delta,

  mem_shift f m1 m2 ->

  valid_access m1 chunk b (Int.signed ofs1) ->

  f b = Some delta ->

  Int.signed (Int.add ofs1 (Int.repr delta)) = Int.signed ofs1 + delta.






Lemma valid_pointer_shift_no_overflow:

  forall f m1 m2 b ofs x,

  mem_shift f m1 m2 ->

  valid_pointer m1 b (Int.signed ofs) = true ->

  f b = Some x ->

  Int.min_signed <= Int.signed ofs + Int.signed (Int.repr x) <= Int.max_signed.






Lemma valid_pointer_shift:

  forall f m1 m2 b ofs b' ofs',

  mem_shift f m1 m2 ->

  valid_pointer m1 b (Int.signed ofs) = true ->

  val_shift f (Vptr b ofs) (Vptr b' ofs') ->

  valid_pointer m2 b' (Int.signed ofs') = true.

Relation between shifts and loads.





Lemma load_shift:

  forall f m1 m2 chunk b ofs delta v1,

  mem_shift f m1 m2 ->

  load chunk m1 b ofs = Some v1 ->

  f b = Some delta ->

  exists v2, load chunk m2 b (ofs + delta) = Some v2 /\ val_shift f v1 v2.






Lemma loadv_shift:

  forall f m1 m2 chunk a1 a2 v1,

  mem_shift f m1 m2 ->

  loadv chunk m1 a1 = Some v1 ->

  val_shift f a1 a2 ->

  exists v2, loadv chunk m2 a2 = Some v2 /\ val_shift f v1 v2.

Relation between shifts and stores.





Lemma store_within_shift:

  forall f chunk m1 b ofs v1 n1 m2 delta v2,

  mem_shift f m1 m2 ->

  store chunk m1 b ofs v1 = Some n1 ->

  f b = Some delta ->

  val_shift f v1 v2 ->

  exists n2,

    store chunk m2 b (ofs + delta) v2 = Some n2

    /\ mem_shift f n1 n2.






Lemma store_outside_shift:

  forall f chunk m1 b ofs m2 v m2' delta,

  mem_shift f m1 m2 ->

  f b = Some delta ->

  high_bound m1 b + delta <= ofs

  \/ ofs + size_chunk chunk <= low_bound m1 b + delta ->

  store chunk m2 b ofs v = Some m2' ->

  mem_shift f m1 m2'.






Lemma storev_shift:

  forall f chunk m1 a1 v1 n1 m2 a2 v2,

  mem_shift f m1 m2 ->

  storev chunk m1 a1 v1 = Some n1 ->

  val_shift f a1 a2 ->

  val_shift f v1 v2 ->

  exists n2,

    storev chunk m2 a2 v2 = Some n2 /\ mem_shift f n1 n2.

Relation between shifts and free.





Lemma free_shift:

  forall f m1 m2 b,

  mem_shift f m1 m2 ->

  mem_shift f (free m1 b) (free m2 b).

Relation between shifts and allocation.





Definition shift_incr (f1 f2: memshift) : Prop :=

  forall b, f1 b = f2 b \/ f1 b = None.




Remark shift_incr_inject_incr:

  forall f1 f2,

  shift_incr f1 f2 -> inject_incr (meminj_of_shift f1) (meminj_of_shift f2).






Lemma val_shift_incr:

  forall f1 f2 v1 v2,

  shift_incr f1 f2 -> val_shift f1 v1 v2 -> val_shift f2 v1 v2.






Lemma alloc_shift:

  forall f m1 m2 lo1 hi1 m1' b delta lo2 hi2,

  mem_shift f m1 m2 ->

  alloc m1 lo1 hi1 = (m1', b) ->

  lo2 <= lo1 + delta -> hi1 + delta <= hi2 ->

  Int.min_signed <= delta <= Int.max_signed ->

  Int.min_signed <= lo2 -> hi2 <= Int.max_signed ->

  inj_offset_aligned delta (hi1-lo1) ->

  exists f', exists m2',

     alloc m2 lo2 hi2 = (m2', b)

  /\ mem_shift f' m1' m2'

  /\ shift_incr f f'

  /\ f' b = Some delta.

Relation between signed and unsigned loads and stores

Target processors do not distinguish between signed and unsigned stores of 8- and 16-bit quantities. We show these are equivalent.

Signed 8- and 16-bit stores can be performed like unsigned stores.





Remark in_bounds_equiv:

  forall chunk1 chunk2 m b ofs (A: Type) (a1 a2: A),

  size_chunk chunk1 = size_chunk chunk2 ->

  (if in_bounds m chunk1 b ofs then a1 else a2) =

  (if in_bounds m chunk2 b ofs then a1 else a2).






Lemma storev_8_signed_unsigned:

  forall m a v,

  storev Mint8signed m a v = storev Mint8unsigned m a v.






Lemma storev_16_signed_unsigned:

  forall m a v,

  storev Mint16signed m a v = storev Mint16unsigned m a v.

Likewise, some target processors (e.g. the PowerPC) do not have a ``load 8-bit signed integer'' instruction. We show that it can be synthesized as a ``load 8-bit unsigned integer'' followed by a sign extension.





Lemma loadv_8_signed_unsigned:

  forall m a,

  loadv Mint8signed m a = option_map (Val.sign_ext 8) (loadv Mint8unsigned m a).