From 336a1f906a9c617e68e9d43e244bf42e9bdbae64 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 9 Apr 2014 13:26:16 +0000
Subject: Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0
 comparisons over booleans. Select*: more systematic constant propagation;
 don't CP shifts by amounts outside of [0..31]. Driver: timer for whole
 compilation.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2452 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/ValueDomain.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'backend/ValueDomain.v')

diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 239dd47..2ece8cd 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -681,6 +681,14 @@ Qed.
 
 Hint Resolve is_uns_mon is_sgn_mon is_uns_sgn is_uns_usize is_sgn_ssize : va.
 
+Lemma is_uns_1:
+  forall n, is_uns 1 n -> n = Int.zero \/ n = Int.one.
+Proof.
+  intros. destruct (Int.testbit n 0) eqn:B0; [right|left]; apply Int.same_bits_eq; intros.
+  rewrite Int.bits_one. destruct (zeq i 0). subst i; auto. apply H; omega. 
+  rewrite Int.bits_zero. destruct (zeq i 0). subst i; auto. apply H; omega.
+Qed.
+
 (** Smart constructors for [Uns] and [Sgn]. *)
 
 Definition uns (n: Z) : aval :=
@@ -749,6 +757,12 @@ Qed.
 
 Hint Resolve vmatch_uns vmatch_uns_undef vmatch_sgn vmatch_sgn_undef : va.
 
+Lemma vmatch_Uns_1:
+  forall v, vmatch v (Uns 1) -> v = Vundef \/ v = Vint Int.zero \/ v = Vint Int.one.
+Proof.
+  intros. inv H; auto. right. exploit is_uns_1; eauto. intuition congruence.
+Qed.
+
 (** Ordering *)
 
 Inductive vge: aval -> aval -> Prop :=
-- 
cgit v1.2.3