detect redundant cmov

1 files changed, 12 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.