From e637d041c5c2ee3a3ed395a7dab6c9101e8eb16c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 1 Oct 2016 17:25:18 +0200 Subject: Support for 64-bit architectures: generic support - Introduce Archi.ptr64 parameter. - Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise). - Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated. - Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers. - Update the memory model accordingly. - Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly. - Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers. - Update the compiler front-end and back-end accordingly. --- common/Memory.v | 166 +++++++++++++++++++++++++++++++------------------------- 1 file changed, 92 insertions(+), 74 deletions(-) (limited to 'common/Memory.v') diff --git a/common/Memory.v b/common/Memory.v index 672012be..d0cbe8a0 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -450,7 +450,7 @@ Definition load (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z): option val : Definition loadv (chunk: memory_chunk) (m: mem) (addr: val) : option val := match addr with - | Vptr b ofs => load chunk m b (Int.unsigned ofs) + | Vptr b ofs => load chunk m b (Ptrofs.unsigned ofs) | _ => None end. @@ -566,7 +566,7 @@ Qed. Definition storev (chunk: memory_chunk) (m: mem) (addr v: val) : option mem := match addr with - | Vptr b ofs => store chunk m b (Int.unsigned ofs) v + | Vptr b ofs => store chunk m b (Ptrofs.unsigned ofs) v | _ => None end. @@ -873,7 +873,7 @@ Qed. Theorem load_int64_split: forall m b ofs v, - load Mint64 m b ofs = Some v -> + load Mint64 m b ofs = Some v -> Archi.ptr64 = false -> exists v1 v2, load Mint32 m b ofs = Some (if Archi.big_endian then v1 else v2) /\ load Mint32 m b (ofs + 4) = Some (if Archi.big_endian then v2 else v1) @@ -897,29 +897,47 @@ Proof. exists (decode_val Mint32 (if Archi.big_endian then bytes2 else bytes1)). split. destruct Archi.big_endian; auto. split. destruct Archi.big_endian; auto. - rewrite EQ. rewrite APP. apply decode_val_int64. + rewrite EQ. rewrite APP. apply decode_val_int64; auto. erewrite loadbytes_length; eauto. reflexivity. erewrite loadbytes_length; eauto. reflexivity. Qed. +Lemma addressing_int64_split: + forall i, + Archi.ptr64 = false -> + (8 | Ptrofs.unsigned i) -> + Ptrofs.unsigned (Ptrofs.add i (Ptrofs.of_int (Int.repr 4))) = Ptrofs.unsigned i + 4. +Proof. + intros. + rewrite Ptrofs.add_unsigned. + replace (Ptrofs.unsigned (Ptrofs.of_int (Int.repr 4))) with (Int.unsigned (Int.repr 4)) + by (symmetry; apply Ptrofs.agree32_of_int; auto). + change (Int.unsigned (Int.repr 4)) with 4. + apply Ptrofs.unsigned_repr. + exploit (Zdivide_interval (Ptrofs.unsigned i) Ptrofs.modulus 8). + omega. apply Ptrofs.unsigned_range. auto. + exists (two_p (Ptrofs.zwordsize - 3)). + unfold Ptrofs.modulus, Ptrofs.zwordsize, Ptrofs.wordsize. + unfold Wordsize_Ptrofs.wordsize. destruct Archi.ptr64; reflexivity. + unfold Ptrofs.max_unsigned. omega. +Qed. + Theorem loadv_int64_split: forall m a v, - loadv Mint64 m a = Some v -> + loadv Mint64 m a = Some v -> Archi.ptr64 = false -> exists v1 v2, loadv Mint32 m a = Some (if Archi.big_endian then v1 else v2) - /\ loadv Mint32 m (Val.add a (Vint (Int.repr 4))) = Some (if Archi.big_endian then v2 else v1) + /\ loadv Mint32 m (Val.add a (Vint (Int.repr 4))) = Some (if Archi.big_endian then v2 else v1) /\ Val.lessdef v (Val.longofwords v1 v2). Proof. - intros. destruct a; simpl in H; try discriminate. + intros. destruct a; simpl in H; inv H. exploit load_int64_split; eauto. intros (v1 & v2 & L1 & L2 & EQ). - assert (NV: Int.unsigned (Int.add i (Int.repr 4)) = Int.unsigned i + 4). - rewrite Int.add_unsigned. apply Int.unsigned_repr. - exploit load_valid_access. eexact H. intros [P Q]. simpl in Q. - exploit (Zdivide_interval (Int.unsigned i) Int.modulus 8). - omega. apply Int.unsigned_range. auto. exists (two_p (32-3)); reflexivity. - unfold Int.max_unsigned. omega. - exists v1; exists v2. -Opaque Int.repr. + unfold Val.add; rewrite H0. + assert (NV: Ptrofs.unsigned (Ptrofs.add i (Ptrofs.of_int (Int.repr 4))) = Ptrofs.unsigned i + 4). + { apply addressing_int64_split; auto. + exploit load_valid_access. eexact H2. intros [P Q]. auto. } + exists v1, v2. +Opaque Ptrofs.repr. split. auto. split. simpl. rewrite NV. auto. auto. @@ -1205,18 +1223,18 @@ Qed. Definition compat_pointer_chunks (chunk1 chunk2: memory_chunk) : Prop := match chunk1, chunk2 with | (Mint32 | Many32), (Mint32 | Many32) => True - | Many64, Many64 => True + | (Mint64 | Many64), (Mint64 | Many64) => True | _, _ => False end. Lemma compat_pointer_chunks_true: forall chunk1 chunk2, - (chunk1 = Mint32 \/ chunk1 = Many32 \/ chunk1 = Many64) -> - (chunk2 = Mint32 \/ chunk2 = Many32 \/ chunk2 = Many64) -> + (chunk1 = Mint32 \/ chunk1 = Many32 \/ chunk1 = Mint64 \/ chunk1 = Many64) -> + (chunk2 = Mint32 \/ chunk2 = Many32 \/ chunk2 = Mint64 \/ chunk2 = Many64) -> quantity_chunk chunk1 = quantity_chunk chunk2 -> compat_pointer_chunks chunk1 chunk2. Proof. - intros. destruct H as [P|[P|P]]; destruct H0 as [Q|[Q|Q]]; + intros. destruct H as [P|[P|[P|P]]]; destruct H0 as [Q|[Q|[Q|Q]]]; subst; red; auto; discriminate. Qed. @@ -1237,10 +1255,11 @@ Proof. destruct CASES as [(A & B) | [(A & B) | (A & B)]]. - (* Same offset *) subst. inv ENC. - assert (chunk = Mint32 \/ chunk = Many32 \/ chunk = Many64) + assert (chunk = Mint32 \/ chunk = Many32 \/ chunk = Mint64 \/ chunk = Many64) by (destruct chunk; auto || contradiction). left; split. rewrite H3. - destruct H4 as [P|[P|P]]; subst chunk'; destruct v0; simpl in H3; congruence. + destruct H4 as [P|[P|[P|P]]]; subst chunk'; destruct v0; simpl in H3; + try congruence; destruct Archi.ptr64; congruence. split. apply compat_pointer_chunks_true; auto. auto. - (* ofs' > ofs *) @@ -1612,7 +1631,7 @@ Qed. Theorem store_int64_split: forall m b ofs v m', - store Mint64 m b ofs v = Some m' -> + store Mint64 m b ofs v = Some m' -> Archi.ptr64 = false -> exists m1, store Mint32 m b ofs (if Archi.big_endian then Val.hiword v else Val.loword v) = Some m1 /\ store Mint32 m1 b (ofs + 4) (if Archi.big_endian then Val.loword v else Val.hiword v) = Some m'. @@ -1620,7 +1639,7 @@ Proof. intros. exploit store_valid_access_3; eauto. intros [A B]. simpl in *. exploit store_storebytes. eexact H. intros SB. - rewrite encode_val_int64 in SB. + rewrite encode_val_int64 in SB by auto. exploit storebytes_split. eexact SB. intros [m1 [SB1 SB2]]. rewrite encode_val_length in SB2. simpl in SB2. exists m1; split. @@ -1632,20 +1651,18 @@ Qed. Theorem storev_int64_split: forall m a v m', - storev Mint64 m a v = Some m' -> + storev Mint64 m a v = Some m' -> Archi.ptr64 = false -> exists m1, storev Mint32 m a (if Archi.big_endian then Val.hiword v else Val.loword v) = Some m1 /\ storev Mint32 m1 (Val.add a (Vint (Int.repr 4))) (if Archi.big_endian then Val.loword v else Val.hiword v) = Some m'. Proof. - intros. destruct a; simpl in H; try discriminate. + intros. destruct a; simpl in H; inv H. rewrite H2. exploit store_int64_split; eauto. intros [m1 [A B]]. exists m1; split. exact A. - unfold storev, Val.add. rewrite Int.add_unsigned. rewrite Int.unsigned_repr. exact B. - exploit store_valid_access_3. eexact H. intros [P Q]. simpl in Q. - exploit (Zdivide_interval (Int.unsigned i) Int.modulus 8). - omega. apply Int.unsigned_range. auto. exists (two_p (32-3)); reflexivity. - change (Int.unsigned (Int.repr 4)) with 4. unfold Int.max_unsigned. omega. + unfold storev, Val.add. rewrite H0. + rewrite addressing_int64_split; auto. + exploit store_valid_access_3. eexact H2. intros [P Q]. exact Q. Qed. (** ** Properties related to [alloc]. *) @@ -1811,7 +1828,8 @@ Theorem load_alloc_same: Proof. intros. exploit load_result; eauto. intro. rewrite H0. injection ALLOC; intros. rewrite <- H2; simpl. rewrite <- H1. - rewrite PMap.gss. destruct chunk; simpl; repeat rewrite ZMap.gi; reflexivity. + rewrite PMap.gss. destruct (size_chunk_nat_pos chunk) as [n E]. rewrite E. simpl. + rewrite ZMap.gi. apply decode_val_undef. Qed. Theorem load_alloc_same': @@ -3142,8 +3160,8 @@ Record inject' (f: meminj) (m1 m2: mem) : Prop := mi_representable: forall b b' delta ofs, f b = Some(b', delta) -> - perm m1 b (Int.unsigned ofs) Max Nonempty \/ perm m1 b (Int.unsigned ofs - 1) Max Nonempty -> - delta >= 0 /\ 0 <= Int.unsigned ofs + delta <= Int.max_unsigned; + perm m1 b (Ptrofs.unsigned ofs) Max Nonempty \/ perm m1 b (Ptrofs.unsigned ofs - 1) Max Nonempty -> + delta >= 0 /\ 0 <= Ptrofs.unsigned ofs + delta <= Ptrofs.max_unsigned; mi_perm_inv: forall b1 ofs b2 delta k p, f b1 = Some(b2, delta) -> @@ -3246,24 +3264,24 @@ Qed. Lemma address_inject: forall f m1 m2 b1 ofs1 b2 delta p, inject f m1 m2 -> - perm m1 b1 (Int.unsigned ofs1) Cur p -> + perm m1 b1 (Ptrofs.unsigned ofs1) Cur p -> f b1 = Some (b2, delta) -> - Int.unsigned (Int.add ofs1 (Int.repr delta)) = Int.unsigned ofs1 + delta. + Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)) = Ptrofs.unsigned ofs1 + delta. Proof. intros. - assert (perm m1 b1 (Int.unsigned ofs1) Max Nonempty) by eauto with mem. + assert (perm m1 b1 (Ptrofs.unsigned ofs1) Max Nonempty) by eauto with mem. exploit mi_representable; eauto. intros [A B]. - assert (0 <= delta <= Int.max_unsigned). - generalize (Int.unsigned_range ofs1). omega. - unfold Int.add. repeat rewrite Int.unsigned_repr; omega. + assert (0 <= delta <= Ptrofs.max_unsigned). + generalize (Ptrofs.unsigned_range ofs1). omega. + unfold Ptrofs.add. repeat rewrite Ptrofs.unsigned_repr; omega. Qed. Lemma address_inject': forall f m1 m2 chunk b1 ofs1 b2 delta, inject f m1 m2 -> - valid_access m1 chunk b1 (Int.unsigned ofs1) Nonempty -> + valid_access m1 chunk b1 (Ptrofs.unsigned ofs1) Nonempty -> f b1 = Some (b2, delta) -> - Int.unsigned (Int.add ofs1 (Int.repr delta)) = Int.unsigned ofs1 + delta. + Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)) = Ptrofs.unsigned ofs1 + delta. Proof. intros. destruct H0. eapply address_inject; eauto. apply H0. generalize (size_chunk_pos chunk). omega. @@ -3272,24 +3290,24 @@ Qed. Theorem weak_valid_pointer_inject_no_overflow: forall f m1 m2 b ofs b' delta, inject f m1 m2 -> - weak_valid_pointer m1 b (Int.unsigned ofs) = true -> + weak_valid_pointer m1 b (Ptrofs.unsigned ofs) = true -> f b = Some(b', delta) -> - 0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned. + 0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned. Proof. intros. rewrite weak_valid_pointer_spec in H0. rewrite ! valid_pointer_nonempty_perm in H0. exploit mi_representable; eauto. destruct H0; eauto with mem. intros [A B]. - pose proof (Int.unsigned_range ofs). - rewrite Int.unsigned_repr; omega. + pose proof (Ptrofs.unsigned_range ofs). + rewrite Ptrofs.unsigned_repr; omega. Qed. Theorem valid_pointer_inject_no_overflow: forall f m1 m2 b ofs b' delta, inject f m1 m2 -> - valid_pointer m1 b (Int.unsigned ofs) = true -> + valid_pointer m1 b (Ptrofs.unsigned ofs) = true -> f b = Some(b', delta) -> - 0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned. + 0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned. Proof. eauto using weak_valid_pointer_inject_no_overflow, valid_pointer_implies. Qed. @@ -3297,9 +3315,9 @@ Qed. Theorem valid_pointer_inject_val: forall f m1 m2 b ofs b' ofs', inject f m1 m2 -> - valid_pointer m1 b (Int.unsigned ofs) = true -> + valid_pointer m1 b (Ptrofs.unsigned ofs) = true -> Val.inject f (Vptr b ofs) (Vptr b' ofs') -> - valid_pointer m2 b' (Int.unsigned ofs') = true. + valid_pointer m2 b' (Ptrofs.unsigned ofs') = true. Proof. intros. inv H1. erewrite address_inject'; eauto. @@ -3310,9 +3328,9 @@ Qed. Theorem weak_valid_pointer_inject_val: forall f m1 m2 b ofs b' ofs', inject f m1 m2 -> - weak_valid_pointer m1 b (Int.unsigned ofs) = true -> + weak_valid_pointer m1 b (Ptrofs.unsigned ofs) = true -> Val.inject f (Vptr b ofs) (Vptr b' ofs') -> - weak_valid_pointer m2 b' (Int.unsigned ofs') = true. + weak_valid_pointer m2 b' (Ptrofs.unsigned ofs') = true. Proof. intros. inv H1. exploit weak_valid_pointer_inject; eauto. intros W. @@ -3320,8 +3338,8 @@ Proof. rewrite ! valid_pointer_nonempty_perm in H0. exploit mi_representable; eauto. destruct H0; eauto with mem. intros [A B]. - pose proof (Int.unsigned_range ofs). - unfold Int.add. repeat rewrite Int.unsigned_repr; auto; omega. + pose proof (Ptrofs.unsigned_range ofs). + unfold Ptrofs.add. repeat rewrite Ptrofs.unsigned_repr; auto; omega. Qed. Theorem inject_no_overlap: @@ -3341,13 +3359,13 @@ Theorem different_pointers_inject: forall f m m' b1 ofs1 b2 ofs2 b1' delta1 b2' delta2, inject f m m' -> b1 <> b2 -> - valid_pointer m b1 (Int.unsigned ofs1) = true -> - valid_pointer m b2 (Int.unsigned ofs2) = true -> + valid_pointer m b1 (Ptrofs.unsigned ofs1) = true -> + valid_pointer m b2 (Ptrofs.unsigned ofs2) = true -> f b1 = Some (b1', delta1) -> f b2 = Some (b2', delta2) -> b1' <> b2' \/ - Int.unsigned (Int.add ofs1 (Int.repr delta1)) <> - Int.unsigned (Int.add ofs2 (Int.repr delta2)). + Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta1)) <> + Ptrofs.unsigned (Ptrofs.add ofs2 (Ptrofs.repr delta2)). Proof. intros. rewrite valid_pointer_valid_access in H1. @@ -3356,8 +3374,8 @@ Proof. rewrite (address_inject' _ _ _ _ _ _ _ _ H H2 H4). inv H1. simpl in H5. inv H2. simpl in H1. eapply mi_no_overlap; eauto. - apply perm_cur_max. apply (H5 (Int.unsigned ofs1)). omega. - apply perm_cur_max. apply (H1 (Int.unsigned ofs2)). omega. + apply perm_cur_max. apply (H5 (Ptrofs.unsigned ofs1)). omega. + apply perm_cur_max. apply (H1 (Ptrofs.unsigned ofs2)). omega. Qed. Require Intv. @@ -3439,8 +3457,8 @@ Proof. intros. inv H1; simpl in H0; try discriminate. exploit load_inject; eauto. intros [v2 [LOAD INJ]]. exists v2; split; auto. unfold loadv. - replace (Int.unsigned (Int.add ofs1 (Int.repr delta))) - with (Int.unsigned ofs1 + delta). + replace (Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta))) + with (Ptrofs.unsigned ofs1 + delta). auto. symmetry. eapply address_inject'; eauto with mem. Qed. @@ -3547,8 +3565,8 @@ Theorem storev_mapped_inject: Proof. intros. inv H1; simpl in H0; try discriminate. unfold storev. - replace (Int.unsigned (Int.add ofs1 (Int.repr delta))) - with (Int.unsigned ofs1 + delta). + replace (Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta))) + with (Ptrofs.unsigned ofs1 + delta). eapply store_mapped_inject; eauto. symmetry. eapply address_inject'; eauto with mem. Qed. @@ -3740,8 +3758,8 @@ Theorem alloc_left_mapped_inject: inject f m1 m2 -> alloc m1 lo hi = (m1', b1) -> valid_block m2 b2 -> - 0 <= delta <= Int.max_unsigned -> - (forall ofs k p, perm m2 b2 ofs k p -> delta = 0 \/ 0 <= ofs < Int.max_unsigned) -> + 0 <= delta <= Ptrofs.max_unsigned -> + (forall ofs k p, perm m2 b2 ofs k p -> delta = 0 \/ 0 <= ofs < Ptrofs.max_unsigned) -> (forall ofs k p, lo <= ofs < hi -> perm m2 b2 (ofs + delta) k p) -> inj_offset_aligned delta (hi-lo) -> (forall b delta' ofs k p, @@ -3803,10 +3821,10 @@ Proof. subst. injection H9; intros; subst b' delta0. destruct H10. exploit perm_alloc_inv; eauto; rewrite dec_eq_true; intro. exploit H3. apply H4 with (k := Max) (p := Nonempty); eauto. - generalize (Int.unsigned_range_2 ofs). omega. + generalize (Ptrofs.unsigned_range_2 ofs). omega. exploit perm_alloc_inv; eauto; rewrite dec_eq_true; intro. exploit H3. apply H4 with (k := Max) (p := Nonempty); eauto. - generalize (Int.unsigned_range_2 ofs). omega. + generalize (Ptrofs.unsigned_range_2 ofs). omega. eapply mi_representable0; try eassumption. destruct H10; eauto using perm_alloc_4. (* perm inv *) @@ -3843,7 +3861,7 @@ Proof. eapply alloc_right_inject; eauto. eauto. instantiate (1 := b2). eauto with mem. - instantiate (1 := 0). unfold Int.max_unsigned. generalize Int.modulus_pos; omega. + instantiate (1 := 0). unfold Ptrofs.max_unsigned. generalize Ptrofs.modulus_pos; omega. auto. intros. apply perm_implies with Freeable; auto with mem. eapply perm_alloc_2; eauto. omega. @@ -4054,13 +4072,13 @@ Proof. destruct (f b) as [[b1 delta1] |] eqn:?; try discriminate. destruct (f' b1) as [[b2 delta2] |] eqn:?; inv H. exploit mi_representable0; eauto. intros [A B]. - set (ofs' := Int.repr (Int.unsigned ofs + delta1)). - assert (Int.unsigned ofs' = Int.unsigned ofs + delta1). - unfold ofs'; apply Int.unsigned_repr. auto. + set (ofs' := Ptrofs.repr (Ptrofs.unsigned ofs + delta1)). + assert (Ptrofs.unsigned ofs' = Ptrofs.unsigned ofs + delta1). + unfold ofs'; apply Ptrofs.unsigned_repr. auto. exploit mi_representable1. eauto. instantiate (1 := ofs'). rewrite H. - replace (Int.unsigned ofs + delta1 - 1) with - ((Int.unsigned ofs - 1) + delta1) by omega. + replace (Ptrofs.unsigned ofs + delta1 - 1) with + ((Ptrofs.unsigned ofs - 1) + delta1) by omega. destruct H0; eauto using perm_inj. rewrite H. omega. (* perm inv *) @@ -4185,7 +4203,7 @@ Proof. apply flat_inj_no_overlap. (* range *) unfold flat_inj; intros. - destruct (plt b (nextblock m)); inv H0. generalize (Int.unsigned_range_2 ofs); omega. + destruct (plt b (nextblock m)); inv H0. generalize (Ptrofs.unsigned_range_2 ofs); omega. (* perm inv *) unfold flat_inj; intros. destruct (plt b1 (nextblock m)); inv H0. -- cgit