diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-02-26 14:48:59 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-02-26 14:48:59 +0000 |
commit | a745efa7f07a10cec625b9c302eb0196b7bfaefb (patch) | |
tree | af32acc8865cf704b63bd27b8eb21da6b29d83b6 /lib/Integers.v | |
parent | 26fcc4dbd92f367ecb20f4457cdf887eea0b6568 (diff) | |
download | compcert-a745efa7f07a10cec625b9c302eb0196b7bfaefb.tar.gz compcert-a745efa7f07a10cec625b9c302eb0196b7bfaefb.zip |
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
Diffstat (limited to 'lib/Integers.v')
-rw-r--r-- | lib/Integers.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/lib/Integers.v b/lib/Integers.v index ff29d2a5..ceda8512 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. |