detect redundant cmov

2 files changed, 34 insertions, 3 deletions

diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp
index bc169006..9932aaf8 100644
--- a/riscV/SelectOp.vp
+++ b/riscV/SelectOp.vp
@@ -419,9 +419,18 @@ Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil).
 
 (** ** Selection *)
 
+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
-   := if Archi.ptr64 then
+  : option expr :=
+  if same_expr_pure e1 e2
+  then Some e1
+  else
+     if Archi.ptr64 then
       match ty with
       | Tlong => Some (Eop Oselectl
                        ((Eop (Ocmp cond) args) ::: e1 ::: e2 ::: Enil))
@@ -488,4 +497,4 @@ Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr
   | BI_bits_of_double => Some (Eop Obits_of_float args)
   | BI_float_of_bits => Some (Eop Osingle_of_bits args)
   | BI_double_of_bits => Some (Eop Ofloat_of_bits args)
-  end.
\ No newline at end of file
+  end.
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v
index 1fe4e662..ce80fc57 100644
--- a/riscV/SelectOpproof.v
+++ b/riscV/SelectOpproof.v
@@ -928,6 +928,19 @@ Proof.
   }
 Qed.
 
+Lemma same_expr_pure_correct:
+  forall le a1 a2 v1 v2
+    (PURE : same_expr_pure a1 a2 = true)
+    (EVAL1 : eval_expr ge sp e m le a1 v1)
+    (EVAL2 : eval_expr ge sp e m le a2 v2),
+    v1 = v2.
+Proof.
+  intros.
+  destruct a1; destruct a2; cbn in *; try discriminate.
+  inv EVAL1. inv EVAL2.
+  destruct (ident_eq i i0); congruence.
+Qed.
+  
 Theorem eval_select:
   forall le ty cond al vl a1 v1 a2 v2 a b,
   select ty cond al a1 a2 = Some a ->
@@ -940,6 +953,15 @@ Theorem eval_select:
   /\ Val.lessdef (Val.select (Some b) v1 v2 ty) v.
 Proof.
   unfold select; intros.
+  pose proof (same_expr_pure_correct le a1 a2 v1 v2) as PURE.
+  destruct (same_expr_pure a1 a2).
+  { rewrite <- PURE by auto.
+    inv H.
+    exists v1. split. assumption.
+    unfold Val.select.
+    destruct b; apply Val.lessdef_normalize.
+  }
+  clear PURE.
   destruct Archi.ptr64 eqn:PTR64.
   2: discriminate.
   destruct ty; cbn in *; try discriminate.