diff options
| -rw-r--r-- | kvx/SelectOp.vp | 14 | ||||
| -rw-r--r-- | kvx/SelectOpproof.v | 15 |
2 files changed, 22 insertions, 7 deletions
diff --git a/kvx/SelectOp.vp b/kvx/SelectOp.vp index 9e5d45a0..65dba3ac 100644 --- a/kvx/SelectOp.vp +++ b/kvx/SelectOp.vp @@ -103,8 +103,14 @@ Nondetfunction select0 (ty : typ) (cond0 : condition0) (e1 e2 e3: expr) := | _, _, _ => (Eop (Osel cond0 ty) (e1 ::: e2 ::: e3 ::: Enil)) end. +Definition same_expr_pure (e1 e2: expr) := + match e1, e2 with + | Evar v1, Evar v2 => if ident_eq v1 v2 then true else false + | _, _ => false + end. + Definition select (ty : typ) (cond : condition) (args : exprlist) (e1 e2: expr) : option expr := - Some( + Some (if same_expr_pure e1 e2 then e1 else match cond_to_condition0 cond args with | None => select0 ty (Ccomp0 Cne) e1 e2 (Eop (Ocmp cond) args) | Some(cond0, ec) => select0 ty cond0 e1 e2 ec @@ -356,12 +362,6 @@ Nondetfunction orimm (n1: int) (e2: expr) := | _ => Eop (Oorimm n1) (e2:::Enil) end. -Definition same_expr_pure (e1 e2: expr) := - match e1, e2 with - | Evar v1, Evar v2 => if ident_eq v1 v2 then true else false - | _, _ => false - end. - Nondetfunction or (e1: expr) (e2: expr) := match e1, e2 with | Eop (Ointconst n1) Enil, t2 => orimm n1 t2 diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v index d1d0b95c..0de9f51f 100644 --- a/kvx/SelectOpproof.v +++ b/kvx/SelectOpproof.v @@ -1533,6 +1533,12 @@ Proof. apply Val.swap_cmplu_bool. Qed. +Lemma if_same : forall {T : Type} (b : bool) (x : T), + (if b then x else x) = x. +Proof. + destruct b; trivial. +Qed. + Theorem eval_select: forall le ty cond al vl a1 v1 a2 v2 a b, select ty cond al a1 a2 = Some a -> @@ -1548,6 +1554,15 @@ Proof. intros until b. intro Hop; injection Hop; clear Hop; intro; subst a. intros HeL He1 He2 HeC. + destruct same_expr_pure eqn:SAME. + { + destruct (eval_same_expr a1 a2 le v1 v2 SAME He1 He2) as [EQ1 EQ2]. + subst a2. subst v2. + exists v1; split; trivial. + cbn. + rewrite if_same. + apply Val.lessdef_normalize. + } unfold cond_to_condition0. destruct (cond_to_condition0_match cond al). { |