diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index f76620160..57f21447f 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1421,7 +1421,41 @@ Boolean values can also be cast to Integers (encoding `true` as `1`). [preserves-definedness] // ensures #numTypeOf is defined ``` -Casts involving `Float` values are currently not implemented. +Casts involving `Float` values: `IntToFloat`, `FloatToInt`, and `FloatToFloat`. + +```k + // IntToFloat: convert integer to float with the target float type's precision + rule #cast(Integer(VAL, _WIDTH, _SIGNEDNESS), castKindIntToFloat, _, TY) + => Float( + Int2Float(VAL, + #significandBits(#floatTypeOf(lookupTy(TY))), + #exponentBits(#floatTypeOf(lookupTy(TY)))), + #bitWidth(#floatTypeOf(lookupTy(TY))) + ) + ... + + [preserves-definedness] + + // FloatToInt: truncate float towards zero and convert to integer + rule #cast(Float(VAL, _WIDTH), castKindFloatToInt, _, TY) + => #intAsType(Float2Int(VAL), 128, #intTypeOf(lookupTy(TY))) + ... + + requires #isIntType(lookupTy(TY)) + [preserves-definedness] + + // FloatToFloat: round float to the target float type's precision + rule #cast(Float(VAL, _WIDTH), castKindFloatToFloat, _, TY) + => Float( + roundFloat(VAL, + #significandBits(#floatTypeOf(lookupTy(TY))), + #exponentBits(#floatTypeOf(lookupTy(TY)))), + #bitWidth(#floatTypeOf(lookupTy(TY))) + ) + ... + + [preserves-definedness] +``` ### Casts between pointer types @@ -1991,6 +2025,18 @@ are correct. rule onInt(binOpRem, X, Y) => X %Int Y requires Y =/=Int 0 [preserves-definedness] // operation undefined otherwise + // performs the given operation on IEEE 754 floats + syntax Float ::= onFloat( BinOp, Float, Float ) [function] + // ------------------------------------------------------- + rule onFloat(binOpAdd, X, Y) => X +Float Y [preserves-definedness] + rule onFloat(binOpAddUnchecked, X, Y) => X +Float Y [preserves-definedness] + rule onFloat(binOpSub, X, Y) => X -Float Y [preserves-definedness] + rule onFloat(binOpSubUnchecked, X, Y) => X -Float Y [preserves-definedness] + 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] + // error cases for isArithmetic(BOP): // * arguments must be Numbers @@ -2059,6 +2105,18 @@ are correct. // infinite precision result must equal truncated result andBool truncate(onInt(BOP, ARG1, ARG2), WIDTH, Unsigned) ==Int onInt(BOP, ARG1, ARG2) [preserves-definedness] + + // Float arithmetic: Rust never emits CheckedBinaryOp for floats (only BinaryOp), + // so the checked flag is always false here. See rustc_const_eval/src/interpret/operator.rs: + // binary_float_op returns a plain value, not a (value, overflow) pair. + rule #applyBinOp( + BOP, + Float(ARG1, WIDTH), + Float(ARG2, WIDTH), + false) + => Float(onFloat(BOP, ARG1, ARG2), WIDTH) + requires isArithmetic(BOP) + [preserves-definedness] ``` #### Comparison operations @@ -2095,6 +2153,14 @@ The argument types must be the same for all comparison operations, however this rule cmpOpBool(binOpGe, X, Y) => cmpOpBool(binOpLe, Y, X) rule cmpOpBool(binOpGt, X, Y) => cmpOpBool(binOpLt, Y, X) + syntax Bool ::= cmpOpFloat ( BinOp, Float, Float ) [function] + rule cmpOpFloat(binOpEq, X, Y) => X ==Float Y + rule cmpOpFloat(binOpLt, X, Y) => X X <=Float Y + rule cmpOpFloat(binOpNe, X, Y) => X =/=Float Y + rule cmpOpFloat(binOpGe, X, Y) => X >=Float Y + rule cmpOpFloat(binOpGt, X, Y) => X >Float Y + // error cases for isComparison and binOpCmp: // * arguments must be numbers or Bool @@ -2122,6 +2188,12 @@ The argument types must be the same for all comparison operations, however this BoolVal(cmpOpBool(OP, VAL1, VAL2)) requires isComparison(OP) [priority(60), preserves-definedness] // OP known to be a comparison + + rule #applyBinOp(OP, Float(VAL1, WIDTH), Float(VAL2, WIDTH), _) + => + BoolVal(cmpOpFloat(OP, VAL1, VAL2)) + requires isComparison(OP) + [preserves-definedness] // OP known to be a comparison ``` The `binOpCmp` operation returns `-1`, `0`, or `+1` (the behaviour of Rust's `std::cmp::Ordering as i8`), indicating `LE`, `EQ`, or `GT`. @@ -2137,6 +2209,11 @@ The `binOpCmp` operation returns `-1`, `0`, or `+1` (the behaviour of Rust's `st rule cmpBool(X, Y) => 0 requires X ==Bool Y rule cmpBool(X, Y) => 1 requires X andBool notBool Y + syntax Int ::= cmpFloat ( Float, Float ) [function] + rule cmpFloat(VAL1, VAL2) => -1 requires VAL1 0 requires VAL1 ==Float VAL2 + rule cmpFloat(VAL1, VAL2) => 1 requires VAL1 >Float VAL2 + rule #applyBinOp(binOpCmp, Integer(VAL1, WIDTH, SIGN), Integer(VAL2, WIDTH, SIGN), _) => Integer(cmpInt(VAL1, VAL2), 8, true) @@ -2144,6 +2221,10 @@ The `binOpCmp` operation returns `-1`, `0`, or `+1` (the behaviour of Rust's `st rule #applyBinOp(binOpCmp, BoolVal(VAL1), BoolVal(VAL2), _) => Integer(cmpBool(VAL1, VAL2), 8, true) + + rule #applyBinOp(binOpCmp, Float(VAL1, WIDTH), Float(VAL2, WIDTH), _) + => + Integer(cmpFloat(VAL1, VAL2), 8, true) ``` #### Unary operations on Boolean and integral values @@ -2159,7 +2240,11 @@ The semantics of the operation in this case is to wrap around (with the given bi ... - // TODO add rule for Floats once they are supported. + rule #applyUnOp(unOpNeg, Float(VAL, WIDTH)) + => + Float(--Float VAL, WIDTH) + ... + ``` The `unOpNot` operation works on boolean and integral values, with the usual semantics for booleans and a bitwise semantics for integral values (overflows cannot occur). diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md b/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md index 98b522012..f7d87552d 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md @@ -52,10 +52,13 @@ and arrays (where layout is trivial). requires #isIntType(TYPEINFO) andBool lengthBytes(BYTES) ==Int #elemSize(TYPEINFO) [preserves-definedness] + // Float: handled in separate module for numeric operations + rule #decodeValue(BYTES, TYPEINFO) => #decodeFloat(BYTES, #floatTypeOf(TYPEINFO)) + requires #isFloatType(TYPEINFO) andBool lengthBytes(BYTES) ==Int #elemSize(TYPEINFO) + [preserves-definedness] + // TODO Char type // rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), typeInfoPrimitiveType(primTypeChar)) => typedValue(Str(...), TY, mutabilityNot) - - // TODO Float decoding: not supported natively in K ``` diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/numbers.md b/kmir/src/kmir/kdist/mir-semantics/rt/numbers.md index d34c62b95..c7597bc1b 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/numbers.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/numbers.md @@ -13,6 +13,7 @@ module RT-NUMBERS imports BOOL imports BYTES imports INT + imports FLOAT ``` ## Helpers and Constants for Integer Operations @@ -38,6 +39,15 @@ module RT-NUMBERS rule #isIntType(typeInfoPrimitiveType(primTypeInt(_))) => true rule #isIntType(typeInfoPrimitiveType(primTypeUint(_))) => true rule #isIntType(_) => false [owise] + + syntax Bool ::= #isFloatType ( TypeInfo ) [function, total] + // -------------------------------------------------------- + rule #isFloatType(typeInfoPrimitiveType(primTypeFloat(_))) => true + rule #isFloatType(_) => false [owise] + + syntax FloatTy ::= #floatTypeOf ( TypeInfo ) [function] + // ---------------------------------------------------- + rule #floatTypeOf(typeInfoPrimitiveType(primTypeFloat(FLOATTY))) => FLOATTY ``` Constants used for overflow-checking and truncation are defined here as macros. @@ -110,6 +120,200 @@ This truncation function is instrumental in the implementation of Integer arithm [preserves-definedness] ``` +## Helpers and Constants for Float Operations + +Rust supports four fixed-width IEEE 754 float types: `f16`, `f32`, `f64`, and `f128`. +The helpers below extract format parameters for each type. First, an overview of the format. + +### IEEE 754 Binary Format + +An IEEE 754 binary floating-point word has three fields stored left-to-right: + +``` + MSB LSB + +---------+----------------+----------------------+ + | sign | exponent | fraction | + | (1 bit) | (EB bits) | (SB - 1 bits) | + +---------+----------------+----------------------+ + total bits = 1 + EB + (SB - 1) +``` + +The **significand** (also called **precision**) is the total number of significant bits +in the represented value, including an implicit leading 1 that is not stored in the +fraction field. For a normal number, the mathematical value is: + + value = (-1)^sign * 2^(exponent - bias) * 1.fraction + +The "1." prefix is the implicit bit, so the significand has `SB` bits of precision +even though only `SB - 1` fraction bits are stored. For example, f64 stores 52 fraction +bits but has 53 bits of significand precision. + +K's built-in `FLOAT` module uses this convention: `Int2Float(x, precision, exponentBits)` +takes `precision = SB` (total significand bits including the implicit 1) and `exponentBits = EB`. +See [IEEE 754 on Wikipedia](https://en.wikipedia.org/wiki/IEEE_754) for full details. + +The exponent is stored as an unsigned integer in +[excess-M encoding](https://en.wikipedia.org/wiki/Offset_binary) with `bias = 2^(EB-1) - 1`, +so that the actual exponent is `stored - bias`. For f64, bias = 1023: a stored value of 1023 +means exponent 0, 1024 means +1, and 1 means -1022. Stored values 0 and `2^EB - 1` are +reserved for zero/subnormals and infinity/NaN respectively. + +| Type | Total bits | Sign | Exponent (EB) | Fraction (SB-1) | Significand (SB) | Bias | +|------|------------|------|---------------|-----------------|------------------|------------| +| f16 | 16 | 1 | 5 | 10 | 11 | 15 | +| f32 | 32 | 1 | 8 | 23 | 24 | 127 | +| f64 | 64 | 1 | 11 | 52 | 53 | 1023 | +| f128 | 128 | 1 | 15 | 112 | 113 | 16383 | + +```k + syntax Int ::= #significandBits ( FloatTy ) [function, total] + // ---------------------------------------------------------- + rule #significandBits(floatTyF16) => 11 + rule #significandBits(floatTyF32) => 24 + rule #significandBits(floatTyF64) => 53 + rule #significandBits(floatTyF128) => 113 + + syntax Int ::= #exponentBits ( FloatTy ) [function, total] + // ------------------------------------------------------- + rule #exponentBits(floatTyF16) => 5 + rule #exponentBits(floatTyF32) => 8 + rule #exponentBits(floatTyF64) => 11 + rule #exponentBits(floatTyF128) => 15 + + syntax Int ::= #bias ( FloatTy ) [function, total] + // ----------------------------------------------- + rule #bias(FLOATTY) => (1 <x` suffix to specify precision and exponent +bits. See IEEE 754 Binary Format above for values of SB and EB. + +For example, `Infinityp53x11` is f64 positive infinity, `NaNp24x8` is f32 NaN. + +```k + syntax Float ::= #posInfFloat ( FloatTy ) [function, total] + // -------------------------------------------------------- + rule #posInfFloat(floatTyF16) => Infinityp11x5 + rule #posInfFloat(floatTyF32) => Infinityp24x8 + rule #posInfFloat(floatTyF64) => Infinityp53x11 + rule #posInfFloat(floatTyF128) => Infinityp113x15 + + syntax Float ::= #nanFloat ( FloatTy ) [function, total] + // ----------------------------------------------------- + rule #nanFloat(floatTyF16) => NaNp11x5 + rule #nanFloat(floatTyF32) => NaNp24x8 + rule #nanFloat(floatTyF64) => NaNp53x11 + rule #nanFloat(floatTyF128) => NaNp113x15 +``` + +## Decoding Float values from `Bytes` for `OperandConstant` + +The `#decodeFloat` function reconstructs a `Float` value from its IEEE 754 byte representation. +The bytes are first converted to a raw integer, then the sign, biased exponent, and stored significand +are extracted. The value is reconstructed using K's `Int2Float` and float arithmetic, with a +high-precision intermediate to avoid overflow when reconstructing subnormals and small normal values. + +```k + syntax Value ::= #decodeFloat ( Bytes, FloatTy ) [function] + // -------------------------------------------------------- + rule #decodeFloat(BYTES, FLOATTY) => #decodeFloatRaw(Bytes2Int(BYTES, LE, Unsigned), FLOATTY) + requires lengthBytes(BYTES) ==Int #bitWidth(FLOATTY) /Int 8 + [preserves-definedness] + + syntax Value ::= #decodeFloatRaw ( Int, FloatTy ) [function, total] + // ---------------------------------------------------------------- + rule #decodeFloatRaw(RAW, FLOATTY) + => #decodeFloatParts( + RAW >>Int (#significandBits(FLOATTY) +Int #exponentBits(FLOATTY) -Int 1), + (RAW >>Int (#significandBits(FLOATTY) -Int 1)) &Int ((1 < Float(#applyFloatSign(Int2Float(0, #significandBits(FLOATTY), #exponentBits(FLOATTY)), SIGN), #bitWidth(FLOATTY)) + [preserves-definedness] + + // Subnormal: no implicit leading 1, exponent is 1 - bias + rule #decodeFloatParts(SIGN, 0, SIG, FLOATTY) + => Float( + #applyFloatSign( + #reconstructFloat(SIG, 2 -Int #bias(FLOATTY) -Int #significandBits(FLOATTY), FLOATTY), + SIGN + ), + #bitWidth(FLOATTY) + ) + requires SIG =/=Int 0 + [preserves-definedness] + + // Normal: implicit leading 1 in significand + rule #decodeFloatParts(SIGN, EXP, SIG, FLOATTY) + => Float( + #applyFloatSign( + #reconstructFloat( + SIG |Int (1 <Int 0 andBool EXP Float(#applyFloatSign(#posInfFloat(FLOATTY), SIGN), #bitWidth(FLOATTY)) + requires EXP ==Int ((1 < Float(#nanFloat(FLOATTY), #bitWidth(FLOATTY)) + requires EXP ==Int ((1 < Int2Float(SIG <=Int 0 + [preserves-definedness] + + rule #reconstructFloat(SIG, AEXP, FLOATTY) + => roundFloat( + Int2Float(SIG, 256, 64) /Float Int2Float(1 < F + rule #applyFloatSign(F, 1) => --Float F + rule #applyFloatSign(F, _) => F [owise] +``` + ## Type Casts Between Different Numeric Types diff --git a/kmir/src/tests/integration/data/exec-smir/structs-tuples/struct_field_update.state b/kmir/src/tests/integration/data/exec-smir/structs-tuples/struct_field_update.state index 57665d4db..bed580f75 100644 --- a/kmir/src/tests/integration/data/exec-smir/structs-tuples/struct_field_update.state +++ b/kmir/src/tests/integration/data/exec-smir/structs-tuples/struct_field_update.state @@ -28,7 +28,7 @@ ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) ) ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 1 , 32 , true ) ) ListItem ( BoolVal ( true ) ) - ListItem ( thunk ( UnableToDecode ( b"33333sE@" , typeInfoPrimitiveType ( primTypeFloat ( floatTyF64 ) ) ) ) ) + ListItem ( Float ( 0.42899999999999999e2 , 64 ) ) ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 1 , 32 , true ) ) ListItem ( Integer ( 10 , 32 , true ) ) ) ) ) , ty ( 28 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 27 ) , mutabilityMut ) ) diff --git a/kmir/src/tests/integration/data/exec-smir/structs-tuples/structs-tuples.state b/kmir/src/tests/integration/data/exec-smir/structs-tuples/structs-tuples.state index 47b68a635..e6dc9aec9 100644 --- a/kmir/src/tests/integration/data/exec-smir/structs-tuples/structs-tuples.state +++ b/kmir/src/tests/integration/data/exec-smir/structs-tuples/structs-tuples.state @@ -1,6 +1,6 @@ - #execStmts ( .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindReturn , span: span ( 73 ) ) ) ~> .K + #execTerminator ( terminator (... kind: terminatorKindReturn , span: span ( 73 ) ) ) ~> .K noReturn @@ -28,17 +28,17 @@ ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) ) ListItem ( typedValue ( Integer ( 10 , 32 , true ) , ty ( 16 ) , mutabilityNot ) ) ListItem ( typedValue ( BoolVal ( false ) , ty ( 26 ) , mutabilityNot ) ) - ListItem ( typedValue ( thunk ( UnableToDecode ( b"\x00\x00\x00\x00\x00\x00$@" , typeInfoPrimitiveType ( primTypeFloat ( floatTyF64 ) ) ) ) , ty ( 27 ) , mutabilityNot ) ) + ListItem ( typedValue ( Float ( 0.10000000000000000e2 , 64 ) , ty ( 27 ) , mutabilityNot ) ) ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( 0 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionContinue , ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) ) ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 10 , 32 , true ) ) ListItem ( BoolVal ( false ) ) - ListItem ( thunk ( UnableToDecode ( b"\x00\x00\x00\x00\x00\x00$@" , typeInfoPrimitiveType ( primTypeFloat ( floatTyF64 ) ) ) ) ) ) , ty ( 28 ) , mutabilityNot ) ) + ListItem ( Float ( 0.10000000000000000e2 , 64 ) ) ) , ty ( 28 ) , mutabilityNot ) ) ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 11 , 32 , true ) ) ListItem ( BoolVal ( true ) ) - ListItem ( thunk ( UnableToDecode ( b"\x00\x00\x00\x00\x00\x00$@" , typeInfoPrimitiveType ( primTypeFloat ( floatTyF64 ) ) ) ) ) ) , ty ( 29 ) , mutabilityNot ) ) + ListItem ( Float ( 0.10000000000000000e2 , 64 ) ) ) , ty ( 29 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 27 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 1 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 16 ) , mutabilityMut ) ) diff --git a/kmir/src/tests/integration/data/prove-rs/float_arith.rs b/kmir/src/tests/integration/data/prove-rs/float_arith.rs new file mode 100644 index 000000000..7a202fea5 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/float_arith.rs @@ -0,0 +1,41 @@ +#![feature(f16)] +#![feature(f128)] + +fn main() { + // f16 + assert!(1.5_f16 + 2.5_f16 == 4.0_f16); + assert!(5.0_f16 - 1.5_f16 == 3.5_f16); + assert!(2.0_f16 * 3.0_f16 == 6.0_f16); + assert!(7.0_f16 / 2.0_f16 == 3.5_f16); + + // f32 + assert!(1.5_f32 + 2.5_f32 == 4.0_f32); + assert!(5.0_f32 - 1.5_f32 == 3.5_f32); + assert!(2.0_f32 * 3.0_f32 == 6.0_f32); + assert!(7.0_f32 / 2.0_f32 == 3.5_f32); + + // f64 + assert!(3.5_f64 + 1.5_f64 == 5.0_f64); + assert!(3.5_f64 - 1.5_f64 == 2.0_f64); + assert!(3.5_f64 * 1.5_f64 == 5.25_f64); + assert!(10.0_f64 / 2.0_f64 == 5.0_f64); + + // f128 + assert!(1.5_f128 + 2.5_f128 == 4.0_f128); + assert!(5.0_f128 - 1.5_f128 == 3.5_f128); + assert!(2.0_f128 * 3.0_f128 == 6.0_f128); + assert!(7.0_f128 / 2.0_f128 == 3.5_f128); + + // Subnormal constant literals + let sub_16: f16 = 5.96e-8_f16; // below f16 min normal (6.1e-5) + assert!(sub_16 + sub_16 == sub_16 * 2.0_f16); + + let sub_32: f32 = 1.0e-45_f32; // below f32 min normal (1.2e-38) + assert!(sub_32 + sub_32 == sub_32 * 2.0_f32); + + let sub_64: f64 = 5e-324_f64; // below f64 min normal (2.2e-308) + assert!(sub_64 + sub_64 == 1e-323_f64); + + let sub_128: f128 = 1.0e-4933_f128; // below f128 min normal (~3.4e-4932) + assert!(sub_128 + sub_128 == sub_128 * 2.0_f128); +} diff --git a/kmir/src/tests/integration/data/prove-rs/float_cast.rs b/kmir/src/tests/integration/data/prove-rs/float_cast.rs new file mode 100644 index 000000000..747c9a7da --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/float_cast.rs @@ -0,0 +1,22 @@ +#![feature(f16)] +#![feature(f128)] + +fn main() { + // FloatToInt + assert!(3.14_f16 as i32 == 3); + assert!(3.14_f32 as i32 == 3); + assert!(3.14_f64 as i32 == 3); + assert!(3.14_f128 as i32 == 3); + + // IntToFloat + assert!(42_i64 as f16 == 42.0_f16); + assert!(42_i64 as f32 == 42.0_f32); + assert!(42_i64 as f64 == 42.0_f64); + assert!(42_i64 as f128 == 42.0_f128); + + // FloatToFloat + assert!(2.5_f32 as f64 == 2.5_f64); + assert!(2.5_f64 as f32 == 2.5_f32); + assert!(2.5_f16 as f64 == 2.5_f64); + assert!(2.5_f64 as f128 == 2.5_f128); +} diff --git a/kmir/src/tests/integration/data/prove-rs/float_cmp.rs b/kmir/src/tests/integration/data/prove-rs/float_cmp.rs new file mode 100644 index 000000000..9144787a2 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/float_cmp.rs @@ -0,0 +1,38 @@ +#![feature(f16)] +#![feature(f128)] + +fn main() { + // f16 + assert!(1.0_f16 < 2.0_f16); + assert!(2.0_f16 >= 2.0_f16); + assert!(3.0_f16 > 1.0_f16); + assert!(1.0_f16 <= 1.0_f16); + + // f32 + assert!(1.0_f32 < 2.0_f32); + assert!(2.0_f32 >= 2.0_f32); + assert!(3.0_f32 > 1.0_f32); + assert!(1.0_f32 <= 1.0_f32); + + // f64 + assert!(1.0_f64 < 2.0_f64); + assert!(2.0_f64 >= 2.0_f64); + assert!(3.0_f64 > 1.0_f64); + assert!(1.0_f64 <= 1.0_f64); + + // f128 + assert!(1.0_f128 < 2.0_f128); + assert!(2.0_f128 >= 2.0_f128); + assert!(3.0_f128 > 1.0_f128); + assert!(1.0_f128 <= 1.0_f128); + + // Negative values + assert!(-1.0_f16 < 0.0_f16); + assert!(-2.0_f16 < -1.0_f16); + assert!(-1.0_f32 < 0.0_f32); + assert!(-2.0_f32 < -1.0_f32); + assert!(-1.0_f64 < 0.0_f64); + assert!(-2.0_f64 < -1.0_f64); + assert!(-1.0_f128 < 0.0_f128); + assert!(-2.0_f128 < -1.0_f128); +} diff --git a/kmir/src/tests/integration/data/prove-rs/float_eq.rs b/kmir/src/tests/integration/data/prove-rs/float_eq.rs new file mode 100644 index 000000000..3e0bbeb43 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/float_eq.rs @@ -0,0 +1,30 @@ +#![feature(f16)] +#![feature(f128)] + +fn main() { + // f16 + assert!(1.0_f16 == 1.0_f16); + assert!(0.0_f16 == 0.0_f16); + assert!(1.0_f16 != 2.0_f16); + + // f32 + assert!(1.0_f32 == 1.0_f32); + assert!(0.0_f32 == 0.0_f32); + assert!(1.0_f32 != 2.0_f32); + + // f64 + assert!(1.0_f64 == 1.0_f64); + assert!(0.0_f64 == 0.0_f64); + assert!(1.0_f64 != 2.0_f64); + + // f128 + assert!(1.0_f128 == 1.0_f128); + assert!(0.0_f128 == 0.0_f128); + assert!(1.0_f128 != 2.0_f128); + + // Negative zero equals positive zero (IEEE 754) + assert!(-0.0_f16 == 0.0_f16); + assert!(-0.0_f32 == 0.0_f32); + assert!(-0.0_f64 == 0.0_f64); + assert!(-0.0_f128 == 0.0_f128); +} diff --git a/kmir/src/tests/integration/data/prove-rs/float_neg.rs b/kmir/src/tests/integration/data/prove-rs/float_neg.rs new file mode 100644 index 000000000..065ff2bc2 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/float_neg.rs @@ -0,0 +1,30 @@ +#![feature(f16)] +#![feature(f128)] + +fn main() { + // f16 + let a16: f16 = 3.5; + assert!(-a16 == -3.5_f16); + assert!(-(-a16) == a16); + + // f32 + let a32: f32 = 3.5; + assert!(-a32 == -3.5_f32); + assert!(-(-a32) == a32); + + // f64 + let a64: f64 = 3.5; + assert!(-a64 == -3.5_f64); + assert!(-(-a64) == a64); + + // f128 + let a128: f128 = 3.5; + assert!(-a128 == -3.5_f128); + assert!(-(-a128) == a128); + + // Negating zero + assert!(-0.0_f16 == 0.0_f16); + assert!(-0.0_f32 == 0.0_f32); + assert!(-0.0_f64 == 0.0_f64); + assert!(-0.0_f128 == 0.0_f128); +} diff --git a/kmir/src/tests/integration/data/prove-rs/float_special.rs b/kmir/src/tests/integration/data/prove-rs/float_special.rs new file mode 100644 index 000000000..aa6449da2 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/float_special.rs @@ -0,0 +1,56 @@ +#![feature(f16)] +#![feature(f128)] + +fn main() { + // f16 infinity + let inf_16: f16 = 1.0_f16 / 0.0_f16; + let neg_inf_16: f16 = -1.0_f16 / 0.0_f16; + assert!(inf_16 == inf_16); + assert!(neg_inf_16 == -inf_16); + + // f16 NaN + let nan_16: f16 = 0.0_f16 / 0.0_f16; + assert!(nan_16 != nan_16); + assert!(!(nan_16 == nan_16)); + + // f32 infinity + let inf_32: f32 = 1.0_f32 / 0.0_f32; + let neg_inf_32: f32 = -1.0_f32 / 0.0_f32; + assert!(inf_32 == inf_32); + assert!(inf_32 > 1.0e38_f32); + assert!(neg_inf_32 < -1.0e38_f32); + assert!(neg_inf_32 == -inf_32); + + // f32 NaN + let nan_32: f32 = 0.0_f32 / 0.0_f32; + assert!(nan_32 != nan_32); + assert!(!(nan_32 == nan_32)); + assert!(!(nan_32 < 0.0_f32)); + assert!(!(nan_32 > 0.0_f32)); + + // f64 infinity + let inf_64: f64 = 1.0_f64 / 0.0_f64; + let neg_inf_64: f64 = -1.0_f64 / 0.0_f64; + assert!(inf_64 == inf_64); + assert!(inf_64 > 1.0e308_f64); + assert!(neg_inf_64 < -1.0e308_f64); + assert!(neg_inf_64 == -inf_64); + + // f64 NaN + let nan_64: f64 = 0.0_f64 / 0.0_f64; + assert!(nan_64 != nan_64); + assert!(!(nan_64 == nan_64)); + assert!(!(nan_64 < 0.0_f64)); + assert!(!(nan_64 > 0.0_f64)); + + // f128 infinity + let inf_128: f128 = 1.0_f128 / 0.0_f128; + let neg_inf_128: f128 = -1.0_f128 / 0.0_f128; + assert!(inf_128 == inf_128); + assert!(neg_inf_128 == -inf_128); + + // f128 NaN + let nan_128: f128 = 0.0_f128 / 0.0_f128; + assert!(nan_128 != nan_128); + assert!(!(nan_128 == nan_128)); +} diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 8c59cce9b..99cf1851c 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -380,6 +380,17 @@ def test_crate_examples(main_crate: Path, kmir: KMIR, update_expected_output: bo ] +# Tests containing float values that the pure kore-exec haskell backend cannot handle. +# The haskell backend has no Float builtins (no Float.hs in kore/src/Kore/Builtin/), +# so kore-exec crashes with "missing hook FLOAT.int2float" at Evaluator.hs:377. +# The booster avoids this by delegating Float evaluation to the LLVM shared library +# via simplifyTerm in booster/library/Booster/LLVM.hs. +EXEC_SMIR_SKIP_HASKELL = { + 'structs-tuples', + 'struct-field-update', +} + + @pytest.mark.parametrize('symbolic', [False, True], ids=['llvm', 'haskell']) @pytest.mark.parametrize( 'test_case', @@ -392,7 +403,9 @@ def test_exec_smir( update_expected_output: bool, tmp_path: Path, ) -> None: - _, input_json, output_kast, depth = test_case + name, input_json, output_kast, depth = test_case + if symbolic and name in EXEC_SMIR_SKIP_HASKELL: + pytest.skip('haskell-backend lacks FLOAT hooks') smir_info = SMIRInfo.from_file(input_json) kmir_backend = KMIR.from_kompiled_kore(smir_info, target_dir=tmp_path, symbolic=symbolic) result = kmir_backend.run_smir(smir_info, depth=depth)