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. --- backend/NeedDomain.v | 64 +++++++++++++++++++++++++++------------------------- 1 file changed, 33 insertions(+), 31 deletions(-) (limited to 'backend/NeedDomain.v') diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v index 442352e7..a53040f9 100644 --- a/backend/NeedDomain.v +++ b/backend/NeedDomain.v @@ -379,6 +379,7 @@ Ltac InvAgree := match goal with | [ H: False |- _ ] => contradiction | [ H: match ?v with Vundef => _ | Vint _ => _ | Vlong _ => _ | Vfloat _ => _ | Vsingle _ => _ | Vptr _ _ => _ end |- _ ] => destruct v + | [ |- context [if Archi.ptr64 then _ else _] ] => destruct Archi.ptr64 eqn:? end). (** And immediate, or immediate *) @@ -608,7 +609,8 @@ Lemma add_sound: Proof. unfold modarith; intros. destruct x; simpl in *. - auto. -- unfold Val.add; InvAgree. apply eqmod_iagree. apply Int.eqmod_add; apply iagree_eqmod; auto. +- unfold Val.add; InvAgree. + apply eqmod_iagree. apply Int.eqmod_add; apply iagree_eqmod; auto. - inv H; auto. inv H0; auto. destruct w1; auto. Qed. @@ -802,20 +804,20 @@ Hypothesis PERM: forall b ofs k p, Mem.perm m1 b ofs k p -> Mem.perm m2 b ofs k Let valid_pointer_inj: forall b1 ofs b2 delta, inject_id b1 = Some(b2, delta) -> - Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true -> - Mem.valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. + Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + Mem.valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true. Proof. - unfold inject_id; intros. inv H. rewrite Int.add_zero. + unfold inject_id; intros. inv H. rewrite Ptrofs.add_zero. rewrite Mem.valid_pointer_nonempty_perm in *. eauto. Qed. Let weak_valid_pointer_inj: forall b1 ofs b2 delta, inject_id b1 = Some(b2, delta) -> - Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true -> - Mem.weak_valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. + Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + Mem.weak_valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true. Proof. - unfold inject_id; intros. inv H. rewrite Int.add_zero. + unfold inject_id; intros. inv H. rewrite Ptrofs.add_zero. rewrite Mem.weak_valid_pointer_spec in *. rewrite ! Mem.valid_pointer_nonempty_perm in *. destruct H0; [left|right]; eauto. @@ -824,21 +826,21 @@ Qed. Let weak_valid_pointer_no_overflow: forall b1 ofs b2 delta, inject_id b1 = Some(b2, delta) -> - Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true -> - 0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned. + Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + 0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned. Proof. - unfold inject_id; intros. inv H. rewrite Zplus_0_r. apply Int.unsigned_range_2. + unfold inject_id; intros. inv H. rewrite Zplus_0_r. apply Ptrofs.unsigned_range_2. Qed. Let valid_different_pointers_inj: forall b1 ofs1 b2 ofs2 b1' delta1 b2' delta2, b1 <> b2 -> - Mem.valid_pointer m1 b1 (Int.unsigned ofs1) = true -> - Mem.valid_pointer m1 b2 (Int.unsigned ofs2) = true -> + Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs1) = true -> + Mem.valid_pointer m1 b2 (Ptrofs.unsigned ofs2) = true -> inject_id b1 = Some (b1', delta1) -> inject_id 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. unfold inject_id; intros. left; congruence. Qed. @@ -855,13 +857,13 @@ Qed. Lemma default_needs_of_operation_sound: forall op args1 v1 args2 nv, - eval_operation ge (Vptr sp Int.zero) op args1 m1 = Some v1 -> + eval_operation ge (Vptr sp Ptrofs.zero) op args1 m1 = Some v1 -> vagree_list args1 args2 nil \/ vagree_list args1 args2 (default nv :: nil) \/ vagree_list args1 args2 (default nv :: default nv :: nil) -> nv <> Nothing -> exists v2, - eval_operation ge (Vptr sp Int.zero) op args2 m2 = Some v2 + eval_operation ge (Vptr sp Ptrofs.zero) op args2 m2 = Some v2 /\ vagree v1 v2 nv. Proof. intros. assert (default nv = All) by (destruct nv; simpl; congruence). @@ -875,7 +877,7 @@ Proof. exploit (@eval_operation_inj _ _ _ _ ge ge inject_id). eassumption. auto. auto. auto. instantiate (1 := op). intros. apply val_inject_lessdef; auto. - apply val_inject_lessdef. instantiate (1 := Vptr sp Int.zero). instantiate (1 := Vptr sp Int.zero). auto. + apply val_inject_lessdef. instantiate (1 := Vptr sp Ptrofs.zero). instantiate (1 := Vptr sp Ptrofs.zero). auto. apply val_inject_list_lessdef; eauto. eauto. intros (v2 & A & B). exists v2; split; auto. @@ -1135,13 +1137,13 @@ Definition nmem_add (nm: nmem) (p: aptr) (sz: Z) : nmem := match p with | Gl id ofs => match gl!id with - | Some iv => NMem stk (PTree.set id (ISet.remove (Int.unsigned ofs) (Int.unsigned ofs + sz) iv) gl) + | Some iv => NMem stk (PTree.set id (ISet.remove (Ptrofs.unsigned ofs) (Ptrofs.unsigned ofs + sz) iv) gl) | None => nm end | Glo id => NMem stk (PTree.remove id gl) | Stk ofs => - NMem (ISet.remove (Int.unsigned ofs) (Int.unsigned ofs + sz) stk) gl + NMem (ISet.remove (Ptrofs.unsigned ofs) (Ptrofs.unsigned ofs + sz) stk) gl | Stack => NMem ISet.empty gl | _ => nmem_all @@ -1153,7 +1155,7 @@ Lemma nlive_add: genv_match bc ge -> bc sp = BCstack -> pmatch bc b ofs p -> - Int.unsigned ofs <= i < Int.unsigned ofs + sz -> + Ptrofs.unsigned ofs <= i < Ptrofs.unsigned ofs + sz -> nlive (nmem_add nm p sz) b i. Proof. intros. unfold nmem_add. destruct nm. apply nlive_all. @@ -1221,12 +1223,12 @@ Definition nmem_remove (nm: nmem) (p: aptr) (sz: Z) : nmem := | Gl id ofs => let iv' := match gl!id with - | Some iv => ISet.add (Int.unsigned ofs) (Int.unsigned ofs + sz) iv - | None => ISet.interval (Int.unsigned ofs) (Int.unsigned ofs + sz) + | Some iv => ISet.add (Ptrofs.unsigned ofs) (Ptrofs.unsigned ofs + sz) iv + | None => ISet.interval (Ptrofs.unsigned ofs) (Ptrofs.unsigned ofs + sz) end in NMem stk (PTree.set id iv' gl) | Stk ofs => - NMem (ISet.add (Int.unsigned ofs) (Int.unsigned ofs + sz) stk) gl + NMem (ISet.add (Ptrofs.unsigned ofs) (Ptrofs.unsigned ofs + sz) stk) gl | _ => nm end end. @@ -1237,17 +1239,17 @@ Lemma nlive_remove: bc sp = BCstack -> pmatch bc b ofs p -> nlive nm b' i -> - b' <> b \/ i < Int.unsigned ofs \/ Int.unsigned ofs + sz <= i -> + b' <> b \/ i < Ptrofs.unsigned ofs \/ Ptrofs.unsigned ofs + sz <= i -> nlive (nmem_remove nm p sz) b' i. Proof. intros. inversion H2; subst. unfold nmem_remove; inv H1; auto. - (* Gl id ofs *) set (iv' := match gl!id with | Some iv => - ISet.add (Int.unsigned ofs) (Int.unsigned ofs + sz) iv + ISet.add (Ptrofs.unsigned ofs) (Ptrofs.unsigned ofs + sz) iv | None => - ISet.interval (Int.unsigned ofs) - (Int.unsigned ofs + sz) + ISet.interval (Ptrofs.unsigned ofs) + (Ptrofs.unsigned ofs + sz) end). assert (Genv.find_symbol ge id = Some b) by (eapply H; eauto). split; simpl; auto; intros. @@ -1272,11 +1274,11 @@ Definition nmem_contains (nm: nmem) (p: aptr) (sz: Z) := match p with | Gl id ofs => match gl!id with - | Some iv => negb (ISet.contains (Int.unsigned ofs) (Int.unsigned ofs + sz) iv) + | Some iv => negb (ISet.contains (Ptrofs.unsigned ofs) (Ptrofs.unsigned ofs + sz) iv) | None => true end | Stk ofs => - negb (ISet.contains (Int.unsigned ofs) (Int.unsigned ofs + sz) stk) + negb (ISet.contains (Ptrofs.unsigned ofs) (Ptrofs.unsigned ofs + sz) stk) | _ => true (**r conservative answer *) end end. @@ -1287,7 +1289,7 @@ Lemma nlive_contains: bc sp = BCstack -> pmatch bc b ofs p -> nmem_contains nm p sz = false -> - Int.unsigned ofs <= i < Int.unsigned ofs + sz -> + Ptrofs.unsigned ofs <= i < Ptrofs.unsigned ofs + sz -> ~(nlive nm b i). Proof. unfold nmem_contains; intros. red; intros L; inv L. @@ -1295,10 +1297,10 @@ Proof. - (* Gl id ofs *) assert (Genv.find_symbol ge id = Some b) by (eapply H; eauto). destruct gl!id as [iv|] eqn:HG; inv H2. - destruct (ISet.contains (Int.unsigned ofs) (Int.unsigned ofs + sz) iv) eqn:IC; try discriminate. + destruct (ISet.contains (Ptrofs.unsigned ofs) (Ptrofs.unsigned ofs + sz) iv) eqn:IC; try discriminate. rewrite ISet.contains_spec in IC. eelim GL; eauto. - (* Stk ofs *) - destruct (ISet.contains (Int.unsigned ofs) (Int.unsigned ofs + sz) stk) eqn:IC; try discriminate. + destruct (ISet.contains (Ptrofs.unsigned ofs) (Ptrofs.unsigned ofs + sz) stk) eqn:IC; try discriminate. rewrite ISet.contains_spec in IC. eelim STK; eauto. eapply bc_stack; eauto. Qed. -- cgit