Fix minor proof

3 files changed, 142 insertions, 27 deletions

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 76404257..b3519064 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -427,6 +427,69 @@ Proof.
     rewrite H0. simpl; auto.
 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. Admitted.
+(*   intros. esplit. split.
+- unfold transl_compl. apply exec_straight_one; simpl; eauto.
+- split.
+  + intros; Simpl.
+  + intros.
+    remember (rs # RTMP <- (compare_long (itest_for_cmp cmp Signed) rs # r1 rs # r2 m)) as rs'.
+    simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+    { 
+      assert ((nextblock tbb rs') # RTMP = (compare_long (itest_for_cmp cmp Signed) rs # r1 rs # r2 m)).
+      { rewrite Heqrs'. auto. }
+      rewrite H0. rewrite <- H.
+      remember (Val.cmpl_bool cmp rs#r1 rs#r2) as cmpbool.
+      destruct cmp; simpl;
+      unfold compare_long;
+      unfold Val.cmpl; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
+      destruct b0; simpl; auto.
+    }
+    rewrite H0. simpl; auto.
+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. Admitted.
+
+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. Admitted.
+
+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. Admitted.
+
 Lemma transl_complu_correct:
   forall cmp r1 r2 lbl k rs m tbb b,
   exists rs',
@@ -751,6 +814,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: