diff options
| -rw-r--r-- | mppa_k1c/SelectLong.vp | 9 | ||||
| -rw-r--r-- | mppa_k1c/SelectLongproof.v | 8 |
2 files changed, 7 insertions, 10 deletions
diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp index f8f5bf3b..f7cb3c82 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -286,10 +286,6 @@ Nondetfunction orl (e1: expr) (e2: expr) := | t1, Eop (Olongconst n2) Enil => orlimm n2 t1 | (Eop Onotl (t1:::Enil)), t2 => Eop Oornl (t1:::t2:::Enil) | t1, (Eop Onotl (t2:::Enil)) => Eop Oornl (t2:::t1:::Enil) - | _, _ => Eop Oorl (e1:::e2:::Enil) - end. - - (* | (Eop Oandl ((Eop Ocast32signed ((Eop Oneg ((Eop (Ocmp (Ccomplimm Ceq zero0)) (y0:::Enil)):::Enil)):::Enil)):::v0:::Enil)), @@ -299,9 +295,10 @@ Nondetfunction orl (e1: expr) (e2: expr) := if same_expr_pure y0 y1 && Int64.eq zero0 Int64.zero && Int64.eq zero1 Int64.zero - then Eop Oselectl (v0:::v1:::y0:::Enil) + then Eop (Oselectl (Ccompl0 Cne)) (v0:::v1:::y0:::Enil) else Eop Oorl (e1:::e2:::Enil) - *) + | _, _ => Eop Oorl (e1:::e2:::Enil) + end. Nondetfunction xorlimm (n1: int64) (e2: expr) := if Int64.eq n1 Int64.zero then e2 else diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v index e18de2ee..3fab35b3 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -452,7 +452,6 @@ Proof. - InvEval. apply eval_orlimm; auto. - (*orn*) InvEval. TrivialExists; simpl; congruence. - (*orn reversed*) InvEval. rewrite Val.orl_commut. TrivialExists; simpl; congruence. - (* - (* selectl *) destruct (same_expr_pure y0 y1) eqn:PURE; simpl; try TrivialExists. predSpec Int64.eq Int64.eq_spec zero0 Int64.zero; simpl; try TrivialExists. @@ -504,7 +503,8 @@ Proof. TrivialExists. simpl. f_equal. - unfold selectl. + rewrite eval_selectl_to2. + unfold eval_selectl2. destruct vtest; simpl; trivial. rewrite Val.andl_commut. destruct v4; simpl; trivial. @@ -512,7 +512,7 @@ Proof. rewrite Val.orl_commut. destruct v9; simpl; trivial. rewrite int64_eq_commut. - destruct (Int64.eq i1 Int64.zero); simpl. + destruct (Int64.eq Int64.zero i1); simpl. + replace (Int64.repr (Int.signed (Int.neg Int.one))) with Int64.mone by Int64.bit_solve. replace (Int64.repr (Int.signed (Int.neg Int.zero))) with Int64.zero by Int64.bit_solve. @@ -526,7 +526,7 @@ Proof. rewrite Int64.and_mone. rewrite Int64.and_zero. rewrite Int64.or_zero. - reflexivity. *) + reflexivity. - TrivialExists. Qed. |