diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-06-21 15:53:05 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-06-21 15:53:05 +0000 |
| commit | 58c7f5045c9cf1b64311fd7a168ed3b496666bb0 (patch) | |
| tree | b71dc7537a473b26a2109339e6ee21dc69581655 /powerpc/SelectOpproof.v | |
| parent | b39791601bb128c37db82eb66a8bc1991047818f (diff) | |
| download | compcert-58c7f5045c9cf1b64311fd7a168ed3b496666bb0.tar.gz compcert-58c7f5045c9cf1b64311fd7a168ed3b496666bb0.zip | |
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
Diffstat (limited to 'powerpc/SelectOpproof.v')
| -rw-r--r-- | powerpc/SelectOpproof.v | 12 |
1 files changed, 12 insertions, 0 deletions
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) -> |