diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-26 19:59:04 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-26 19:59:04 +0100 |
| commit | 0a708569d1fe213305c731cfa32fd6a41f5811e3 (patch) | |
| tree | 2ba291924ae1f4c465c2740e57deb784bd37f772 /mppa_k1c | |
| parent | 464a6b67e374440c22b6abcbca938f84fbf13871 (diff) | |
| download | compcert-kvx-0a708569d1fe213305c731cfa32fd6a41f5811e3.tar.gz compcert-kvx-0a708569d1fe213305c731cfa32fd6a41f5811e3.zip | |
some progress
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/SelectOp.vp | 9 | ||||
| -rw-r--r-- | mppa_k1c/SelectOpproof.v | 22 |
2 files changed, 12 insertions, 19 deletions
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 2a07afc4..8f188f7e 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -300,14 +300,13 @@ Nondetfunction or (e1: expr) (e2: expr) := else Eop Oor (e1:::e2:::Enil) | (Eop Onot (t1:::Enil)), t2 => Eop Oorn (t1:::t2:::Enil) | t1, (Eop Onot (t2:::Enil)) => Eop Oorn (t2:::t1:::Enil) - | (Eop Oand ((Eop Osub ((Eop (Ocmp (Ccomp Ceq)) - (y1:::(Eop (Ointconst zero1) Enil):::Enil)):::(Eop (Ointconst one1) Enil):::Enil)):::v1:::Enil)), - (Eop Oand ((Eop Oneg ((Eop (Ocmp (Ccomp Ceq)) - (y0:::(Eop (Ointconst zero0) Enil):::Enil)):::Enil)):::v0:::Enil)) => + | (Eop Oand ((Eop Oneg ((Eop (Ocmp (Ccomp Ceq)) + (y0:::(Eop (Ointconst zero0) Enil):::Enil)):::Enil)):::v0:::Enil)), + (Eop Oand ((Eop Oneg ((Eop (Ocmp (Ccomp Cne)) + (y1:::(Eop (Ointconst zero1) Enil):::Enil)):::Enil)):::v1:::Enil)) => if same_expr_pure y0 y1 && Int.eq zero0 Int.zero && Int.eq zero1 Int.zero - && Int.eq one1 Int.one then Eop Oselect (v0:::v1:::y0:::Enil) else Eop Oor (e1:::e2:::Enil) | _, _ => Eop Oor (e1:::e2:::Enil) diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 221d994f..23a883ec 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -696,13 +696,10 @@ Proof. exists (Val.ror v1 (Vint n2)); split. EvalOp. rewrite Val.or_commut. apply ROR; auto. - (*orn*) TrivialExists; simpl; congruence. - (*orn reversed*) rewrite Val.or_commut. TrivialExists; simpl; congruence. - - (* select *) - rename v12 into ret0. - rename v7 into ret1. + - (* select *) Show. destruct (same_expr_pure y0 y1) eqn:PURE; simpl; try exact DEFAULT. predSpec Int.eq Int.eq_spec zero0 Int.zero; simpl; try exact DEFAULT. predSpec Int.eq Int.eq_spec zero1 Int.zero; simpl; try exact DEFAULT. - predSpec Int.eq Int.eq_spec one1 Int.one; simpl; try exact DEFAULT. TrivialExists. simpl in *. unfold select. @@ -711,28 +708,25 @@ Proof. inv H7. inv H9. inv H11. - inv H14. inv H12. - inv H16. + inv H15. unfold same_expr_pure in PURE. destruct y0; try congruence. destruct y1; try congruence. destruct (ident_eq i i0); try congruence. rewrite <- e0 in *. clear e0. clear PURE. inv H2. inv H5. - replace v10 with v4 in * by congruence. + replace v9 with v4 in * by congruence. rename v4 into vselect. destruct vselect; simpl; trivial. - rewrite (Val.and_commut _ ret0). + rewrite (Val.and_commut _ v6). + destruct v6; simpl; trivial. + rewrite (Val.and_commut _ v11). rewrite Val.or_commut. - destruct ret0; simpl; trivial. - rewrite (Val.and_commut _ ret1). - rewrite Val.or_commut. - destruct ret1; simpl; trivial. + destruct v11; simpl; trivial. rewrite int_eq_commut. destruct (Int.eq i1 Int.zero); simpl. - + rewrite Int.sub_idem. - rewrite Int.and_zero. + + rewrite Int.and_zero. rewrite Int.or_commut. rewrite Int.or_zero. rewrite Int.and_mone. |