From 58c7f5045c9cf1b64311fd7a168ed3b496666bb0 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 21 Jun 2011 15:53:05 +0000 Subject: Recognition of rlwimi instruction (useful for bitfield assignment) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1676 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/SelectOpproof.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'powerpc/SelectOpproof.v') diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 6d1e3c5c..b23e5a50 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -124,6 +124,7 @@ Theorem eval_notint: eval_expr ge sp e m le (notint a) (Vint (Int.not x)). Proof. unfold notint; intros until x; case (notint_match a); intros; InvEval. + EvalOp. EvalOp. simpl. congruence. EvalOp. simpl. congruence. EvalOp. simpl. congruence. @@ -524,11 +525,22 @@ Proof. generalize (Int.eq_spec amount1 amount2). rewrite H6. intro. subst amount2. exploit eval_same_expr; eauto. intros [EQ1 EQ2]. inv EQ1. inv EQ2. simpl. EvalOp. simpl. rewrite Int.or_rolm. auto. + caseEq (Int.eq amount1 Int.zero && Int.eq mask1 (Int.not mask2)); intro. + destruct (andb_prop _ _ H4). + generalize (Int.eq_spec amount1 Int.zero). rewrite H5. intro. + generalize (Int.eq_spec mask1 (Int.not mask2)). rewrite H6. intro. + subst. rewrite Int.rolm_zero. EvalOp. + caseEq (Int.eq amount2 Int.zero && Int.eq mask2 (Int.not mask1)); intro. + destruct (andb_prop _ _ H5). + generalize (Int.eq_spec amount2 Int.zero). rewrite H6. intro. + generalize (Int.eq_spec mask2 (Int.not mask1)). rewrite H7. intro. + subst. rewrite Int.rolm_zero. rewrite Int.or_commut. EvalOp. simpl. apply eval_Eop with (Vint x :: Vint y :: nil). econstructor. EvalOp. simpl. congruence. econstructor. EvalOp. simpl. congruence. constructor. auto. EvalOp. Qed. + Theorem eval_divs: forall le a b x y, eval_expr ge sp e m le a (Vint x) -> -- cgit