diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 4e7f79076..f9b07909d 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -61,7 +61,7 @@ jobs: - name: 'LLVM Concrete Tests' test-args: '-k "llvm or test_run_smir_random"' parallel: 12 - timeout: 30 + timeout: 60 - name: 'Haskell Exec SMIR' test-args: '-k "test_exec_smir and haskell"' parallel: 6 @@ -69,15 +69,15 @@ jobs: - name: 'Haskell Termination' test-args: '-k test_prove_termination' parallel: 6 - timeout: 20 + timeout: 60 - name: 'Haskell Proofs' test-args: '-k "test_prove and not test_prove_termination"' parallel: 6 - timeout: 120 + timeout: 150 - name: 'Remainder' test-args: '-k "not llvm and not test_run_smir_random and not test_exec_smir and not test_prove_termination and not test_prove"' parallel: 6 - timeout: 20 + timeout: 60 steps: - name: 'Check out code' uses: actions/checkout@v4 diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 5839521b4..2cc068084 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1412,41 +1412,7 @@ Boolean values can also be cast to Integers (encoding `true` as `1`). [preserves-definedness] // ensures #numTypeOf is defined ``` -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 involving `Float` values are currently not implemented. ### Casts between pointer types @@ -2043,20 +2009,6 @@ 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 - // Note: Rust's float % is truncating remainder: x - trunc(x/y) * y - // This differs from K's %Float which is IEEE 754 remainder (round to nearest). - 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 *Float truncFloat(X /Float Y)) [preserves-definedness] - // error cases for isArithmetic(BOP): // * arguments must be Numbers @@ -2125,18 +2077,6 @@ 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 @@ -2173,14 +2113,6 @@ 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 @@ -2208,19 +2140,9 @@ 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 ``` -Types that are equivlance relations can implement [Eq](https://doc.rust-lang.org/std/cmp/trait.Eq.html), -and then they may implement [Ord](https://doc.rust-lang.org/std/cmp/trait.Ord.html) for a total ordering. -For types that implement `Ord` the `cmp` method must be implemented which can compare any two elements respective to their total ordering. -Here we provide the `binOpCmp` for `Bool` and `Int` operation which returns `-1`, `0`, or `+1` (the behaviour of Rust's `std::cmp::Ordering as i8`), -indicating `LE`, `EQ`, or `GT`. +The `binOpCmp` operation returns `-1`, `0`, or `+1` (the behaviour of Rust's `std::cmp::Ordering as i8`), indicating `LE`, `EQ`, or `GT`. ```k syntax Int ::= cmpInt ( Int , Int ) [function , total] @@ -2255,11 +2177,7 @@ The semantics of the operation in this case is to wrap around (with the given bi ... - rule #applyUnOp(unOpNeg, Float(VAL, WIDTH)) - => - Float(--Float VAL, WIDTH) - ... - + // TODO add rule for Floats once they are supported. ``` 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 f7d87552d..98b522012 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md @@ -52,13 +52,10 @@ 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 1f3f2688d..d34c62b95 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/numbers.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/numbers.md @@ -5,7 +5,6 @@ The code in this file implements functionality for `Integer` and `Float` values ```k requires "./value.md" requires "../ty.md" -requires "rat.md" module RT-NUMBERS imports TYPES @@ -14,8 +13,6 @@ module RT-NUMBERS imports BOOL imports BYTES imports INT - imports FLOAT - imports RAT ``` ## Helpers and Constants for Integer Operations @@ -41,15 +38,6 @@ 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. @@ -122,197 +110,6 @@ 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)) - - // 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 - - // 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 < StringVal( "ERRORFailedToDecodeFloat" ) [owise] - -``` - -Reconstruct a float from its integer significand and adjusted exponent. -For positive exponents, shift the significand left and convert directly. -For negative exponents, use `Rat2Float` to convert the exact rational -`SIG / 2^|AEXP|` to the target float precision. - -```k - syntax Float ::= #reconstructFloat ( sig: Int, adjExp: Int, FloatTy ) [function] - // ------------------------------------------------------------------------------- - rule #reconstructFloat(SIG, AEXP, FLOATTY) - => Int2Float(SIG <=Int 0 - [preserves-definedness] - - rule #reconstructFloat(SIG, AEXP, FLOATTY) - => Rat2Float(SIG /Rat (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 bed580f75..57665d4db 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 ( Float ( 0.42899999999999999e2 , 64 ) ) + ListItem ( thunk ( UnableToDecode ( b"33333sE@" , typeInfoPrimitiveType ( primTypeFloat ( floatTyF64 ) ) ) ) ) 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 e6dc9aec9..47b68a635 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 @@ - #execTerminator ( terminator (... kind: terminatorKindReturn , span: span ( 73 ) ) ) ~> .K + #execStmts ( .Statements ) ~> #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 ( Float ( 0.10000000000000000e2 , 64 ) , ty ( 27 ) , mutabilityNot ) ) + ListItem ( typedValue ( thunk ( UnableToDecode ( b"\x00\x00\x00\x00\x00\x00$@" , typeInfoPrimitiveType ( primTypeFloat ( floatTyF64 ) ) ) ) , 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 ( Float ( 0.10000000000000000e2 , 64 ) ) ) , ty ( 28 ) , mutabilityNot ) ) + ListItem ( thunk ( UnableToDecode ( b"\x00\x00\x00\x00\x00\x00$@" , typeInfoPrimitiveType ( primTypeFloat ( floatTyF64 ) ) ) ) ) ) , ty ( 28 ) , mutabilityNot ) ) ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 11 , 32 , true ) ) ListItem ( BoolVal ( true ) ) - ListItem ( Float ( 0.10000000000000000e2 , 64 ) ) ) , ty ( 29 ) , mutabilityNot ) ) + ListItem ( thunk ( UnableToDecode ( b"\x00\x00\x00\x00\x00\x00$@" , typeInfoPrimitiveType ( primTypeFloat ( floatTyF64 ) ) ) ) ) ) , 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 deleted file mode 100644 index a8edf36d5..000000000 --- a/kmir/src/tests/integration/data/prove-rs/float_arith.rs +++ /dev/null @@ -1,47 +0,0 @@ -#![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); - - // Modulo (truncating) - assert!(7.0_f16 % 4.0_f16 == 3.0_f16); - assert!(7.0_f32 % 4.0_f32 == 3.0_f32); - assert!(7.0_f64 % 4.0_f64 == 3.0_f64); - assert!(7.0_f128 % 4.0_f128 == 3.0_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 deleted file mode 100644 index 747c9a7da..000000000 --- a/kmir/src/tests/integration/data/prove-rs/float_cast.rs +++ /dev/null @@ -1,22 +0,0 @@ -#![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 deleted file mode 100644 index 9144787a2..000000000 --- a/kmir/src/tests/integration/data/prove-rs/float_cmp.rs +++ /dev/null @@ -1,38 +0,0 @@ -#![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 deleted file mode 100644 index 3e0bbeb43..000000000 --- a/kmir/src/tests/integration/data/prove-rs/float_eq.rs +++ /dev/null @@ -1,30 +0,0 @@ -#![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 deleted file mode 100644 index 065ff2bc2..000000000 --- a/kmir/src/tests/integration/data/prove-rs/float_neg.rs +++ /dev/null @@ -1,30 +0,0 @@ -#![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 deleted file mode 100644 index aa6449da2..000000000 --- a/kmir/src/tests/integration/data/prove-rs/float_special.rs +++ /dev/null @@ -1,56 +0,0 @@ -#![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 250d00f51..8bcd12cb6 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -388,17 +388,6 @@ 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', @@ -411,9 +400,7 @@ def test_exec_smir( update_expected_output: bool, tmp_path: Path, ) -> None: - name, input_json, output_kast, depth = test_case - if symbolic and name in EXEC_SMIR_SKIP_HASKELL: - pytest.skip('haskell-backend lacks FLOAT hooks') + _, input_json, output_kast, depth = test_case 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)