diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-02 19:00:55 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-02 19:00:55 +0100 |
commit | 48d2d8755ec840cc15cfab9663f0e1e1ef47d65f (patch) | |
tree | 4f700afed300b8e97dbee6aef1cac557856fdc27 /riscV/SelectOpproof.v | |
parent | 90493ef36faa2925dbb107a994a57f010424fcbd (diff) | |
download | compcert-kvx-48d2d8755ec840cc15cfab9663f0e1e1ef47d65f.tar.gz compcert-kvx-48d2d8755ec840cc15cfab9663f0e1e1ef47d65f.zip |
detect redundant cmov
Diffstat (limited to 'riscV/SelectOpproof.v')
-rw-r--r-- | riscV/SelectOpproof.v | 22 |
1 files changed, 22 insertions, 0 deletions
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. |