From bb9d14a3f95fc0e3c8cad10d8ea8e2b2738da7fc Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 11 Jan 2009 11:57:02 +0000 Subject: - Added alignment constraints to memory loads and stores. - In Cminor and below, removed pointer validity check in semantics of comparisons, so that evaluation of expressions is independent of memory state. - In Cminor and below, removed "alloc" instruction. - Cleaned up commented-away parts. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@945 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Mem.v | 234 +++++++++++++++++++++++++++++++++++++++++++---------------- 1 file changed, 173 insertions(+), 61 deletions(-) (limited to 'common') diff --git a/common/Mem.v b/common/Mem.v index 3db2ceba..de3e8c94 100644 --- a/common/Mem.v +++ b/common/Mem.v @@ -122,6 +122,51 @@ 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. @@ -376,13 +421,19 @@ Proof. 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]. *) + 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 @@ -395,7 +446,9 @@ Proof. 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. @@ -577,7 +630,24 @@ Proof. intros. inv H; auto. Qed. -Hint Resolve valid_not_valid_diff valid_access_valid_block: mem. +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] *) @@ -661,7 +731,7 @@ 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. + intros. inv H. constructor; auto with mem. rewrite low_bound_store; auto. rewrite high_bound_store; auto. Qed. @@ -670,7 +740,7 @@ 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. + intros. inv H. constructor; auto with mem. rewrite low_bound_store in H1; auto. rewrite high_bound_store in H2; auto. Qed. @@ -698,6 +768,7 @@ Proof. 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: @@ -801,12 +872,6 @@ Inductive load_store_cases b1 = b2 -> ofs1 = ofs2 -> size_chunk chunk1 <> size_chunk chunk2 -> load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2. -Remark size_chunk_pos: - forall chunk1, size_chunk chunk1 > 0. -Proof. - destruct chunk1; simpl; omega. -Qed. - Definition load_store_classification: forall (chunk1: memory_chunk) (b1: block) (ofs1: Z) (chunk2: memory_chunk) (b2: block) (ofs2: Z), @@ -949,17 +1014,17 @@ Lemma valid_access_alloc_other: valid_access m1 chunk b' ofs -> valid_access m2 chunk b' ofs. Proof. - intros. inv H. constructor. auto with mem. + 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 -> + lo <= ofs -> ofs + size_chunk chunk <= hi -> (align_chunk chunk | ofs) -> valid_access m2 chunk b ofs. Proof. - intros. constructor. auto with mem. + intros. constructor; auto with mem. rewrite low_bound_alloc_same; auto. rewrite high_bound_alloc_same; auto. Qed. @@ -970,14 +1035,14 @@ 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). + (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. + left. constructor; auto. rewrite low_bound_alloc_other in H1; auto. rewrite high_bound_alloc_other in H2; auto. Qed. @@ -1020,14 +1085,14 @@ Qed. Theorem load_alloc_same': forall chunk ofs, - lo <= ofs -> ofs + size_chunk chunk <= hi -> + 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 H1 as [v LOAD]. rewrite LOAD. decEq. + destruct H2 as [v LOAD]. rewrite LOAD. decEq. eapply load_alloc_same; eauto. Qed. @@ -1089,7 +1154,7 @@ Lemma valid_access_free_1: valid_access m chunk b ofs -> b <> bf -> valid_access (free m bf) chunk b ofs. Proof. - intros. inv H. constructor. auto with mem. + intros. inv H. constructor; auto with mem. rewrite low_bound_free; auto. rewrite high_bound_free; auto. Qed. @@ -1180,6 +1245,7 @@ Proof. 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. @@ -1215,13 +1281,6 @@ Definition meminj : Set := block -> option (block * Z). Variable val_inj: meminj -> val -> val -> Prop. -(* -Hypothesis val_inj_ptr: - forall mi b1 ofs1 b2 ofs2, - val_inj mi (Vptr b1 ofs1) (Vptr b2 ofs2) <-> - exists delta, mi b1 = Some(b2, delta) /\ ofs2 = Int.repr (Int.signed ofs1 + delta). -*) - Hypothesis val_inj_undef: forall mi, val_inj mi Vundef Vundef. @@ -1350,6 +1409,9 @@ Proof. 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 -> @@ -1357,24 +1419,26 @@ Lemma alloc_parallel_inj: 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]]]. + intros [A | [A [B [C D]]]]. assert (load chunk m1 b0 ofs = Some v1). - rewrite <- H6. symmetry. eapply load_alloc_unchanged; eauto with mem. + 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 H5. inversion H5. subst b3 delta0. + 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. - destruct H7 as [v2 LOAD2]. + 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. @@ -1420,19 +1484,21 @@ Lemma alloc_left_mapped_inj: 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]]]. + intros [A | [A [B [C D]]]]. eapply H; eauto. - rewrite <- H6. symmetry. eapply load_alloc_unchanged; eauto with mem. - subst b0. rewrite H1 in H5. inversion H5. subst b3 delta0. + 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. - destruct H7 as [v2 LOAD2]. exists v2; split. auto. + apply Zdivide_plus_r; auto. apply H5. omega. + destruct H8 as [v2 LOAD2]. exists v2; split. auto. apply val_inj_undef_any. Qed. @@ -1547,6 +1613,7 @@ Proof. unfold val_inj_id; auto. unfold inject_id; eauto. omega. omega. + red; intros. apply Zdivide_0. Qed. Theorem free_extends: @@ -1716,6 +1783,7 @@ Proof. unfold val_inj_lessdef; auto. unfold inject_id; eauto. omega. omega. + red; intros. apply Zdivide_0. Qed. Lemma free_lessdef: @@ -1887,7 +1955,7 @@ Proof. 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 H9. + 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. @@ -2256,6 +2324,7 @@ Lemma alloc_mapped_inject: 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 \/ @@ -2270,34 +2339,34 @@ Proof. constructor. (* inj *) eapply alloc_left_mapped_inj; eauto. - red; intros. unfold extend_inject in H9. - rewrite zeq_false in H9. + 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 H9; eauto with mem. + 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 H9. auto. eauto. + 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 H10|idtac]; - (destruct (zeq b2 b); [inv H11|idtac]). + destruct (zeq b1 b); [inv H11|idtac]; + (destruct (zeq b2 b); [inv H12|idtac]). congruence. - destruct (zeq b1' b2'). subst b2'. generalize (H7 _ _ H11). tauto. auto. - destruct (zeq b1' b2'). subst b2'. generalize (H7 _ _ H10). tauto. auto. + 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 H9. auto. eauto. + destruct (zeq b0 b). inv H10. auto. eauto. unfold extend_inject; intros. - destruct (zeq b0 b). inv H9. auto. eauto. + destruct (zeq b0 b). inv H10. auto. eauto. Qed. Lemma alloc_parallel_inject: @@ -2318,6 +2387,7 @@ Proof. 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. @@ -2406,6 +2476,7 @@ Proof. 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 *) @@ -2415,21 +2486,6 @@ Qed. Definition memshift := block -> option Z. -(* -Inductive val_shift (mi: memshift): val -> val -> Prop := - | val_shift_int: - forall i, val_shift mi (Vint i) (Vint i) - | val_shift_float: - forall f, val_shift mi (Vfloat f) (Vfloat f) - | val_shift_ptr: - forall b ofs1 ofs2 x, - mi b = Some x -> - ofs2 = Int.add ofs1 (Int.repr x) -> - val_shift mi (Vptr b ofs1) (Vptr b ofs2) - | val_shift_undef: - val_shift mi Vundef Vundef. -*) - Definition meminj_of_shift (mi: memshift) : meminj := fun b => match mi b with None => None | Some x => Some (b, x) end. @@ -2688,6 +2744,7 @@ Lemma alloc_shift: 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' @@ -2719,7 +2776,7 @@ Proof. assert (mem_inj val_inject (meminj_of_shift f') m1 m2). red; intros. assert (meminj_of_shift f b1 = Some (b2, delta0)). - rewrite <- H7. unfold meminj_of_shift, f'. + rewrite <- H8. unfold meminj_of_shift, f'. destruct (zeq b1 b); auto. subst b1. assert (valid_block m1 b) by eauto with mem. @@ -2753,3 +2810,58 @@ Proof. 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: Set) (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. + -- cgit