Float: Introduce floating point api infinite (rems-project#522)

* Remove undefined_gen for if-else type * Remove the TODO workaround as fixed. Signed-off-by: Pan Li <[email protected]> * Float: Introduce floating point api infinite * Introduce new float api float_is_inf. * Add test case for half, single and double floating point. * Add inf to interface. Signed-off-by: Pan Li <[email protected]> * Fix typo for ifndef/define macro Signed-off-by: Pan Li <[email protected]> * Fix var name. Signed-off-by: Pan Li <[email protected]> * Fix typo and cleanup some spaces. Signed-off-by: Pan Li <[email protected]> --------- Signed-off-by: Pan Li <[email protected]>
trdthg · May 14, 2024 · 36eb33a · 36eb33a
1 parent 2b258a2
commit 36eb33a
Show file tree

Hide file tree

Showing 4 changed files with 118 additions and 0 deletions.
diff --git a/lib/float/inf.sail b/lib/float/inf.sail
@@ -0,0 +1,44 @@
+/*==========================================================================*/
+/*     Sail                                                                 */
+/*                                                                          */
+/* Copyright 2024 Intel Corporation                                         */
+/*   Pan Li - [email protected]                                             */
+/*                                                                          */
+/* Redistribution and use in source and binary forms, with or without       */
+/* modification, are permitted provided that the following conditions are   */
+/* met:                                                                     */
+/*                                                                          */
+/* 1. Redistributions of source code must retain the above copyright        */
+/*    notice, this list of conditions and the following disclaimer.         */
+/* 2. Redistributions in binary form must reproduce the above copyright     */
+/*    notice, this list of conditions and the following disclaimer in the   */
+/*    documentation and/or other materials provided with the distribution.  */
+/*                                                                          */
+/* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS      */
+/* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT        */
+/* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A  */
+/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT       */
+/* HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,   */
+/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED */
+/* TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR   */
+/* PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF   */
+/* LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING     */
+/* NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS       */
+/* SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.             */
+/*==========================================================================*/
+
+$ifndef _FLOAT_INF
+$define _FLOAT_INF
+
+$include <float/common.sail>
+
+val      float_is_inf : fp_bits -> bool
+function float_is_inf (op) = {
+  let struct {_, exp, mantissa} = float_decompose(op);
+  let is_inf = exp == sail_ones(length(exp))
+               & mantissa == sail_zeros(length(mantissa));
+
+  is_inf
+}
+
+$endif
diff --git a/lib/float/interface.sail b/lib/float/interface.sail
@@ -32,5 +32,6 @@ $define _FLOAT_INTERFACE
 
 $include <float/common.sail>
 $include <float/nan.sail>
+$include <float/inf.sail>
 
 $endif
diff --git a/src/bin/dune b/src/bin/dune
@@ -154,6 +154,7 @@
   (%{workspace_root}/lib/float.sail as lib/float.sail)
   (%{workspace_root}/lib/float/common.sail as lib/float/common.sail)
   (%{workspace_root}/lib/float/nan.sail as lib/float/nan.sail)
+  (%{workspace_root}/lib/float/inf.sail as lib/float/inf.sail)
   (%{workspace_root}/lib/float/interface.sail as lib/float/interface.sail)
   (%{workspace_root}/lib/reverse_endianness.sail
    as

diff --git a/test/float/inf_test.sail b/test/float/inf_test.sail
@@ -0,0 +1,72 @@
+/*==========================================================================*/
+/*     Sail                                                                 */
+/*                                                                          */
+/* Copyright 2024 Intel Corporation                                         */
+/*   Pan Li - [email protected]                                             */
+/*                                                                          */
+/* Redistribution and use in source and binary forms, with or without       */
+/* modification, are permitted provided that the following conditions are   */
+/* met:                                                                     */
+/*                                                                          */
+/* 1. Redistributions of source code must retain the above copyright        */
+/*    notice, this list of conditions and the following disclaimer.         */
+/* 2. Redistributions in binary form must reproduce the above copyright     */
+/*    notice, this list of conditions and the following disclaimer in the   */
+/*    documentation and/or other materials provided with the distribution.  */
+/*                                                                          */
+/* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS      */
+/* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT        */
+/* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A  */
+/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT       */
+/* HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,   */
+/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED */
+/* TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR   */
+/* PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF   */
+/* LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING     */
+/* NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS       */
+/* SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.             */
+/*==========================================================================*/
+
+default Order dec
+
+$include <prelude.sail>
+$include <float/inf.sail>
+
+function test_float_is_inf () -> unit = {
+  /* Half floating point */
+  assert(float_is_inf(0x7c00));
+  assert(float_is_inf(0xfc00));
+
+  assert(float_is_inf(0x7a00) == false);
+  assert(float_is_inf(0x7b00) == false);
+  assert(float_is_inf(0x7e00) == false);
+  assert(float_is_inf(0xca00) == false);
+  assert(float_is_inf(0xdb00) == false);
+  assert(float_is_inf(0xfe00) == false);
+
+  /* Single floating point */
+  assert(float_is_inf(0x7f800000));
+  assert(float_is_inf(0xff800000));
+
+  assert(float_is_inf(0x7fc00000) == false);
+  assert(float_is_inf(0x7f000001) == false);
+  assert(float_is_inf(0x7e800000) == false);
+  assert(float_is_inf(0xffc00000) == false);
+  assert(float_is_inf(0xff000001) == false);
+  assert(float_is_inf(0xfe800000) == false);
+
+  /* Double floating point */
+  assert(float_is_inf(0x7ff0000000000000));
+  assert(float_is_inf(0xfff0000000000000));
+
+  assert(float_is_inf(0x7ff8000000000000) == false);
+  assert(float_is_inf(0x7ff0000000000001) == false);
+  assert(float_is_inf(0x7fc0000000000000) == false);
+  assert(float_is_inf(0xfff8000000000000) == false);
+  assert(float_is_inf(0xfff0000000000001) == false);
+  assert(float_is_inf(0xffc0000000000000) == false);
+}
+
+function main () -> unit = {
+  test_float_is_inf();
+}