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.

1 files changed, 454 insertions, 3 deletions

diff --git a/lib/Integers.v b/lib/Integers.v
index 16c95e01..593f0ccc 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -15,10 +15,9 @@
 
 (** Formalizations of machine integers modulo $2^N$ #2<sup>N</sup>#. *)
 
-Require Import Eqdep_dec.
-Require Import Zquot.
-Require Import Zwf.
+Require Import Eqdep_dec Zquot Zwf.
 Require Import Coqlib.
+Require Archi.
 
 (** * Comparisons *)
 
@@ -3652,6 +3651,53 @@ Proof.
     unfold min_signed, max_signed; omega.
 Qed.
 
+Lemma signed_eq:
+  forall x y, eq x y = zeq (signed x) (signed y).
+Proof.
+  intros. unfold eq. unfold proj_sumbool.
+  destruct (zeq (unsigned x) (unsigned y));
+  destruct (zeq (signed x) (signed y)); auto.
+  elim n. unfold signed. rewrite e; auto.
+  elim n. apply eqm_small_eq; auto with ints.
+  eapply eqm_trans. apply eqm_sym. apply eqm_signed_unsigned.
+  rewrite e. apply eqm_signed_unsigned.
+Qed.
+
+Lemma not_lt:
+  forall x y, negb (lt y x) = (lt x y || eq x y).
+Proof.
+  intros. unfold lt. rewrite signed_eq. unfold proj_sumbool.
+  destruct (zlt (signed y) (signed x)).
+  rewrite zlt_false. rewrite zeq_false. auto. omega. omega.
+  destruct (zeq (signed x) (signed y)).
+  rewrite zlt_false. auto. omega.
+  rewrite zlt_true. auto. omega.
+Qed.
+
+Lemma lt_not:
+  forall x y, lt y x = negb (lt x y) && negb (eq x y).
+Proof.
+  intros. rewrite <- negb_orb. rewrite <- not_lt. rewrite negb_involutive. auto.
+Qed.
+
+Lemma not_ltu:
+  forall x y, negb (ltu y x) = (ltu x y || eq x y).
+Proof.
+  intros. unfold ltu, eq.
+  destruct (zlt (unsigned y) (unsigned x)).
+  rewrite zlt_false. rewrite zeq_false. auto. omega. omega.
+  destruct (zeq (unsigned x) (unsigned y)).
+  rewrite zlt_false. auto. omega.
+  rewrite zlt_true. auto. omega.
+Qed.
+
+Lemma ltu_not:
+  forall x y, ltu y x = negb (ltu x y) && negb (eq x y).
+Proof.
+  intros. rewrite <- negb_orb. rewrite <- not_ltu. rewrite negb_involutive. auto.
+Qed.
+
+
 (** Non-overlapping test *)
 
 Definition no_overlap (ofs1: int) (sz1: Z) (ofs2: int) (sz2: Z) : bool :=
@@ -4007,6 +4053,130 @@ Proof.
   omega.
 Qed.
 
+Lemma shl'_mul_two_p:
+  forall x y,
+  shl' x y = mul x (repr (two_p (Int.unsigned y))).
+Proof.
+  intros. unfold shl', mul. apply eqm_samerepr.
+  rewrite Zshiftl_mul_two_p. apply eqm_mult. apply eqm_refl. apply eqm_unsigned_repr. 
+  generalize (Int.unsigned_range y); omega.
+Qed.
+
+Lemma shl'_one_two_p:
+  forall y, shl' one y = repr (two_p (Int.unsigned y)).
+Proof.
+  intros. rewrite shl'_mul_two_p. rewrite mul_commut. rewrite mul_one. auto.
+Qed.
+
+Theorem shl'_mul:
+  forall x y,
+  shl' x y = mul x (shl' one y).
+Proof.
+  intros. rewrite shl'_one_two_p. apply shl'_mul_two_p.
+Qed.
+
+(** Powers of two with exponents given as 32-bit ints *)
+
+Definition one_bits' (x: int) : list Int.int :=
+  List.map Int.repr (Z_one_bits wordsize (unsigned x) 0).
+
+Definition is_power2' (x: int) : option Int.int :=
+  match Z_one_bits wordsize (unsigned x) 0 with
+  | i :: nil => Some (Int.repr i)
+  | _ => None
+  end.
+
+Theorem one_bits'_range:
+  forall x i, In i (one_bits' x) -> Int.ltu i iwordsize' = true.
+Proof.
+  intros.
+  destruct (list_in_map_inv _ _ _ H) as [i0 [EQ IN]].
+  exploit Z_one_bits_range; eauto. intros R.
+  unfold Int.ltu. rewrite EQ. rewrite Int.unsigned_repr. 
+  change (Int.unsigned iwordsize') with zwordsize. apply zlt_true. omega. 
+  assert (zwordsize < Int.max_unsigned) by reflexivity. omega.
+Qed.
+
+Fixpoint int_of_one_bits' (l: list Int.int) : int :=
+  match l with
+  | nil => zero
+  | a :: b => add (shl' one a) (int_of_one_bits' b)
+  end.
+
+Theorem one_bits'_decomp:
+  forall x, x = int_of_one_bits' (one_bits' x).
+Proof.
+  assert (REC: forall l,
+           (forall i, In i l -> 0 <= i < zwordsize) ->
+           int_of_one_bits' (List.map Int.repr l) = repr (powerserie l)).
+  { induction l; simpl; intros.
+  - auto.
+  - rewrite IHl by eauto. apply eqm_samerepr; apply eqm_add.
+  + rewrite shl'_one_two_p. rewrite Int.unsigned_repr. apply eqm_sym; apply eqm_unsigned_repr.  
+    exploit (H a). auto. assert (zwordsize < Int.max_unsigned) by reflexivity. omega.
+  + apply eqm_sym; apply eqm_unsigned_repr. 
+  }
+  intros. rewrite <- (repr_unsigned x) at 1. unfold one_bits'. rewrite REC. 
+  rewrite <- Z_one_bits_powerserie. auto. apply unsigned_range.
+  apply Z_one_bits_range.    
+Qed.
+
+Lemma is_power2'_rng:
+  forall n logn,
+  is_power2' n = Some logn ->
+  0 <= Int.unsigned logn < zwordsize.
+Proof.
+  unfold is_power2'; intros n logn P2. 
+  destruct (Z_one_bits wordsize (unsigned n) 0) as [ | i [ | ? ?]] eqn:B; inv P2.
+  assert (0 <= i < zwordsize).
+  { apply Z_one_bits_range with (unsigned n). rewrite B; auto with coqlib. }
+  rewrite Int.unsigned_repr. auto.
+  assert (zwordsize < Int.max_unsigned) by reflexivity.
+  omega.
+Qed.
+
+Theorem is_power2'_range:
+  forall n logn,
+  is_power2' n = Some logn -> Int.ltu logn iwordsize' = true.
+Proof.
+  intros. unfold Int.ltu. change (Int.unsigned iwordsize') with zwordsize. 
+  apply zlt_true. generalize (is_power2'_rng _ _ H). tauto.
+Qed.
+
+Lemma is_power2'_correct:
+  forall n logn,
+  is_power2' n = Some logn ->
+  unsigned n = two_p (Int.unsigned logn).
+Proof.
+  unfold is_power2'; intros.
+  destruct (Z_one_bits wordsize (unsigned n) 0) as [ | i [ | ? ?]] eqn:B; inv H.
+  rewrite (Z_one_bits_powerserie (unsigned n)) by (apply unsigned_range).
+  rewrite Int.unsigned_repr. rewrite B; simpl. omega.
+  assert (0 <= i < zwordsize).
+  { apply Z_one_bits_range with (unsigned n). rewrite B; auto with coqlib. }
+  assert (zwordsize < Int.max_unsigned) by reflexivity.
+  omega.
+Qed.
+   
+Theorem mul_pow2':
+  forall x n logn,
+  is_power2' n = Some logn ->
+  mul x n = shl' x logn.
+Proof.
+  intros. rewrite shl'_mul. f_equal. rewrite shl'_one_two_p. 
+  rewrite <- (repr_unsigned n). f_equal. apply is_power2'_correct; auto.
+Qed.
+
+Theorem divu_pow2':
+  forall x n logn,
+  is_power2' n = Some logn ->
+  divu x n = shru' x logn.
+Proof.
+  intros. generalize (is_power2'_correct n logn H). intro.
+  symmetry. unfold divu. rewrite H0. unfold shru'. rewrite Zshiftr_div_two_p. auto.
+  eapply is_power2'_rng; eauto.
+Qed.
+
 (** Decomposing 64-bit ints as pairs of 32-bit ints *)
 
 Definition loword (n: int) : Int.int := Int.repr (unsigned n).
@@ -4528,3 +4698,284 @@ Strategy 0 [Wordsize_64.wordsize].
 Notation int64 := Int64.int.
 
 Global Opaque Int.repr Int64.repr Byte.repr.
+
+(** * Specialization to offsets in pointer values *)
+
+Module Wordsize_Ptrofs.
+  Definition wordsize := if Archi.ptr64 then 64%nat else 32%nat.
+  Remark wordsize_not_zero: wordsize <> 0%nat.
+  Proof. unfold wordsize; destruct Archi.ptr64; congruence. Qed.
+End Wordsize_Ptrofs.
+
+Strategy opaque [Wordsize_Ptrofs.wordsize].
+
+Module Ptrofs.
+
+Include Make(Wordsize_Ptrofs).
+
+Definition to_int (x: int): Int.int := Int.repr (unsigned x).
+
+Definition to_int64 (x: int): Int64.int := Int64.repr (unsigned x).
+
+Definition of_int (x: Int.int) : int := repr (Int.unsigned x).
+
+Definition of_intu := of_int.
+
+Definition of_ints (x: Int.int) : int := repr (Int.signed x).
+
+Definition of_int64 (x: Int64.int) : int := repr (Int64.unsigned x).
+
+Definition of_int64u := of_int64.
+
+Definition of_int64s (x: Int64.int) : int := repr (Int64.signed x).
+
+Section AGREE32.
+
+Hypothesis _32: Archi.ptr64 = false.
+
+Lemma modulus_eq32: modulus = Int.modulus.
+Proof.
+  unfold modulus, wordsize. 
+  change Wordsize_Ptrofs.wordsize with (if Archi.ptr64 then 64%nat else 32%nat).
+  rewrite _32. reflexivity.
+Qed.
+
+Lemma eqm32:
+  forall x y, Int.eqm x y <-> eqm x y.
+Proof.
+  intros. unfold Int.eqm, eqm. rewrite modulus_eq32; tauto.
+Qed.
+
+Definition agree32 (a: Ptrofs.int) (b: Int.int) : Prop :=
+  Ptrofs.unsigned a = Int.unsigned b.
+
+Lemma agree32_repr:
+  forall i, agree32 (Ptrofs.repr i) (Int.repr i).
+Proof.
+  intros; red. rewrite Ptrofs.unsigned_repr_eq, Int.unsigned_repr_eq.
+  apply f_equal2. auto. apply modulus_eq32.
+Qed.
+
+Lemma agree32_signed:
+  forall a b, agree32 a b -> Ptrofs.signed a = Int.signed b.
+Proof.
+  unfold agree32; intros. unfold signed, Int.signed, half_modulus, Int.half_modulus. 
+  rewrite modulus_eq32. rewrite H. auto. 
+Qed.
+
+Lemma agree32_of_int:
+  forall b, agree32 (of_int b) b.
+Proof.
+  unfold of_int; intros. rewrite <- (Int.repr_unsigned b) at 2. apply agree32_repr.
+Qed.
+ 
+Lemma agree32_of_ints:
+  forall b, agree32 (of_ints b) b.
+Proof.
+  unfold of_int; intros. rewrite <- (Int.repr_signed b) at 2. apply agree32_repr.
+Qed.
+
+Lemma agree32_of_int_eq:
+  forall a b, agree32 a b -> of_int b = a.
+Proof.
+  unfold agree32, of_int; intros. rewrite <- H. apply repr_unsigned. 
+Qed.
+
+Lemma agree32_of_ints_eq:
+  forall a b, agree32 a b -> of_ints b = a.
+Proof.
+  unfold of_ints; intros. erewrite <- agree32_signed by eauto. apply repr_signed.
+Qed.
+
+Lemma agree32_to_int:
+  forall a, agree32 a (to_int a).
+Proof.
+  unfold agree32, to_int; intros. rewrite <- (agree32_repr (unsigned a)). 
+  rewrite repr_unsigned; auto.
+Qed.
+
+Lemma agree32_to_int_eq:
+  forall a b, agree32 a b -> to_int a = b.
+Proof.
+  unfold agree32, to_int; intros. rewrite H. apply Int.repr_unsigned.
+Qed.
+
+Lemma agree32_neg:
+  forall a1 b1, agree32 a1 b1 -> agree32 (Ptrofs.neg a1) (Int.neg b1).
+Proof.
+  unfold agree32, Ptrofs.neg, Int.neg; intros. rewrite H. apply agree32_repr.
+Qed.
+
+Lemma agree32_add:
+  forall a1 b1 a2 b2,
+  agree32 a1 b1 -> agree32 a2 b2 -> agree32 (Ptrofs.add a1 a2) (Int.add b1 b2).
+Proof.
+  unfold agree32, Ptrofs.add, Int.add; intros. rewrite H, H0. apply agree32_repr. 
+Qed.
+
+Lemma agree32_sub:
+  forall a1 b1 a2 b2,
+  agree32 a1 b1 -> agree32 a2 b2 -> agree32 (Ptrofs.sub a1 a2) (Int.sub b1 b2).
+Proof.
+  unfold agree32, Ptrofs.sub, Int.sub; intros. rewrite H, H0. apply agree32_repr. 
+Qed.
+
+Lemma agree32_mul:
+  forall a1 b1 a2 b2,
+  agree32 a1 b1 -> agree32 a2 b2 -> agree32 (Ptrofs.mul a1 a2) (Int.mul b1 b2).
+Proof.
+  unfold agree32, Ptrofs.mul, Int.mul; intros. rewrite H, H0. apply agree32_repr. 
+Qed.
+
+Lemma agree32_divs:
+  forall a1 b1 a2 b2,
+  agree32 a1 b1 -> agree32 a2 b2 -> agree32 (Ptrofs.divs a1 a2) (Int.divs b1 b2).
+Proof.
+  intros; unfold agree32, Ptrofs.divs, Int.divs.
+  erewrite ! agree32_signed by eauto. apply agree32_repr.
+Qed.
+
+Lemma of_int_to_int:
+  forall n, of_int (to_int n) = n.
+Proof.
+  intros; unfold of_int, to_int. apply eqm_repr_eq. rewrite <- eqm32.
+  apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
+Qed.   
+
+End AGREE32.
+
+Section AGREE64.
+
+Hypothesis _64: Archi.ptr64 = true.
+
+Lemma modulus_eq64: modulus = Int64.modulus.
+Proof.
+  unfold modulus, wordsize. 
+  change Wordsize_Ptrofs.wordsize with (if Archi.ptr64 then 64%nat else 32%nat).
+  rewrite _64. reflexivity.
+Qed.
+
+Lemma eqm64:
+  forall x y, Int64.eqm x y <-> eqm x y.
+Proof.
+  intros. unfold Int64.eqm, eqm. rewrite modulus_eq64; tauto.
+Qed.
+
+Definition agree64 (a: Ptrofs.int) (b: Int64.int) : Prop :=
+  Ptrofs.unsigned a = Int64.unsigned b.
+
+Lemma agree64_repr:
+  forall i, agree64 (Ptrofs.repr i) (Int64.repr i).
+Proof.
+  intros; red. rewrite Ptrofs.unsigned_repr_eq, Int64.unsigned_repr_eq.
+  apply f_equal2. auto. apply modulus_eq64.
+Qed.
+
+Lemma agree64_signed:
+  forall a b, agree64 a b -> Ptrofs.signed a = Int64.signed b.
+Proof.
+  unfold agree64; intros. unfold signed, Int64.signed, half_modulus, Int64.half_modulus. 
+  rewrite modulus_eq64. rewrite H. auto. 
+Qed.
+
+Lemma agree64_of_int:
+  forall b, agree64 (of_int64 b) b.
+Proof.
+  unfold of_int64; intros. rewrite <- (Int64.repr_unsigned b) at 2. apply agree64_repr.
+Qed.
+
+Lemma agree64_of_int_eq:
+  forall a b, agree64 a b -> of_int64 b = a.
+Proof.
+  unfold agree64, of_int64; intros. rewrite <- H. apply repr_unsigned. 
+Qed.
+
+Lemma agree64_to_int:
+  forall a, agree64 a (to_int64 a).
+Proof.
+  unfold agree64, to_int64; intros. rewrite <- (agree64_repr (unsigned a)). 
+  rewrite repr_unsigned; auto.
+Qed.
+
+Lemma agree64_to_int_eq:
+  forall a b, agree64 a b -> to_int64 a = b.
+Proof.
+  unfold agree64, to_int64; intros. rewrite H. apply Int64.repr_unsigned.
+Qed.
+
+Lemma agree64_neg:
+  forall a1 b1, agree64 a1 b1 -> agree64 (Ptrofs.neg a1) (Int64.neg b1).
+Proof.
+  unfold agree64, Ptrofs.neg, Int64.neg; intros. rewrite H. apply agree64_repr.
+Qed.
+
+Lemma agree64_add:
+  forall a1 b1 a2 b2,
+  agree64 a1 b1 -> agree64 a2 b2 -> agree64 (Ptrofs.add a1 a2) (Int64.add b1 b2).
+Proof.
+  unfold agree64, Ptrofs.add, Int.add; intros. rewrite H, H0. apply agree64_repr. 
+Qed.
+
+Lemma agree64_sub:
+  forall a1 b1 a2 b2,
+  agree64 a1 b1 -> agree64 a2 b2 -> agree64 (Ptrofs.sub a1 a2) (Int64.sub b1 b2).
+Proof.
+  unfold agree64, Ptrofs.sub, Int.sub; intros. rewrite H, H0. apply agree64_repr. 
+Qed.
+
+Lemma agree64_mul:
+  forall a1 b1 a2 b2,
+  agree64 a1 b1 -> agree64 a2 b2 -> agree64 (Ptrofs.mul a1 a2) (Int64.mul b1 b2).
+Proof.
+  unfold agree64, Ptrofs.mul, Int.mul; intros. rewrite H, H0. apply agree64_repr. 
+Qed.
+
+Lemma agree64_divs:
+  forall a1 b1 a2 b2,
+  agree64 a1 b1 -> agree64 a2 b2 -> agree64 (Ptrofs.divs a1 a2) (Int64.divs b1 b2).
+Proof.
+  intros; unfold agree64, Ptrofs.divs, Int64.divs.
+  erewrite ! agree64_signed by eauto. apply agree64_repr.
+Qed.
+
+Lemma of_int64_to_int64:
+  forall n, of_int64 (to_int64 n) = n.
+Proof.
+  intros; unfold of_int64, to_int64. apply eqm_repr_eq. rewrite <- eqm64.
+  apply Int64.eqm_sym; apply Int64.eqm_unsigned_repr.
+Qed.   
+
+End AGREE64.
+
+Hint Resolve 
+  agree32_repr agree32_of_int agree32_of_ints agree32_of_int_eq agree32_of_ints_eq
+  agree32_to_int agree32_to_int_eq agree32_neg agree32_add agree32_sub agree32_mul agree32_divs
+  agree64_repr agree64_of_int agree64_of_int_eq
+  agree64_to_int agree64_to_int_eq agree64_neg agree64_add agree64_sub agree64_mul agree64_divs : ptrofs.
+              
+End Ptrofs.
+
+Strategy 0 [Wordsize_Ptrofs.wordsize].
+
+Notation ptrofs := Ptrofs.int.
+
+Global Opaque Ptrofs.repr.
+
+Hint Resolve Int.modulus_pos Int.eqm_refl Int.eqm_refl2 Int.eqm_sym Int.eqm_trans
+  Int.eqm_small_eq Int.eqm_add Int.eqm_neg Int.eqm_sub Int.eqm_mult
+  Int.eqm_unsigned_repr Int.eqm_unsigned_repr_l Int.eqm_unsigned_repr_r
+  Int.unsigned_range Int.unsigned_range_2
+  Int.repr_unsigned Int.repr_signed Int.unsigned_repr : ints.
+
+Hint Resolve Int64.modulus_pos Int64.eqm_refl Int64.eqm_refl2 Int64.eqm_sym Int64.eqm_trans
+  Int64.eqm_small_eq Int64.eqm_add Int64.eqm_neg Int64.eqm_sub Int64.eqm_mult
+  Int64.eqm_unsigned_repr Int64.eqm_unsigned_repr_l Int64.eqm_unsigned_repr_r
+  Int64.unsigned_range Int64.unsigned_range_2
+  Int64.repr_unsigned Int64.repr_signed Int64.unsigned_repr : ints.
+
+Hint Resolve Ptrofs.modulus_pos Ptrofs.eqm_refl Ptrofs.eqm_refl2 Ptrofs.eqm_sym Ptrofs.eqm_trans
+  Ptrofs.eqm_small_eq Ptrofs.eqm_add Ptrofs.eqm_neg Ptrofs.eqm_sub Ptrofs.eqm_mult
+  Ptrofs.eqm_unsigned_repr Ptrofs.eqm_unsigned_repr_l Ptrofs.eqm_unsigned_repr_r
+  Ptrofs.unsigned_range Ptrofs.unsigned_range_2
+  Ptrofs.repr_unsigned Ptrofs.repr_signed Ptrofs.unsigned_repr : ints.
+