Hybrid 64bit/32bit PowerPC port

This commit adds code generation for 64bit PowerPC architectures which execute
32bit applications.

The main difference to the normal 32bit PowerPC port is that it uses the
available 64bit instructions instead of using the runtime library functions.
However pointers are still 32bit and the 32bit calling convention is used.

In order to use this port the target architecture must be either in Server
execution mode or if in Embedded execution mode the high order 32 bits of GPRs
must be implemented in 32-bit mode. Furthermore the operating system must
preserve the high order 32 bits of GPRs.

1 files changed, 134 insertions, 43 deletions

diff --git a/lib/Integers.v b/lib/Integers.v
index b1fa982d..c44fa55f 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -1224,9 +1224,9 @@ Proof.
   { unfold Q, R, Z.div, Z.modulo. destruct (Z.div_eucl N D); auto. }
   rewrite E2. rewrite zle_true. auto.
   assert (unsigned d <> 0).
-  { red; intros. elim H. rewrite <- (repr_unsigned d). rewrite H0; auto. }   
+  { red; intros. elim H. rewrite <- (repr_unsigned d). rewrite H0; auto. }
   assert (0 < D).
-  { unfold D. generalize (unsigned_range d); intros. omega. } 
+  { unfold D. generalize (unsigned_range d); intros. omega. }
   assert (0 <= Q <= max_unsigned).
   { unfold Q. apply Zdiv_interval_2.
     rewrite <- E1; apply unsigned_range_2.
@@ -1262,7 +1262,7 @@ Proof.
   set (Q := Z.quot N D); set (R := Z.rem N D).
   assert (E2: Z.quotrem N D = (Q, R)).
   { unfold Q, R, Z.quot, Z.rem. destruct (Z.quotrem N D); auto. }
-  rewrite E2. 
+  rewrite E2.
   assert (min_signed <= N <= max_signed) by (rewrite H2; apply signed_range).
   assert (min_signed <= Q <= max_signed).
   { unfold Q. destruct (zeq D 1); [ | destruct (zeq D (-1))].
@@ -1284,7 +1284,7 @@ Proof.
       rewrite Z.mul_1_r. unfold min_signed, max_signed in H3; xomega.
       apply Zmult_lt_compat_l. generalize half_modulus_pos; omega. xomega. }
     rewrite Z.abs_lt in H4.
-    unfold min_signed, max_signed; omega. 
+    unfold min_signed, max_signed; omega.
   }
   unfold proj_sumbool; rewrite ! zle_true by omega; simpl.
   unfold Q, R; rewrite H2; auto.
@@ -2186,6 +2186,16 @@ Proof.
     + omega.
 Qed.
 
+Theorem sub_ltu:
+  forall x y,
+    ltu x y = true ->
+    0 <= unsigned y - unsigned x <= unsigned y.
+Proof.
+  intros.
+  generalize (ltu_inv x y H). intros .
+  split. omega. omega.
+Qed.
+
 Theorem shru_zero: forall x, shru x zero = x.
 Proof.
   bit_solve. rewrite unsigned_zero. rewrite zlt_true. f_equal; omega. omega.
@@ -4036,8 +4046,13 @@ Definition shru' (x: int) (y: Int.int): int :=
   repr (Z.shiftr (unsigned x) (Int.unsigned y)).
 Definition shr' (x: int) (y: Int.int): int :=
   repr (Z.shiftr (signed x) (Int.unsigned y)).
+Definition rol' (x: int) (y: Int.int): int :=
+  rol x (repr (Int.unsigned y)).
 Definition shrx' (x: int) (y: Int.int): int :=
   divs x (shl' one y).
+Definition shr_carry' (x: int) (y: Int.int): int :=
+  if lt x zero && negb (eq (and x (sub (shl' one y) one)) zero)
+  then one else zero.
 
 Lemma bits_shl':
   forall x y i,
@@ -4082,7 +4097,7 @@ Lemma shl'_mul_two_p:
   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. 
+  rewrite Zshiftl_mul_two_p. apply eqm_mult. apply eqm_refl. apply eqm_unsigned_repr.
   generalize (Int.unsigned_range y); omega.
 Qed.
 
@@ -4099,11 +4114,50 @@ Proof.
   intros. rewrite shl'_one_two_p. apply shl'_mul_two_p.
 Qed.
 
+Theorem shl'_zero:
+  forall x, shl' x Int.zero = x.
+Proof.
+  intros. unfold shl'. rewrite Int.unsigned_zero. unfold Z.shiftl.
+  apply repr_unsigned.
+Qed.
+
+Theorem shru'_zero :
+  forall x, shru' x Int.zero = x.
+Proof.
+  intros. unfold shru'. rewrite Int.unsigned_zero. unfold Z.shiftr.
+  apply repr_unsigned.
+Qed.
+
+Theorem shr'_zero :
+  forall x, shr' x Int.zero = x.
+Proof.
+  intros. unfold shr'. rewrite Int.unsigned_zero. unfold Z.shiftr.
+  apply repr_signed.
+Qed.
+
 Theorem shrx'_zero:
   forall x, shrx' x Int.zero = x.
 Proof.
-  intros. change (shrx' x Int.zero) with (shrx x zero). apply shrx_zero. compute; auto. 
-Qed. 
+  intros. change (shrx' x Int.zero) with (shrx x zero). apply shrx_zero. compute; auto.
+Qed.
+
+Theorem shrx'_carry:
+  forall x y,
+  Int.ltu y (Int.repr 63) = true ->
+  shrx' x y = add (shr' x y) (shr_carry' x y).
+Proof.
+  intros. apply Int.ltu_inv in H. change (Int.unsigned (Int.repr 63)) with 63 in H.
+  set (y1 := Int64.repr (Int.unsigned y)).
+  assert (U: unsigned y1 = Int.unsigned y).
+  { apply unsigned_repr. assert (63 < max_unsigned) by reflexivity. omega. }
+  transitivity (shrx x y1).
+- unfold shrx', shrx, shl', shl. rewrite U; auto.
+- rewrite shrx_carry. 
++ f_equal. 
+  unfold shr, shr'. rewrite U; auto.
+  unfold shr_carry, shr_carry', shl, shl'. rewrite U; auto.
++ unfold ltu. apply zlt_true. rewrite U; tauto. 
+Qed.
 
 Theorem shrx'_shr_2:
   forall x y,
@@ -4119,7 +4173,7 @@ Proof.
   { unfold z; apply unsigned_repr; omega. }
   assert (B: unsigned (sub (repr 64) z) = Int.unsigned (Int.sub (Int.repr 64) y)).
   { unfold z. unfold sub, Int.sub.
-    change (unsigned (repr 64)) with 64.  
+    change (unsigned (repr 64)) with 64.
     change (Int.unsigned (Int.repr 64)) with 64.
     rewrite (unsigned_repr (Int.unsigned y)) by omega.
     rewrite unsigned_repr, Int.unsigned_repr by omega.
@@ -4172,7 +4226,7 @@ Proof.
   replace (shl' x y) with (shl x (repr (Int.unsigned y))).
   replace (shru' x z) with (shru x (repr (Int.unsigned z))).
   apply or_ror; auto. rewrite F, H1. reflexivity.
-  unfold shru, shru'; rewrite <- B; auto. 
+  unfold shru, shru'; rewrite <- B; auto.
   unfold shl, shl'; rewrite <- A; auto.
 Qed.
 
@@ -4190,7 +4244,7 @@ Proof.
   replace (shl' x y) with (shl x y').
   replace (shl' (shl x y') z) with (shl (shl x y') z').
   replace (shl' x (Int.add y z)) with (shl x (add y' z')).
-  apply shl_shl; auto. apply zlt_true. rewrite <- E. 
+  apply shl_shl; auto. apply zlt_true. rewrite <- E.
   change (unsigned iwordsize) with zwordsize. tauto.
   unfold shl, shl'. rewrite E; auto.
   unfold shl at 1, shl'. rewrite <- B; auto.
@@ -4211,7 +4265,7 @@ Proof.
   replace (shru' x y) with (shru x y').
   replace (shru' (shru x y') z) with (shru (shru x y') z').
   replace (shru' x (Int.add y z)) with (shru x (add y' z')).
-  apply shru_shru; auto. apply zlt_true. rewrite <- E. 
+  apply shru_shru; auto. apply zlt_true. rewrite <- E.
   change (unsigned iwordsize) with zwordsize. tauto.
   unfold shru, shru'. rewrite E; auto.
   unfold shru at 1, shru'. rewrite <- B; auto.
@@ -4232,7 +4286,7 @@ Proof.
   replace (shr' x y) with (shr x y').
   replace (shr' (shr x y') z) with (shr (shr x y') z').
   replace (shr' x (Int.add y z)) with (shr x (add y' z')).
-  apply shr_shr; auto. apply zlt_true. rewrite <- E. 
+  apply shr_shr; auto. apply zlt_true. rewrite <- E.
   change (unsigned iwordsize) with zwordsize. tauto.
   unfold shr, shr'. rewrite E; auto.
   unfold shr at 1, shr'. rewrite <- B; auto.
@@ -4256,8 +4310,8 @@ 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. 
+  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.
 
@@ -4276,13 +4330,13 @@ Proof.
   { 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.  
+  + 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. 
+  + apply eqm_sym; apply eqm_unsigned_repr.
   }
-  intros. rewrite <- (repr_unsigned x) at 1. unfold one_bits'. rewrite REC. 
+  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.    
+  apply Z_one_bits_range.
 Qed.
 
 Lemma is_power2'_rng:
@@ -4290,7 +4344,7 @@ Lemma is_power2'_rng:
   is_power2' n = Some logn ->
   0 <= Int.unsigned logn < zwordsize.
 Proof.
-  unfold is_power2'; intros n logn P2. 
+  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. }
@@ -4303,7 +4357,7 @@ 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. 
+  intros. unfold Int.ltu. change (Int.unsigned iwordsize') with zwordsize.
   apply zlt_true. generalize (is_power2'_rng _ _ H). tauto.
 Qed.
 
@@ -4321,13 +4375,13 @@ Proof.
   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. 
+  intros. rewrite shl'_mul. f_equal. rewrite shl'_one_two_p.
   rewrite <- (repr_unsigned n). f_equal. apply is_power2'_correct; auto.
 Qed.
 
@@ -4855,6 +4909,43 @@ Proof.
   rewrite zlt_true by omega; auto.
 Qed.
 
+(** Utility proofs for mixed 32bit and 64bit arithmetic *)
+
+Remark int_unsigned_range:
+  forall x, 0 <= Int.unsigned x <= max_unsigned.
+Proof.
+  intros.
+  unfold max_unsigned. unfold modulus.
+  generalize (Int.unsigned_range x).
+  unfold Int.modulus in *.
+  change (wordsize) with  64%nat in *.
+  change (Int.wordsize) with 32%nat in *.
+  unfold two_power_nat. simpl.
+  omega.
+Qed.
+
+Remark int_unsigned_repr:
+  forall x, unsigned (repr (Int.unsigned x)) = Int.unsigned x.
+Proof.
+  intros. rewrite unsigned_repr. auto.
+  apply int_unsigned_range.
+Qed.
+
+Lemma int_sub_ltu:
+  forall x y,
+    Int.ltu x y= true ->
+    Int.unsigned (Int.sub y x) = unsigned (sub (repr (Int.unsigned y)) (repr (Int.unsigned x))).
+Proof.
+  intros. generalize (Int.sub_ltu x y H). intros. unfold Int.sub. unfold sub.
+  rewrite Int.unsigned_repr. rewrite unsigned_repr.
+  rewrite unsigned_repr by apply int_unsigned_range. rewrite int_unsigned_repr. reflexivity.
+  rewrite unsigned_repr by apply int_unsigned_range.
+  rewrite int_unsigned_repr. generalize (int_unsigned_range y).
+  omega.
+  generalize (Int.sub_ltu x y H). intros.
+  generalize (Int.unsigned_range_2 y). intros. omega.
+Qed.
+
 End Int64.
 
 Strategy 0 [Wordsize_64.wordsize].
@@ -4899,7 +4990,7 @@ Hypothesis _32: Archi.ptr64 = false.
 
 Lemma modulus_eq32: modulus = Int.modulus.
 Proof.
-  unfold modulus, wordsize. 
+  unfold modulus, wordsize.
   change Wordsize_Ptrofs.wordsize with (if Archi.ptr64 then 64%nat else 32%nat).
   rewrite _32. reflexivity.
 Qed.
@@ -4923,8 +5014,8 @@ 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. 
+  unfold agree32; intros. unfold signed, Int.signed, half_modulus, Int.half_modulus.
+  rewrite modulus_eq32. rewrite H. auto.
 Qed.
 
 Lemma agree32_of_int:
@@ -4932,7 +5023,7 @@ Lemma agree32_of_int:
 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.
@@ -4942,7 +5033,7 @@ 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. 
+  unfold agree32, of_int; intros. rewrite <- H. apply repr_unsigned.
 Qed.
 
 Lemma agree32_of_ints_eq:
@@ -4954,7 +5045,7 @@ Qed.
 Lemma agree32_to_int:
   forall a, agree32 a (to_int a).
 Proof.
-  unfold agree32, to_int; intros. rewrite <- (agree32_repr (unsigned a)). 
+  unfold agree32, to_int; intros. rewrite <- (agree32_repr (unsigned a)).
   rewrite repr_unsigned; auto.
 Qed.
 
@@ -4974,21 +5065,21 @@ 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. 
+  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. 
+  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. 
+  unfold agree32, Ptrofs.mul, Int.mul; intros. rewrite H, H0. apply agree32_repr.
 Qed.
 
 Lemma agree32_divs:
@@ -5004,7 +5095,7 @@ Lemma of_int_to_int:
 Proof.
   intros; unfold of_int, to_int. apply eqm_repr_eq. rewrite <- eqm32.
   apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
-Qed.   
+Qed.
 
 End AGREE32.
 
@@ -5014,7 +5105,7 @@ Hypothesis _64: Archi.ptr64 = true.
 
 Lemma modulus_eq64: modulus = Int64.modulus.
 Proof.
-  unfold modulus, wordsize. 
+  unfold modulus, wordsize.
   change Wordsize_Ptrofs.wordsize with (if Archi.ptr64 then 64%nat else 32%nat).
   rewrite _64. reflexivity.
 Qed.
@@ -5038,8 +5129,8 @@ 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. 
+  unfold agree64; intros. unfold signed, Int64.signed, half_modulus, Int64.half_modulus.
+  rewrite modulus_eq64. rewrite H. auto.
 Qed.
 
 Lemma agree64_of_int:
@@ -5051,13 +5142,13 @@ 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. 
+  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)). 
+  unfold agree64, to_int64; intros. rewrite <- (agree64_repr (unsigned a)).
   rewrite repr_unsigned; auto.
 Qed.
 
@@ -5077,21 +5168,21 @@ 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. 
+  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. 
+  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. 
+  unfold agree64, Ptrofs.mul, Int.mul; intros. rewrite H, H0. apply agree64_repr.
 Qed.
 
 Lemma agree64_divs:
@@ -5107,16 +5198,16 @@ Lemma of_int64_to_int64:
 Proof.
   intros; unfold of_int64, to_int64. apply eqm_repr_eq. rewrite <- eqm64.
   apply Int64.eqm_sym; apply Int64.eqm_unsigned_repr.
-Qed.   
+Qed.
 
 End AGREE64.
 
-Hint Resolve 
+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].