Support for 64-bit architectures: update the PowerPC port

The PowerPC port remains 32-bit only, no support is added for PPC 64.
This shows how much work is needed to update an existing port a minima.

1 files changed, 89 insertions, 74 deletions

diff --git a/powerpc/Op.v b/powerpc/Op.v
index c8028557..d59afd97 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -34,6 +34,7 @@ Require Import Globalenvs.
 Require Import Events.
 
 Set Implicit Arguments.
+Local Transparent Archi.ptr64.
 
 (** Conditions (boolean-valued operators). *)
 
@@ -55,14 +56,14 @@ Inductive operation : Type :=
   | Ointconst: int -> operation         (**r [rd] is set to the given integer constant *)
   | Ofloatconst: float -> operation     (**r [rd] is set to the given float constant *)
   | Osingleconst: float32 -> operation  (**r [rd] is set to the given float constant *)
-  | Oaddrsymbol: ident -> int -> operation (**r [rd] is set to the the address of the symbol plus the offset *)
-  | Oaddrstack: int -> operation        (**r [rd] is set to the stack pointer plus the given offset *)
+  | Oaddrsymbol: ident -> ptrofs -> operation (**r [rd] is set to the the address of the symbol plus the offset *)
+  | Oaddrstack: ptrofs -> operation        (**r [rd] is set to the stack pointer plus the given offset *)
 (*c Integer arithmetic: *)
   | Ocast8signed: operation             (**r [rd] is 8-bit sign extension of [r1] *)
   | Ocast16signed: operation            (**r [rd] is 16-bit sign extension of [r1] *)
   | Oadd: operation                     (**r [rd = r1 + r2] *)
   | Oaddimm: int -> operation           (**r [rd = r1 + n] *)
-  | Oaddsymbol: ident -> int -> operation (**r [rd = addr(id + ofs) + r1] *)
+  | Oaddsymbol: ident -> ptrofs -> operation (**r [rd = addr(id + ofs) + r1] *)
   | Osub: operation                     (**r [rd = r1 - r2] *)
   | Osubimm: int -> operation           (**r [rd = n - r1] *)
   | Omul: operation                     (**r [rd = r1 * r2] *)
@@ -124,9 +125,9 @@ Inductive operation : Type :=
 Inductive addressing: Type :=
   | Aindexed: int -> addressing         (**r Address is [r1 + offset] *)
   | Aindexed2: addressing               (**r Address is [r1 + r2] *)
-  | Aglobal: ident -> int -> addressing (**r Address is [symbol + offset] *)
-  | Abased: ident -> int -> addressing (**r Address is [symbol + offset + r1] *)
-  | Ainstack: int -> addressing.        (**r Address is [stack_pointer + offset] *)
+  | Aglobal: ident -> ptrofs -> addressing (**r Address is [symbol + offset] *)
+  | Abased: ident -> ptrofs -> addressing (**r Address is [symbol + offset + r1] *)
+  | Ainstack: ptrofs -> addressing.        (**r Address is [stack_pointer + offset] *)
 
 (** Comparison functions (used in module [CSE]). *)
 
@@ -140,17 +141,15 @@ Defined.
 
 Definition eq_operation (x y: operation): {x=y} + {x<>y}.
 Proof.
-  generalize Int.eq_dec; intro.
+  generalize Int.eq_dec Ptrofs.eq_dec ident_eq; intro.
   generalize Float.eq_dec Float32.eq_dec; intros.
-  assert (forall (x y: ident), {x=y}+{x<>y}). exact peq.
   generalize eq_condition; intro.
   decide equality.
 Defined.
 
 Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}.
 Proof.
-  generalize Int.eq_dec; intro.
-  assert (forall (x y: ident), {x=y}+{x<>y}). exact peq.
+  generalize Int.eq_dec Ptrofs.eq_dec ident_eq; intro.
   decide equality.
 Defined.
 
@@ -185,7 +184,7 @@ Definition eval_operation
   | Ofloatconst n, nil => Some (Vfloat n)
   | Osingleconst n, nil => Some (Vsingle n)
   | Oaddrsymbol s ofs, nil => Some (Genv.symbol_address genv s ofs)
-  | Oaddrstack ofs, nil => Some (Val.add sp (Vint ofs))
+  | Oaddrstack ofs, nil => Some (Val.offset_ptr sp ofs)
   | Ocast8signed, v1::nil => Some (Val.sign_ext 8 v1)
   | Ocast16signed, v1::nil => Some (Val.sign_ext 16 v1)
   | Oadd, v1::v2::nil => Some (Val.add v1 v2)
@@ -253,10 +252,24 @@ Definition eval_addressing
   | Aindexed2, v1::v2::nil => Some (Val.add v1 v2)
   | Aglobal s ofs, nil => Some (Genv.symbol_address genv s ofs)
   | Abased s ofs, v1::nil => Some (Val.add (Genv.symbol_address genv s ofs) v1)
-  | Ainstack ofs, nil => Some(Val.add sp (Vint ofs))
+  | Ainstack ofs, nil => Some(Val.offset_ptr sp ofs)
   | _, _ => None
   end.
 
+Remark eval_addressing_Ainstack:
+  forall (F V: Type) (genv: Genv.t F V) sp ofs,
+  eval_addressing genv sp (Ainstack ofs) nil = Some (Val.offset_ptr sp ofs).
+Proof.
+  intros. reflexivity.
+Qed.
+
+Remark eval_addressing_Ainstack_inv:
+  forall (F V: Type) (genv: Genv.t F V) sp ofs vl v,
+  eval_addressing genv sp (Ainstack ofs) vl = Some v -> vl = nil /\ v = Val.offset_ptr sp ofs.
+Proof.
+  unfold eval_addressing; intros; destruct vl; inv H; auto.
+Qed.
+
 Ltac FuncInv :=
   match goal with
   | H: (match ?x with nil => _ | _ :: _ => _ end = Some _) |- _ =>
@@ -371,7 +384,7 @@ Lemma type_of_operation_sound:
   op <> Omove ->
   eval_operation genv sp op vl m = Some v ->
   Val.has_type v (snd (type_of_operation op)).
-Proof with (try exact I).
+Proof with (try exact I; try reflexivity).
   intros.
   destruct op; simpl in H0; FuncInv; subst; simpl.
   congruence.
@@ -496,15 +509,15 @@ Qed.
 
 (** Shifting stack-relative references.  This is used in [Stacking]. *)
 
-Definition shift_stack_addressing (delta: int) (addr: addressing) :=
+Definition shift_stack_addressing (delta: Z) (addr: addressing) :=
   match addr with
-  | Ainstack ofs => Ainstack (Int.add delta ofs)
+  | Ainstack ofs => Ainstack (Ptrofs.add (Ptrofs.repr delta) ofs)
   | _ => addr
   end.
 
-Definition shift_stack_operation (delta: int) (op: operation) :=
+Definition shift_stack_operation (delta: Z) (op: operation) :=
   match op with
-  | Oaddrstack ofs => Oaddrstack (Int.add delta ofs)
+  | Oaddrstack ofs => Oaddrstack (Ptrofs.add (Ptrofs.repr delta) ofs)
   | _ => op
   end.
 
@@ -522,47 +535,50 @@ Qed.
 
 Lemma eval_shift_stack_addressing:
   forall F V (ge: Genv.t F V) sp addr vl delta,
-  eval_addressing ge sp (shift_stack_addressing delta addr) vl =
-  eval_addressing ge (Val.add sp (Vint delta)) addr vl.
+  eval_addressing ge (Vptr sp Ptrofs.zero) (shift_stack_addressing delta addr) vl =
+  eval_addressing ge (Vptr sp (Ptrofs.repr delta)) addr vl.
 Proof.
   intros. destruct addr; simpl; auto.
-  rewrite Val.add_assoc. simpl. auto.
+  rewrite Ptrofs.add_zero_l; auto.
 Qed.
 
 Lemma eval_shift_stack_operation:
   forall F V (ge: Genv.t F V) sp op vl m delta,
-  eval_operation ge sp (shift_stack_operation delta op) vl m =
-  eval_operation ge (Val.add sp (Vint delta)) op vl m.
+  eval_operation ge (Vptr sp Ptrofs.zero) (shift_stack_operation delta op) vl m =
+  eval_operation ge (Vptr sp (Ptrofs.repr delta)) op vl m.
 Proof.
   intros. destruct op; simpl; auto.
-  rewrite Val.add_assoc. simpl. auto.
+  rewrite Ptrofs.add_zero_l; auto.
 Qed.
 
 (** Offset an addressing mode [addr] by a quantity [delta], so that
   it designates the pointer [delta] bytes past the pointer designated
   by [addr].  May be undefined, in which case [None] is returned. *)
 
-Definition offset_addressing (addr: addressing) (delta: int) : option addressing :=
+Definition offset_addressing (addr: addressing) (delta: Z) : option addressing :=
   match addr with
-  | Aindexed n => Some(Aindexed (Int.add n delta))
+  | Aindexed n => Some(Aindexed (Int.add n (Int.repr delta)))
   | Aindexed2 => None
-  | Aglobal s n => Some(Aglobal s (Int.add n delta))
-  | Abased s n => Some(Abased s (Int.add n delta))
-  | Ainstack n => Some(Ainstack (Int.add n delta))
+  | Aglobal s n => Some(Aglobal s (Ptrofs.add n (Ptrofs.repr delta)))
+  | Abased s n => Some(Abased s (Ptrofs.add n (Ptrofs.repr delta)))
+  | Ainstack n => Some(Ainstack (Ptrofs.add n (Ptrofs.repr delta)))
   end.
 
 Lemma eval_offset_addressing:
   forall (F V: Type) (ge: Genv.t F V) sp addr args delta addr' v,
   offset_addressing addr delta = Some addr' ->
   eval_addressing ge sp addr args = Some v ->
-  eval_addressing ge sp addr' args = Some(Val.add v (Vint delta)).
+  eval_addressing ge sp addr' args = Some(Val.add v (Vint (Int.repr delta))).
 Proof.
-  intros. destruct addr; simpl in H; inv H; simpl in *; FuncInv; subst.
-  rewrite Val.add_assoc; auto.
-  unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); auto.
-  unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); auto.
-  rewrite Val.add_assoc. rewrite Val.add_permut. rewrite Val.add_commut. auto.
-  rewrite Val.add_assoc. auto.
+  intros. 
+  assert (D: Ptrofs.repr delta = Ptrofs.of_int (Int.repr delta)) by (symmetry; auto with ptrofs).
+  destruct addr; simpl in H; inv H; simpl in *; FuncInv; subst.
+- rewrite Val.add_assoc; auto.
+- unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); auto. rewrite D; auto.
+- unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); auto.
+  rewrite Val.add_assoc. rewrite Val.add_permut. rewrite Val.add_commut.
+  simpl. rewrite D. auto.
+- destruct sp; simpl; auto. rewrite Ptrofs.add_assoc, D. auto.
 Qed.
 
 (** Operations that are so cheap to recompute that CSE should not factor them out. *)
@@ -662,30 +678,30 @@ Variable m2: mem.
 Hypothesis valid_pointer_inj:
   forall b1 ofs b2 delta,
   f 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.
 
 Hypothesis weak_valid_pointer_inj:
   forall b1 ofs b2 delta,
   f 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.
 
 Hypothesis weak_valid_pointer_no_overflow:
   forall b1 ofs b2 delta,
   f 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.
 
 Hypothesis 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 ->
   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)).
 
 Ltac InvInject :=
   match goal with
@@ -740,16 +756,13 @@ Lemma eval_operation_inj:
 Proof.
   intros until v1; intros GL; intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists.
   apply GL; simpl; auto.
-  apply Values.Val.add_inject; auto.
+  apply Val.offset_ptr_inject; auto.
   inv H4; simpl; auto.
   inv H4; simpl; auto.
-  apply Values.Val.add_inject; auto.
-  apply Values.Val.add_inject; auto.
-  apply Values.Val.add_inject; auto. apply GL; simpl; auto.
-  inv H4; inv H2; simpl; auto. econstructor; eauto.
-    rewrite Int.sub_add_l. auto.
-    destruct (eq_block b1 b0); auto. subst. rewrite H1 in H0. inv H0. rewrite dec_eq_true.
-    rewrite Int.sub_shifted. auto.
+  apply Val.add_inject; auto.
+  apply Val.add_inject; auto.
+  apply Val.add_inject; auto. apply GL; simpl; auto.
+  apply Val.sub_inject; auto.
   inv H4; auto.
   inv H4; inv H2; simpl; auto.
   inv H4; simpl; auto.
@@ -820,9 +833,9 @@ Lemma eval_addressing_inj:
   exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ Val.inject f v1 v2.
 Proof.
   intros. destruct addr; simpl in H2; simpl; FuncInv; InvInject; TrivialExists;
-    auto using Values.Val.add_inject.
+    auto using Val.add_inject, Val.offset_ptr_inject.
   apply H; simpl; auto.
-  apply Values.Val.add_inject; auto. apply H; simpl; auto.
+  apply Val.add_inject; auto. apply H; simpl; auto.
 Qed.
 
 End EVAL_COMPAT.
@@ -838,40 +851,40 @@ Remark valid_pointer_extends:
   forall m1 m2, Mem.extends m1 m2 ->
   forall b1 ofs b2 delta,
   Some(b1, 0) = 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.
-  intros. inv H0. rewrite Int.add_zero. eapply Mem.valid_pointer_extends; eauto.
+  intros. inv H0. rewrite Ptrofs.add_zero. eapply Mem.valid_pointer_extends; eauto.
 Qed.
 
 Remark weak_valid_pointer_extends:
   forall m1 m2, Mem.extends m1 m2 ->
   forall b1 ofs b2 delta,
   Some(b1, 0) = 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.
-  intros. inv H0. rewrite Int.add_zero. eapply Mem.weak_valid_pointer_extends; eauto.
+  intros. inv H0. rewrite Ptrofs.add_zero. eapply Mem.weak_valid_pointer_extends; eauto.
 Qed.
 
 Remark weak_valid_pointer_no_overflow_extends:
   forall m1 b1 ofs b2 delta,
   Some(b1, 0) = 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.
-  intros. inv H. rewrite Zplus_0_r. apply Int.unsigned_range_2.
+  intros. inv H. rewrite Zplus_0_r. apply Ptrofs.unsigned_range_2.
 Qed.
 
 Remark valid_different_pointers_extends:
   forall m1 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 ->
   Some(b1, 0) = Some (b1', delta1) ->
   Some(b2, 0) = 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. inv H2; inv H3. auto.
 Qed.
@@ -950,7 +963,7 @@ Remark symbol_address_inject:
 Proof.
   intros. unfold Genv.symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto.
   exploit (proj1 globals); eauto. intros.
-  econstructor; eauto. rewrite Int.add_zero; auto.
+  econstructor; eauto. rewrite Ptrofs.add_zero; auto.
 Qed.
 
 Lemma eval_condition_inject:
@@ -970,34 +983,36 @@ Qed.
 Lemma eval_addressing_inject:
   forall addr vl1 vl2 v1,
   Val.inject_list f vl1 vl2 ->
-  eval_addressing genv (Vptr sp1 Int.zero) addr vl1 = Some v1 ->
+  eval_addressing genv (Vptr sp1 Ptrofs.zero) addr vl1 = Some v1 ->
   exists v2,
-     eval_addressing genv (Vptr sp2 Int.zero) (shift_stack_addressing (Int.repr delta) addr) vl2 = Some v2
+     eval_addressing genv (Vptr sp2 Ptrofs.zero) (shift_stack_addressing delta addr) vl2 = Some v2
   /\ Val.inject f v1 v2.
 Proof.
   intros.
-  rewrite eval_shift_stack_addressing. simpl.
-  eapply eval_addressing_inj with (sp1 := Vptr sp1 Int.zero); eauto.
+  rewrite eval_shift_stack_addressing.
+  eapply eval_addressing_inj with (sp1 := Vptr sp1 Ptrofs.zero); eauto.
   intros. apply symbol_address_inject.
+  econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. 
 Qed.
 
 Lemma eval_operation_inject:
   forall op vl1 vl2 v1 m1 m2,
   Val.inject_list f vl1 vl2 ->
   Mem.inject f m1 m2 ->
-  eval_operation genv (Vptr sp1 Int.zero) op vl1 m1 = Some v1 ->
+  eval_operation genv (Vptr sp1 Ptrofs.zero) op vl1 m1 = Some v1 ->
   exists v2,
-     eval_operation genv (Vptr sp2 Int.zero) (shift_stack_operation (Int.repr delta) op) vl2 m2 = Some v2
+     eval_operation genv (Vptr sp2 Ptrofs.zero) (shift_stack_operation delta op) vl2 m2 = Some v2
   /\ Val.inject f v1 v2.
 Proof.
   intros.
   rewrite eval_shift_stack_operation. simpl.
-  eapply eval_operation_inj with (sp1 := Vptr sp1 Int.zero) (m1 := m1); eauto.
+  eapply eval_operation_inj with (sp1 := Vptr sp1 Ptrofs.zero) (m1 := m1); eauto.
   intros; eapply Mem.valid_pointer_inject_val; eauto.
   intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
   intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
   intros; eapply Mem.different_pointers_inject; eauto.
   intros. apply symbol_address_inject.
+  econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. 
 Qed.
 
 End EVAL_INJECT.