Basic support for floats (f16, f32, f64, f128)#995
Conversation
Mirror of existing IntTy rules
Heavily inspired from c-semantics ieee754.md
The haskell backend does not natively support floats. So the exec-smir tests that use the haskell backend will fail now that the floats can be decoded. This is not a problem for the LLVM backend, nor the booster as it will call the LLVM backend to evaulate the float terms. The solution is to skip tests that have floats and the haskell backend for exec-smir (with an explanatory comment for anyone to follow).
dkcumming
requested review from
Stevengre,
jberthold,
mariaKt and
palinatolmach
mariaKt
left a comment
mariaKt
left a comment
There was a problem hiding this comment.
I have left some questions and some comments. Feel free to address them with other PRs, so as not to block you.
| FLOATTY | ||
| ) | ||
|
|
||
| syntax Value ::= #decodeFloatParts ( sign: Int, biasedExp: Int, storedSig: Int, FloatTy ) [function] |
There was a problem hiding this comment.
This is not explicitly marked as total, however it would need to be (because #decodeFloatRaw is). It seems that the arguments' match is exhaustive. Consider making it total?
|
|
||
| rule #reconstructFloat(SIG, AEXP, FLOATTY) | ||
| => roundFloat( | ||
| Int2Float(SIG, 256, 64) /Float Int2Float(1 <<Int (0 -Int AEXP), 256, 64), |
There was a problem hiding this comment.
I understand the conversion here, but is seems different from the approach in the c-semantics. This conversion has an additional rounding step. I wonder if is intentional (avoid the Rat sort and Rat2Float for some reason?). If not, the following rule should work equally well with only one rounding, and no arbitrary precision. (imports RAT is needed)
rule #reconstructFloat(SIG, AEXP, FLOATTY)
=> Rat2Float(SIG /Rat (1 <<Int (0 -Int AEXP)),
#significandBits(FLOATTY), #exponentBits(FLOATTY))
requires AEXP <Int 0
| syntax Int ::= cmpFloat ( Float, Float ) [function] | ||
| rule cmpFloat(VAL1, VAL2) => -1 requires VAL1 <Float VAL2 | ||
| rule cmpFloat(VAL1, VAL2) => 0 requires VAL1 ==Float VAL2 | ||
| rule cmpFloat(VAL1, VAL2) => 1 requires VAL1 >Float VAL2 |
There was a problem hiding this comment.
How are the comparisons with NaN handled? How do they not get stuck with some of the tests' values where NaN and another float reach here? Do they not?
| rule onFloat(binOpMul, X, Y) => X *Float Y [preserves-definedness] | ||
| rule onFloat(binOpMulUnchecked, X, Y) => X *Float Y [preserves-definedness] | ||
| rule onFloat(binOpDiv, X, Y) => X /Float Y [preserves-definedness] | ||
| rule onFloat(binOpRem, X, Y) => X %Float Y [preserves-definedness] |
There was a problem hiding this comment.
%Float implements the % operation according to the IEEE 754 standard:
"IEEE 754 Remainder: The result r=x-y*n, where n is the integer nearest to the exact value x/y"
- https://github.com/runtimeverification/k/blob/c9205d683b9c1d299c482c1506ce7dde3f4dc9c0/k-distribution/include/kframework/builtin/domains.md?plain=1#L1556
- https://github.com/runtimeverification/llvm-backend/blob/618f530031870d6e8a74633b122d46afb5d7ad8e/runtime/arithmetic/float.cpp#L421
It seems that Rust computes it in a slightly different way, wherenis calculated by dropping the fractional part, i.e., truncated.
The tests do not exercise this yet, but here is a suggestion if needed.
rule onFloat(binOpRem, X, Y)
=> X -Float Y *Float truncFloat(X /Float Y)
|
A test for |
2 participants
This PR adds basic support for IEEE 754 Floating Point Numbers, specifically
f16,f32,f64,f128.These are already supported in K through builtins (see domains.md). This work is derivative of the implementation in the c-semantics (see ieee754.k in that repository).
In particular:
Haskell Backend
The haskell backend has no
Floatbuiltins (no Float.hs in kore/src/Kore/Builtin/). This meanskore-execcrashes with "missing hook FLOAT.int2float" when attempting to evaluate a float. The booster avoids this by delegating Float evaluation to the LLVM shared library viasimplifyTermin booster/library/Booster/LLVM.hs.Prior to being able to decode floats, they were left as
UnableToDecodewhich did not throw and error in the exec-smir test suite for--haskell-backend. Now that they are able to be decoded, the haskell backend throws on these decoded values. So I am now skipping any tests with decoded floats for exec-smir with haskell backend.