From 48d2d8755ec840cc15cfab9663f0e1e1ef47d65f Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 2 Feb 2021 19:00:55 +0100
Subject: detect redundant cmov

---
 riscV/SelectOpproof.v | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

(limited to 'riscV/SelectOpproof.v')

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