From 48d2d8755ec840cc15cfab9663f0e1e1ef47d65f Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 2 Feb 2021 19:00:55 +0100 Subject: detect redundant cmov --- riscV/SelectOp.vp | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) (limited to 'riscV/SelectOp.vp') 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. -- cgit