Float: Introduce floating point api NAN

[Incarnation-p-lee]

• Introduce new float api nan/snan/qnan.
• Introduce common for types and helper functions.
• Introduce interface for all-in-one float api.
• Add test framework for float api.
• Add test cases for float nan api.

Signed-off-by: Pan Li [email protected]

[Incarnation-p-lee]

Hi @Alasdair

Could you please help to enlighten me the best practice to run the nan_test.sail here when you are free?
Just work out a POC of the standalone float lib but would like to consult from expert like you for the right direction.

Thanks and CC @billmcspadden-riscv for awareness.

[Alasdair]

Hi, I'll take a look next week. Please ping me again if I forget and don't get around to it.

[Incarnation-p-lee]

Sure thing and thanks a lot. It is not urgent, take your time.

[Incarnation-p-lee]

Kindly ping for this, take your time if you are in the middle of sth.

[Alasdair]

One thing I noticed - it seems like you have some cmi and cmo files accidentally checked in.

[Incarnation-p-lee]

One thing I noticed - it seems like you have some cmi and cmo files accidentally checked in.

Yeah, for the first commit, and I eliminated that from the newest commit.

[Incarnation-p-lee]

is there any suggestion for get the size(bits) of mantissa here?
For now we will have the below error.

Type error:
/home/pli/repos/sail/sail-fork/lib/float/nan.sail:46.20-40:
46 |  let highest_bit = sizeof(mantissa) - 1;
   |                    ^------------------^
   | No overloading for (operator -), tried:
   | * sub_atom
   |    Cannot re-write sizeof(mantissa)
   | * sub_int
   |    Cannot re-write sizeof(mantissa)

Meanwhile, 'mantissa like let (_, exp, 'mantissa) = float_decompose(op); won't work here too.

[Alasdair]

Do you need sizeof at all here?

[Incarnation-p-lee]

Sorry not very familiar as green hand for sail, is there any alternatives?

[Alasdair]

I think just let highest_bit = mantissa - 1;?

sizeof is used for converting a type back into a runtime value, which I'm not sure is needed here.

[Incarnation-p-lee]

If mantissa indicates bits[22 .. 0] (take single as example) of floating-point, the let highest_bit = mantissa - 1 may not be the value 22 which is the highest bit index of mantissa?
For snan, we only need to check the highest bits here.

[Incarnation-p-lee]

Or one silly way is that we can have a helper function to return the highest bit of float, may similar to

function float_mantissa_bits (op) = {
  match 'n {
    16 => 10,
    32 => 23,
    64 => 52
  }
}

It may works but not that perfect.

[Incarnation-p-lee]

Or one silly way is that we can have a helper function to return the highest bit of float, may similar to

function float_mantissa_bits (op) = {
  match 'n {
    16 => 10,
    32 => 23,
    64 => 52
  }
}

It may works but not that perfect.

Tried this approach but meet another issue for vector bits access. Updated code for aligning the below error, not sure if I missed something.

47 |  let tmp_1 = mantissa[highest_bit - 1];
   |              ^-----------------------^
   | No overloading for vector_access, tried:
   | * bitvector_access
   |    Could not resolve quantifiers for bitvector_access
   |    * (0 <= ('_#highest_bit - 1) & ('_#highest_bit - 1) < (if 'ex284# == 16 then 10 else (if 'ex284# == 32 then 23 else 52)))
   | * plain_vector_access
   |    Could not unify vector('n, 'a) and bitvector((if 'ex284# == 16 then 10 else (if 'ex284# == 32 then 23 else 52)))
   |
   | Caused by /home/pli/repos/sail/sail-fork/lib/float/nan.sail:47.14-39:
   | 47 |  let tmp_1 = mantissa[highest_bit - 1];
   |    |              ^-----------------------^
   |    | Vector access could not be interpreted as a bitfield access

[Alasdair]

I had a look at your code, I think the following may be what you want:

default Order dec

$include <prelude.sail>

type fp_bits = {'n, 'n in {16, 32, 64}. bits('n)}

struct float_bits('n: Int) = {
  sign: bits(1),
  exp : bits(if 'n == 16 then 5 else (if 'n == 32 then 8 else 11)),
  mantissa : bits(if 'n == 16 then 10 else (if 'n == 32 then 23 else 52)),
}

val float_decompose : forall 'n, 'n in {16, 32, 64}. bits('n) -> float_bits('n)

function float_decompose(op) = {
  if length(op) == 16 then {
    struct { sign = op[15 .. 15], exp = op[14 .. 10], mantissa = op[9 .. 0] }
  } else if length(op) == 32 then {
    struct { sign = op[31 .. 31], exp = op[30 .. 23], mantissa = op[22 .. 0] }
  } else {
    struct { sign = op[63 .. 63], exp = op[62 .. 52], mantissa = op[51 .. 0] }
  }
}

val mantissa_length : forall 'n, 'n in {16, 32, 64}.
  bits('n) -> {'m, ('n == 16 & 'm == 10) | ('n == 32 & 'm == 23) | ('n == 64 & 'm == 52). int('m)}

function mantissa_length(op) = {
  match length(op) {
    16 => 10,
    32 => 23,
    64 => 52,
  }
}

val float_is_snan : fp_bits -> bool

function float_is_snan(op) = {
  let struct { sign = _, exp, mantissa } = float_decompose(op);
  let highest_bit = length(mantissa);
  exp == sail_ones(length(exp))
  & mantissa != sail_zeros(length(mantissa))
  & mantissa[highest_bit - 1] == bitzero
}

I didn't end up using the mantissa_length function, so maybe we just don't need it as float_decompose is enough. The Sail library is a bit more bare-bones than what the RISC-V model has, so we use the sail_ones and sail_zeros builtins which have no implicit arguments.

[Incarnation-p-lee]

I had a look at your code, I think the following may be what you want:

default Order dec

$include <prelude.sail>

type fp_bits = {'n, 'n in {16, 32, 64}. bits('n)}

struct float_bits('n: Int) = {
  sign: bits(1),
  exp : bits(if 'n == 16 then 5 else (if 'n == 32 then 8 else 11)),
  mantissa : bits(if 'n == 16 then 10 else (if 'n == 32 then 23 else 52)),
}

val float_decompose : forall 'n, 'n in {16, 32, 64}. bits('n) -> float_bits('n)

function float_decompose(op) = {
  if length(op) == 16 then {
    struct { sign = op[15 .. 15], exp = op[14 .. 10], mantissa = op[9 .. 0] }
  } else if length(op) == 32 then {
    struct { sign = op[31 .. 31], exp = op[30 .. 23], mantissa = op[22 .. 0] }
  } else {
    struct { sign = op[63 .. 63], exp = op[62 .. 52], mantissa = op[51 .. 0] }
  }
}

val mantissa_length : forall 'n, 'n in {16, 32, 64}.
  bits('n) -> {'m, ('n == 16 & 'm == 10) | ('n == 32 & 'm == 23) | ('n == 64 & 'm == 52). int('m)}

function mantissa_length(op) = {
  match length(op) {
    16 => 10,
    32 => 23,
    64 => 52,
  }
}

val float_is_snan : fp_bits -> bool

function float_is_snan(op) = {
  let struct { sign = _, exp, mantissa } = float_decompose(op);
  let highest_bit = length(mantissa);
  exp == sail_ones(length(exp))
  & mantissa != sail_zeros(length(mantissa))
  & mantissa[highest_bit - 1] == bitzero
}

I didn't end up using the mantissa_length function, so maybe we just don't need it as float_decompose is enough. The Sail library is a bit more bare-bones than what the RISC-V model has, so we use the sail_ones and sail_zeros builtins which have no implicit arguments.

Thanks a lot, let me have a try and update it.

[Incarnation-p-lee]

Updated, I think length is what we need here and we don't need the function float_mantissa_bitsize.
Thanks again and then I think the next step is how to run the test cases if there is no more issues. For now, I guess the script only does something like type check.

[Alasdair]

For the test script you could look at the one in tests/c/run_tests.py for how to run things. If the code is otherwise ready we could always merge it, then I could set up the tests and CI things. I think we can be incremental and improve things as we go.

[Incarnation-p-lee]

For the test script you could look at the one in tests/c/run_tests.py for how to run things. If the code is otherwise ready we could always merge it, then I could set up the tests and CI things. I think we can be incremental and improve things as we go.

Got it. Let me have a try for this.

[Incarnation-p-lee]

Just have a try to convert the sail code to c for build and run. And there is one type check error similar to below, but it works well if I only let the n = 16 with the struct has fixed bitsize.

Seems comes from the struct with if-then-else for its' fields length, will have another try for this...

Failed: /home/pli/repos/sail/sail-fork/sail -no_warn -c  nan_test.sail 1> nan_test.c
stdout:

stderr:
Type error:
{('ex426# : Int), ('ex426# == 5 | ('ex426# == 8 | 'ex426# == 11)). int('ex426#)} is not a subtype of int((if 'n == 16 then 5 else (if 'n == 32 then 8 else 11)))
as 'ex427 == (if 'n == 16 then 5 else (if 'n == 32 then 8 else 11)) could not be proven

type variable 'ex427:
has constraint: ('ex427 == 5 | ('ex427 == 8 | 'ex427 == 11))

[Alasdair]

The type level if-then-else is something I recently added, I think there's some awkward interaction between it and the code that produces a function to generate undefined values of some type. You should be able to do:

$[undefined_gen forbid]
struct float_bits('n: Int) = {
  sign: bits(1),
  exp : bits(if 'n == 16 then 5 else (if 'n == 32 then 8 else 11)),
  mantissa : bits(if 'n == 16 then 10 else (if 'n == 32 then 23 else 52)),
}

to make sure that doesn't happen for the time being.

[Incarnation-p-lee]

The type level if-then-else is something I recently added, I think there's some awkward interaction between it and the code that produces a function to generate undefined values of some type. You should be able to do:

$[undefined_gen forbid]
struct float_bits('n: Int) = {
  sign: bits(1),
  exp : bits(if 'n == 16 then 5 else (if 'n == 32 then 8 else 11)),
  mantissa : bits(if 'n == 16 then 10 else (if 'n == 32 then 23 else 52)),
}

to make sure that doesn't happen for the time being.

Cool, $[undefined_gen forbid] can help eliminate the type check error. Thanks a lot, it really saved my day.
If-else for type is a very useful feature in my option, that it can avoid many similar code in many cases.
I will add more test for it and mark this PR as Ready for review soon.

[github-actions]

Test Results

    9 files  ±0     20 suites  ±0   0s ⏱️ ±0s
  619 tests ±0    619 ✅ ±0  0 💤 ±0  0 ❌ ±0 
1 984 runs  ±0  1 983 ✅ ±0  1 💤 ±0  0 ❌ ±0 

Results for commit 70a734f. ± Comparison against base commit f6b8985.

[Alasdair]

Merged, thanks!

I think the issue you ran into should be fixed by ededb75

[Incarnation-p-lee]

Merged, thanks!

I think the issue you ran into should be fixed by ededb75

Great, thanks a lot. Let me have a try and file another PR to remove the TODO and workaround.