From abe2bb5c40260a31ce5ee27b841bcbd647ff8b88 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 9 Apr 2011 16:59:13 +0000 Subject: Merge of branch "unsigned-offsets": - In pointer values "Vptr b ofs", interpret "ofs" as an unsigned int. (Fixes issue with wrong comparison of pointers across 0x8000_0000) - Revised Stacking pass to not use negative SP offsets. - Add pointer validity checks to Cminor ... Mach to support the use of memory injections in Stacking. - Cleaned up Stacklayout modules. - IA32: improved code generation for Mgetparam. - ARM: improved code generation for op-immediate instructions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1632 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Integers.v | 162 +++++++++++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 139 insertions(+), 23 deletions(-) (limited to 'lib') diff --git a/lib/Integers.v b/lib/Integers.v index 1087728..4ed1396 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -1287,29 +1287,6 @@ Proof. intros. apply (bitwise_binop_idem andb). destruct a; auto. Qed. -Theorem add_and: - forall x y z, - and y z = zero -> - add (and x y) (and x z) = and x (or y z). -Proof. - intros. unfold add, and, bitwise_binop. - repeat rewrite unsigned_repr; auto with ints. decEq. - apply Z_of_bits_excl; intros. - assert (forall a b c, a && b && (a && c) = a && (b && c)). - destruct a; destruct b; destruct c; reflexivity. - rewrite H1. - replace (bits_of_Z wordsize (unsigned y) i && - bits_of_Z wordsize (unsigned z) i) - with (bits_of_Z wordsize (unsigned (and y z)) i). - rewrite H. rewrite unsigned_zero. - rewrite bits_of_Z_zero. apply andb_b_false. - unfold and, bitwise_binop. rewrite unsigned_repr; auto with ints. - rewrite bits_of_Z_of_bits. reflexivity. auto. - rewrite <- demorgan1. - unfold or, bitwise_binop. rewrite unsigned_repr; auto with ints. - rewrite bits_of_Z_of_bits; auto. -Qed. - Theorem or_commut: forall x y, or x y = or y x. Proof (bitwise_binop_commut orb orb_comm). @@ -1393,12 +1370,129 @@ Proof. auto. Qed. +(** Properties of bitwise complement.*) + Theorem not_involutive: forall (x: int), not (not x) = x. Proof. intros. unfold not. rewrite xor_assoc. rewrite xor_idem. apply xor_zero. Qed. +Theorem not_zero: + not zero = mone. +Proof. + unfold not. rewrite xor_commut. apply xor_zero. +Qed. + +Theorem not_mone: + not mone = zero. +Proof. + rewrite <- (not_involutive zero). symmetry. decEq. apply not_zero. +Qed. + +Theorem not_or_and_not: + forall x y, not (or x y) = and (not x) (not y). +Proof. + intros; unfold not, xor, and, or, bitwise_binop. + repeat rewrite unsigned_repr; auto with ints. + decEq; apply Z_of_bits_exten; intros. + repeat rewrite bits_of_Z_of_bits; repeat rewrite Zplus_0_r; auto. + rewrite unsigned_mone. rewrite bits_of_Z_mone; auto. + assert (forall a b, xorb (a || b) true = xorb a true && xorb b true). + destruct a; destruct b; reflexivity. + auto. +Qed. + +Theorem not_and_or_not: + forall x y, not (and x y) = or (not x) (not y). +Proof. + intros. rewrite <- (not_involutive x) at 1. rewrite <- (not_involutive y) at 1. + rewrite <- not_or_and_not. apply not_involutive. +Qed. + +Theorem and_not_self: + forall x, and x (not x) = zero. +Proof. + intros. unfold not. rewrite and_xor_distrib. + rewrite and_idem. rewrite and_mone. apply xor_idem. +Qed. + +Theorem or_not_self: + forall x, or x (not x) = mone. +Proof. + intros. rewrite <- (not_involutive x) at 1. rewrite or_commut. + rewrite <- not_and_or_not. rewrite and_not_self. apply not_zero. +Qed. + +Theorem xor_not_self: + forall x, xor x (not x) = mone. +Proof. + intros. unfold not. rewrite <- xor_assoc. rewrite xor_idem. apply not_zero. +Qed. + +(** Connections between [add] and bitwise logical operations. *) + +Theorem add_is_or: + forall x y, + and x y = zero -> + add x y = or x y. +Proof. + intros. unfold add, or, bitwise_binop. + apply eqm_samerepr. eapply eqm_trans. apply eqm_add. + apply eqm_sym. apply Z_of_bits_of_Z. + apply eqm_sym. apply Z_of_bits_of_Z. + apply eqm_refl2. + apply Z_of_bits_excl. + intros. + replace (bits_of_Z wordsize (unsigned x) i && + bits_of_Z wordsize (unsigned y) i) + with (bits_of_Z wordsize (unsigned (and x y)) i). + rewrite H. rewrite unsigned_zero. rewrite bits_of_Z_zero. auto. + unfold and, bitwise_binop. rewrite unsigned_repr; auto with ints. + rewrite bits_of_Z_of_bits. reflexivity. auto. + auto. +Qed. + +Theorem xor_is_or: + forall x y, and x y = zero -> xor x y = or x y. +Proof. + intros. unfold xor, or, bitwise_binop. + decEq. apply Z_of_bits_exten; intros. + set (bitx := bits_of_Z wordsize (unsigned x) (i + 0)). + set (bity := bits_of_Z wordsize (unsigned y) (i + 0)). + assert (bitx && bity = false). + replace (bitx && bity) + with (bits_of_Z wordsize (unsigned (and x y)) (i + 0)). + rewrite H. rewrite unsigned_zero. apply bits_of_Z_zero. + unfold and, bitwise_binop. rewrite unsigned_repr; auto with ints. + unfold bitx, bity. rewrite bits_of_Z_of_bits. reflexivity. + omega. + destruct bitx; destruct bity; auto; simpl in H1; congruence. +Qed. + +Theorem add_is_xor: + forall x y, + and x y = zero -> + add x y = xor x y. +Proof. + intros. rewrite xor_is_or; auto. apply add_is_or; auto. +Qed. + +Theorem add_and: + forall x y z, + and y z = zero -> + add (and x y) (and x z) = and x (or y z). +Proof. + intros. rewrite add_is_or. + rewrite and_or_distrib; auto. + rewrite (and_commut x y). + rewrite and_assoc. + repeat rewrite <- (and_assoc x). + rewrite (and_commut (and x x)). + rewrite <- and_assoc. + rewrite H. rewrite and_commut. apply and_zero. +Qed. + (** ** Properties of shifts *) Theorem shl_zero: forall x, shl x zero = x. @@ -2685,6 +2779,28 @@ Proof. omega. omega. Qed. +Lemma translate_ltu: + forall x y d, + 0 <= unsigned x + unsigned d <= max_unsigned -> + 0 <= unsigned y + unsigned d <= max_unsigned -> + ltu (add x d) (add y d) = ltu x y. +Proof. + intros. unfold add. unfold ltu. + repeat rewrite unsigned_repr; auto. case (zlt (unsigned x) (unsigned y)); intro. + apply zlt_true. omega. + apply zlt_false. omega. +Qed. + +Theorem translate_cmpu: + forall c x y d, + 0 <= unsigned x + unsigned d <= max_unsigned -> + 0 <= unsigned y + unsigned d <= max_unsigned -> + cmpu c (add x d) (add y d) = cmpu c x y. +Proof. + intros. unfold cmpu. + rewrite translate_eq. repeat rewrite translate_ltu; auto. +Qed. + Lemma translate_lt: forall x y d, min_signed <= signed x + signed d <= max_signed -> -- cgit v1.2.3