From 64d7dab2720d63e1b40ae893d76895a23c11e2d1 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 12 Apr 2019 13:08:58 +0200 Subject: more simplifications --- mppa_k1c/SelectLong.vp | 3 +++ mppa_k1c/SelectLongproof.v | 18 ++++++++++-------- 2 files changed, 13 insertions(+), 8 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp index f7cb3c82..6389bca2 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -302,6 +302,9 @@ Nondetfunction orl (e1: expr) (e2: expr) := Nondetfunction xorlimm (n1: int64) (e2: expr) := if Int64.eq n1 Int64.zero then e2 else + if Int64.eq n1 Int64.mone + then Eop Onotl (e2:::Enil) + else match e2 with | Eop (Olongconst n2) Enil => longconst (Int64.xor n1 n2) | Eop (Oxorlimm n2) (t2:::Enil) => diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v index 3fab35b3..d4893eb8 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -534,14 +534,16 @@ Theorem eval_xorlimm: forall n, unary_constructor_sound (xorlimm n) (fun v => Va Proof. unfold xorlimm; intros; red; intros. predSpec Int64.eq Int64.eq_spec n Int64.zero. - exists x; split; auto. subst. destruct x; simpl; auto. rewrite Int64.xor_zero; auto. - destruct (xorlimm_match a); InvEval; subst. -- econstructor; split. apply eval_longconst. simpl. rewrite Int64.xor_commut; auto. -- rewrite Val.xorl_assoc. simpl. rewrite (Int64.xor_commut n2). - predSpec Int64.eq Int64.eq_spec (Int64.xor n n2) Int64.zero. -+ rewrite H. exists v1; split; auto. destruct v1; simpl; auto. rewrite Int64.xor_zero; auto. -+ TrivialExists. -- TrivialExists. + - exists x; split; auto. subst. destruct x; simpl; auto. rewrite Int64.xor_zero; auto. + - predSpec Int64.eq Int64.eq_spec n Int64.mone. + -- subst n. intros. rewrite <- Val.notl_xorl. TrivialExists. + -- destruct (xorlimm_match a); InvEval; subst. + + econstructor; split. apply eval_longconst. simpl. rewrite Int64.xor_commut; auto. + + rewrite Val.xorl_assoc. simpl. rewrite (Int64.xor_commut n2). + predSpec Int64.eq Int64.eq_spec (Int64.xor n n2) Int64.zero. + * rewrite H. exists v1; split; auto. destruct v1; simpl; auto. rewrite Int64.xor_zero; auto. + * TrivialExists. + + TrivialExists. Qed. Theorem eval_xorl: binary_constructor_sound xorl Val.xorl. -- cgit