Open
Conversation
Concrete floats are supported and so the rules that decode them are added in k blocks with `.concrete`, which will mean symbolic floats will decode to `#UnableToDecode`. The casting rules were branching non-deterministically when evaluating the args so I added `#UnsupportedFloatTransmute` as a `MIRError`. I think I have caught all the cases where floats could crash the haskell backend now or create nd branching but I could be wrong.
With decoding for symbolic floats yielding `#UnableToDecode`, (nearly) all float tests can be replaced for the haskell backend as they will not be able to crash on the unsupported hooks. This requires two `.state` files since we have to compare both successful LLVM and unsuccessful Haskell handling of floats. The casts are in a different category as there is `IntToFloat` which does not start with an `#UnableToDecode` and so will reach an unsupported hook and crash. In practice, I believe it is not possible to construct a symbolic float, so these casts are the only danger for crashing the backend. Note: The .state.haskell files are quite large because `kmir run` does not have the ability to `--terminate-on-thunk`. Probably well and truly time to remove `thunk`.
mariaKt
reviewed
Apr 8, 2026
| requires 0 <=Int I andBool I <Int size(LOCALS) | ||
| andBool isTypedLocal(LOCALS[I]) | ||
| andBool #isFloatType(lookupTy({getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS)}:>Ty)) | ||
| [priority(40), preserves-definedness] |
Collaborator
There was a problem hiding this comment.
The float transmute rules cover operandCopy and operandMove source types but not operandConstant. It seems that OperandConstant can reach this rule though.
| # UnableToDecode default rule for float constants. | ||
| if symbolic: | ||
| haskell_output = output_kast.with_suffix('.state.haskell') | ||
| if haskell_output.is_file() or update_expected_output: |
Collaborator
There was a problem hiding this comment.
It seems that the --update-expected-output path creates .state.haskell files for all tests unconditionally. For tests where haskell output is identical to LLVM, this creates files that
- are redundant
- can become stale if
.stateis later updated independently.
I don't mind the redundancy that much, but having stale files can easily lead to mistakes, so I would like a solution that creates the.state.haskellfiles only if needed.
Suggestion: generate fresh .state (LLVM) first, then generate .state.haskell and only keep it when it differs.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR:
.concreteor.symbolicto the md specifiers of the k source;#UnableToDecodeproduced which willthunkany operation containing it, therefore not evaluating it and avoiding crashing the haskell backend which does not have hooks for float functions;exec-smirand separated LLVM and Haskell backendkmir runexpected test files so both behaviours can be tested;kmir runtest inprove-rs/which callskmir proveinvoking the booster backend successfully evaluating the concrete floats;One thing to note is that the expected files for the haskell backend KMIR run are rather large, this is because it branches on
thunk. This could be avoided ifkmir runcould take--terminate-on-thunkaskmir provedoes. Alternatively, and probably most sensible would be to removethunkall together. Any value we could of gained from it is likely already achieved and for myself has been more a source of frustration than benefit for a while.With this inclusion #985 can continue as it will have proper error case for symbolic floats