diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-04 23:16:35 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-04 23:16:35 +0200 |
commit | b5352b040da8c38b371316d67c2180dbab758295 (patch) | |
tree | d90352b59294c4521300435542d76d5b95f148ca | |
parent | 68a6d0dd0ea5774529d823fb9a9ca981c1ecebb0 (diff) | |
download | compcert-kvx-b5352b040da8c38b371316d67c2180dbab758295.tar.gz compcert-kvx-b5352b040da8c38b371316d67c2180dbab758295.zip |
move with immediates
-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: |