diff options
Diffstat (limited to 'common/Mem.v')
| -rw-r--r-- | common/Mem.v | 2887 |
1 files changed, 0 insertions, 2887 deletions
diff --git a/common/Mem.v b/common/Mem.v deleted file mode 100644 index 252ee29..0000000 --- a/common/Mem.v +++ /dev/null @@ -1,2887 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* Sandrine Blazy, ENSIIE and INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** 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. -Proof. - intros; unfold update. apply zeq_true. -Qed. - -Lemma update_o: - forall (A: Type) (x: Z) (v: A) (f: Z -> A) (y: Z), - x <> y -> update x v f y = f y. -Proof. - intros; unfold update. apply zeq_false; auto. -Qed. - -(** * 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 (**r undefined contents *) - | Datum: nat -> val -> content (**r first byte of a value *) - | Cont: content. (**r 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). -Proof. - destruct chunk; auto. -Qed. - -Lemma size_chunk_pos: - forall chunk, size_chunk chunk > 0. -Proof. - intros. rewrite size_chunk_pred. omega. -Qed. - -(** 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. -Proof. - intro. destruct chunk; simpl; omega. -Qed. - -Lemma align_size_chunk_divides: - forall chunk, (align_chunk chunk | size_chunk chunk). -Proof. - intros. destruct chunk; simpl; try apply Zdivide_refl. exists 2; auto. -Qed. - -Lemma align_chunk_compat: - forall chunk1 chunk2, - size_chunk chunk1 = size_chunk chunk2 -> align_chunk chunk1 = align_chunk chunk2. -Proof. - intros chunk1 chunk2. - destruct chunk1; destruct chunk2; simpl; congruence. -Qed. - -(** The initial store. *) - -Remark one_pos: 1 > 0. -Proof. omega. Qed. - -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. -Proof. intro. generalize (nextblock_pos m). omega. Qed. - -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}. -Proof. decide equality. Defined. - -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). -Proof. - induction n; intros. - simpl. intros; omegaContradiction. - simpl check_cont. repeat rewrite inj_S. caseEq (m p); intros. - exists p; split. omega. congruence. - exists p; split. omega. congruence. - generalize (IHn m (p + 1)). case (check_cont n (p + 1) m). - intros. assert (p = q \/ p + 1 <= q < p + Zsucc (Z_of_nat n)) by omega. - elim H2; intro. congruence. apply H0; omega. - intros [q [A B]]. exists q; split. omega. auto. -Qed. - -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. -Proof. - intros. generalize (check_cont_spec n m p). - destruct (check_cont n p m). auto. - intros [q [A B]]. elim B; auto. -Qed. - -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. -Proof. - intros. generalize (check_cont_spec n m p). - destruct (check_cont n p m). - intros. elim H0; auto. - auto. -Qed. - -Lemma set_cont_inside: - forall n p m q, - p <= q < p + Z_of_nat n -> - (set_cont n p m) q = Cont. -Proof. - induction n; intros. - unfold Z_of_nat in H. omegaContradiction. - simpl. - assert (p = q \/ p + 1 <= q < (p + 1) + Z_of_nat n). - rewrite inj_S in H. omega. - elim H0; intro. - subst q. apply update_s. - rewrite update_o. apply IHn. auto. - red; intro; subst q. omega. -Qed. - -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. -Proof. - induction n; intros. - simpl. auto. - simpl. rewrite inj_S in H. - rewrite update_o. apply IHn. omega. omega. -Qed. - -Lemma getN_setN_same: - forall n p v m, - getN n p (setN n p v m) = v. -Proof. - intros. unfold getN, setN. rewrite update_s. - rewrite check_cont_true. unfold proj_sumbool. - rewrite dec_eq_true. auto. - intros. rewrite update_o. apply set_cont_inside. auto. - omega. -Qed. - -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. -Proof. - intros. unfold getN, setN. - generalize (check_cont_spec n2 m (p2 + 1)); - destruct (check_cont n2 (p2 + 1) m); intros. - rewrite check_cont_true. - rewrite update_o. rewrite set_cont_outside. auto. - omega. omega. - intros. rewrite update_o. rewrite set_cont_outside. auto. - omega. omega. - destruct H0 as [q [A B]]. - rewrite (check_cont_false n2 (update p1 (Datum n1 v) (set_cont n1 (p1 + 1) m)) (p2 + 1) q). - rewrite update_o. rewrite set_cont_outside. auto. - omega. omega. omega. - rewrite update_o. rewrite set_cont_outside. auto. - omega. omega. -Qed. - -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. -Proof. - intros. unfold getN, setN. - rewrite update_o; auto. - destruct (zlt p2 p1). - (* [p1] belongs to [[p2, p2 + n2 - 1]], - therefore [check_cont n2 (p2 + 1) ...] is false. *) - rewrite (check_cont_false n2 (update p1 (Datum n1 v) (set_cont n1 (p1 + 1) m)) (p2 + 1) p1). - destruct (set_cont n1 (p1 + 1) m p2); auto. - destruct (eq_nat n2 n); auto. - omega. - rewrite update_s. congruence. - (* [p2] belongs to [[p1 + 1, p1 + n1 - 1]], - therefore [set_cont n1 (p1 + 1) m p2] is [Cont]. *) - rewrite set_cont_inside. auto. omega. -Qed. - -Lemma getN_setN_mismatch: - forall n1 n2 p v m, - n1 <> n2 -> - getN n2 p (setN n1 p v m) = Vundef. -Proof. - intros. unfold getN, setN. rewrite update_s. - unfold proj_sumbool; rewrite dec_eq_false; simpl. auto. auto. -Qed. - -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. -Proof. - intros. destruct (zeq p1 p2). subst p2. - destruct (eq_nat n1 n2). subst n2. - left; apply getN_setN_same. - right; right; apply getN_setN_mismatch; auto. - destruct (zlt (p1 + Z_of_nat n1) p2). - right; left; apply getN_setN_other; auto. - destruct (zlt (p2 + Z_of_nat n2) p1). - right; left; apply getN_setN_other; auto. - right; right; apply getN_setN_overlap; omega. -Qed. - -Lemma getN_init: - forall n p, - getN n p (fun y => Undef) = Vundef. -Proof. - intros. auto. -Qed. - -(** [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}. -Proof. - intros. - destruct (zlt b m.(nextblock)). - destruct (zle (low_bound m b) ofs). - destruct (zle (ofs + size_chunk chunk) (high_bound m b)). - destruct (Zdivide_dec (align_chunk chunk) ofs (align_chunk_pos chunk)). - left; constructor; auto. - right; red; intro V; inv V; contradiction. - right; red; intro V; inv V; omega. - right; red; intro V; inv V; omega. - right; red; intro V; inv V; contradiction. -Defined. - -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. -Proof. - intros. destruct (in_bounds m chunk b ofs). auto. contradiction. -Qed. - -(** [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))). -Proof. - intros until v; unfold load. - destruct (in_bounds m chunk b ofs); intros. - split. auto. congruence. - congruence. -Qed. - -(** [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. - -(* The memory state [m] after a store of value [v] at offset [ofs] - in block [b]. *) - -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. -Proof. - intros until m'; unfold store. - destruct (in_bounds m chunk b ofs); intros. - split. auto. congruence. - congruence. -Qed. - -(** [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' => - (* Not handled properly yet *) - 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 - 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. -Proof. - induction id; simpl. - omega. - assert (size_init_data a >= 0). destruct a; simpl; try omega. - generalize (Zmax2 z 0). omega. omega. -Qed. - -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. -Proof. - auto. -Qed. - -(** * 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'. -Proof. - intros; red; intros. subst b'. contradiction. -Qed. - -Lemma valid_access_valid_block: - forall m chunk b ofs, - valid_access m chunk b ofs -> valid_block m b. -Proof. - intros. inv H; auto. -Qed. - -Lemma valid_access_aligned: - forall m chunk b ofs, - valid_access m chunk b ofs -> (align_chunk chunk | ofs). -Proof. - intros. inv H; auto. -Qed. - -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. -Proof. - intros. inv H0. rewrite H in H3. constructor; auto. - rewrite <- (align_chunk_compat _ _ H). auto. -Qed. - -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. -Proof. - intros. econstructor. unfold load. rewrite in_bounds_true; auto. -Qed. - -Theorem load_valid_access: - forall m chunk b ofs v, - load chunk m b ofs = Some v -> - valid_access m chunk b ofs. -Proof. - intros. generalize (load_inv _ _ _ _ _ H). tauto. -Qed. - -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. -Proof. - intros. econstructor. unfold store. rewrite in_bounds_true; auto. -Qed. - -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'. -Proof. - intro. elim (store_inv _ _ _ _ _ _ STORE); intros. - subst m2. unfold low_bound, unchecked_store; simpl. - unfold update. destruct (zeq b' b); auto. subst b'; auto. -Qed. - -Lemma high_bound_store: - forall b', high_bound m2 b' = high_bound m1 b'. -Proof. - intro. elim (store_inv _ _ _ _ _ _ STORE); intros. - subst m2. unfold high_bound, unchecked_store; simpl. - unfold update. destruct (zeq b' b); auto. subst b'; auto. -Qed. - -Lemma nextblock_store: - nextblock m2 = nextblock m1. -Proof. - intros. elim (store_inv _ _ _ _ _ _ STORE); intros. - subst m2; reflexivity. -Qed. - -Lemma store_valid_block_1: - forall b', valid_block m1 b' -> valid_block m2 b'. -Proof. - unfold valid_block; intros. rewrite nextblock_store; auto. -Qed. - -Lemma store_valid_block_2: - forall b', valid_block m2 b' -> valid_block m1 b'. -Proof. - unfold valid_block; intros. rewrite nextblock_store in H; auto. -Qed. - -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'. -Proof. - intros. inv H. constructor; auto with mem. - rewrite low_bound_store; auto. - rewrite high_bound_store; auto. -Qed. - -Lemma store_valid_access_2: - forall chunk' b' ofs', - valid_access m2 chunk' b' ofs' -> valid_access m1 chunk' b' ofs'. -Proof. - intros. inv H. constructor; auto with mem. - rewrite low_bound_store in H1; auto. - rewrite high_bound_store in H2; auto. -Qed. - -Lemma store_valid_access_3: - valid_access m1 chunk b ofs. -Proof. - elim (store_inv _ _ _ _ _ _ STORE); intros. auto. -Qed. - -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). -Proof. - intros. destruct (store_inv _ _ _ _ _ _ STORE). - unfold load. rewrite in_bounds_true. - decEq. decEq. rewrite H1. unfold unchecked_store; simpl. - rewrite update_s. simpl. - replace (pred_size_chunk chunk) with (pred_size_chunk chunk'). - apply getN_setN_same. - repeat rewrite size_chunk_pred in H. omega. - apply store_valid_access_1. - inv H0. constructor; auto. congruence. - rewrite (align_chunk_compat _ _ H). auto. -Qed. - -Theorem load_store_same: - load chunk m2 b ofs = Some (Val.load_result chunk v). -Proof. - eapply load_store_similar; eauto. -Qed. - -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'. -Proof. - intros. destruct (store_inv _ _ _ _ _ _ STORE). - unfold load. destruct (in_bounds m1 chunk' b' ofs'). - rewrite in_bounds_true. decEq. decEq. - rewrite H1; unfold unchecked_store; simpl. - unfold update. destruct (zeq b' b). subst b'. - simpl. repeat rewrite size_chunk_pred in H. - apply getN_setN_other. elim H; intro. congruence. omega. - auto. - eauto with mem. - destruct (in_bounds m2 chunk' b' ofs'); auto. - elim n. eauto with mem. -Qed. - -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. -Proof. - intros. destruct (store_inv _ _ _ _ _ _ STORE). - destruct (load_inv _ _ _ _ _ H). rewrite H6. - rewrite H4. unfold unchecked_store. simpl. rewrite update_s. - simpl. rewrite getN_setN_overlap. - destruct chunk'; reflexivity. - auto. rewrite size_chunk_pred in H2. omega. - rewrite size_chunk_pred in H1. omega. -Qed. - -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. -Proof. - intros. - assert (exists v', load chunk' m2 b ofs' = Some v'). - eauto with mem. - destruct H3 as [v' LOAD]. rewrite LOAD. decEq. - eapply load_store_overlap; eauto. -Qed. - -Theorem load_store_mismatch: - forall chunk' v', - load chunk' m2 b ofs = Some v' -> - size_chunk chunk' <> size_chunk chunk -> - v' = Vundef. -Proof. - intros. destruct (store_inv _ _ _ _ _ _ STORE). - destruct (load_inv _ _ _ _ _ H). rewrite H4. - rewrite H2. unfold unchecked_store. simpl. rewrite update_s. - simpl. rewrite getN_setN_mismatch. - destruct chunk'; reflexivity. - repeat rewrite size_chunk_pred in H0; omega. -Qed. - -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. -Proof. - intros. - assert (exists v', load chunk' m2 b ofs = Some v'). - eauto with mem. - destruct H1 as [v' LOAD]. rewrite LOAD. decEq. - eapply load_store_mismatch; eauto. -Qed. - -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. -Proof. - intros. destruct (eq_block b1 b2). - destruct (zeq ofs1 ofs2). - destruct (zeq (size_chunk chunk1) (size_chunk chunk2)). - apply lsc_similar; auto. - apply lsc_mismatch; auto. - destruct (zle (ofs2 + size_chunk chunk2) ofs1). - apply lsc_other. tauto. - destruct (zle (ofs1 + size_chunk chunk1) ofs2). - apply lsc_other. tauto. - apply lsc_overlap; auto. - apply lsc_other; tauto. -Qed. - -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. -Proof. - intros. - assert (exists v', load chunk' m2 b' ofs' = Some v') by eauto with mem. - destruct H0 as [v' LOAD]. - destruct (load_store_classification chunk b ofs chunk' b' ofs'). - subst b' ofs'. apply load_store_similar; auto. - apply load_store_other; intuition. - subst b'. rewrite LOAD. decEq. - eapply load_store_overlap; eauto. - subst b' ofs'. rewrite LOAD. decEq. - eapply load_store_mismatch; eauto. -Qed. - -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). -Proof. - injection ALLOC; intros. rewrite <- H0; auto. -Qed. - -Lemma alloc_result: - b = nextblock m1. -Proof. - injection ALLOC; auto. -Qed. - -Lemma valid_block_alloc: - forall b', valid_block m1 b' -> valid_block m2 b'. -Proof. - unfold valid_block; intros. rewrite nextblock_alloc. omega. -Qed. - -Lemma fresh_block_alloc: - ~(valid_block m1 b). -Proof. - unfold valid_block. rewrite alloc_result. omega. -Qed. - -Lemma valid_new_block: - valid_block m2 b. -Proof. - unfold valid_block. rewrite alloc_result. rewrite nextblock_alloc. omega. -Qed. - -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'. -Proof. - unfold valid_block; intros. - rewrite nextblock_alloc in H. rewrite alloc_result. - unfold block; omega. -Qed. - -Lemma low_bound_alloc: - forall b', low_bound m2 b' = if zeq b' b then lo else low_bound m1 b'. -Proof. - intros. injection ALLOC; intros. rewrite <- H0; unfold low_bound; simpl. - unfold update. rewrite H. destruct (zeq b' b); auto. -Qed. - -Lemma low_bound_alloc_same: - low_bound m2 b = lo. -Proof. - rewrite low_bound_alloc. apply zeq_true. -Qed. - -Lemma low_bound_alloc_other: - forall b', valid_block m1 b' -> low_bound m2 b' = low_bound m1 b'. -Proof. - intros; rewrite low_bound_alloc. - apply zeq_false. eauto with mem. -Qed. - -Lemma high_bound_alloc: - forall b', high_bound m2 b' = if zeq b' b then hi else high_bound m1 b'. -Proof. - intros. injection ALLOC; intros. rewrite <- H0; unfold high_bound; simpl. - unfold update. rewrite H. destruct (zeq b' b); auto. -Qed. - -Lemma high_bound_alloc_same: - high_bound m2 b = hi. -Proof. - rewrite high_bound_alloc. apply zeq_true. -Qed. - -Lemma high_bound_alloc_other: - forall b', valid_block m1 b' -> high_bound m2 b' = high_bound m1 b'. -Proof. - intros; rewrite high_bound_alloc. - apply zeq_false. eauto with mem. -Qed. - -Lemma valid_access_alloc_other: - forall chunk b' ofs, - valid_access m1 chunk b' ofs -> - valid_access m2 chunk b' ofs. -Proof. - intros. inv H. constructor; auto with mem. - rewrite low_bound_alloc_other; auto. - rewrite high_bound_alloc_other; auto. -Qed. - -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. -Proof. - intros. constructor; auto with mem. - rewrite low_bound_alloc_same; auto. - rewrite high_bound_alloc_same; auto. -Qed. - -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)). -Proof. - intros. inv H. - elim (valid_block_alloc_inv _ H0); intro. - subst b'. rewrite low_bound_alloc_same in H1. - rewrite high_bound_alloc_same in H2. - right. tauto. - left. constructor; auto. - rewrite low_bound_alloc_other in H1; auto. - rewrite high_bound_alloc_other in H2; auto. -Qed. - -Theorem load_alloc_unchanged: - forall chunk b' ofs, - valid_block m1 b' -> - load chunk m2 b' ofs = load chunk m1 b' ofs. -Proof. - intros. unfold load. - destruct (in_bounds m2 chunk b' ofs). - elim (valid_access_alloc_inv _ _ _ v). intro. - rewrite in_bounds_true; auto. - injection ALLOC; intros. rewrite <- H2; simpl. - rewrite update_o. auto. rewrite H1. apply sym_not_equal. eauto with mem. - intros [A [B C]]. subst b'. elimtype False. eauto with mem. - destruct (in_bounds m1 chunk b' ofs). - elim n; eauto with mem. - auto. -Qed. - -Theorem load_alloc_other: - forall chunk b' ofs v, - load chunk m1 b' ofs = Some v -> - load chunk m2 b' ofs = Some v. -Proof. - intros. rewrite <- H. apply load_alloc_unchanged. eauto with mem. -Qed. - -Theorem load_alloc_same: - forall chunk ofs v, - load chunk m2 b ofs = Some v -> - v = Vundef. -Proof. - intros. destruct (load_inv _ _ _ _ _ H). rewrite H1. - injection ALLOC; intros. rewrite <- H3; simpl. - rewrite <- H2. rewrite update_s. - simpl. rewrite getN_init. destruct chunk; auto. -Qed. - -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. -Proof. - intros. assert (exists v, load chunk m2 b ofs = Some v). - apply valid_access_load. constructor; eauto with mem. - rewrite low_bound_alloc_same. auto. - rewrite high_bound_alloc_same. auto. - destruct H2 as [v LOAD]. rewrite LOAD. decEq. - eapply load_alloc_same; eauto. -Qed. - -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. -Proof. - unfold valid_block, free; intros; simpl; auto. -Qed. - -Lemma valid_block_free_2: - forall b, valid_block (free m bf) b -> valid_block m b. -Proof. - unfold valid_block, free; intros; simpl in *; auto. -Qed. - -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. -Proof. - intros. unfold low_bound, free; simpl. - rewrite update_o; auto. -Qed. - -Lemma high_bound_free: - forall b, b <> bf -> high_bound (free m bf) b = high_bound m b. -Proof. - intros. unfold high_bound, free; simpl. - rewrite update_o; auto. -Qed. - -Lemma low_bound_free_same: - forall m b, low_bound (free m b) b = 0. -Proof. - intros. unfold low_bound; simpl. rewrite update_s. simpl; omega. -Qed. - -Lemma high_bound_free_same: - forall m b, high_bound (free m b) b = 0. -Proof. - intros. unfold high_bound; simpl. rewrite update_s. simpl; omega. -Qed. - -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. -Proof. - intros. inv H. constructor; auto with mem. - rewrite low_bound_free; auto. rewrite high_bound_free; auto. -Qed. - -Lemma valid_access_free_2: - forall chunk ofs, ~(valid_access (free m bf) chunk bf ofs). -Proof. - intros; red; intros. inv H. - unfold free, low_bound in H1; simpl in H1. rewrite update_s in H1. simpl in H1. - unfold free, high_bound in H2; simpl in H2. rewrite update_s in H2. simpl in H2. - generalize (size_chunk_pos chunk). omega. -Qed. - -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. -Proof. - intros. destruct (eq_block b bf). subst b. - elim (valid_access_free_2 _ _ H). - inv H. rewrite low_bound_free in H1; auto. - rewrite high_bound_free in H2; auto. - split; auto. constructor; auto with mem. -Qed. - -Theorem load_free: - forall chunk b ofs, - b <> bf -> - load chunk (free m bf) b ofs = load chunk m b ofs. -Proof. - intros. unfold load. - destruct (in_bounds m chunk b ofs). - rewrite in_bounds_true; auto with mem. - unfold free; simpl. rewrite update_o; auto. - destruct (in_bounds (free m bf) chunk b ofs); auto. - elim n. elim (valid_access_free_inv _ _ _ v); auto. -Qed. - -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. -Proof. - induction bl; simpl; intros. auto. - apply valid_block_free_1; auto. -Qed. - -Lemma valid_block_free_list_2: - forall bl m b, valid_block (free_list m bl) b -> valid_block m b. -Proof. - induction bl; simpl; intros. auto. - apply IHbl. apply valid_block_free_2 with a; auto. -Qed. - -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. -Proof. - induction bl; simpl; intros. auto. - apply valid_access_free_1. apply IHbl. auto. intuition. intuition congruence. -Qed. - -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. -Proof. - induction bl; simpl; intros. - tauto. - elim (valid_access_free_inv _ _ _ _ _ H); intros. - elim (IHbl H0); intros. - intuition congruence. -Qed. - -(** ** 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. -Proof. - unfold valid_pointer; intros; split; intros. - destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0). - constructor. red. eapply proj_sumbool_true; eauto. - eapply proj_sumbool_true; eauto. - change (size_chunk Mint8unsigned) with 1. - generalize (proj_sumbool_true _ H1). omega. - simpl. apply Zone_divide. - inv H. unfold proj_sumbool. - rewrite zlt_true; auto. rewrite zle_true; auto. - change (size_chunk Mint8unsigned) with 1 in H2. - rewrite zlt_true. auto. omega. -Qed. - -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. -Proof. - intros. rewrite valid_pointer_valid_access in H0. - rewrite valid_pointer_valid_access. - eauto with mem. -Qed. - -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. -Proof. - intros. rewrite valid_pointer_valid_access in H0. - rewrite valid_pointer_valid_access. - eauto with mem. -Qed. - -(** * 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). -Proof. - intros. - assert (exists v1, load chunk m1 b1 ofs = Some v1) by eauto with mem. - destruct H2 as [v1 LOAD1]. - destruct (H0 _ _ _ _ _ _ H LOAD1) as [v2 [LOAD2 VCP]]. - eauto with mem. -Qed. - -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. -Proof. - intros; red; intros. - assert (load chunk0 m1 b1 ofs0 = Some v1). - rewrite <- H3; symmetry. eapply load_store_other; eauto. - left. congruence. - eapply H; eauto. -Qed. - -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'. -Proof. - intros; red; intros. - exploit H; eauto. intros [v2 [LOAD2 VINJ]]. - exists v2; split; auto. - rewrite <- LOAD2. eapply load_store_other; eauto. - destruct (eq_block b2 b). subst b2. - right. generalize (H0 _ _ H2); intro. - assert (valid_access m1 chunk0 b1 ofs0) by eauto with mem. - inv H5. omega. auto. -Qed. - -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'. -Proof. - intros. - assert (exists m2', store chunk m2 b2 (ofs + delta) v2 = Some m2') by eauto with mem. - destruct H4 as [m2' STORE2]. - exists m2'; split. auto. - red. intros chunk' b1' ofs' v b2' delta' CP LOAD1. - assert (valid_access m1 chunk' b1' ofs') by eauto with mem. - generalize (load_store_characterization _ _ _ _ _ _ H2 _ _ _ H4). - destruct (load_store_classification chunk b1 ofs chunk' b1' ofs'); - intro. - (* similar *) - subst b1' ofs'. - rewrite CP in H1. inv H1. - rewrite LOAD1 in H5. inv H5. - exists (Val.load_result chunk' v2). split. - eapply load_store_similar; eauto. - auto. - (* disjoint *) - rewrite LOAD1 in H5. - destruct (H _ _ _ _ _ _ CP (sym_equal H5)) as [v2' [LOAD2 VCP]]. - exists v2'. split; auto. - rewrite <- LOAD2. eapply load_store_other; eauto. - destruct (eq_block b1 b1'). subst b1'. - rewrite CP in H1; inv H1. - right. elim o; [congruence | omega]. - assert (valid_access m1 chunk b1 ofs) by eauto with mem. - generalize (H0 _ _ _ _ _ _ n H1 CP). intros [A | [A | [A | A]]]. - auto. - inv H6. generalize (size_chunk_pos chunk). intro. omegaContradiction. - inv H4. generalize (size_chunk_pos chunk'). intro. omegaContradiction. - right. inv H4. inv H6. omega. - (* overlapping *) - subst b1'. rewrite CP in H1; inv H1. - assert (exists v2', load chunk' m2' b2 (ofs' + delta) = Some v2') by eauto with mem. - destruct H1 as [v2' LOAD2']. - assert (v2' = Vundef). eapply load_store_overlap; eauto. - omega. omega. omega. - exists v2'; split. auto. - replace v with Vundef by congruence. subst v2'. apply val_inj_undef. - (* mismatch *) - subst b1' ofs'. rewrite CP in H1; inv H1. - assert (exists v2', load chunk' m2' b2 (ofs + delta) = Some v2') by eauto with mem. - destruct H1 as [v2' LOAD2']. - assert (v2' = Vundef). eapply load_store_mismatch; eauto. - exists v2'; split. auto. - replace v with Vundef by congruence. subst v2'. apply val_inj_undef. -Qed. - -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'. -Proof. - intros; red; intros. - exploit (valid_access_alloc_inv m1); eauto with mem. - intros [A | [A [B [C D]]]]. - assert (load chunk m1 b0 ofs = Some v1). - rewrite <- H7. symmetry. eapply load_alloc_unchanged; eauto with mem. - exploit H; eauto. intros [v2 [LOAD2 VINJ]]. - exists v2; split. - rewrite <- LOAD2. eapply load_alloc_unchanged; eauto with mem. - auto. - subst b0. rewrite H2 in H6. inversion H6. subst b3 delta0. - assert (v1 = Vundef). eapply load_alloc_same with (m1 := m1); eauto. - subst v1. - assert (exists v2, load chunk m2' b2 (ofs + delta) = Some v2). - apply valid_access_load. - eapply valid_access_alloc_same; eauto. omega. omega. - apply Zdivide_plus_r; auto. apply H5. omega. - destruct H8 as [v2 LOAD2]. - assert (v2 = Vundef). eapply load_alloc_same with (m1 := m2); eauto. - subst v2. - exists Vundef; split. auto. apply val_inj_undef. -Qed. - -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'. -Proof. - intros; red; intros. - exploit H; eauto. intros [v2 [LOAD2 VINJ]]. - exists v2; split; auto. - assert (valid_block m2 b0). - apply valid_access_valid_block with chunk (ofs + delta). - eauto with mem. - rewrite <- LOAD2. eapply load_alloc_unchanged; eauto. -Qed. - -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. -Proof. - intros; red; intros. - exploit (valid_access_alloc_inv m1); eauto with mem. - intros [A | [A [B C]]]. - eapply H; eauto. - rewrite <- H3. symmetry. eapply load_alloc_unchanged; eauto with mem. - subst b0. congruence. -Qed. - -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. -Proof. - intros; red; intros. - exploit (valid_access_alloc_inv m1); eauto with mem. - intros [A | [A [B [C D]]]]. - eapply H; eauto. - rewrite <- H7. symmetry. eapply load_alloc_unchanged; eauto with mem. - subst b0. rewrite H1 in H6. inversion H6. subst b3 delta0. - assert (v1 = Vundef). eapply load_alloc_same with (m1 := m1); eauto. - subst v1. - assert (exists v2, load chunk m2 b2 (ofs + delta) = Some v2). - apply valid_access_load. constructor. auto. omega. omega. - apply Zdivide_plus_r; auto. apply H5. omega. - destruct H8 as [v2 LOAD2]. exists v2; split. auto. - apply val_inj_undef_any. -Qed. - -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). -Proof. - intros; red; intros. - exploit valid_access_free_inv; eauto with mem. intros [A B]. - assert (load chunk m1 b0 ofs = Some v1). - rewrite <- H3. symmetry. apply load_free. auto. - exploit H; eauto. intros [v2 [LOAD2 INJ]]. - exists v2; split. - rewrite <- LOAD2. apply load_free. - red; intro; subst b3. elim B. eauto. - auto. -Qed. - -Lemma free_left_inj: - forall mi m1 m2 b1, - mem_inj mi m1 m2 -> - mem_inj mi (free m1 b1) m2. -Proof. - intros; red; intros. - exploit valid_access_free_inv; eauto with mem. intros [A B]. - eapply H; eauto with mem. - rewrite <- H1; symmetry; eapply load_free; eauto. -Qed. - -Lemma free_list_left_inj: - forall mi bl m1 m2, - mem_inj mi m1 m2 -> - mem_inj mi (free_list m1 bl) m2. -Proof. - induction bl; intros; simpl. - auto. - apply free_left_inj. auto. -Qed. - -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). -Proof. - intros; red; intros. - assert (b0 <> b2). - red; intro; subst b0. elim (H0 b1 delta chunk ofs H1). - eauto with mem. - exploit H; eauto. intros [v2 [LOAD2 INJ]]. - exists v2; split; auto. - rewrite <- LOAD2. apply load_free. auto. -Qed. - -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. -Proof. - intros. rewrite valid_pointer_valid_access in H1. - rewrite valid_pointer_valid_access. eauto with mem. -Qed. - -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. -Proof. - intros; split. auto. - red; unfold inject_id; intros. inv H. - exists v1; split. replace (ofs + 0) with ofs by omega. auto. - unfold val_inj_id; auto. -Qed. - -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'. -Proof. - intros. destruct H. - assert (b1 = b2). - transitivity (nextblock m1). eapply alloc_result; eauto. - symmetry. rewrite H. eapply alloc_result; eauto. - subst b2. split. auto. split. - rewrite (nextblock_alloc _ _ _ _ _ H2). - rewrite (nextblock_alloc _ _ _ _ _ H3). - congruence. - eapply alloc_parallel_inj; eauto. - unfold val_inj_id; auto. - unfold inject_id; eauto. - omega. omega. - red; intros. apply Zdivide_0. -Qed. - -Theorem free_extends: - forall (m1 m2: mem) (b: block), - extends m1 m2 -> - extends (free m1 b) (free m2 b). -Proof. - intros. destruct H. split. - simpl; auto. - eapply free_parallel_inj; eauto. - unfold inject_id. eauto. - unfold inject_id; intros. congruence. -Qed. - -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. -Proof. - intros. destruct H. - exploit H1; eauto. unfold inject_id. eauto. - unfold val_inj_id. intros [v2 [LOAD EQ]]. - replace (ofs + 0) with ofs in LOAD by omega. congruence. -Qed. - -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'. -Proof. - intros. destruct H. - exploit store_mapped_inj; eauto. - unfold val_inj_id; eauto. - unfold meminj_no_overlap, inject_id; intros. - inv H3. inv H4. auto. - unfold inject_id; eauto. - unfold val_inj_id; intros. eauto. - intros [m2' [STORE MINJ]]. - exists m2'; split. - replace (ofs + 0) with ofs in STORE by omega. auto. - split. - rewrite (nextblock_store _ _ _ _ _ _ H0). - rewrite (nextblock_store _ _ _ _ _ _ STORE). - auto. - auto. -Qed. - -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'. -Proof. - intros. destruct H. split. - rewrite (nextblock_store _ _ _ _ _ _ H1). auto. - eapply store_outside_inj; eauto. - unfold inject_id; intros. inv H3. omega. -Qed. - -Theorem valid_pointer_extends: - forall m1 m2 b ofs, - extends m1 m2 -> valid_pointer m1 b ofs = true -> - valid_pointer m2 b ofs = true. -Proof. - intros. destruct H. - replace ofs with (ofs + 0) by omega. - apply valid_pointer_inj with val_inj_id inject_id m1 b; auto. -Qed. - -(** * 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. -Proof. - intros; split. auto. - red; intros. unfold inject_id in H. inv H. - exists v1; split. replace (ofs + 0) with ofs by omega. auto. - red. constructor. -Qed. - -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. -Proof. - intros. destruct H. - exploit H1; eauto. unfold inject_id. eauto. - intros [v2 [LOAD INJ]]. exists v2; split. - replace ofs with (ofs + 0) by omega. auto. - auto. -Qed. - -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. -Proof. - intros. inv H0. - destruct addr2; simpl in *; try discriminate. - eapply load_lessdef; eauto. - simpl in H1; discriminate. -Qed. - -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'. -Proof. - intros. destruct H. - exploit store_mapped_inj; eauto. - unfold val_inj_lessdef; intros; constructor. - red; unfold inject_id; intros. inv H4. inv H5. auto. - unfold inject_id; eauto. - unfold val_inj_lessdef; intros. - apply Val.load_result_lessdef. eexact H0. - intros [m2' [STORE MINJ]]. - exists m2'; split. replace ofs with (ofs + 0) by omega. auto. - split. - rewrite (nextblock_store _ _ _ _ _ _ H1). - rewrite (nextblock_store _ _ _ _ _ _ STORE). - auto. - auto. -Qed. - -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'. -Proof. - intros. inv H0. - destruct addr2; simpl in H2; try discriminate. - simpl. eapply store_lessdef; eauto. - discriminate. -Qed. - -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'. -Proof. - intros. destruct H. - assert (b1 = b2). - transitivity (nextblock m1). eapply alloc_result; eauto. - symmetry. rewrite H. eapply alloc_result; eauto. - subst b2. split. auto. split. - rewrite (nextblock_alloc _ _ _ _ _ H0). - rewrite (nextblock_alloc _ _ _ _ _ H1). - congruence. - eapply alloc_parallel_inj; eauto. - unfold val_inj_lessdef; auto. - unfold inject_id; eauto. - omega. omega. - red; intros. apply Zdivide_0. -Qed. - -Lemma free_lessdef: - forall m1 m2 b, lessdef m1 m2 -> lessdef (free m1 b) (free m2 b). -Proof. - intros. destruct H. split. - simpl; auto. - eapply free_parallel_inj; eauto. - unfold inject_id. eauto. - unfold inject_id; intros. congruence. -Qed. - -Lemma free_left_lessdef: - forall m1 m2 b, - lessdef m1 m2 -> lessdef (free m1 b) m2. -Proof. - intros. destruct H. split. - rewrite <- H. auto. - apply free_left_inj; auto. -Qed. - -Lemma free_right_lessdef: - forall m1 m2 b, - lessdef m1 m2 -> low_bound m1 b >= high_bound m1 b -> - lessdef m1 (free m2 b). -Proof. - intros. destruct H. unfold lessdef. split. - rewrite H. auto. - apply free_right_inj; auto. intros. unfold inject_id in H2. inv H2. - red; intro. inv H2. generalize (size_chunk_pos chunk); intro. omega. -Qed. - -Lemma valid_block_lessdef: - forall m1 m2 b, lessdef m1 m2 -> valid_block m1 b -> valid_block m2 b. -Proof. - unfold valid_block. intros. destruct H. rewrite <- H; auto. -Qed. - -Lemma valid_pointer_lessdef: - forall m1 m2 b ofs, - lessdef m1 m2 -> valid_pointer m1 b ofs = true -> valid_pointer m2 b ofs = true. -Proof. - intros. destruct H. - replace ofs with (ofs + 0) by omega. - apply valid_pointer_inj with val_inj_lessdef inject_id m1 b; auto. -Qed. - -(** ** 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. -Proof. - intros. inversion H. - elim (mi_range_4 _ _ _ H1); intro. - (* delta = 0 *) - subst delta. change (Int.repr 0) with Int.zero. - rewrite Int.add_zero. omega. - (* delta <> 0 *) - rewrite Int.add_signed. - repeat rewrite Int.signed_repr. auto. - eauto. - assert (valid_access m2 chunk b2 (Int.signed ofs1 + delta)). - eapply valid_access_inj; eauto. - inv H3. generalize (size_chunk_pos chunk); omega. - eauto. -Qed. - -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. -Proof. - intros. inv H. rewrite valid_pointer_valid_access in H0. - assert (valid_access m2 Mint8unsigned b' (Int.signed ofs + x)). - eapply valid_access_inj; eauto. - inv H. change (size_chunk Mint8unsigned) with 1 in H4. - rewrite Int.signed_repr; eauto. - exploit mi_range_4; eauto. intros [A | [A B]]. - subst x. rewrite Zplus_0_r. apply Int.signed_range. - omega. -Qed. - -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. -Proof. - intros. inv H1. - exploit valid_pointer_inject_no_overflow; eauto. intro NOOV. - inv H. rewrite Int.add_signed. rewrite Int.signed_repr; auto. - rewrite Int.signed_repr; eauto. - eapply valid_pointer_inj; eauto. -Qed. - -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)). -Proof. - intros. - rewrite valid_pointer_valid_access in H1. - rewrite valid_pointer_valid_access in H2. - rewrite (address_inject _ _ _ _ _ _ _ _ H H1 H3). - rewrite (address_inject _ _ _ _ _ _ _ _ H H2 H4). - inv H1. simpl in H7. inv H2. simpl in H10. - exploit (mi_no_overlap _ _ _ H); eauto. - intros [A | [A | [A | [A | A]]]]. - auto. omegaContradiction. omegaContradiction. - right. omega. right. omega. -Qed. - -(** 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. -Proof. - intros. inversion H. - eapply mi_inj0; eauto. -Qed. - -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. -Proof. - intros. inv H1; simpl in H0; try discriminate. - exploit load_inject; eauto. intros [v2 [LOAD INJ]]. - exists v2; split; auto. simpl. - replace (Int.signed (Int.add ofs1 (Int.repr x))) - with (Int.signed ofs1 + x). - auto. symmetry. eapply address_inject; eauto with mem. -Qed. - -(** 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). -Proof. - intros. inv H; simpl. - inv H1; destruct chunk'; simpl; econstructor; eauto. - - elim H1; intro; subst chunk; - destruct chunk'; simpl in H0; try discriminate; simpl. - replace (Int.sign_ext 8 n1) with (Int.sign_ext 8 n2). - constructor. apply Int.sign_ext_equal_if_zero_equal; auto. compute; auto. - rewrite H2. constructor. - replace (Int.sign_ext 8 n1) with (Int.sign_ext 8 n2). - constructor. apply Int.sign_ext_equal_if_zero_equal; auto. compute; auto. - rewrite H2. constructor. - - elim H1; intro; subst chunk; - destruct chunk'; simpl in H0; try discriminate; simpl. - replace (Int.sign_ext 16 n1) with (Int.sign_ext 16 n2). - constructor. apply Int.sign_ext_equal_if_zero_equal; auto. compute; auto. - rewrite H2. constructor. - replace (Int.sign_ext 16 n1) with (Int.sign_ext 16 n2). - constructor. apply Int.sign_ext_equal_if_zero_equal; auto. compute; auto. - rewrite H2. constructor. - - destruct chunk'; simpl in H0; try discriminate; simpl. - constructor. rewrite H1; constructor. -Qed. - -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. -Proof. - intros. inversion H. - exploit store_mapped_inj; eauto. - intros; constructor. - intros. apply load_result_inject with chunk; eauto. - intros [n2 [STORE MINJ]]. - exists n2; split. auto. constructor. - (* inj *) - auto. - (* freeblocks *) - intros. apply mi_freeblocks0. red; intro. elim H3. eauto with mem. - (* mappedblocks *) - intros. eauto with mem. - (* no_overlap *) - red; intros. - repeat rewrite (low_bound_store _ _ _ _ _ _ H0). - repeat rewrite (high_bound_store _ _ _ _ _ _ H0). - eapply mi_no_overlap0; eauto. - (* range *) - auto. - intros. - repeat rewrite (low_bound_store _ _ _ _ _ _ STORE). - repeat rewrite (high_bound_store _ _ _ _ _ _ STORE). - eapply mi_range_4; eauto. -Qed. - -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. -Proof. - intros. eapply store_mapped_inject_1; eauto. -Qed. - -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. -Proof. - intros. inversion H. - constructor. - (* inj *) - eapply store_unmapped_inj; eauto. - (* freeblocks *) - intros. apply mi_freeblocks0. red; intros; elim H2; eauto with mem. - (* mappedblocks *) - intros. eapply mi_mappedblocks0; eauto with mem. - (* no_overlap *) - red; intros. - repeat rewrite (low_bound_store _ _ _ _ _ _ H0). - repeat rewrite (high_bound_store _ _ _ _ _ _ H0). - eapply mi_no_overlap0; eauto. - (* range *) - auto. auto. -Qed. - -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. -Proof. - intros. inv H1; simpl in H0; try discriminate. - simpl. replace (Int.signed (Int.add ofs1 (Int.repr x))) - with (Int.signed ofs1 + x). - eapply store_mapped_inject_1; eauto. - symmetry. eapply address_inject; eauto with mem. -Qed. - -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. -Proof. - intros. eapply storev_mapped_inject_1; eauto. -Qed. - -(** 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). -Proof. - intros; red; intros. - assert (low_bound (free m b) b >= high_bound (free m b) b). - rewrite low_bound_free_same; rewrite high_bound_free_same; auto. - omega. - destruct (eq_block b1 b); destruct (eq_block b2 b); subst; auto. - repeat (rewrite low_bound_free; auto). - repeat (rewrite high_bound_free; auto). -Qed. - -Lemma meminj_no_overlap_free_list: - forall mi m bl, - meminj_no_overlap mi m -> - meminj_no_overlap mi (free_list m bl). -Proof. - induction bl; simpl; intros. auto. - apply meminj_no_overlap_free. auto. -Qed. - -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). -Proof. - intros. inversion H0. constructor. - (* inj *) - apply free_right_inj. apply free_list_left_inj. auto. - intros; red; intros. - elim (valid_access_free_list_inv _ _ _ _ _ H2); intros. - elim H3; eauto. - (* freeblocks *) - intros. apply mi_freeblocks0. red; intro; elim H1. - apply valid_block_free_list_1; auto. - (* mappedblocks *) - intros. apply valid_block_free_1. eauto. - (* overlap *) - apply meminj_no_overlap_free_list; auto. - (* range *) - auto. - intros. destruct (eq_block b' b). subst b'. - rewrite low_bound_free_same; rewrite high_bound_free_same. - right; compute; intuition congruence. - rewrite low_bound_free; auto. rewrite high_bound_free; auto. - eauto. -Qed. - -(** 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 . -Proof. unfold inject_incr . intros. left . auto . Qed. - -Lemma inject_incr_trans : - forall f1 f2 f3, - inject_incr f1 f2 -> inject_incr f2 f3 -> inject_incr f1 f3 . -Proof . - unfold inject_incr; intros. - generalize (H b); generalize (H0 b); intuition congruence. -Qed. - -Lemma val_inject_incr: - forall f1 f2 v v', - inject_incr f1 f2 -> - val_inject f1 v v' -> - val_inject f2 v v'. -Proof. - intros. inversion H0. - constructor. - constructor. - elim (H b1); intro. - apply val_inject_ptr with x. congruence. auto. - congruence. - constructor. -Qed. - -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'. -Proof. - induction vl; intros; inv H0. auto. - constructor. eapply val_inject_incr; eauto. auto. -Qed. - -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). -Proof. - intros; red; intros. unfold extend_inject. - destruct (zeq b0 b). subst b0; auto. auto. -Qed. - -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'. -Proof. - intros. inversion H. constructor. - eapply alloc_right_inj; eauto. - auto. - intros. eauto with mem. - auto. - auto. - intros. replace (low_bound m2' b') with (low_bound m2 b'). - replace (high_bound m2' b') with (high_bound m2 b'). - eauto. - symmetry. eapply high_bound_alloc_other; eauto. - symmetry. eapply low_bound_alloc_other; eauto. -Qed. - -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). -Proof. - intros. inversion H. - assert (inject_incr f (extend_inject b None f)). - apply extend_inject_incr. apply mi_freeblocks0. eauto with mem. - split; auto. constructor. - (* inj *) - eapply alloc_left_unmapped_inj; eauto. - red; intros. unfold extend_inject in H2. - destruct (zeq b1 b). congruence. - exploit mi_inj0; eauto. intros [v2 [LOAD VINJ]]. - exists v2; split. auto. - apply val_inject_incr with f; auto. - unfold extend_inject. apply zeq_true. - (* freeblocks *) - intros. unfold extend_inject. destruct (zeq b0 b). auto. - apply mi_freeblocks0; red; intro. elim H2. eauto with mem. - (* mappedblocks *) - intros. unfold extend_inject in H2. destruct (zeq b0 b). - discriminate. eauto. - (* overlap *) - red; unfold extend_inject, update; intros. - repeat rewrite (low_bound_alloc _ _ _ _ _ H0). - repeat rewrite (high_bound_alloc _ _ _ _ _ H0). - destruct (zeq b1 b); try discriminate. - destruct (zeq b2 b); try discriminate. - eauto. - (* range *) - unfold extend_inject; intros. - destruct (zeq b0 b). discriminate. eauto. - unfold extend_inject; intros. - destruct (zeq b0 b). discriminate. eauto. -Qed. - -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). -Proof. - intros. inversion H. - assert (inject_incr f (extend_inject b (Some (b', ofs)) f)). - apply extend_inject_incr. apply mi_freeblocks0. eauto with mem. - split; auto. - constructor. - (* inj *) - eapply alloc_left_mapped_inj; eauto. - red; intros. unfold extend_inject in H10. - rewrite zeq_false in H10. - exploit mi_inj0; eauto. intros [v2 [LOAD VINJ]]. - exists v2; split. auto. eapply val_inject_incr; eauto. - eauto with mem. - unfold extend_inject. apply zeq_true. - (* freeblocks *) - intros. unfold extend_inject. rewrite zeq_false. - apply mi_freeblocks0. red; intro. elim H10; eauto with mem. - apply sym_not_equal; eauto with mem. - (* mappedblocks *) - unfold extend_inject; intros. - destruct (zeq b0 b). inv H10. auto. eauto. - (* overlap *) - red; unfold extend_inject, update; intros. - repeat rewrite (low_bound_alloc _ _ _ _ _ H0). - repeat rewrite (high_bound_alloc _ _ _ _ _ H0). - destruct (zeq b1 b); [inv H11|idtac]; - (destruct (zeq b2 b); [inv H12|idtac]). - congruence. - destruct (zeq b1' b2'). subst b2'. generalize (H8 _ _ H12). tauto. auto. - destruct (zeq b1' b2'). subst b2'. generalize (H8 _ _ H11). tauto. auto. - eauto. - (* range *) - unfold extend_inject; intros. - destruct (zeq b0 b). inv H10. auto. eauto. - unfold extend_inject; intros. - destruct (zeq b0 b). inv H10. auto. eauto. -Qed. - -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). -Proof. - intros. - eapply alloc_mapped_inject; eauto. - eapply alloc_right_inject; eauto. - eauto with mem. - compute; intuition congruence. - rewrite (low_bound_alloc_same _ _ _ _ _ H1). auto. - rewrite (high_bound_alloc_same _ _ _ _ _ H1). auto. - rewrite (low_bound_alloc_same _ _ _ _ _ H1). omega. - rewrite (high_bound_alloc_same _ _ _ _ _ H1). omega. - red; intros. apply Zdivide_0. - intros. elimtype False. inv H. - exploit mi_mappedblocks0; eauto. - change (~ valid_block m2 b2). eauto with mem. -Qed. - -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. -Proof. - intros; constructor. - (* inj *) - red; intros. unfold meminj_init in H0. - destruct (zlt b1 (nextblock m)); inversion H0. - subst b2 delta. exists v1; split. - rewrite Zplus_0_r. auto. eapply H; eauto. - (* free blocks *) - unfold valid_block, meminj_init; intros. - apply zlt_false. omega. - (* mapped blocks *) - unfold valid_block, meminj_init; intros. - destruct (zlt b (nextblock m)); inversion H0. subst b'; auto. - (* overlap *) - red; unfold meminj_init; intros. - destruct (zlt b1 (nextblock m)); inversion H1. - destruct (zlt b2 (nextblock m)); inversion H2. - left; congruence. - (* range *) - unfold meminj_init; intros. - destruct (zlt b (nextblock m)); inversion H0. subst delta. - compute; intuition congruence. - unfold meminj_init; intros. - destruct (zlt b (nextblock m)); inversion H0. subst delta. - auto. -Qed. - -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)). -Proof. - intros. - destruct (getN_setN_characterization m v n1 p1 n2 p2) - as [A | [A | A]]; rewrite A; auto. -Qed. - -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)). -Proof. - induction id; simpl; intros. - repeat rewrite getN_init. constructor. - destruct a; auto; apply getN_setN_inject; auto. -Qed. - -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'. -Proof. - intros. injection H0; intros A B. - red; intros. - exploit load_inv; eauto. intros [C D]. - rewrite <- B in D; simpl in D. rewrite A in D. - unfold update in D. destruct (zeq b0 b). - subst b0. rewrite D. simpl. - apply load_result_inject with chunk. constructor. - apply getN_contents_init_data_inject. auto. - apply H with chunk b0 ofs. unfold load. - rewrite in_bounds_true. congruence. - inversion C. constructor. - generalize H2. unfold valid_block. rewrite <- B; simpl. - rewrite A. unfold block in n; intros. omega. - replace (low_bound m b0) with (low_bound m' b0). auto. - unfold low_bound; rewrite <- B; simpl; rewrite A. rewrite update_o; auto. - replace (high_bound m b0) with (high_bound m' b0). auto. - unfold high_bound; rewrite <- B; simpl; rewrite A. rewrite update_o; auto. - auto. -Qed. - -(** ** 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. -Proof. - intros. inversion H. - elim (ms_range_4 _ _ H1); intros. - rewrite Int.add_signed. - repeat rewrite Int.signed_repr. auto. - eauto. - assert (valid_access m2 chunk b (Int.signed ofs1 + delta)). - eapply valid_access_inj with (mi := meminj_of_shift f); eauto. - unfold meminj_of_shift. rewrite H1; auto. - inv H4. generalize (size_chunk_pos chunk); omega. - eauto. -Qed. - -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. -Proof. - intros. inv H. rewrite valid_pointer_valid_access in H0. - assert (valid_access m2 Mint8unsigned b (Int.signed ofs + x)). - eapply valid_access_inj with (mi := meminj_of_shift f); eauto. - unfold meminj_of_shift. rewrite H1; auto. - inv H. change (size_chunk Mint8unsigned) with 1 in H4. - rewrite Int.signed_repr; eauto. - exploit ms_range_4; eauto. intros [A B]. omega. -Qed. - -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. -Proof. - intros. unfold val_shift in H1. inv H1. - assert (f b = Some x). - unfold meminj_of_shift in H5. destruct (f b); congruence. - exploit valid_pointer_shift_no_overflow; eauto. intro NOOV. - inv H. rewrite Int.add_signed. rewrite Int.signed_repr; auto. - rewrite Int.signed_repr; eauto. - eapply valid_pointer_inj; eauto. -Qed. - -(** 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. -Proof. - intros. inversion H. - unfold val_shift. eapply ms_inj0; eauto. - unfold meminj_of_shift; rewrite H1; auto. -Qed. - -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. -Proof. - intros. unfold val_shift in H1. inv H1; simpl in H0; try discriminate. - generalize H2. unfold meminj_of_shift. caseEq (f b1); intros; inv H3. - exploit load_shift; eauto. intros [v2 [LOAD INJ]]. - exists v2; split; auto. simpl. - replace (Int.signed (Int.add ofs1 (Int.repr x))) - with (Int.signed ofs1 + x). - auto. symmetry. eapply address_shift; eauto with mem. -Qed. - -(** 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. -Proof. - intros. inversion H. - exploit store_mapped_inj; eauto. - intros; constructor. - red. intros until delta2. unfold meminj_of_shift. - destruct (f b1). destruct (f b2). intros. inv H4. inv H5. auto. - congruence. congruence. - unfold meminj_of_shift. rewrite H1. auto. - intros. apply load_result_inject with chunk; eauto. - unfold val_shift in H2. eauto. - intros [n2 [STORE MINJ]]. - exists n2; split. auto. constructor. - (* inj *) - auto. - (* samedomain *) - rewrite (nextblock_store _ _ _ _ _ _ H0). - rewrite (nextblock_store _ _ _ _ _ _ STORE). - auto. - (* domain *) - rewrite (nextblock_store _ _ _ _ _ _ H0). auto. - (* range *) - auto. - intros. - repeat rewrite (low_bound_store _ _ _ _ _ _ STORE). - repeat rewrite (high_bound_store _ _ _ _ _ _ STORE). - eapply ms_range_4; eauto. -Qed. - -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'. -Proof. - intros. inversion H. constructor. - (* inj *) - eapply store_outside_inj; eauto. - unfold meminj_of_shift. intros b' d'. caseEq (f b'); intros; inv H4. - congruence. - (* samedomain *) - rewrite (nextblock_store _ _ _ _ _ _ H2). - auto. - (* domain *) - auto. - (* range *) - auto. - intros. - repeat rewrite (low_bound_store _ _ _ _ _ _ H2). - repeat rewrite (high_bound_store _ _ _ _ _ _ H2). - eapply ms_range_4; eauto. -Qed. - -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. -Proof. - intros. unfold val_shift in H1. inv H1; simpl in H0; try discriminate. - generalize H3. unfold meminj_of_shift. caseEq (f b1); intros; inv H4. - exploit store_within_shift; eauto. intros [n2 [A B]]. - exists n2; split; auto. - unfold storev. - replace (Int.signed (Int.add ofs1 (Int.repr x))) - with (Int.signed ofs1 + x). - auto. symmetry. eapply address_shift; eauto with mem. -Qed. - -(** 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). -Proof. - intros. inv H. constructor. - (* inj *) - apply free_right_inj. apply free_left_inj; auto. - intros until ofs. unfold meminj_of_shift. caseEq (f b1); intros; inv H0. - apply valid_access_free_2. - (* samedomain *) - simpl. auto. - (* domain *) - simpl. auto. - (* range *) - auto. - intros. destruct (eq_block b0 b). - subst b0. rewrite low_bound_free_same. rewrite high_bound_free_same. - vm_compute; intuition congruence. - rewrite low_bound_free; auto. rewrite high_bound_free; auto. eauto. -Qed. - -(** 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). -Proof. - intros. unfold meminj_of_shift. red. intros. - elim (H b); intro. rewrite H0. auto. rewrite H0. auto. -Qed. - -Lemma val_shift_incr: - forall f1 f2 v1 v2, - shift_incr f1 f2 -> val_shift f1 v1 v2 -> val_shift f2 v1 v2. -Proof. - unfold val_shift; intros. - apply val_inject_incr with (meminj_of_shift f1). - apply shift_incr_inject_incr. auto. auto. -Qed. - -(*** -Remark mem_inj_incr: - forall f1 f2 m1 m2, - inject_incr f1 f2 -> mem_inj val_inject f1 m1 m2 -> mem_inj val_inject f2 m1 m2. -Proof. - intros; red; intros. - destruct (H b1). rewrite <- H3 in H1. - exploit H0; eauto. intros [v2 [A B]]. - exists v2; split. auto. apply val_inject_incr with f1; auto. - congruence. -***) - -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. -Proof. - intros. inv H. caseEq (alloc m2 lo2 hi2). intros m2' b' ALLOC2. - assert (b' = b). - rewrite (alloc_result _ _ _ _ _ H0). - rewrite (alloc_result _ _ _ _ _ ALLOC2). - auto. - subst b'. - assert (f b = None). - generalize (ms_domain0 b). - rewrite (alloc_result _ _ _ _ _ H0). - destruct (f (nextblock m1)). - intros. omegaContradiction. - auto. - set (f' := fun (b': block) => if zeq b' b then Some delta else f b'). - assert (shift_incr f f'). - red; unfold f'; intros. - destruct (zeq b0 b); auto. - subst b0. auto. - exists f'; exists m2'. - split. auto. - (* mem_shift *) - split. constructor. - (* inj *) - assert (mem_inj val_inject (meminj_of_shift f') m1 m2). - red; intros. - assert (meminj_of_shift f b1 = Some (b2, delta0)). - rewrite <- H8. unfold meminj_of_shift, f'. - destruct (zeq b1 b); auto. - subst b1. - assert (valid_block m1 b) by eauto with mem. - assert (~valid_block m1 b) by eauto with mem. - contradiction. - exploit ms_inj0; eauto. intros [v2 [A B]]. - exists v2; split; auto. - apply val_inject_incr with (meminj_of_shift f). - apply shift_incr_inject_incr. auto. auto. - eapply alloc_parallel_inj; eauto. - unfold meminj_of_shift, f'. rewrite zeq_true. auto. - (* samedomain *) - rewrite (nextblock_alloc _ _ _ _ _ H0). - rewrite (nextblock_alloc _ _ _ _ _ ALLOC2). - congruence. - (* domain *) - intros. unfold f'. - rewrite (nextblock_alloc _ _ _ _ _ H0). - rewrite (alloc_result _ _ _ _ _ H0). - destruct (zeq b0 (nextblock m1)). omega. - generalize (ms_domain0 b0). destruct (f b0); omega. - (* range *) - unfold f'; intros. destruct (zeq b0 b). congruence. eauto. - unfold f'; intros. - rewrite (low_bound_alloc _ _ _ _ _ ALLOC2). - rewrite (high_bound_alloc _ _ _ _ _ ALLOC2). - destruct (zeq b0 b). auto. eauto. - (* shift_incr *) - split. auto. - (* f' b = delta *) - unfold f'. apply zeq_true. -Qed. - -(** ** 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). -Proof. - intros. destruct (in_bounds m chunk1 b ofs). - rewrite in_bounds_true. auto. eapply valid_access_compat; eauto. - destruct (in_bounds m chunk2 b ofs); auto. - elim n. eapply valid_access_compat with (chunk1 := chunk2); eauto. -Qed. - -Lemma storev_8_signed_unsigned: - forall m a v, - storev Mint8signed m a v = storev Mint8unsigned m a v. -Proof. - intros. unfold storev. destruct a; auto. - unfold store. rewrite (in_bounds_equiv Mint8signed Mint8unsigned). - auto. auto. -Qed. - -Lemma storev_16_signed_unsigned: - forall m a v, - storev Mint16signed m a v = storev Mint16unsigned m a v. -Proof. - intros. unfold storev. destruct a; auto. - unfold store. rewrite (in_bounds_equiv Mint16signed Mint16unsigned). - auto. auto. -Qed. - -(** 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). -Proof. - intros. unfold Mem.loadv. destruct a; try reflexivity. - unfold load. rewrite (in_bounds_equiv Mint8signed Mint8unsigned). - destruct (in_bounds m Mint8unsigned b (Int.signed i)); auto. - simpl. - destruct (getN 0 (Int.signed i) (contents (blocks m b))); auto. - simpl. rewrite Int.sign_ext_zero_ext. auto. compute; auto. - auto. -Qed. - |