Implemented float comparisons (no branching yet, and no negation)

8 files changed, 132 insertions, 29 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index dcce98d0..49f2d23c 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -131,6 +131,7 @@ Inductive instruction : Type :=
   (** Arith RRR *)

   | Pcompw  (it: itest) (rd rs1 rs2: ireg)          (**r comparison word *)

   | Pcompl  (it: itest) (rd rs1 rs2: ireg)          (**r comparison long *)

+  | Pfcompw (ft: ftest) (rd rs1 rs2: ireg)          (**r comparison float *)

 

   | Paddw               (rd rs1 rs2: ireg)          (**r add word *)

   | Psubw               (rd rs1 rs2: ireg)          (**r sub word *)

@@ -251,6 +252,7 @@ Definition basic_to_instruction (b: basic) :=
   (* RRR *)

   | PArithRRR (Asmblock.Pcompw it) rd rs1 rs2 => Pcompw it rd rs1 rs2

   | PArithRRR (Asmblock.Pcompl it) rd rs1 rs2 => Pcompl it rd rs1 rs2

+  | PArithRRR (Asmblock.Pfcompw ft) rd rs1 rs2 => Pfcompw ft rd rs1 rs2

   | PArithRRR Asmblock.Paddw rd rs1 rs2       => Paddw rd rs1 rs2

   | PArithRRR Asmblock.Psubw rd rs1 rs2       => Psubw rd rs1 rs2

   | PArithRRR Asmblock.Pmulw rd rs1 rs2       => Pmulw rd rs1 rs2

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 54bf247f..274d90a1 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -126,6 +126,17 @@ Inductive itest: Type :=
   | ITnone                              (**r Not Any Bits Set in Mask *)
   .
 
+Inductive ftest: Type :=
+  | FTone                               (**r Ordered and Not Equal *)
+  | FTueq                               (**r Unordered or Equal *)
+  | FToeq                               (**r Ordered and Equal *)
+  | FTune                               (**r Unordered or Not Equal *)
+  | FTolt                               (**r Ordered and Less Than *)
+  | FTuge                               (**r Unordered or Greater Than or Equal *)
+  | FToge                               (**r Ordered and Greater Than or Equal *)
+  | FTult                               (**r Unordered or Less Than *)
+  .
+
 (** Offsets for load and store instructions.  An offset is either an
   immediate integer or the low part of a symbol. *)
 
@@ -320,6 +331,7 @@ Inductive arith_name_rf64 : Type :=
 Inductive arith_name_rrr : Type :=
   | Pcompw  (it: itest)                             (**r comparison word *)
   | Pcompl  (it: itest)                             (**r comparison long *)
+  | Pfcompw (it: ftest)                             (**r comparison float32 *)
 
   | Paddw                                           (**r add word *)
   | Psubw                                           (**r sub word *)
@@ -816,6 +828,31 @@ Definition itest_for_cmp (c: comparison) (s: signedness) :=
   | Cgt, Unsigned => ITgtu
   end.
 
+Inductive oporder_ftest :=
+  | Normal (ft: ftest)
+  | Reversed (ft: ftest)
+.
+
+Definition ftest_for_cmp (c: comparison) :=
+  match c with
+  | Ceq => Normal FToeq
+  | Cne => Normal FTune
+  | Clt => Normal FTolt
+  | Cle => Reversed FToge
+  | Cgt => Reversed FTolt
+  | Cge => Normal FToge
+  end.
+
+Definition notftest_for_cmp (c: comparison) :=
+  match c with
+  | Ceq => Normal FTune
+  | Cne => Normal FToeq
+  | Clt => Normal FTuge
+  | Cle => Reversed FTult
+  | Cgt => Reversed FTuge
+  | Cge => Normal FTult
+  end.
+
 (* CoMPare Signed Words to Zero *)
 Definition btest_for_cmpswz (c: comparison) :=
   match c with
@@ -910,6 +947,17 @@ Definition compare_long (t: itest) (v1 v2: val) (m: mem): val :=
   end
   .
 
+Definition compare_single (t: ftest) (v1 v2: val): val :=
+  match t with
+  | FTone | FTueq => Vundef (* unused *)
+  | FToeq => Val.cmpfs Ceq v1 v2
+  | FTune => Val.cmpfs Cne v1 v2
+  | FTolt => Val.cmpfs Clt v1 v2
+  | FTuge => Val.notbool (Val.cmpfs Clt v1 v2)
+  | FToge => Val.cmpfs Cge v1 v2
+  | FTult => Val.notbool (Val.cmpfs Cge v1 v2)
+  end.
+
 (** Execution of arith instructions 
 
 TODO: subsplitting by instruction type ? Could be useful for expressing auxiliary lemma...
@@ -980,6 +1028,7 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset) (m: mem) : regset
       match n with
       | Pcompw c => rs#d <- (compare_int c rs#s1 rs#s2 m)
       | Pcompl c => rs#d <- (compare_long c rs#s1 rs#s2 m)
+      | Pfcompw c => rs#d <- (compare_single c rs#s1 rs#s2)
       | Paddw  => rs#d <- (Val.add  rs#s1 rs#s2)
       | Psubw  => rs#d <- (Val.sub  rs#s1 rs#s2)
       | Pmulw  => rs#d <- (Val.mul  rs#s1 rs#s2)
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 67ca94e2..69d3d0cc 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -159,6 +159,8 @@ Definition arith_eval (ao: arith_op) (l: list value) :=
 
   | OArithRRR n, [Val v1; Val v2] =>
       match n with
+      | Pfcompw c => Some (Val (compare_single c v1 v2))
+
       | Paddw  => Some (Val (Val.add  v1 v2))
       | Psubw  => Some (Val (Val.sub  v1 v2))
       | Pmulw  => Some (Val (Val.mul  v1 v2))
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 56d061c2..fb6ba16e 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -282,6 +282,18 @@ 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
+  | Reversed ft => Pfcompw ft rd r2 r1 ::i k
+  end.
+
+Definition transl_cond_notfloat32 (cmp: comparison) (rd r1 r2: ireg) (k: bcode) :=
+  match notftest_for_cmp cmp with
+  | Normal ft => Pfcompw ft rd r1 r2 ::i k
+  | Reversed ft => Pfcompw ft rd r2 r1 ::i k
+  end.
+
 Definition transl_cond_op
            (cond: condition) (rd: ireg) (args: list mreg) (k: bcode) :=
   match cond, args with
@@ -309,10 +321,14 @@ Definition transl_cond_op
   | Ccompluimm c n, a1 :: nil =>
       do r1 <- ireg_of a1;
       OK (transl_condimm_int64u c rd r1 n k)
+  | 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 =>
+      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 *)
   | Ccompf _, _ => Error(msg "Asmblockgen.transl_cond_op: Ccompf")
   | Cnotcompf _, _ => Error(msg "Asmblockgen.transl_cond_op: Cnotcompf")
-  | Ccompfs _, _ => Error(msg "Asmblockgen.transl_cond_op: Ccompfs")
-  | Cnotcompfs _, _ => Error(msg "Asmblockgen.transl_cond_op: Cnotcompfs")
 (*| 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
@@ -388,13 +404,7 @@ Definition transl_op
       OK (Pmulw rd rs1 rs2 ::i k)
   | Omulhs, _ => Error(msg "Asmblockgen.transl_op: Omulhs")
   | Omulhu, _ => Error(msg "Asmblockgen.transl_op: Omulhu")
-(*| Omulhs, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pmulhw rd rs1 rs2 :: k)
-  | Omulhu, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pmulhuw rd rs1 rs2 :: k)
-*)| Odiv, a1 :: a2 :: nil => Error(msg "Asmblockgen.transl_op: Odiv: 32-bits division not supported yet. Please use 64-bits.")
+  | Odiv, a1 :: a2 :: nil => Error(msg "Asmblockgen.transl_op: Odiv: 32-bits division not supported yet. Please use 64-bits.")
       (* do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pdivw rd rs1 rs2 :: k) *)
   | Odivu, a1 :: a2 :: nil => Error(msg "Asmblockgen.transl_op: Odivu: 32-bits division not supported yet. Please use 64-bits.")
@@ -483,25 +493,7 @@ Definition transl_op
   | Odivlu, _ => Error (msg "Asmblockgen.transl_op: Odivlu")
   | Omodl, _ => Error (msg "Asmblockgen.transl_op: Omodl")
   | Omodlu, _ => Error (msg "Asmblockgen.transl_op: Omodlu")
-(*| Omullhs, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pmulhl rd rs1 rs2 :: k)
-  | Omullhu, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pmulhul rd rs1 rs2 :: k)
-  | Odivl, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pdivl rd rs1 rs2 :: k)
-  | Odivlu, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pdivul rd rs1 rs2 :: k)
-  | Omodl, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Preml rd rs1 rs2 :: k)
-  | Omodlu, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Premul rd rs1 rs2 :: k)
-*)| Oandl, a1 :: a2 :: nil =>
+  | Oandl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pandl rd rs1 rs2 ::i k)
   | Oandlimm n, a1 :: nil =>
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index 9cba8402..2b79c78e 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -950,6 +950,7 @@ Proof.
   - simpl in TIB. monadInv TIB. unfold loadind in EQ. exploreInst; try discriminate.

   - 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.

   - 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 175eca73..f7207c88 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -968,6 +968,36 @@ Proof.
   split; intros; Simpl.
 Qed.
 
+Lemma swap_comparison_cmpfs:
+  forall v1 v2 cmp,
+  Val.lessdef (Val.cmpfs cmp v1 v2) (Val.cmpfs (swap_comparison cmp) v2 v1).
+Proof.
+  intros. unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct v1; destruct v2; auto.
+  rewrite Float32.cmp_swap. auto.
+Qed.
+
+Lemma transl_cond_float32_correct:
+  forall cmp rd r1 r2 k rs m,
+  exists rs',
+     exec_straight ge (basics_to_code (transl_cond_float32 cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m
+  /\ Val.lessdef (Val.cmpfs 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.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl. apply swap_comparison_cmpfs.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl. apply swap_comparison_cmpfs.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+Qed.
+
 Lemma transl_cond_op_correct:
   forall cond rd args k c rs m,
   transl_cond_op cond rd args k = OK c ->
@@ -1003,6 +1033,8 @@ 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 *) 
+  exploit transl_cond_float32_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto.
 Qed.
 
 (*
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index c3473b9f..d9c22666 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -55,6 +55,7 @@ let arith_rr_str = function
 let arith_rrr_str = function
   | Pcompw it -> "Pcompw"
   | Pcompl it -> "Pcompl"
+  | Pfcompw ft -> "Pfcompw"
   | Paddw -> "Paddw"
   | Psubw -> "Psubw"
   | Pmulw -> "Pmulw"
@@ -305,6 +306,10 @@ let alu_lite : int array = let resmap = fun r -> match r with
   | "ISSUE" -> 1 | "TINY" -> 1 | "LITE" -> 1 |  _ -> 0 
   in Array.of_list (List.map resmap resource_names)
 
+let alu_lite_x : int array = let resmap = fun r -> match r with 
+  | "ISSUE" -> 2 | "TINY" -> 1 | "LITE" -> 1 |  _ -> 0 
+  in Array.of_list (List.map resmap resource_names)
+
 let alu_full : int array = let resmap = fun r -> match r with
   | "ISSUE" -> 1 | "TINY" -> 1 | "LITE" -> 1 | "ALU" -> 1 | _ -> 0
   in Array.of_list (List.map resmap resource_names)
@@ -373,6 +378,7 @@ type real_instruction =
   | Fabsd | Fabsw | Fnegw | Fnegd
   | Faddd | Faddw | Fsbfd | Fsbfw | Fmuld | Fmulw
   | Fnarrowdw | Fwidenlwd | Floatwz | Floatuwz | Floatdz | Floatudz | Fixedwz | Fixeduwz | Fixeddz | Fixedudz
+  | Fcompw
 
 let ab_inst_to_real = function
   | "Paddw" | "Paddiw" | "Pcvtl2w" -> Addw
@@ -381,6 +387,7 @@ let ab_inst_to_real = function
   | "Pandl" | "Pandil" -> Andd
   | "Pcompw" | "Pcompiw" -> Compw
   | "Pcompl" | "Pcompil" -> Compd
+  | "Pfcompw" -> Fcompw
   | "Pmulw" -> Mulw
   | "Pmull" -> Muld
   | "Porw" | "Poriw" -> Orw
@@ -470,6 +477,9 @@ let rec_to_usage r =
   | Compd -> (match encoding with None | Some U6 | Some S10 -> alu_tiny
                                 | Some U27L5 | Some U27L10 -> alu_tiny_x
                                 | Some E27U27L10 -> alu_tiny_y)
+  | Fcompw -> (match encoding with None -> alu_lite
+                                | Some U6 | Some S10 | Some U27L5 -> alu_lite_x
+                                | _ -> raise InvalidEncoding)
   | Make -> (match encoding with Some U6 | Some S10 -> alu_tiny 
                           | Some U27L5 | Some U27L10 -> alu_tiny_x 
                           | Some E27U27L10 -> alu_tiny_y 
@@ -502,7 +512,7 @@ let real_inst_to_latency = function
   | Nop -> 0 (* Only goes through ID *)
   | Addw | Andw | Compw | Orw | Sbfw | Sraw | Srlw | Sllw | Xorw
   | Addd | Andd | Compd | Ord | Sbfd | Srad | Srld | Slld | Xord | Make
-  | Sxwd | Zxwd
+  | Sxwd | Zxwd | Fcompw
         -> 1
   | Floatwz | Floatuwz | Fixeduwz | Fixedwz | Floatdz | Floatudz | Fixeddz | Fixedudz -> 4
   | Mulw | Muld -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *)
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index acb128de..ac2e3b27 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -173,6 +173,18 @@ module Target (*: TARGET*) =
       | ITnone -> "none"
 
     let icond oc c = fprintf oc "%s" (icond_name c)
+
+    let fcond_name = let open Asmblock in function
+      | FTone -> "one"
+      | FTueq -> "ueq"
+      | FToeq -> "oeq"
+      | FTune -> "une"
+      | FTolt -> "olt"
+      | FTuge -> "uge"
+      | FToge -> "oge"
+      | FTult -> "ult"
+
+    let fcond oc c = fprintf oc "%s" (fcond_name c)
   
     let bcond_name = let open Asmblock in function
       | BTwnez -> "wnez"
@@ -345,6 +357,9 @@ module Target (*: TARGET*) =
       | Pcompl (it, rd, rs1, rs2) ->
          fprintf oc "	compd.%a	%a = %a, %a\n" icond it ireg rd ireg rs1 ireg rs2
 
+      | Pfcompw (ft, rd, rs1, rs2) ->
+         fprintf oc "	fcompw.%a	%a = %a, %a\n" fcond ft ireg rd ireg rs1 ireg rs2
+
       | Paddw (rd, rs1, rs2) ->
          fprintf oc "	addw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
       | Psubw (rd, rs1, rs2) ->