diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-10-09 14:17:30 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-10-09 14:17:30 +0200 |
| commit | 0372472c17ceac36765c8921548672503115bb04 (patch) | |
| tree | 6fc6f7a4dba45e1ec993c688be446c9527a44098 /kvx/SelectOpproof.v | |
| parent | a66650006bd85a196d4a986ad36ee265d57b828c (diff) | |
| download | compcert-kvx-0372472c17ceac36765c8921548672503115bb04.tar.gz compcert-kvx-0372472c17ceac36765c8921548672503115bb04.zip | |
do not synthesize select if both operands are identical
Diffstat (limited to 'kvx/SelectOpproof.v')
| -rw-r--r-- | kvx/SelectOpproof.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v index d1d0b95c..0de9f51f 100644 --- a/kvx/SelectOpproof.v +++ b/kvx/SelectOpproof.v @@ -1533,6 +1533,12 @@ Proof. apply Val.swap_cmplu_bool. Qed. +Lemma if_same : forall {T : Type} (b : bool) (x : T), + (if b then x else x) = x. +Proof. + destruct b; trivial. +Qed. + Theorem eval_select: forall le ty cond al vl a1 v1 a2 v2 a b, select ty cond al a1 a2 = Some a -> @@ -1548,6 +1554,15 @@ Proof. intros until b. intro Hop; injection Hop; clear Hop; intro; subst a. intros HeL He1 He2 HeC. + destruct same_expr_pure eqn:SAME. + { + destruct (eval_same_expr a1 a2 le v1 v2 SAME He1 He2) as [EQ1 EQ2]. + subst a2. subst v2. + exists v1; split; trivial. + cbn. + rewrite if_same. + apply Val.lessdef_normalize. + } unfold cond_to_condition0. destruct (cond_to_condition0_match cond al). { |