From bc8e088edb75493b57f6801b88d808f81820a578 Mon Sep 17 00:00:00 2001 From: JianHong Zhao Date: Tue, 7 Apr 2026 12:35:08 +0800 Subject: [PATCH 1/5] ci(stable-mir-ui): make manual UI workflow runnable (#975) ## Summary - make the manual `test-stable-mir-ui` workflow runnable on the self-hosted runner - derive the Rust toolchain from repo-tracked `rust-toolchain.toml` instead of hardcoding it in the workflow - derive the `rust-lang/rust` checkout commit from the active toolchain's `rustc -vV` output instead of maintaining a separate fixed Rust source pin - upload the real failure outputs from inside the Docker container, including updated `skip.txt` when requested ## Context - Stacked on #968 / `codex/import-stable-mir-ui-tests` - The base PR adds the workflow; this PR makes that workflow usable end-to-end in the containerized setup while keeping both the installed toolchain and the checked-out Rust source tree aligned to the same nightly ## Testing - Manual validation on `zhaoji`: rebuilt the workflow image after deriving `RUST_TOOLCHAIN=nightly-2024-11-29` from `rust-toolchain.toml` - Manual validation on `zhaoji`: verified `make stable-mir-json` succeeds before the UI run - Manual validation on `zhaoji`: verified `test-filter='foo or bar'` is passed through correctly - Manual validation on `zhaoji`: verified proof artifacts and updated `skip.txt` are copied back from the container - Local container validation: verified `rustc -vV` in the workflow image resolves `commit-hash: a2545fd6fc66b4323f555223a860c451885d1d2b` for `nightly-2024-11-29`, and the workflow's shallow `rust-lang/rust` checkout can `fetch` and `checkout` that commit successfully - Local container validation: verified `make stable-mir-json` and `make build` succeed after aligning the Rust checkout from the active toolchain - Local container validation: ran a single-case smoke path (`tests/ui/issues/issue-11205.rs`) through `RUST_DIR_ROOT=rust make test-stable-mir-ui`; workflow plumbing succeeded and the test reached the proof stage, while the proof itself still failed with `AssertionError: Proof did not pass` --- .github/actions/with-docker/action.yml | 3 + .github/workflows/Dockerfile | 5 +- .github/workflows/test-stable-mir-ui.yml | 133 +++++++++++++++++++++++ 3 files changed, 139 insertions(+), 2 deletions(-) create mode 100644 .github/workflows/test-stable-mir-ui.yml diff --git a/.github/actions/with-docker/action.yml b/.github/actions/with-docker/action.yml index 4768fc740..a4f6b589c 100644 --- a/.github/actions/with-docker/action.yml +++ b/.github/actions/with-docker/action.yml @@ -17,6 +17,8 @@ runs: TAG=runtimeverificationinc/${CONTAINER_NAME} K_COMMIT=$(grep -Po '[0-9.]+' ./deps/k_release) UV_VERSION=$(cat deps/uv_release) + RUST_TOOLCHAIN=$(sed -nE 's/^channel = "([^"]+)"/\1/p' rust-toolchain.toml) + test -n "${RUST_TOOLCHAIN}" USER=github-user GROUP=${USER} @@ -30,6 +32,7 @@ runs: --build-arg GROUP=${GROUP} \ --build-arg USER_ID=${USER_ID} \ --build-arg GROUP_ID=${GROUP_ID} \ + --build-arg RUST_TOOLCHAIN=${RUST_TOOLCHAIN} \ --build-arg UV_VERSION=${UV_VERSION} docker run \ diff --git a/.github/workflows/Dockerfile b/.github/workflows/Dockerfile index fabcdd03a..54cc1ad44 100644 --- a/.github/workflows/Dockerfile +++ b/.github/workflows/Dockerfile @@ -10,13 +10,14 @@ ARG USER=user ARG GROUP ARG USER_ID=1000 ARG GROUP_ID=1000 +ARG RUST_TOOLCHAIN=nightly-2024-11-29 RUN groupadd -g ${GROUP_ID} ${GROUP} && useradd -m -u ${USER_ID} -s /bin/sh -g ${GROUP} ${USER} USER ${USER}:${GROUP} ENV PATH="/home/${USER}/.cargo/bin:${PATH}" RUN curl https://sh.rustup.rs -sSf | bash -s -- -y -RUN rustup toolchain install nightly-2024-11-29 --component llvm-tools --component rustc-dev --component rust-src -RUN rustup default nightly-2024-11-29-x86_64-unknown-linux-gnu +RUN rustup toolchain install ${RUST_TOOLCHAIN} --component llvm-tools --component rustc-dev --component rust-src +RUN rustup default ${RUST_TOOLCHAIN} RUN mkdir /home/${USER}/workspace WORKDIR /home/${USER}/workspace diff --git a/.github/workflows/test-stable-mir-ui.yml b/.github/workflows/test-stable-mir-ui.yml new file mode 100644 index 000000000..77286abab --- /dev/null +++ b/.github/workflows/test-stable-mir-ui.yml @@ -0,0 +1,133 @@ +name: 'Stable MIR UI Tests' +on: + workflow_dispatch: + inputs: + test-filter: + description: 'Passed as -k to pytest (empty = all tests)' + type: string + default: '' + update-skip: + description: 'Enable --update-skip mode to shrink skip.txt' + type: boolean + default: false + timeout: + description: 'Per-test timeout in seconds' + type: string + default: '300' + +jobs: + stable-mir-ui-tests: + name: 'Stable MIR UI Tests' + runs-on: [self-hosted, linux, normal] + env: + CONTAINER_NAME: mir-ui-ci-${{ github.sha }} + steps: + - name: 'Check out code' + uses: actions/checkout@v4 + with: + token: ${{ secrets.JENKINS_GITHUB_PAT }} + submodules: recursive + + - name: 'Check out Rust repo' + uses: actions/checkout@v4 + with: + repository: rust-lang/rust + path: rust + fetch-depth: 1 + + - name: 'Set up Docker' + uses: ./.github/actions/with-docker + with: + container-name: ${{ env.CONTAINER_NAME }} + + - name: 'Copy Rust repo into container' + run: docker cp rust ${{ env.CONTAINER_NAME }}:/home/github-user/workspace/rust + + - name: 'Align Rust checkout with active toolchain' + run: | + docker exec --user github-user ${{ env.CONTAINER_NAME }} bash -lc ' + set -euo pipefail + cd /home/github-user/workspace + rust_commit="$(rustc -vV | sed -n "s/^commit-hash: //p")" + test -n "$rust_commit" + git -C rust fetch origin "$rust_commit" --depth 1 + git -C rust checkout "$rust_commit" + ' + + - name: 'Build stable-mir-json' + run: docker exec --user github-user ${{ env.CONTAINER_NAME }} make stable-mir-json + + - name: 'Build kmir' + run: docker exec --user github-user ${{ env.CONTAINER_NAME }} make build + + - name: 'Run stable-mir-ui tests' + env: + INPUT_FILTER: ${{ inputs.test-filter }} + INPUT_TIMEOUT: ${{ inputs.timeout }} + INPUT_UPDATE_SKIP: ${{ inputs.update-skip }} + run: | + test_args=(--timeout="${INPUT_TIMEOUT}") + if [ -n "${INPUT_FILTER}" ]; then + test_args+=(-k "${INPUT_FILTER}") + fi + if [ "${INPUT_UPDATE_SKIP}" = "true" ]; then + test_args+=(--update-skip) + fi + printf -v test_args_escaped '%q ' "${test_args[@]}" + docker exec --user github-user \ + --env RUST_DIR_ROOT=rust \ + ${{ env.CONTAINER_NAME }} \ + make test-stable-mir-ui "TEST_ARGS=${test_args_escaped}" + + - name: 'Copy proof artifacts from container' + if: failure() + run: | + rm -rf .github-artifacts/proof-artifacts + mkdir -p .github-artifacts/proof-artifacts + docker exec --user github-user ${{ env.CONTAINER_NAME }} bash -lc ' + set -euo pipefail + artifact_dir=/home/github-user/workspace/.github-artifacts/proof-artifacts + rm -rf "$artifact_dir" + mkdir -p "$artifact_dir" + find /tmp -type f \( -name show.txt -o -path "*/smir.json" \) -print0 | while IFS= read -r -d "" path; do + case_dir="$(dirname "$path")" + if [ "$(basename "$path")" = "smir.json" ]; then + case_dir="$(dirname "$case_dir")" + fi + rel="${case_dir#/tmp/}" + dest="$artifact_dir/$rel" + rm -rf "$dest" + mkdir -p "$(dirname "$dest")" + cp -R "$case_dir" "$dest" + done + ' + docker cp ${{ env.CONTAINER_NAME }}:/home/github-user/workspace/.github-artifacts/proof-artifacts/. .github-artifacts/proof-artifacts/ || true + + - name: 'Upload proof artifacts on failure' + if: failure() + uses: actions/upload-artifact@v4 + with: + name: proof-artifacts + path: .github-artifacts/proof-artifacts + if-no-files-found: ignore + + - name: 'Copy updated skip.txt from container' + if: ${{ always() && inputs.update-skip }} + run: | + rm -rf .github-artifacts/update-skip + mkdir -p .github-artifacts/update-skip + docker cp \ + ${{ env.CONTAINER_NAME }}:/home/github-user/workspace/kmir/src/tests/external/data/stable-mir-ui/skip.txt \ + .github-artifacts/update-skip/skip.txt || true + + - name: 'Upload updated skip.txt' + if: inputs.update-skip + uses: actions/upload-artifact@v4 + with: + name: updated-skip-txt + path: .github-artifacts/update-skip/skip.txt + if-no-files-found: ignore + + - name: 'Tear down Docker' + if: always() + run: docker stop --time 0 ${{ env.CONTAINER_NAME }} From 63ce7ebecdc1916ac5adaeef36b525049e30de6e Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Tue, 7 Apr 2026 12:38:52 -0500 Subject: [PATCH 2/5] Increased timeout of `Haskell Exec SMIR` CI test (#1021) Our PRs currently mostly fail CI due to the `Haskell Exec SMIR` CI test timing out. I increased it from 20 to 30 minutes. --- .github/workflows/test.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 9cd42fc1c..b19f8dbbe 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -65,7 +65,7 @@ jobs: - name: 'Haskell Exec SMIR' test-args: '-k "test_exec_smir and haskell"' parallel: 6 - timeout: 20 + timeout: 30 - name: 'Haskell Termination' test-args: '-k test_prove_termination' parallel: 6 From 2bc8a1645bf9ec2b7e841b20521d8fd8089029e4 Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Tue, 7 Apr 2026 18:11:16 -0500 Subject: [PATCH 3/5] Another increase of timeout for Haskell Exec SMIR CI test (#1023) The timeout increase [here](https://github.com/runtimeverification/mir-semantics/pull/1021) is not enough (depending on the state of the GH runners, this is still a bit too tight). I measured locally, and it took around 40 minutes, so I added another 10 as a leeway for a total of 50 min. --- .github/workflows/test.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index b19f8dbbe..4e7f79076 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -65,7 +65,7 @@ jobs: - name: 'Haskell Exec SMIR' test-args: '-k "test_exec_smir and haskell"' parallel: 6 - timeout: 30 + timeout: 60 - name: 'Haskell Termination' test-args: '-k test_prove_termination' parallel: 6 From f096f6b11d95c8fb45e4a41da82f16b181cc3fe9 Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Wed, 8 Apr 2026 12:21:56 -0500 Subject: [PATCH 4/5] Increase timeouts in CI (#1025) The timeout limits for our CI tests are tight. Depending on the state of the github runners, our CI often fails with just a few more minutes needed. I have noticed test runs being cancelled while making progress, at 90% + (even just after the test have been completed). It would be better to have them be more generous, as having to rerun jobs cancelled due to this is actually leading to more time on the runners. --- .github/workflows/test.yml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) 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 From abd122e33d3dcb28d224dcdf4689843418c10960 Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Fri, 10 Apr 2026 09:53:32 -0500 Subject: [PATCH 5/5] Revert "Basic support for floats (`f16`, `f32`, `f64`, `f128`) (#995)" (#1057) This reverts commit b694d02c3648377a8a1ef221e797ddb988da09a3 (merge commit of PR [#995](https://github.com/runtimeverification/mir-semantics/pull/995) in master). It caused a regression in the spl-token initialize_multisig proofs, where the Haskell backend tried to evaluate Int2Float (the FLOAT.int2float hook). --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 88 +------- .../kmir/kdist/mir-semantics/rt/decoding.md | 7 +- .../kmir/kdist/mir-semantics/rt/numbers.md | 203 ------------------ .../structs-tuples/struct_field_update.state | 2 +- .../structs-tuples/structs-tuples.state | 8 +- .../integration/data/prove-rs/float_arith.rs | 47 ---- .../integration/data/prove-rs/float_cast.rs | 22 -- .../integration/data/prove-rs/float_cmp.rs | 38 ---- .../integration/data/prove-rs/float_eq.rs | 30 --- .../integration/data/prove-rs/float_neg.rs | 30 --- .../data/prove-rs/float_special.rs | 56 ----- .../src/tests/integration/test_integration.py | 15 +- 12 files changed, 11 insertions(+), 535 deletions(-) delete mode 100644 kmir/src/tests/integration/data/prove-rs/float_arith.rs delete mode 100644 kmir/src/tests/integration/data/prove-rs/float_cast.rs delete mode 100644 kmir/src/tests/integration/data/prove-rs/float_cmp.rs delete mode 100644 kmir/src/tests/integration/data/prove-rs/float_eq.rs delete mode 100644 kmir/src/tests/integration/data/prove-rs/float_neg.rs delete mode 100644 kmir/src/tests/integration/data/prove-rs/float_special.rs 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 14b5221c3..16d5f157c 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -386,17 +386,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', @@ -409,9 +398,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)