From 4bf8b331372388dc9cb39154c986c918df9e071c Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 28 Jul 2013 08:45:56 +0000 Subject: Add another expansion of shrx in terms of shifts and adds (from Hacker's Delight). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2299 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Integers.v | 114 ++++++++++++++++++++++++++++++++++++--------------------- 1 file changed, 72 insertions(+), 42 deletions(-) (limited to 'lib') diff --git a/lib/Integers.v b/lib/Integers.v index 88a9683..23f2294 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -2209,6 +2209,48 @@ Proof. rewrite and_shru. rewrite and_shr_shru. auto. Qed. +Theorem shru_lt_zero: + forall x, + shru x (repr (zwordsize - 1)) = if lt x zero then one else zero. +Proof. + intros. apply same_bits_eq; intros. + rewrite bits_shru; auto. + rewrite unsigned_repr. + destruct (zeq i 0). + subst i. rewrite Zplus_0_l. rewrite zlt_true. + rewrite sign_bit_of_unsigned. + unfold lt. rewrite signed_zero. unfold signed. + destruct (zlt (unsigned x) half_modulus). + rewrite zlt_false. auto. generalize (unsigned_range x); omega. + rewrite zlt_true. unfold one; rewrite testbit_repr; auto. + generalize (unsigned_range x); omega. + omega. + rewrite zlt_false. + unfold testbit. rewrite Ztestbit_eq. rewrite zeq_false. + destruct (lt x zero). + rewrite unsigned_one. simpl Z.div2. rewrite Z.testbit_0_l; auto. + rewrite unsigned_zero. simpl Z.div2. rewrite Z.testbit_0_l; auto. + auto. omega. omega. + generalize wordsize_max_unsigned; omega. +Qed. + +Theorem shr_lt_zero: + forall x, + shr x (repr (zwordsize - 1)) = if lt x zero then mone else zero. +Proof. + intros. apply same_bits_eq; intros. + rewrite bits_shr; auto. + rewrite unsigned_repr. + transitivity (testbit x (zwordsize - 1)). + f_equal. destruct (zlt (i + (zwordsize - 1)) zwordsize); omega. + rewrite sign_bit_of_unsigned. + unfold lt. rewrite signed_zero. unfold signed. + destruct (zlt (unsigned x) half_modulus). + rewrite zlt_false. rewrite bits_zero; auto. generalize (unsigned_range x); omega. + rewrite zlt_true. rewrite bits_mone; auto. generalize (unsigned_range x); omega. + generalize wordsize_max_unsigned; omega. +Qed. + (** ** Properties of rotations *) Lemma bits_rol: @@ -2815,6 +2857,36 @@ Proof. assert (two_p uy - 1 <= max_signed). unfold max_signed. omega. omega. Qed. +Theorem shrx_shr_2: + forall x y, + ltu y (repr (zwordsize - 1)) = true -> + shrx x y = shr (add x (shru (shr x (repr (zwordsize - 1))) (sub iwordsize y))) y. +Proof. + intros. + rewrite shrx_shr by auto. f_equal. + rewrite shr_lt_zero. destruct (lt x zero). +- set (uy := unsigned y). + generalize (unsigned_range y); fold uy; intros. + assert (0 <= uy < zwordsize - 1). + exploit ltu_inv; eauto. rewrite unsigned_repr. auto. + generalize wordsize_pos wordsize_max_unsigned; omega. + assert (two_p uy < modulus). + rewrite modulus_power. apply two_p_monotone_strict. omega. + f_equal. rewrite shl_mul_two_p. fold uy. rewrite mul_commut. rewrite mul_one. + unfold sub. rewrite unsigned_one. rewrite unsigned_repr. + rewrite unsigned_repr_wordsize. fold uy. + apply same_bits_eq; intros. rewrite bits_shru by auto. + rewrite testbit_repr by auto. rewrite Ztestbit_two_p_m1 by omega. + rewrite unsigned_repr by (generalize wordsize_max_unsigned; omega). + destruct (zlt i uy). + rewrite zlt_true by omega. rewrite bits_mone by omega. auto. + rewrite zlt_false by omega. auto. + assert (two_p uy > 0) by (apply two_p_gt_ZERO; omega). unfold max_unsigned; omega. +- replace (shru zero (sub iwordsize y)) with zero. + rewrite add_zero; auto. + bit_solve. destruct (zlt (i + unsigned (sub iwordsize y)) zwordsize); auto. +Qed. + Lemma Zdiv_shift: forall x y, y > 0 -> (x + (y - 1)) / y = x / y + if zeq (Zmod x y) 0 then 0 else 1. @@ -3414,48 +3486,6 @@ Proof. contradiction. auto. Qed. -Theorem shru_lt_zero: - forall x, - shru x (repr (zwordsize - 1)) = if lt x zero then one else zero. -Proof. - intros. apply same_bits_eq; intros. - rewrite bits_shru; auto. - rewrite unsigned_repr. - destruct (zeq i 0). - subst i. rewrite Zplus_0_l. rewrite zlt_true. - rewrite sign_bit_of_unsigned. - unfold lt. rewrite signed_zero. unfold signed. - destruct (zlt (unsigned x) half_modulus). - rewrite zlt_false. auto. generalize (unsigned_range x); omega. - rewrite zlt_true. unfold one; rewrite testbit_repr; auto. - generalize (unsigned_range x); omega. - omega. - rewrite zlt_false. - unfold testbit. rewrite Ztestbit_eq. rewrite zeq_false. - destruct (lt x zero). - rewrite unsigned_one. simpl Z.div2. rewrite Z.testbit_0_l; auto. - rewrite unsigned_zero. simpl Z.div2. rewrite Z.testbit_0_l; auto. - auto. omega. omega. - generalize wordsize_max_unsigned; omega. -Qed. - -Theorem shr_lt_zero: - forall x, - shr x (repr (zwordsize - 1)) = if lt x zero then mone else zero. -Proof. - intros. apply same_bits_eq; intros. - rewrite bits_shr; auto. - rewrite unsigned_repr. - transitivity (testbit x (zwordsize - 1)). - f_equal. destruct (zlt (i + (zwordsize - 1)) zwordsize); omega. - rewrite sign_bit_of_unsigned. - unfold lt. rewrite signed_zero. unfold signed. - destruct (zlt (unsigned x) half_modulus). - rewrite zlt_false. rewrite bits_zero; auto. generalize (unsigned_range x); omega. - rewrite zlt_true. rewrite bits_mone; auto. generalize (unsigned_range x); omega. - generalize wordsize_max_unsigned; omega. -Qed. - Theorem ltu_range_test: forall x y, ltu x y = true -> unsigned y <= max_signed -> -- cgit v1.2.3