diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-06-28 11:23:52 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-06-28 11:23:52 +0000 |
commit | 7a614ea53948423b0266eefd98ea5714559c3cfc (patch) | |
tree | b590210c9db8a450bd16cece9311ca47f68d0b89 /lib/Integers.v | |
parent | 5312915c1b29929f82e1f8de80609a277584913f (diff) | |
download | compcert-kvx-7a614ea53948423b0266eefd98ea5714559c3cfc.tar.gz compcert-kvx-7a614ea53948423b0266eefd98ea5714559c3cfc.zip |
Changelog: updated
driver/Interp.ml: clean up dead code
lib/Integers.v: add shifted_or_is_add
lib/Floats.v: add from_words_eq
.depend: updated
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1940 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib/Integers.v')
-rw-r--r-- | lib/Integers.v | 40 |
1 files changed, 40 insertions, 0 deletions
diff --git a/lib/Integers.v b/lib/Integers.v index 0dc79979..8dc5b6f5 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -1224,6 +1224,24 @@ Proof. rewrite inj_S in H. omega. rewrite inj_S in H. omega. Qed. +Lemma bits_of_Z_greater: + forall n x i, + 0 <= x < two_p i -> bits_of_Z n x i = false. +Proof. + induction n; intros. + auto. + destruct (zlt i 0). apply bits_of_Z_below. auto. + simpl. + destruct (Z_bin_decomp x) as [b x1]_eqn. + destruct (zeq i 0). + subst i. simpl in H. assert (x = 0) by omega. subst x. simpl in Heqp. congruence. + apply IHn. + rewrite <- (Z_shift_add_bin_decomp x) in H. rewrite Heqp in H. simpl in H. + replace i with (Zsucc (i-1)) in H by omega. rewrite two_p_S in H. + unfold Z_shift_add in H. destruct b; omega. + omega. +Qed. + Lemma bits_of_Z_of_bits_gen': forall n f i j, bits_of_Z n (Z_of_bits n f j) i = @@ -2283,6 +2301,28 @@ Proof. auto. Qed. +Theorem shifted_or_is_add: + forall x y n, + 0 <= n < Z_of_nat wordsize -> + unsigned y < two_p n -> + or (shl x (repr n)) y = repr(unsigned x * two_p n + unsigned y). +Proof. + intros. rewrite <- add_is_or. + rewrite shl_mul_two_p. rewrite unsigned_repr. + unfold add. apply eqm_samerepr. unfold mul. auto with ints. + generalize wordsize_max_unsigned; omega. + unfold and, shl, bitwise_binop. unfold zero. decEq. apply Z_of_bits_false. intros. + rewrite unsigned_repr; auto with ints. rewrite bits_of_Z_of_bits_gen. + rewrite unsigned_repr. apply andb_false_iff. + destruct (zlt j n). + left. apply bits_of_Z_below. omega. + right. apply bits_of_Z_greater. + split. generalize (unsigned_range y); omega. + assert (two_p n <= two_p j). apply two_p_monotone. omega. omega. + generalize wordsize_max_unsigned; omega. + omega. +Qed. + (** Unsigned right shifts and unsigned divisions by powers of 2. *) Lemma Z_of_bits_shift_right: |