Ajouté la négation des comparateurs single

3 files changed, 42 insertions, 3 deletions

diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index fb6ba16e..73ecd67f 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -324,9 +324,9 @@ Definition transl_cond_op
   | Ccompfs c, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2;
       OK (transl_cond_float32 c rd r1 r2 k)
-(*   | Cnotcompfs c, a1 :: a2 :: nil =>
+  | Cnotcompfs c, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_cond_notfloat32 c rd r1 r2 k) *) (* FIXME - because of proofs, might have to use a xor instead *)
+      OK (transl_cond_notfloat32 c rd r1 r2 k) (* FIXME - because of proofs, might have to use a xor instead *)
   | Ccompf _, _ => Error(msg "Asmblockgen.transl_cond_op: Ccompf")
   | Cnotcompf _, _ => Error(msg "Asmblockgen.transl_cond_op: Cnotcompf")
 (*| Ccompf c, f1 :: f2 :: nil =>
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index 2b79c78e..1e3a40d4 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -951,6 +951,7 @@ Proof.
   - simpl in TIB. unfold transl_op in TIB. exploreInst; try discriminate.

     unfold transl_cond_op in EQ0. exploreInst; try discriminate.

     unfold transl_cond_float32. exploreInst; try discriminate.

+    unfold transl_cond_notfloat32. exploreInst; try discriminate.

   - simpl in TIB. unfold transl_load in TIB. exploreInst; try discriminate.

     all: unfold transl_memory_access in EQ0; exploreInst; try discriminate.

   - simpl in TIB. unfold transl_store in TIB. exploreInst; try discriminate.

diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index f7207c88..e6093290 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -998,6 +998,42 @@ Proof.
   split; intros; Simpl.
 Qed.
 
+Lemma transl_cond_nofloat32_correct:
+  forall cmp rd r1 r2 k rs m,
+  exists rs',
+     exec_straight ge (basics_to_code (transl_cond_notfloat32 cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m
+  /\ Val.lessdef (Val.of_optbool (option_map negb (Val.cmpfs_bool cmp (rs r1) (rs r2)))) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
+Proof.
+  intros. destruct cmp; simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct (rs r1); auto. destruct (rs r2); auto.
+  rewrite Float32.cmp_ne_eq. auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct (rs r1); auto. destruct (rs r2); auto.
+  rewrite Float32.cmp_ne_eq. simpl. destruct (Float32.cmp Ceq f f0); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl.
+  destruct (Float32.cmp Clt f f0); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl.
+  cutrewrite (Cge = swap_comparison Cle); auto. rewrite Float32.cmp_swap.
+  destruct (Float32.cmp _ _ _); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl.
+  cutrewrite (Clt = swap_comparison Cgt); auto. rewrite Float32.cmp_swap.
+  destruct (Float32.cmp _ _ _); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl.
+  destruct (Float32.cmp _ _ _); auto.
+Qed.
+
 Lemma transl_cond_op_correct:
   forall cond rd args k c rs m,
   transl_cond_op cond rd args k = OK c ->
@@ -1033,8 +1069,10 @@ Proof.
   exploit transl_condimm_int64u_correct; eauto. instantiate (1 := x); eauto with asmgen. simpl. 
   intros (rs' & A & B & C).
   exists rs'; repeat split; eauto. rewrite MKTOT; eauto.
-+ (* cmpfloat *) 
++ (* cmpsingle *) 
   exploit transl_cond_float32_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto.
++ (* cmpnosingle *)
+  exploit transl_cond_nofloat32_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto.
 Qed.
 
 (*