diff options
| -rw-r--r-- | mppa_k1c/SelectOp.vp | 4 | ||||
| -rw-r--r-- | mppa_k1c/SelectOpproof.v | 28 |
2 files changed, 31 insertions, 1 deletions
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 2618983b..3df0c682 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -95,8 +95,12 @@ Nondetfunction select0 (ty : typ) (cond0 : condition0) (e1 e2 e3: expr) := match ty, cond0, e1, e2, e3 with | Tint, cond0, e1, (Eop (Ointconst imm) Enil), e3 => (Eop (Oselimm cond0 imm) (e1 ::: e3 ::: Enil)) + | Tint, cond0, (Eop (Ointconst imm) Enil), e2, e3 => + (Eop (Oselimm (negate_condition0 cond0) imm) (e2 ::: e3 ::: Enil)) | Tlong, cond0, e1, (Eop (Olongconst imm) Enil), e3 => (Eop (Osellimm cond0 imm) (e1 ::: e3 ::: Enil)) + | Tlong, cond0, (Eop (Olongconst imm) Enil), e2, e3 => + (Eop (Osellimm (negate_condition0 cond0) imm) (e2 ::: e3 ::: Enil)) | _, _, _ => (Eop (Osel cond0 ty) (e1 ::: e2 ::: e3 ::: Enil)) end. diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 39ad763e..21a06857 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -1441,6 +1441,31 @@ Proof. Qed. *) +Lemma eval_neg_condition0: + forall cond0: condition0, + forall v1: val, + forall m: mem, + (eval_condition0 (negate_condition0 cond0) v1 m) = + option_map negb (eval_condition0 cond0 v1 m). +Proof. + intros. + destruct cond0; simpl; + try rewrite Val.negate_cmp_bool; + try rewrite Val.negate_cmpu_bool; + try rewrite Val.negate_cmpl_bool; + try rewrite Val.negate_cmplu_bool; + reflexivity. +Qed. + +Lemma select_neg: + forall a b c, + Val.select (option_map negb a) b c = + Val.select a c b. +Proof. + destruct a; simpl; trivial. + destruct b; simpl; trivial. +Qed. + Lemma eval_select0: forall le ty cond0 ac vc a1 v1 a2 v2, eval_expr ge sp e m le ac vc -> @@ -1454,7 +1479,8 @@ Proof. unfold select0. destruct (select0_match ty cond0 a1 a2 ac). all: InvEval; econstructor; split; - repeat (try econstructor; try eassumption). + try repeat (try econstructor; try eassumption). + all: rewrite eval_neg_condition0; rewrite select_neg; constructor. Qed. Lemma bool_cond0_ne: |