Reserve register GPR13 for compatibility with EABI. Optimize operations 'x >= 0' and 'x < 0'.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@999 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 20 insertions, 0 deletions

diff --git a/lib/Integers.v b/lib/Integers.v
index ff29d2a..ceda851 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -2545,4 +2545,24 @@ Proof.
   contradiction. auto.
 Qed.
 
+Theorem shru_lt_zero:
+  forall x,
+  shru x (repr (Z_of_nat wordsize - 1)) = if lt x zero then one else zero.
+Proof.
+  intros. rewrite shru_div_two_p. 
+  change (two_p (unsigned (repr (Z_of_nat wordsize - 1))))
+    with half_modulus.
+  generalize (unsigned_range x); intro. 
+  unfold lt. change (signed zero) with 0. unfold signed. 
+  destruct (zlt (unsigned x) half_modulus).
+  rewrite zlt_false.
+  replace (unsigned x / half_modulus) with 0. reflexivity. 
+  symmetry. apply Zdiv_unique with (unsigned x). ring. omega. omega.
+  rewrite zlt_true. 
+  replace (unsigned x / half_modulus) with 1. reflexivity.
+  symmetry. apply Zdiv_unique with (unsigned x - half_modulus). ring. 
+  replace modulus with (2 * half_modulus) in H. omega. reflexivity. 
+  omega. 
+Qed.
+
 End Int.