diff options
| -rw-r--r-- | common/Values.v | 5 | ||||
| -rw-r--r-- | powerpc/SelectOp.vp | 2 | ||||
| -rw-r--r-- | powerpc/SelectOpproof.v | 3 |
3 files changed, 10 insertions, 0 deletions
diff --git a/common/Values.v b/common/Values.v index 54eac86..1e274ad 100644 --- a/common/Values.v +++ b/common/Values.v @@ -740,6 +740,11 @@ Proof. decEq. apply Int.xor_assoc. Qed. +Theorem not_xor: forall x, notint x = xor x (Vint Int.mone). +Proof. + destruct x; simpl; auto. +Qed. + Theorem shl_mul: forall x y, mul x (shl Vone y) = shl x y. Proof. destruct x; destruct y; simpl; auto. diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index d7944b6..c54beed 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -304,6 +304,8 @@ Nondetfunction xor (e1: expr) (e2: expr) := match e1, e2 with | Eop (Ointconst n1) Enil, t2 => xorimm n1 t2 | t1, Eop (Ointconst n2) Enil => xorimm n2 t1 + | Eop Onot (t1:::Enil), t2 => Eop Onxor (t1:::t2:::Enil) + | t1, Eop Onot (t2:::Enil) => Eop Onxor (t1:::t2:::Enil) | _, _ => Eop Oxor (e1:::e2:::Enil) end. diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 27a0fd0..b42503f 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -490,6 +490,9 @@ Proof. red; intros until y; unfold xor; case (xor_match a b); intros; InvEval. rewrite Val.xor_commut. apply eval_xorimm; auto. apply eval_xorimm; auto. + subst x. rewrite Val.xor_commut. rewrite Val.not_xor. rewrite <- Val.xor_assoc. + rewrite <- Val.not_xor. rewrite Val.xor_commut. TrivialExists. + subst y. rewrite Val.not_xor. rewrite <- Val.xor_assoc. rewrite <- Val.not_xor. TrivialExists. TrivialExists. Qed. |