From a82c9c0e4a0b8e37c9c3ea5ae99714982563606f Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 14 Jan 2012 14:23:26 +0000 Subject: Merge of the nonstrict-ops branch: - Most RTL operators now evaluate to Some Vundef instead of None when undefined behavior occurs. - More aggressive instruction selection. - "Bertotization" of pattern-matchings now implemented by a proper preprocessor. - Cast optimization moved to cfrontend/Cminorgen; removed backend/CastOptim. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1790 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Integers.v | 147 +++++++++++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 127 insertions(+), 20 deletions(-) (limited to 'lib') diff --git a/lib/Integers.v b/lib/Integers.v index 75bc63d..9f58de3 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -243,15 +243,6 @@ Definition shr (x y: int): int := let sx := fun i => fx (if zlt i (Z_of_nat wordsize) then i else Z_of_nat wordsize - 1) in repr (Z_of_bits wordsize sx (unsigned y)). -(** Viewed as signed divisions by powers of two, [shrx] rounds towards - zero, while [shr] rounds towards minus infinity. *) - -Definition shrx (x y: int): int := - divs x (shl one y). - -Definition shr_carry (x y: int) := - sub (shrx x y) (shr x y). - Definition rol (x y: int) : int := let fx := bits_of_Z wordsize (unsigned x) in let rx := fun i => fx (Zmod i (Z_of_nat wordsize)) in @@ -264,6 +255,17 @@ Definition ror (x y: int) : int := Definition rolm (x a m: int): int := and (rol x a) m. +(** Viewed as signed divisions by powers of two, [shrx] rounds towards + zero, while [shr] rounds towards minus infinity. *) + +Definition shrx (x y: int): int := + divs x (shl one y). + +(** [shr_carry x y] is 1 if [x] is negative and at least one 1 bit is shifted away. *) + +Definition shr_carry (x y: int) := + if lt x zero && negb (eq (and x (sub (shl one y) one)) zero) then one else zero. + (** Zero and sign extensions *) Definition zero_ext (n: Z) (x: int) : int := @@ -1789,6 +1791,34 @@ Proof. apply two_p_m1_range. omega. Qed. +Theorem and_shr_shru: + forall x y z, + and (shr x z) (shru y z) = shru (and x y) z. +Proof. + intros. unfold and, shr, shru, bitwise_binop. + repeat rewrite unsigned_repr; auto with ints. + decEq; apply Z_of_bits_exten; intros. + repeat rewrite Zplus_0_r. + rewrite bits_of_Z_of_bits_gen; auto. + rewrite bits_of_Z_of_bits_gen; auto. + generalize (unsigned_range z); intros. + destruct (zlt (i + unsigned z) (Z_of_nat wordsize)). + rewrite bits_of_Z_of_bits_gen. + repeat rewrite Zplus_0_r. auto. omega. + set (b := bits_of_Z wordsize (unsigned x) (Z_of_nat wordsize - 1)). + repeat rewrite bits_of_Z_above; auto. apply andb_false_r. +Qed. + +Theorem shr_and_shru_and: + forall x y z, + shru (shl z y) y = z -> + and (shr x y) z = and (shru x y) z. +Proof. + intros. + rewrite <- H. + rewrite and_shru. rewrite and_shr_shru. auto. +Qed. + (** ** Properties of rotations *) Theorem shl_rolm: @@ -2404,15 +2434,6 @@ Qed. (** ** Properties of [shrx] (signed division by a power of 2) *) -Theorem shrx_carry: - forall x y, - add (shr x y) (shr_carry x y) = shrx x y. -Proof. - intros. unfold shr_carry. - rewrite sub_add_opp. rewrite add_permut. - rewrite add_neg_zero. apply add_zero. -Qed. - Lemma Zdiv_round_Zdiv: forall x y, y > 0 -> @@ -2436,8 +2457,7 @@ Qed. Theorem shrx_shr: forall x y, ltu y (repr (Z_of_nat wordsize - 1)) = true -> - shrx x y = - shr (if lt x zero then add x (sub (shl one y) one) else x) y. + shrx x y = shr (if lt x zero then add x (sub (shl one y) one) else x) y. Proof. intros. rewrite shr_div_two_p. unfold shrx. unfold divs. exploit ltu_inv; eauto. rewrite unsigned_repr. @@ -2474,6 +2494,69 @@ Proof. generalize wordsize_pos wordsize_max_unsigned; omega. 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. +Proof. + intros. generalize (Z_div_mod_eq x y H). generalize (Z_mod_lt x y H). + set (q := x / y). set (r := x mod y). intros. + destruct (zeq r 0). + apply Zdiv_unique with (y - 1). rewrite H1. rewrite e. ring. omega. + apply Zdiv_unique with (r - 1). rewrite H1. ring. omega. +Qed. + +Theorem shrx_carry: + forall x y, + ltu y (repr (Z_of_nat wordsize - 1)) = true -> + shrx x y = add (shr x y) (shr_carry x y). +Proof. + intros. rewrite shrx_shr; auto. unfold shr_carry. + unfold lt. set (sx := signed x). rewrite signed_zero. + destruct (zlt sx 0); simpl. + 2: rewrite add_zero; auto. + set (uy := unsigned y). + assert (0 <= uy < Z_of_nat wordsize - 1). + exploit ltu_inv; eauto. rewrite unsigned_repr. auto. + generalize wordsize_pos wordsize_max_unsigned; omega. + assert (shl one y = repr (two_p uy)). + rewrite shl_mul_two_p. rewrite mul_commut. apply mul_one. + assert (and x (sub (shl one y) one) = modu x (repr (two_p uy))). + symmetry. rewrite H1. apply modu_and with (logn := y). + rewrite is_power2_two_p. unfold uy. rewrite repr_unsigned. auto. + omega. + rewrite H2. rewrite H1. + repeat rewrite shr_div_two_p. fold sx. fold uy. + assert (two_p uy > 0). apply two_p_gt_ZERO. omega. + assert (two_p uy < modulus). + rewrite modulus_power. apply two_p_monotone_strict. omega. + assert (two_p uy < half_modulus). + rewrite half_modulus_power. + apply two_p_monotone_strict. auto. + assert (two_p uy < modulus). + rewrite modulus_power. apply two_p_monotone_strict. omega. + assert (sub (repr (two_p uy)) one = repr (two_p uy - 1)). + unfold sub. apply eqm_samerepr. apply eqm_sub. apply eqm_sym; apply eqm_unsigned_repr. + rewrite unsigned_one. apply eqm_refl. + rewrite H7. rewrite add_signed. fold sx. + rewrite (signed_repr (two_p uy - 1)). rewrite signed_repr. + unfold modu. rewrite unsigned_repr. + unfold eq. rewrite unsigned_zero. rewrite unsigned_repr. + assert (unsigned x mod two_p uy = sx mod two_p uy). + apply eqmod_mod_eq; auto. apply eqmod_divides with modulus. + fold eqm. unfold sx. apply eqm_sym. apply eqm_signed_unsigned. + unfold modulus. rewrite two_power_nat_two_p. + exists (two_p (Z_of_nat wordsize - uy)). rewrite <- two_p_is_exp. + decEq. omega. omega. omega. + rewrite H8. rewrite Zdiv_shift; auto. + unfold add. apply eqm_samerepr. apply eqm_add. + apply eqm_unsigned_repr. + destruct (zeq (sx mod two_p uy) 0); simpl; apply eqmod_mod; apply modulus_pos. + generalize (Z_mod_lt (unsigned x) (two_p uy) H3). unfold max_unsigned. omega. + unfold max_unsigned; omega. + generalize (signed_range x). fold sx. intros. split. omega. unfold max_signed. omega. + generalize min_signed_neg. unfold max_signed. omega. +Qed. + (** ** Properties of integer zero extension and sign extension. *) Section EXTENSIONS. @@ -2740,6 +2823,30 @@ Proof. rewrite bits_of_Z_of_bits. apply zlt_false. omega. omega. Qed. +Theorem zero_ext_narrow: + forall x n n', + 0 < n < Z_of_nat wordsize -> n <= n' < Z_of_nat wordsize -> + zero_ext n (zero_ext n' x) = zero_ext n x. +Proof. + intros. unfold zero_ext. + repeat rewrite unsigned_repr; auto with ints. + decEq; apply Z_of_bits_exten; intros; rewrite Zplus_0_r. + destruct (zlt i n); auto. + rewrite bits_of_Z_of_bits; auto. apply zlt_true. omega. +Qed. + +Theorem zero_sign_ext_narrow: + forall x n n', + 0 < n < Z_of_nat wordsize -> n <= n' < Z_of_nat wordsize -> + zero_ext n (sign_ext n' x) = zero_ext n x. +Proof. + intros. unfold sign_ext, zero_ext. + repeat rewrite unsigned_repr; auto with ints. + decEq; apply Z_of_bits_exten; intros; rewrite Zplus_0_r. + destruct (zlt i n); auto. + rewrite bits_of_Z_of_bits; auto. apply zlt_true. omega. +Qed. + (** ** Properties of [one_bits] (decomposition in sum of powers of two) *) Theorem one_bits_range: -- cgit v1.2.3