Merge remote-tracking branch 'origin/mppa_postpass' into mppa_memory_model_patch

5 files changed, 387 insertions, 42 deletions

diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index ec5c3cf5..b7e7b87c 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -292,7 +292,7 @@ Definition iandb (ib1 ib2: ?? bool): ?? bool :=
 
 Definition arith_op_eq (o1 o2: arith_op): ?? bool :=
   match o1, o2 with
-  | OArithR n1, OArithR n2 => phys_eq n1 n2
+  | OArithR n1, OArithR n2 => struct_eq n1 n2
   | OArithRR n1, OArithRR n2 => phys_eq n1 n2
   | OArithRI32 n1 i1, OArithRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2)
   | OArithRI64 n1 i1, OArithRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2)
@@ -359,16 +359,17 @@ Proof.
   - rewrite Z.eqb_eq in * |-. congruence.
 Qed.
 
-(*
+
 Definition op_eq (o1 o2: op): ?? bool :=
   match o1, o2 with
   | Arith i1, Arith i2 => arith_op_eq i1 i2
   | Load i1, Load i2 => load_op_eq i1 i2
   | Store i1, Store i2 => store_op_eq i1 i2
   | Control i1, Control i2 => control_op_eq i1 i2
-  | Allocframe sz1 pos1, Allocframe sz2 pos2 => iandb (phys_eq sz1 sz2) (phys_eq pos1 pos2)
-  | Freeframe sz1 pos1, Freeframe sz2 pos2 => iandb (phys_eq sz1 sz2) (phys_eq pos1 pos2)
-  | Freeframe2 sz1 pos1, Freeframe2 sz2 pos2 => iandb (phys_eq sz1 sz2) (phys_eq pos1 pos2)
+  | Allocframe sz1 pos1, Allocframe sz2 pos2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq pos1 pos2)
+  | Allocframe2 sz1 pos1, Allocframe2 sz2 pos2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq pos1 pos2)
+  | Freeframe sz1 pos1, Freeframe sz2 pos2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq pos1 pos2)
+  | Freeframe2 sz1 pos1, Freeframe2 sz2 pos2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq pos1 pos2)
   | Constant c1, Constant c2 => phys_eq c1 c2
   | Fail, Fail => RET true
   | _, _ => RET false
@@ -383,22 +384,25 @@ Proof.
   - simpl in Hexta. exploit load_op_eq_correct. eassumption. eauto. congruence.
   - simpl in Hexta. exploit store_op_eq_correct. eassumption. eauto. congruence.
   - simpl in Hexta. exploit control_op_eq_correct. eassumption. eauto. congruence.
-  - apply andb_prop in H1; inversion H1; apply H in H2; apply H0 in H3; congruence.
-  - apply andb_prop in H1; inversion H1; apply H in H2; apply H0 in H3; congruence.
-  - apply andb_prop in H1; inversion H1; apply H in H2; apply H0 in H3; congruence.
+  - apply andb_prop in H0; inversion_clear H0. apply H in H2. apply Z.eqb_eq in H1. congruence.
+  - apply andb_prop in H0; inversion_clear H0. apply H in H2. apply Z.eqb_eq in H1. congruence.
+  - apply andb_prop in H0; inversion_clear H0. apply H in H2. apply Z.eqb_eq in H1. congruence.
+  - apply andb_prop in H0; inversion_clear H0. apply H in H2. apply Z.eqb_eq in H1. congruence.
   - congruence.
 Qed.
-*)
+
 
 (* QUICK FIX WITH struct_eq *)
 
-Definition op_eq (o1 o2: op): ?? bool := struct_eq o1 o2. 
+(* Definition op_eq (o1 o2: op): ?? bool := struct_eq o1 o2. 
+
 
 Theorem op_eq_correct o1 o2: 
  WHEN op_eq o1 o2 ~> b THEN b=true -> o1 = o2.
 Proof.
   wlp_simplify.
 Qed.
+ *)
 
 End IMPPARAM.
 
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index edffd879..8c6457a6 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -190,14 +190,29 @@ Definition transl_opt_compluimm
     loadimm64 RTMP n ::g (transl_compl c Unsigned r1 RTMP lbl k)
   .
 
-(*   match select_compl n c with
-  | Some Ceq => Pcbu BTdeqz r1 lbl ::g k
-  | Some Cne => Pcbu BTdnez r1 lbl ::g k
-  | Some _   => nil (* Never happens *)
-  | None     => loadimm64 RTMP n ::g (transl_compl c Unsigned r1 RTMP lbl k)
-  end
-  .
- *)
+Definition transl_comp_float32 (cmp: comparison) (r1 r2: ireg) (lbl: label) (k: code) :=
+  match ftest_for_cmp cmp with
+  | Normal ft => Pfcompw ft GPR32 r1 r2 ::g Pcb BTwnez GPR32 lbl ::g k
+  | Reversed ft => Pfcompw ft GPR32 r2 r1 ::g Pcb BTwnez GPR32 lbl ::g k
+  end.
+
+Definition transl_comp_notfloat32 (cmp: comparison) (r1 r2: ireg) (lbl: label) (k: code) :=
+  match notftest_for_cmp cmp with
+  | Normal ft => Pfcompw ft GPR32 r1 r2 ::g Pcb BTwnez GPR32 lbl ::g k
+  | Reversed ft => Pfcompw ft GPR32 r2 r1 ::g Pcb BTwnez GPR32 lbl ::g k
+  end.
+
+Definition transl_comp_float64 (cmp: comparison) (r1 r2: ireg) (lbl: label) (k: code) :=
+  match ftest_for_cmp cmp with
+  | Normal ft => Pfcompl ft GPR32 r1 r2 ::g Pcb BTwnez GPR32 lbl ::g k
+  | Reversed ft => Pfcompl ft GPR32 r2 r1 ::g Pcb BTwnez GPR32 lbl ::g k
+  end.
+
+Definition transl_comp_notfloat64 (cmp: comparison) (r1 r2: ireg) (lbl: label) (k: code) :=
+  match notftest_for_cmp cmp with
+  | Normal ft => Pfcompl ft GPR32 r1 r2 ::g Pcb BTwnez GPR32 lbl ::g k
+  | Reversed ft => Pfcompl ft GPR32 r2 r1 ::g Pcb BTwnez GPR32 lbl ::g k
+  end.
 
 Definition transl_cbranch
     (cond: condition) (args: list mreg) (lbl: label) (k: code) : res (list instruction ) :=
@@ -234,23 +249,19 @@ Definition transl_cbranch
           else
             loadimm64 RTMP n ::g (transl_compl c Signed r1 RTMP lbl k)
          )
-(*| Ccompf c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_float c rd r1 r2 in
-      OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k)
-  | Cnotcompf c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_float c rd r1 r2 in
-      OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k)
-  | Ccompfs c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_single c rd r1 r2 in
-      OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k)
-  | Cnotcompfs c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_single c rd r1 r2 in
-      OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k)
-*)| _, _ =>
+  | Ccompf c, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (transl_comp_float64 c r1 r2 lbl k)
+  | Cnotcompf c, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (transl_comp_notfloat64 c r1 r2 lbl k)
+  | Ccompfs c, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (transl_comp_float32 c r1 r2 lbl k)
+  | Cnotcompfs c, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (transl_comp_notfloat32 c r1 r2 lbl k)
+  | _, _ =>
       Error(msg "Asmgenblock.transl_cbranch")
   end.
 
@@ -282,6 +293,7 @@ Definition transl_condimm_int64s (cmp: comparison) (rd r1: ireg) (n: int64) (k:
 Definition transl_condimm_int64u (cmp: comparison) (rd r1: ireg) (n: int64) (k: bcode) :=
   Pcompil (itest_for_cmp cmp Unsigned) rd r1 n ::i k.
 
+
 Definition transl_cond_float32 (cmp: comparison) (rd r1 r2: ireg) (k: bcode) :=
   match ftest_for_cmp cmp with
   | Normal ft => Pfcompw ft rd r1 r2 ::i k
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index 1ac9a211..84877488 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -891,6 +891,10 @@ Proof.
     + simpl in TIC. unfold transl_cbranch in TIC. exploreInst; simpl; eauto.

       * unfold transl_opt_compuimm. exploreInst; simpl; eauto.

       * unfold transl_opt_compluimm. exploreInst; simpl; eauto.

+      * unfold transl_comp_float64. exploreInst; simpl; eauto.

+      * unfold transl_comp_notfloat64. exploreInst; simpl; eauto.

+      * unfold transl_comp_float32. exploreInst; simpl; eauto.

+      * unfold transl_comp_notfloat32. exploreInst; simpl; eauto.

     + simpl in TIC. inv TIC.

     + simpl in TIC. monadInv TIC. simpl. eauto.

   - monadInv TIC. simpl; auto.

@@ -990,6 +994,10 @@ Proof.
     + simpl in TIC. unfold transl_cbranch in TIC. exploreInst; try discriminate.

       * unfold transl_opt_compuimm. exploreInst; try discriminate.

       * unfold transl_opt_compluimm. exploreInst; try discriminate.

+      * unfold transl_comp_float64. exploreInst; try discriminate.

+      * unfold transl_comp_notfloat64. exploreInst; try discriminate.

+      * unfold transl_comp_float32. exploreInst; try discriminate.

+      * unfold transl_comp_notfloat32. exploreInst; try discriminate.

   - contradict Hnonil; auto.

 Qed.

 

@@ -1005,8 +1013,12 @@ Proof.
   - assert False. eapply Hnobuiltin; eauto. destruct H.

   - unfold transl_cbranch in TIC. exploreInst.

     all: try discriminate.

-    + unfold transl_opt_compuimm. exploreInst. all: try discriminate.

-    + unfold transl_opt_compluimm. exploreInst. all: try discriminate.

+    * unfold transl_opt_compuimm. exploreInst. all: try discriminate.

+    * unfold transl_opt_compluimm. exploreInst. all: try discriminate.

+    * unfold transl_comp_float64. exploreInst; try discriminate.

+    * unfold transl_comp_notfloat64. exploreInst; try discriminate.

+    * unfold transl_comp_float32. exploreInst; try discriminate.

+    * unfold transl_comp_notfloat32. exploreInst; try discriminate.

 Qed.

 

 Theorem match_state_codestate:

diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index d9ce95ab..1a55f58e 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -222,8 +222,6 @@ Qed.
 *)
 *)
 
-Definition yolo := 4.
-
 Lemma opimm64_correct:
   forall (op: arith_name_rrr)
          (opi: arith_name_rri64)
@@ -428,6 +426,288 @@ Proof.
     rewrite H0. simpl; auto.
 Qed.
 
+Lemma swap_comparison_cmpf_eq:
+  forall v1 v2 cmp,
+  (Val.cmpf cmp v1 v2) = (Val.cmpf (swap_comparison cmp) v2 v1).
+Proof.
+  intros. unfold Val.cmpf. unfold Val.cmpf_bool. destruct v1; destruct v2; auto.
+  rewrite Float.cmp_swap. auto.
+Qed.
+
+Lemma swap_comparison_cmpf_bool:
+  forall cmp ft v1 v2,
+  ftest_for_cmp cmp = Reversed ft ->
+  Val.cmpf_bool cmp v1 v2 = Val.cmpf_bool (swap_comparison cmp) v2 v1.
+Proof.
+  intros. unfold Val.cmpf_bool. destruct v1; destruct v2; auto. rewrite Float.cmp_swap. reflexivity.
+Qed.
+
+Lemma transl_compf_correct:
+  forall cmp r1 r2 lbl k rs m tbb b,
+  exists rs',
+     exec_straight ge (transl_comp_float64 cmp r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
+  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
+  /\ ( Val.cmpf_bool cmp rs#r1 rs#r2 = Some b ->
+       exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
+        = eval_branch fn lbl (nextblock tbb rs') m (Some b))
+  .
+Proof.
+  intros. unfold transl_comp_float64. destruct (ftest_for_cmp cmp) eqn:FT.
+  * esplit. split.
+    - apply exec_straight_one; simpl; eauto.
+    - split.
+      + intros; Simpl.
+      + intros. remember (rs # RTMP <- (compare_float _ _ _)) as rs'.
+        simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+        { 
+          assert ((nextblock tbb rs') # RTMP = (compare_float ft (rs r1) (rs r2))).
+          { rewrite Heqrs'. auto. }
+          rewrite H0. rewrite <- H.
+          remember (Val.cmpf_bool cmp rs#r1 rs#r2) as cmpbool.
+          destruct cmp; simpl;
+          unfold compare_float;
+          unfold Val.cmpf; simpl in FT; inversion FT; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
+          destruct b0; simpl; auto.
+        }
+        rewrite H0. simpl; auto.
+  * esplit. split.
+    - apply exec_straight_one; simpl; eauto.
+    - split.
+      + intros; Simpl.
+      + intros. remember (rs # RTMP <- (compare_float _ _ _)) as rs'.
+        simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+        { 
+          assert ((nextblock tbb rs') # RTMP = (compare_float ft (rs r2) (rs r1))).
+          { rewrite Heqrs'. auto. }
+          rewrite H0. rewrite <- H.
+          remember (Val.cmpf_bool cmp rs#r1 rs#r2) as cmpbool.
+          erewrite swap_comparison_cmpf_bool in Heqcmpbool; eauto.
+          destruct cmp; simpl;
+          unfold compare_float;
+          unfold Val.cmpf; simpl in FT; inversion FT; simpl in Heqcmpbool; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
+          destruct b0; simpl; auto.
+        }
+        rewrite H0. simpl; auto.
+Qed.
+
+Lemma cmpf_bool_ne_eq:
+  forall v1 v2,
+  Val.cmpf_bool Cne v1 v2 = option_map negb (Val.cmpf_bool Ceq v1 v2).
+Proof.
+  intros. unfold Val.cmpf_bool. destruct v1; destruct v2; auto. rewrite Float.cmp_ne_eq. simpl. reflexivity.
+Qed.
+
+Lemma cmpf_bool_ne_eq_rev:
+  forall v1 v2,
+  Val.cmpf_bool Ceq v1 v2 = option_map negb (Val.cmpf_bool Cne v1 v2).
+Proof.
+  intros. unfold Val.cmpf_bool. destruct v1; destruct v2; auto. rewrite Float.cmp_ne_eq. simpl. rewrite negb_involutive. reflexivity.
+Qed.
+
+Lemma option_map_negb_negb:
+  forall v,
+  option_map negb (option_map negb v) = v.
+Proof.
+  destruct v; simpl; auto. rewrite negb_involutive. reflexivity.
+Qed.
+
+Lemma notbool_option_map_negb:
+  forall v, Val.notbool (Val.of_optbool v) = Val.of_optbool (option_map negb v).
+Proof.
+  unfold Val.notbool. unfold Val.of_optbool.
+  destruct v; auto. destruct b; auto.
+Qed.
+
+Lemma swap_comparison_cmpf_bool_notftest:
+  forall cmp ft v1 v2,
+  notftest_for_cmp cmp = Reversed ft ->
+  Val.cmpf_bool cmp v1 v2 = Val.cmpf_bool (swap_comparison cmp) v2 v1.
+Proof.
+  intros. unfold Val.cmpf_bool. destruct v1; destruct v2; auto. rewrite Float.cmp_swap. reflexivity.
+Qed.
+
+Lemma transl_compnotf_correct:
+  forall cmp r1 r2 lbl k rs m tbb b,
+  exists rs',
+     exec_straight ge (transl_comp_notfloat64 cmp r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
+  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
+  /\   (option_map negb (Val.cmpf_bool cmp rs#r1 rs#r2) = Some b ->
+       exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
+        = eval_branch fn lbl (nextblock tbb rs') m (Some b))
+  .
+Proof.
+  intros. unfold transl_comp_notfloat64. destruct (notftest_for_cmp cmp) eqn:FT.
+  * esplit. split.
+    - apply exec_straight_one; simpl; eauto.
+    - split.
+      + intros; Simpl.
+      + intros. remember (rs # RTMP <- (compare_float _ _ _)) as rs'.
+        simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+        { 
+          assert ((nextblock tbb rs') # RTMP = (compare_float ft (rs r1) (rs r2))).
+          { rewrite Heqrs'. auto. }
+          rewrite H0. rewrite <- H.
+          remember (option_map negb (Val.cmpf_bool cmp rs#r1 rs#r2)) as cmpbool.
+          destruct cmp; simpl;
+          unfold compare_float;
+          unfold Val.cmpf; simpl in FT; inversion FT.
+          * rewrite cmpf_bool_ne_eq; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+          * rewrite cmpf_bool_ne_eq_rev. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+          * rewrite notbool_option_map_negb. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+          * rewrite notbool_option_map_negb. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+        }
+        rewrite H0. simpl; auto.
+  * esplit. split.
+    - apply exec_straight_one; simpl; eauto.
+    - split.
+      + intros; Simpl.
+      + intros. remember (rs # RTMP <- (compare_float _ _ _)) as rs'.
+        simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+        { 
+          assert ((nextblock tbb rs') # RTMP = (compare_float ft (rs r2) (rs r1))).
+          { rewrite Heqrs'. auto. }
+          rewrite H0. rewrite <- H.
+          remember (Val.cmpf_bool cmp rs#r1 rs#r2) as cmpbool.
+          erewrite swap_comparison_cmpf_bool_notftest in Heqcmpbool; eauto.
+          destruct cmp; simpl;
+          unfold compare_float;
+          unfold Val.cmpf; simpl in FT; inversion FT; simpl in Heqcmpbool.
+          * rewrite notbool_option_map_negb. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+          * rewrite notbool_option_map_negb. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+        }
+        rewrite H0. simpl; auto.
+Qed.
+
+Lemma swap_comparison_cmpfs_bool:
+  forall cmp ft v1 v2,
+  ftest_for_cmp cmp = Reversed ft ->
+  Val.cmpfs_bool cmp v1 v2 = Val.cmpfs_bool (swap_comparison cmp) v2 v1.
+Proof.
+  intros. unfold Val.cmpfs_bool. destruct v1; destruct v2; auto. rewrite Float32.cmp_swap. reflexivity.
+Qed.
+
+Lemma transl_compfs_correct:
+  forall cmp r1 r2 lbl k rs m tbb b,
+  exists rs',
+     exec_straight ge (transl_comp_float32 cmp r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
+  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
+  /\ ( Val.cmpfs_bool cmp rs#r1 rs#r2 = Some b ->
+       exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
+        = eval_branch fn lbl (nextblock tbb rs') m (Some b))
+  .
+Proof.
+  intros. unfold transl_comp_float32. destruct (ftest_for_cmp cmp) eqn:FT.
+  * esplit. split.
+    - apply exec_straight_one; simpl; eauto.
+    - split.
+      + intros; Simpl.
+      + intros. remember (rs # RTMP <- (compare_single _ _ _)) as rs'.
+        simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+        { 
+          assert ((nextblock tbb rs') # RTMP = (compare_single ft (rs r1) (rs r2))).
+          { rewrite Heqrs'. auto. }
+          rewrite H0. rewrite <- H.
+          remember (Val.cmpfs_bool cmp rs#r1 rs#r2) as cmpbool.
+          destruct cmp; simpl;
+          unfold compare_single;
+          unfold Val.cmpfs; simpl in FT; inversion FT; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
+          destruct b0; simpl; auto.
+        }
+        rewrite H0. simpl; auto.
+  * esplit. split.
+    - apply exec_straight_one; simpl; eauto.
+    - split.
+      + intros; Simpl.
+      + intros. remember (rs # RTMP <- (compare_single _ _ _)) as rs'.
+        simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+        { 
+          assert ((nextblock tbb rs') # RTMP = (compare_single ft (rs r2) (rs r1))).
+          { rewrite Heqrs'. auto. }
+          rewrite H0. rewrite <- H.
+          remember (Val.cmpfs_bool cmp rs#r1 rs#r2) as cmpbool.
+          erewrite swap_comparison_cmpfs_bool in Heqcmpbool; eauto.
+          destruct cmp; simpl;
+          unfold compare_single;
+          unfold Val.cmpfs; simpl in FT; inversion FT; simpl in Heqcmpbool; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
+          destruct b0; simpl; auto.
+        }
+        rewrite H0. simpl; auto.
+Qed.
+
+Lemma swap_comparison_cmpfs_bool_notftest:
+  forall cmp ft v1 v2,
+  notftest_for_cmp cmp = Reversed ft ->
+  Val.cmpfs_bool cmp v1 v2 = Val.cmpfs_bool (swap_comparison cmp) v2 v1.
+Proof.
+  intros. unfold Val.cmpfs_bool. destruct v1; destruct v2; auto. rewrite Float32.cmp_swap. reflexivity.
+Qed.
+
+Lemma cmpfs_bool_ne_eq:
+  forall v1 v2,
+  Val.cmpfs_bool Cne v1 v2 = option_map negb (Val.cmpfs_bool Ceq v1 v2).
+Proof.
+  intros. unfold Val.cmpfs_bool. destruct v1; destruct v2; auto. rewrite Float32.cmp_ne_eq. simpl. reflexivity.
+Qed.
+
+Lemma cmpfs_bool_ne_eq_rev:
+  forall v1 v2,
+  Val.cmpfs_bool Ceq v1 v2 = option_map negb (Val.cmpfs_bool Cne v1 v2).
+Proof.
+  intros. unfold Val.cmpfs_bool. destruct v1; destruct v2; auto. rewrite Float32.cmp_ne_eq. simpl. rewrite negb_involutive. reflexivity.
+Qed.
+
+Lemma transl_compnotfs_correct:
+  forall cmp r1 r2 lbl k rs m tbb b,
+  exists rs',
+     exec_straight ge (transl_comp_notfloat32 cmp r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
+  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
+  /\   (option_map negb (Val.cmpfs_bool cmp rs#r1 rs#r2) = Some b ->
+       exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
+        = eval_branch fn lbl (nextblock tbb rs') m (Some b))
+  .
+Proof.
+  intros. unfold transl_comp_notfloat32. destruct (notftest_for_cmp cmp) eqn:FT.
+  * esplit. split.
+    - apply exec_straight_one; simpl; eauto.
+    - split.
+      + intros; Simpl.
+      + intros. remember (rs # RTMP <- (compare_single _ _ _)) as rs'.
+        simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+        { 
+          assert ((nextblock tbb rs') # RTMP = (compare_single ft (rs r1) (rs r2))).
+          { rewrite Heqrs'. auto. }
+          rewrite H0. rewrite <- H.
+          remember (option_map negb (Val.cmpfs_bool cmp rs#r1 rs#r2)) as cmpbool.
+          destruct cmp; simpl;
+          unfold compare_single;
+          unfold Val.cmpfs; simpl in FT; inversion FT.
+          * rewrite cmpfs_bool_ne_eq; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+          * rewrite cmpfs_bool_ne_eq_rev. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+          * rewrite notbool_option_map_negb. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+          * rewrite notbool_option_map_negb. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+        }
+        rewrite H0. simpl; auto.
+  * esplit. split.
+    - apply exec_straight_one; simpl; eauto.
+    - split.
+      + intros; Simpl.
+      + intros. remember (rs # RTMP <- (compare_single _ _ _)) as rs'.
+        simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+        { 
+          assert ((nextblock tbb rs') # RTMP = (compare_single ft (rs r2) (rs r1))).
+          { rewrite Heqrs'. auto. }
+          rewrite H0. rewrite <- H.
+          remember (Val.cmpfs_bool cmp rs#r1 rs#r2) as cmpbool.
+          erewrite swap_comparison_cmpfs_bool_notftest in Heqcmpbool; eauto.
+          destruct cmp; simpl;
+          unfold compare_single;
+          unfold Val.cmpfs; simpl in FT; inversion FT; simpl in Heqcmpbool.
+          * rewrite notbool_option_map_negb. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+          * rewrite notbool_option_map_negb. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+        }
+        rewrite H0. simpl; auto.
+Qed.
+
 Lemma transl_complu_correct:
   forall cmp r1 r2 lbl k rs m tbb b,
   exists rs',
@@ -753,6 +1033,34 @@ Proof.
     * split; auto.
       { apply C'; auto. rewrite B, C; eauto with asmgen. }
       { intros. rewrite B'; eauto with asmgen. }
+
+(* Ccompf *)
+- exploit (transl_compf_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C).
+  exists rs', (Pcb BTwnez RTMP lbl).
+  split.
+  + constructor. eexact A.
+  + split; auto. apply C; auto.
+
+(* Cnotcompf *)
+- exploit (transl_compnotf_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C).
+  exists rs', (Pcb BTwnez RTMP lbl).
+  split.
+  + constructor. eexact A.
+  + split; auto. apply C; auto.
+
+(* Ccompfs *)
+- exploit (transl_compfs_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C).
+  exists rs', (Pcb BTwnez RTMP lbl).
+  split.
+  + constructor. eexact A.
+  + split; auto. apply C; auto.
+
+(* Cnotcompfs *)
+- exploit (transl_compnotfs_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C).
+  exists rs', (Pcb BTwnez RTMP lbl).
+  split.
+  + constructor. eexact A.
+  + split; auto. apply C; auto.
 Qed.
 
 Lemma transl_cbranch_correct_true:
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index db50e3a5..b4b87031 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -135,11 +135,20 @@ let load_str = function
 let set_str = "Pset"
 let get_str = "Pget"
 
-let arith_rri32_rec i rd rs imm32 = { inst = arith_rri32_str i; write_locs = [Reg rd]; read_locs = [Reg rs]; imm = imm32; is_control = false }
+let arith_rri32_rec i rd rs imm32 = 
+  match i with
+  | Pcompiw _ -> { inst = arith_rri32_str i; write_locs = [Reg rd]; read_locs = [Reg rs; Mem]; imm = imm32; is_control = false }
+  | _ -> { inst = arith_rri32_str i; write_locs = [Reg rd]; read_locs = [Reg rs]; imm = imm32; is_control = false }
 
-let arith_rri64_rec i rd rs imm64 = { inst = arith_rri64_str i; write_locs = [Reg rd]; read_locs = [Reg rs]; imm = imm64; is_control = false }
+let arith_rri64_rec i rd rs imm64 =
+  match i with
+  | Pcompil _ -> { inst = arith_rri64_str i; write_locs = [Reg rd]; read_locs = [Reg rs; Mem]; imm = imm64; is_control = false } 
+  | _ -> { inst = arith_rri64_str i; write_locs = [Reg rd]; read_locs = [Reg rs]; imm = imm64; is_control = false }
 
-let arith_rrr_rec i rd rs1 rs2 = { inst = arith_rrr_str i; write_locs = [Reg rd]; read_locs = [Reg rs1; Reg rs2]; imm = None; is_control = false}
+let arith_rrr_rec i rd rs1 rs2 =  (* FIXME - hack for memory problem with Pcompw and Pcompl, performance decreased *)
+  match i with
+  | Pcompw _ | Pcompl _ -> { inst = arith_rrr_str i; write_locs = [Reg rd]; read_locs = [Reg rs1; Reg rs2; Mem]; imm = None; is_control = false}
+  | _ -> { inst = arith_rrr_str i; write_locs = [Reg rd]; read_locs = [Reg rs1; Reg rs2]; imm = None; is_control = false}
 
 let arith_rr_rec i rd rs = { inst = arith_rr_str i; write_locs = [Reg rd]; read_locs = [Reg rs]; imm = None; is_control = false}