From 0372472c17ceac36765c8921548672503115bb04 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 9 Oct 2020 14:17:30 +0200
Subject: do not synthesize select if both operands are identical

---
 kvx/SelectOp.vp | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'kvx/SelectOp.vp')

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
-- 
cgit