From 996f2e071baaf52105714283d141af2eac8ffbfb Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Mon, 15 Apr 2019 15:21:49 +0200
Subject: Implement a `Osel` operation for x86

The operation compiles down to conditional moves.
---
 x86/Asmgenproof.v | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

(limited to 'x86/Asmgenproof.v')

diff --git a/x86/Asmgenproof.v b/x86/Asmgenproof.v
index 3aa87a4c..f1fd41e3 100644
--- a/x86/Asmgenproof.v
+++ b/x86/Asmgenproof.v
@@ -194,6 +194,14 @@ Proof.
   intros. destruct xc; simpl; TailNoLabel.
 Qed.
 
+Remark mk_sel_label:
+  forall xc rd r2 k c,
+  mk_sel xc rd r2 k = OK c ->
+  tail_nolabel k c.
+Proof.
+  unfold mk_sel; intros; destruct xc; inv H; TailNoLabel.
+Qed.
+
 Remark transl_cond_label:
   forall cond args k c,
   transl_cond cond args k = OK c ->
@@ -221,6 +229,9 @@ Proof.
   destruct (Float32.eq_dec n Float32.zero); TailNoLabel.
   destruct (normalize_addrmode_64 x) as [am' [delta|]]; TailNoLabel.
   eapply tail_nolabel_trans. eapply transl_cond_label; eauto. eapply mk_setcc_label.
+  unfold transl_sel in EQ2. destruct (ireg_eq x x0); monadInv EQ2.
+  TailNoLabel.
+  eapply tail_nolabel_trans. eapply transl_cond_label; eauto. eapply mk_sel_label; eauto.
 Qed.
 
 Remark transl_load_label:
@@ -706,7 +717,7 @@ Opaque loadind.
   intros. simpl in TR.
   destruct (transl_cond_correct tge tf cond args _ _ rs0 m' TR)
   as [rs' [A [B C]]].
-  rewrite EC in B.
+  rewrite EC in B. destruct B as [B _].
   destruct (testcond_for_condition cond); simpl in *.
 (* simple jcc *)
   exists (Pjcc c1 lbl); exists k; exists rs'.
@@ -744,7 +755,7 @@ Opaque loadind.
   left; eapply exec_straight_steps; eauto. intros. simpl in TR.
   destruct (transl_cond_correct tge tf cond args _ _ rs0 m' TR)
   as [rs' [A [B C]]].
-  rewrite EC in B.
+  rewrite EC in B. destruct B as [B _].
   destruct (testcond_for_condition cond); simpl in *.
 (* simple jcc *)
   econstructor; split.
-- 
cgit