Switch floating-point comparisons to using softfloat to avoid missed corner-cases in hand-rolled helpers.

8 files changed, 199 insertions, 55 deletions

diff --git a/c_emulator/riscv_softfloat.c b/c_emulator/riscv_softfloat.c
index d0f8069..3556616 100644
--- a/c_emulator/riscv_softfloat.c
+++ b/c_emulator/riscv_softfloat.c
@@ -397,3 +397,81 @@ unit softfloat_f64tof32(mach_bits rm, mach_bits v) {
 
   return UNIT;
 }
+
+unit softfloat_f32lt(mach_bits v1, mach_bits v2) {
+  SOFTFLOAT_PRELUDE(0);
+
+  float32_t a, b, res;
+  a.v = v1;
+  b.v = v2;
+  res.v = f32_lt(a, b);
+
+  SOFTFLOAT_POSTLUDE(res);
+
+  return UNIT;
+}
+
+unit softfloat_f32le(mach_bits v1, mach_bits v2) {
+  SOFTFLOAT_PRELUDE(0);
+
+  float32_t a, b, res;
+  a.v = v1;
+  b.v = v2;
+  res.v = f32_le(a, b);
+
+  SOFTFLOAT_POSTLUDE(res);
+
+  return UNIT;
+}
+
+unit softfloat_f32eq(mach_bits v1, mach_bits v2) {
+  SOFTFLOAT_PRELUDE(0);
+
+  float32_t a, b, res;
+  a.v = v1;
+  b.v = v2;
+  res.v = f32_eq(a, b);
+
+  SOFTFLOAT_POSTLUDE(res);
+
+  return UNIT;
+}
+
+unit softfloat_f64lt(mach_bits v1, mach_bits v2) {
+  SOFTFLOAT_PRELUDE(0);
+
+  float64_t a, b, res;
+  a.v = v1;
+  b.v = v2;
+  res.v = f64_lt(a, b);
+
+  SOFTFLOAT_POSTLUDE(res);
+
+  return UNIT;
+}
+
+unit softfloat_f64le(mach_bits v1, mach_bits v2) {
+  SOFTFLOAT_PRELUDE(0);
+
+  float64_t a, b, res;
+  a.v = v1;
+  b.v = v2;
+  res.v = f64_le(a, b);
+
+  SOFTFLOAT_POSTLUDE(res);
+
+  return UNIT;
+}
+
+unit softfloat_f64eq(mach_bits v1, mach_bits v2) {
+  SOFTFLOAT_PRELUDE(0);
+
+  float64_t a, b, res;
+  a.v = v1;
+  b.v = v2;
+  res.v = f64_eq(a, b);
+
+  SOFTFLOAT_POSTLUDE(res);
+
+  return UNIT;
+}
diff --git a/c_emulator/riscv_softfloat.h b/c_emulator/riscv_softfloat.h
index bd7edf0..57ae0f2 100644
--- a/c_emulator/riscv_softfloat.h
+++ b/c_emulator/riscv_softfloat.h
@@ -38,3 +38,10 @@ unit softfloat_ui64tof64(mach_bits rm, mach_bits v);
 
 unit softfloat_f32tof64(mach_bits rm, mach_bits v);
 unit softfloat_f64tof32(mach_bits rm, mach_bits v);
+
+unit softfloat_f32lt(mach_bits v1, mach_bits v2);
+unit softfloat_f32le(mach_bits v1, mach_bits v2);
+unit softfloat_f32eq(mach_bits v1, mach_bits v2);
+unit softfloat_f64lt(mach_bits v1, mach_bits v2);
+unit softfloat_f64le(mach_bits v1, mach_bits v2);
+unit softfloat_f64eq(mach_bits v1, mach_bits v2);
diff --git a/handwritten_support/0.11/riscv_extras_fdext.lem b/handwritten_support/0.11/riscv_extras_fdext.lem
index 3c79089..12cfe00 100644
--- a/handwritten_support/0.11/riscv_extras_fdext.lem
+++ b/handwritten_support/0.11/riscv_extras_fdext.lem
@@ -106,4 +106,20 @@ val softfloat_f64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> b
 let softfloat_f64_to_f32 _ _ = ()
 
 
+val softfloat_f32_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+let softfloat_f32_lt _ _ = ()
 
+val softfloat_f32_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+let softfloat_f32_le _ _ = ()
+
+val softfloat_f32_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+let softfloat_f32_eq _ _ = ()
+
+val softfloat_f64_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+let softfloat_f64_lt _ _ = ()
+
+val softfloat_f64_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+let softfloat_f64_le _ _ = ()
+
+val softfloat_f64_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+let softfloat_f64_eq _ _ = ()
diff --git a/handwritten_support/riscv_extras_fdext.lem b/handwritten_support/riscv_extras_fdext.lem
index 3c79089..12cfe00 100644
--- a/handwritten_support/riscv_extras_fdext.lem
+++ b/handwritten_support/riscv_extras_fdext.lem
@@ -106,4 +106,20 @@ val softfloat_f64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> b
 let softfloat_f64_to_f32 _ _ = ()
 
 
+val softfloat_f32_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+let softfloat_f32_lt _ _ = ()
 
+val softfloat_f32_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+let softfloat_f32_le _ _ = ()
+
+val softfloat_f32_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+let softfloat_f32_eq _ _ = ()
+
+val softfloat_f64_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+let softfloat_f64_lt _ _ = ()
+
+val softfloat_f64_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+let softfloat_f64_le _ _ = ()
+
+val softfloat_f64_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+let softfloat_f64_eq _ _ = ()
diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail
index 4fcf7b1..d1d1fca 100644
--- a/model/riscv_insts_dext.sail
+++ b/model/riscv_insts_dext.sail
@@ -720,15 +720,10 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D)) = {
   let rs1_val_D = F(rs1);
   let rs2_val_D = F(rs2);
 
-  let (rs1_eq_rs2, fflags) = feq_quiet_D (rs1_val_D, rs2_val_D);
+  let (fflags, rd_val) : (bits_fflags, bits_LU) =
+      riscv_f64Eq (rs1_val_D, rs2_val_D);
 
-  let rd_val : xlenbits =
-      if      (f_is_SNaN_D(rs1_val_D) | f_is_SNaN_D(rs2_val_D)) then zeros()
-      else if (f_is_QNaN_D(rs1_val_D) | f_is_QNaN_D(rs2_val_D)) then zeros()
-      else if rs1_eq_rs2                                        then EXTZ(0b1)
-      else                                                           zeros();
-
-  accrue_fflags(fflags);
+  write_fflags(fflags);
   X(rd) = rd_val;
   RETIRE_SUCCESS
 }
@@ -737,16 +732,10 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLT_D)) = {
   let rs1_val_D = F(rs1);
   let rs2_val_D = F(rs2);
 
-  let is_quiet  = false;
-  let (rs1_lt_rs2, fflags) = flt_D (rs1_val_D, rs2_val_D, is_quiet);
+  let (fflags, rd_val) : (bits_fflags, bits_LU) =
+      riscv_f64Lt (rs1_val_D, rs2_val_D);
 
-  let rd_val : xlenbits =
-      if      (f_is_SNaN_D(rs1_val_D) | f_is_SNaN_D(rs2_val_D)) then zeros()
-      else if (f_is_QNaN_D(rs1_val_D) | f_is_QNaN_D(rs2_val_D)) then zeros()
-      else if rs1_lt_rs2                                        then EXTZ(0b1)
-      else                                                           zeros();
-
-  accrue_fflags(fflags);
+  write_fflags(fflags);
   X(rd) = rd_val;
   RETIRE_SUCCESS
 }
@@ -755,16 +744,10 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLE_D)) = {
   let rs1_val_D = F(rs1);
   let rs2_val_D = F(rs2);
 
-  let is_quiet  = false;
-  let (rs1_le_rs2, fflags) = fle_D (rs1_val_D, rs2_val_D, is_quiet);
-
-  let rd_val : xlenbits =
-      if      (f_is_SNaN_D(rs1_val_D) | f_is_SNaN_D(rs2_val_D)) then zeros()
-      else if (f_is_QNaN_D(rs1_val_D) | f_is_QNaN_D(rs2_val_D)) then zeros()
-      else if rs1_le_rs2                                        then EXTZ(0b1)
-      else                                                           zeros();
+  let (fflags, rd_val) : (bits_fflags, bits_LU) =
+      riscv_f64Le (rs1_val_D, rs2_val_D);
 
-  accrue_fflags(fflags);
+  write_fflags(fflags);
   X(rd) = rd_val;
   RETIRE_SUCCESS
 }
diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail
index 280389a..34b6c91 100644
--- a/model/riscv_insts_fext.sail
+++ b/model/riscv_insts_fext.sail
@@ -896,16 +896,11 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FEQ_S)) = {
   let rs1_val_S = nan_unbox (F(rs1));
   let rs2_val_S = nan_unbox (F(rs2));
 
-  let (rs1_eq_rs2, fflags) = feq_quiet_S (rs1_val_S, rs2_val_S);
+  let (fflags, rd_val) : (bits_fflags, bits_WU) =
+      riscv_f32Eq (rs1_val_S, rs2_val_S);
 
-  let rd_val : xlenbits =
-      if      (f_is_SNaN_S(rs1_val_S) | f_is_SNaN_S(rs2_val_S)) then zeros()
-      else if (f_is_QNaN_S(rs1_val_S) | f_is_QNaN_S(rs2_val_S)) then zeros()
-      else if rs1_eq_rs2                                        then EXTZ(0b1)
-      else                                                           zeros();
-
-  accrue_fflags(fflags);
-  X(rd) = rd_val;
+  write_fflags(fflags);
+  X(rd) = EXTZ(rd_val);
   RETIRE_SUCCESS
 }
 
@@ -913,17 +908,11 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLT_S)) = {
   let rs1_val_S = nan_unbox (F(rs1));
   let rs2_val_S = nan_unbox (F(rs2));
 
-  let is_quiet  = false;
-  let (rs1_lt_rs2, fflags) = flt_S (rs1_val_S, rs2_val_S, is_quiet);
+  let (fflags, rd_val) : (bits_fflags, bits_WU) =
+      riscv_f32Lt (rs1_val_S, rs2_val_S);
 
-  let rd_val : xlenbits =
-      if      (f_is_SNaN_S(rs1_val_S) | f_is_SNaN_S(rs2_val_S)) then zeros()
-      else if (f_is_QNaN_S(rs1_val_S) | f_is_QNaN_S(rs2_val_S)) then zeros()
-      else if rs1_lt_rs2                                        then EXTZ(0b1)
-      else                                                           zeros();
-
-  accrue_fflags(fflags);
-  X(rd) = rd_val;
+  write_fflags(fflags);
+  X(rd) = EXTZ(rd_val);
   RETIRE_SUCCESS
 }
 
@@ -931,17 +920,11 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLE_S)) = {
   let rs1_val_S = nan_unbox (F(rs1));
   let rs2_val_S = nan_unbox (F(rs2));
 
-  let is_quiet  = false;
-  let (rs1_le_rs2, fflags) = fle_S (rs1_val_S, rs2_val_S, is_quiet);
-
-  let rd_val : xlenbits =
-      if      (f_is_SNaN_S(rs1_val_S) | f_is_SNaN_S(rs2_val_S)) then zeros()
-      else if (f_is_QNaN_S(rs1_val_S) | f_is_QNaN_S(rs2_val_S)) then zeros()
-      else if rs1_le_rs2                                        then EXTZ(0b1)
-      else                                                           zeros();
+  let (fflags, rd_val) : (bits_fflags, bits_WU) =
+      riscv_f32Le (rs1_val_S, rs2_val_S);
 
-  accrue_fflags(fflags);
-  X(rd) = rd_val;
+  write_fflags(fflags);
+  X(rd) = EXTZ(rd_val);
   RETIRE_SUCCESS
 }
 
diff --git a/model/riscv_softfloat_interface.sail b/model/riscv_softfloat_interface.sail
index 88bbdc6..8c3653b 100644
--- a/model/riscv_softfloat_interface.sail
+++ b/model/riscv_softfloat_interface.sail
@@ -264,3 +264,47 @@ function riscv_f64ToF32 (rm, v) = {
 }
 
 /* **************************************************************** */
+/* COMPARISONS                                                      */
+
+val     extern_f32Lt = {c: "softfloat_f32lt", ocaml: "Softfloat.f32_lt", lem: "softfloat_f32_lt"} : (bits_S, bits_S) -> unit
+val      riscv_f32Lt : (bits_S, bits_S) -> (bits_fflags, bits_WU) effect {rreg}
+function riscv_f32Lt (v1, v2) = {
+  extern_f32Lt(v1, v2);
+  (float_fflags[4 .. 0], float_result[31 .. 0])
+}
+
+val     extern_f32Le = {c: "softfloat_f32le", ocaml: "Softfloat.f32_le", lem: "softfloat_f32_le"} : (bits_S, bits_S) -> unit
+val      riscv_f32Le : (bits_S, bits_S) -> (bits_fflags, bits_WU) effect {rreg}
+function riscv_f32Le (v1, v2) = {
+  extern_f32Le(v1, v2);
+  (float_fflags[4 .. 0], float_result[31 .. 0])
+}
+
+val     extern_f32Eq = {c: "softfloat_f32eq", ocaml: "Softfloat.f32_eq", lem: "softfloat_f32_eq"} : (bits_S, bits_S) -> unit
+val      riscv_f32Eq : (bits_S, bits_S) -> (bits_fflags, bits_WU) effect {rreg}
+function riscv_f32Eq (v1, v2) = {
+  extern_f32Eq(v1, v2);
+  (float_fflags[4 .. 0], float_result[31 .. 0])
+}
+
+val     extern_f64Lt = {c: "softfloat_f64lt", ocaml: "Softfloat.f64_lt", lem: "softfloat_f64_lt"} : (bits_D, bits_D) -> unit
+val      riscv_f64Lt : (bits_D, bits_D) -> (bits_fflags, bits_LU) effect {rreg}
+function riscv_f64Lt (v1, v2) = {
+  extern_f64Lt(v1, v2);
+  (float_fflags[4 .. 0], float_result)
+}
+
+val     extern_f64Le = {c: "softfloat_f64le", ocaml: "Softfloat.f64_le", lem: "softfloat_f64_le"} : (bits_D, bits_D) -> unit
+val      riscv_f64Le : (bits_D, bits_D) -> (bits_fflags, bits_LU) effect {rreg}
+function riscv_f64Le (v1, v2) = {
+  extern_f64Le(v1, v2);
+  (float_fflags[4 .. 0], float_result)
+}
+
+val     extern_f64Eq = {c: "softfloat_f64eq", ocaml: "Softfloat.f64_eq", lem: "softfloat_f64_eq"} : (bits_D, bits_D) -> unit
+val      riscv_f64Eq : (bits_D, bits_D) -> (bits_fflags, bits_LU) effect {rreg}
+function riscv_f64Eq (v1, v2) = {
+  extern_f64Eq(v1, v2);
+  (float_fflags[4 .. 0], float_result)
+}
+/* **************************************************************** */
diff --git a/ocaml_emulator/softfloat.ml b/ocaml_emulator/softfloat.ml
index ef84185..0de5e09 100644
--- a/ocaml_emulator/softfloat.ml
+++ b/ocaml_emulator/softfloat.ml
@@ -89,3 +89,20 @@ let f32_to_f64 rm v =
 let f64_to_f32 rm v =
   ()
 
+let f32_lt v1 v2 =
+  ()
+
+let f32_le v1 v2 =
+  ()
+
+let f32_eq v1 v2 =
+  ()
+
+let f64_lt v1 v2 =
+  ()
+
+let f64_le v1 v2 =
+  ()
+
+let f64_eq v1 v2 =
+  ()