diff options
| -rw-r--r-- | mppa_k1c/SelectOp.vp | 7 | ||||
| -rw-r--r-- | mppa_k1c/SelectOpproof.v | 21 |
2 files changed, 17 insertions, 11 deletions
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index c5a86ac1..72f5616c 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -327,7 +327,12 @@ Nondetfunction or (e1: expr) (e2: expr) := end. Nondetfunction xorimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then e2 else + if Int.eq n1 Int.zero + then e2 + else + if Int.eq n1 Int.mone + then Eop Onot (e2:::Enil) + else match e2 with | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.xor n1 n2)) Enil | Eop (Oxorimm n2) (t2:::Enil) => diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 65038038..023f2a3c 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -648,16 +648,17 @@ Proof. intros; red; intros until x. unfold xorimm. predSpec Int.eq Int.eq_spec n Int.zero. - intros. exists x; split. auto. - destruct x; simpl; auto. subst n. rewrite Int.xor_zero. auto. - - intros. destruct (xorimm_match a); intros; InvEval. - - TrivialExists. simpl. rewrite Int.xor_commut; auto. - - subst. rewrite Val.xor_assoc. simpl. rewrite Int.xor_commut. - predSpec Int.eq Int.eq_spec (Int.xor n2 n) Int.zero. - + exists v1; split; auto. destruct v1; simpl; auto. rewrite H0, Int.xor_zero; auto. - + TrivialExists. - - TrivialExists. + - intros. exists x; split. auto. + destruct x; simpl; auto. subst n. rewrite Int.xor_zero. auto. + - predSpec Int.eq Int.eq_spec n Int.mone. + -- subst n. intros. rewrite <- Val.not_xor. TrivialExists. + -- intros. destruct (xorimm_match a); intros; InvEval. + + TrivialExists. simpl. rewrite Int.xor_commut; auto. + + subst. rewrite Val.xor_assoc. simpl. rewrite Int.xor_commut. + predSpec Int.eq Int.eq_spec (Int.xor n2 n) Int.zero. + * exists v1; split; auto. destruct v1; simpl; auto. rewrite H1, Int.xor_zero; auto. + * TrivialExists. + + TrivialExists. Qed. Theorem eval_xor: binary_constructor_sound xor Val.xor. |