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

1 files changed, 49 insertions, 0 deletions

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)