diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-12 13:08:58 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-12 13:08:58 +0200 |
| commit | 64d7dab2720d63e1b40ae893d76895a23c11e2d1 (patch) | |
| tree | 825f95d64dc9bfa50565c03daf6e983d6c7ba5cc /mppa_k1c | |
| parent | 43e2036b6f10efdb7e63613067da16fa7fa4b421 (diff) | |
| download | compcert-kvx-64d7dab2720d63e1b40ae893d76895a23c11e2d1.tar.gz compcert-kvx-64d7dab2720d63e1b40ae893d76895a23c11e2d1.zip | |
more simplifications
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/SelectLong.vp | 3 | ||||
| -rw-r--r-- | mppa_k1c/SelectLongproof.v | 18 |
2 files changed, 13 insertions, 8 deletions
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. |