diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-02-24 15:49:19 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-02-24 15:49:19 +0000 |
| commit | 91dcfe11ff321386f7924da053be83523073a50c (patch) | |
| tree | dc8291da94c66665ca8dd2496cdd74e32e08ae92 /powerpc/SelectOpproof.v | |
| parent | 0e76ac320601a81a67c700759526d0f8b7a8ed7b (diff) | |
| download | compcert-91dcfe11ff321386f7924da053be83523073a50c.tar.gz compcert-91dcfe11ff321386f7924da053be83523073a50c.zip | |
Improved instruction selection for "notint".
powerpc/PrintAsm.ml: fixed MacOS X problems with malloc and free
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1824 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc/SelectOpproof.v')
| -rw-r--r-- | powerpc/SelectOpproof.v | 27 |
1 files changed, 19 insertions, 8 deletions
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 59f2a419..39205dbd 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -134,18 +134,24 @@ Qed. Theorem eval_notint: unary_constructor_sound notint Val.notint. Proof. + assert (forall v, Val.lessdef (Val.notint (Val.notint v)) v). + destruct v; simpl; auto. rewrite Int.not_involutive; auto. unfold notint; red; intros until x; case (notint_match a); intros; InvEval. - TrivialExists. + TrivialExists. + subst. exists v1; split; auto. subst. TrivialExists. subst. TrivialExists. subst. TrivialExists. - econstructor; split; eauto. - eapply eval_Elet. eexact H. - eapply eval_Eop. - eapply eval_Econs. apply eval_Eletvar. simpl. reflexivity. - eapply eval_Econs. apply eval_Eletvar. simpl. reflexivity. - apply eval_Enil. - simpl. destruct x; simpl; auto. rewrite Int.or_idem. auto. + subst. exists (Val.and v1 v0); split; auto. EvalOp. + subst. exists (Val.or v1 v0); split; auto. EvalOp. + subst. exists (Val.xor v1 v0); split; auto. EvalOp. + subst. exists (Val.or v0 (Val.notint v1)); split. EvalOp. + destruct v0; destruct v1; simpl; auto. rewrite Int.not_and_or_not. rewrite Int.not_involutive. + rewrite Int.or_commut. auto. + subst. exists (Val.and v0 (Val.notint v1)); split. EvalOp. + destruct v0; destruct v1; simpl; auto. rewrite Int.not_or_and_not. rewrite Int.not_involutive. + rewrite Int.and_commut. auto. + TrivialExists. Qed. Theorem eval_boolval: unary_constructor_sound boolval Val.boolval. @@ -407,6 +413,8 @@ Proof. red; intros until y; unfold and; case (and_match a b); intros; InvEval. rewrite Val.and_commut. apply eval_andimm; auto. apply eval_andimm; auto. + subst. rewrite Val.and_commut. TrivialExists. + subst. TrivialExists. TrivialExists. Qed. @@ -460,6 +468,9 @@ Proof. (* intconst *) InvEval. rewrite Val.or_commut. apply eval_orimm; auto. InvEval. apply eval_orimm; auto. +(* orc *) + InvEval. subst. rewrite Val.or_commut. TrivialExists. + InvEval. subst. TrivialExists. (* default *) TrivialExists. Qed. |