From a745efa7f07a10cec625b9c302eb0196b7bfaefb Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 26 Feb 2009 14:48:59 +0000 Subject: 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 --- lib/Integers.v | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) (limited to 'lib') 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. -- cgit v1.2.3