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/Separation.v | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) (limited to 'common/Separation.v') diff --git a/common/Separation.v b/common/Separation.v index efcd3281..c0a3c9cf 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -319,7 +319,7 @@ Qed. Program Definition range (b: block) (lo hi: Z) : massert := {| m_pred := fun m => - 0 <= lo /\ hi <= Int.modulus + 0 <= lo /\ hi <= Ptrofs.modulus /\ (forall i k p, lo <= i < hi -> Mem.perm m b i k p); m_footprint := fun b' ofs' => b' = b /\ lo <= ofs' < hi |}. @@ -333,7 +333,7 @@ Qed. Lemma alloc_rule: forall m lo hi b m' P, Mem.alloc m lo hi = (m', b) -> - 0 <= lo -> hi <= Int.modulus -> + 0 <= lo -> hi <= Ptrofs.modulus -> m |= P -> m' |= range b lo hi ** P. Proof. @@ -413,7 +413,7 @@ Qed. Program Definition contains (chunk: memory_chunk) (b: block) (ofs: Z) (spec: val -> Prop) : massert := {| m_pred := fun m => - 0 <= ofs <= Int.max_unsigned + 0 <= ofs <= Ptrofs.max_unsigned /\ Mem.valid_access m chunk b ofs Freeable /\ exists v, Mem.load chunk m b ofs = Some v /\ spec v; m_footprint := fun b' ofs' => b' = b /\ ofs <= ofs' < ofs + size_chunk chunk @@ -431,7 +431,7 @@ Qed. Lemma contains_no_overflow: forall spec m chunk b ofs, m |= contains chunk b ofs spec -> - 0 <= ofs <= Int.max_unsigned. + 0 <= ofs <= Ptrofs.max_unsigned. Proof. intros. simpl in H. tauto. Qed. @@ -448,10 +448,10 @@ Qed. Lemma loadv_rule: forall spec m chunk b ofs, m |= contains chunk b ofs spec -> - exists v, Mem.loadv chunk m (Vptr b (Int.repr ofs)) = Some v /\ spec v. + exists v, Mem.loadv chunk m (Vptr b (Ptrofs.repr ofs)) = Some v /\ spec v. Proof. intros. exploit load_rule; eauto. intros (v & A & B). exists v; split; auto. - simpl. rewrite Int.unsigned_repr; auto. eapply contains_no_overflow; eauto. + simpl. rewrite Ptrofs.unsigned_repr; auto. eapply contains_no_overflow; eauto. Qed. Lemma store_rule: @@ -477,10 +477,10 @@ Lemma storev_rule: m |= contains chunk b ofs spec1 ** P -> spec (Val.load_result chunk v) -> exists m', - Mem.storev chunk m (Vptr b (Int.repr ofs)) v = Some m' /\ m' |= contains chunk b ofs spec ** P. + Mem.storev chunk m (Vptr b (Ptrofs.repr ofs)) v = Some m' /\ m' |= contains chunk b ofs spec ** P. Proof. intros. exploit store_rule; eauto. intros (m' & A & B). exists m'; split; auto. - simpl. rewrite Int.unsigned_repr; auto. eapply contains_no_overflow. eapply sep_pick1; eauto. + simpl. rewrite Ptrofs.unsigned_repr; auto. eapply contains_no_overflow. eapply sep_pick1; eauto. Qed. Lemma range_contains: @@ -493,7 +493,7 @@ Proof. split; [|split]. - assert (Mem.valid_access m chunk b ofs Freeable). { split; auto. red; auto. } - split. generalize (size_chunk_pos chunk). unfold Int.max_unsigned. omega. + split. generalize (size_chunk_pos chunk). unfold Ptrofs.max_unsigned. omega. split. auto. + destruct (Mem.valid_access_load m chunk b ofs) as [v LOAD]. eauto with mem. @@ -530,7 +530,7 @@ Lemma storev_rule': forall chunk m b ofs v (spec1: val -> Prop) P, m |= contains chunk b ofs spec1 ** P -> exists m', - Mem.storev chunk m (Vptr b (Int.repr ofs)) v = Some m' /\ m' |= hasvalue chunk b ofs (Val.load_result chunk v) ** P. + Mem.storev chunk m (Vptr b (Ptrofs.repr ofs)) v = Some m' /\ m' |= hasvalue chunk b ofs (Val.load_result chunk v) ** P. Proof. intros. eapply storev_rule; eauto. Qed. @@ -656,9 +656,9 @@ Proof. intros. destruct H as (A & B & C). simpl in A. exploit Mem.storev_mapped_inject; eauto. intros (m2' & STORE & INJ). inv H1; simpl in STORE; try discriminate. - assert (VALID: Mem.valid_access m1 chunk b1 (Int.unsigned ofs1) Writable) + assert (VALID: Mem.valid_access m1 chunk b1 (Ptrofs.unsigned ofs1) Writable) by eauto with mem. - assert (EQ: Int.unsigned (Int.add ofs1 (Int.repr delta)) = Int.unsigned ofs1 + delta). + assert (EQ: Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)) = Ptrofs.unsigned ofs1 + delta). { eapply Mem.address_inject'; eauto with mem. } exists m2'; split; auto. split; [|split]. @@ -681,7 +681,7 @@ Lemma alloc_parallel_rule: (8 | delta) -> lo = delta -> hi = delta + Zmax 0 sz1 -> - 0 <= sz2 <= Int.max_unsigned -> + 0 <= sz2 <= Ptrofs.max_unsigned -> 0 <= delta -> hi <= sz2 -> exists j', m2' |= range b2 0 lo ** range b2 hi sz2 ** minjection j' m1' ** P @@ -709,7 +709,7 @@ Proof. exists j'; split; auto. rewrite <- ! sep_assoc. split; [|split]. -+ simpl. intuition auto; try (unfold Int.max_unsigned in *; omega). ++ simpl. intuition auto; try (unfold Ptrofs.max_unsigned in *; omega). * apply Mem.perm_implies with Freeable; auto with mem. eapply Mem.perm_alloc_2; eauto. omega. * apply Mem.perm_implies with Freeable; auto with mem. @@ -891,7 +891,7 @@ Lemma alloc_parallel_rule_2: (8 | delta) -> lo = delta -> hi = delta + Zmax 0 sz1 -> - 0 <= sz2 <= Int.max_unsigned -> + 0 <= sz2 <= Ptrofs.max_unsigned -> 0 <= delta -> hi <= sz2 -> exists j', m2' |= range b2 0 lo ** range b2 hi sz2 ** minjection j' m1' ** globalenv_inject ge j' ** P -- cgit