refactor(kmir): simplify terminator call setup#1072
refactor(kmir): simplify terminator call setup#1072
Conversation
Stevengre
force-pushed
the
jh/refactor-exec-terminator-call
branch
from
52dfd19 to
a96997c
Compare
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: f95cabe0b3
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| rule #switchMatch(1, BoolVal(B) ) => B | ||
| rule #switchMatch(I, Integer(I2, WIDTH, _)) => I ==Int truncate(I2, WIDTH, Unsigned) requires 0 <Int WIDTH | ||
| rule #switchMatch(I, Integer(I2, 0 , _)) => I ==Int I2 | ||
| rule #switchMatch(_, _ ) => false [owise] |
There was a problem hiding this comment.
The new catch-all rule #switchMatch(_, _) => false [owise] makes #switchMatch return false for symbolic discriminants like thunk(_), which means #selectBlock will always discard explicit branches and fall through to the default block. Because #switchCanUse(thunk(_)) is still true, this is a behavioral regression for symbolic execution: unknown SwitchInt conditions no longer fork and can hide reachable error paths/assertion failures.
Useful? React with 👍 / 👎.
| // Non-intrinsic calls materialize their arguments while the caller frame is still current. | ||
| // Closure-shim tuple arguments are normalized before entering the callee, so | ||
| // the callee sees the argument values to assign to locals `_1`, `_2`, ... | ||
| rule <k> #prepareTerminatorCall(FTY, monoItemFn(symbol(NAME), _, someBody(BODY)), ARGS, DEST, TARGET, UNWIND, SPAN) | ||
| => #prepareBodyCall(.List, NAME, BODY, ARGS, ARGS, LOCALS, FTY, DEST, TARGET, UNWIND, SPAN) | ||
| </k> | ||
| <locals> LOCALS </locals> | ||
|
|
||
| rule <k> #prepareBodyCall(ACC, NAME, BODY, ORIGINAL, .Operands, CALLERLOCALS, FTY, DEST, TARGET, UNWIND, SPAN) | ||
| => #execTerminatorCall(NAME, #normalizeCallValues(BODY, ORIGINAL, ACC, CALLERLOCALS), BODY, FTY, DEST, TARGET, UNWIND, SPAN) | ||
| ... | ||
| </k> | ||
|
|
||
| rule <k> #prepareBodyCall(ACC, NAME, BODY, ORIGINAL, OP:Operand REST:Operands, CALLERLOCALS, FTY, DEST, TARGET, UNWIND, SPAN) | ||
| => OP ~> #prepareBodyCall(ACC, NAME, BODY, ORIGINAL, REST, CALLERLOCALS, FTY, DEST, TARGET, UNWIND, SPAN) | ||
| ... | ||
| </k> | ||
|
|
||
| rule <k> VAL:Value ~> #prepareBodyCall(ACC, NAME, BODY, ORIGINAL, REST:Operands, CALLERLOCALS, FTY, DEST, TARGET, UNWIND, SPAN) | ||
| => #prepareBodyCall(ACC ListItem(VAL), NAME, BODY, ORIGINAL, REST, CALLERLOCALS, FTY, DEST, TARGET, UNWIND, SPAN) | ||
| ... | ||
| </k> |
There was a problem hiding this comment.
This looks like #prepareBodyCall is basically used to heat/cool the Operands into Value, is that right? In that case, could we just mark #execTerminatorCall as strict on the 5th argument, and have heating and cooling take care of it? It could heat the entire list of Operands, turn them into Values, then cool it back in? Not sure if it would work as currently configured, but maybe it would be a simpler approach?
There was a problem hiding this comment.
Fixed here: f92b40d
I use #readOperands to achieve this goal, but the side effect is to add syntax KResult := List. Another way to solve this might change #readOperands implementation and generate a Range Value in the end.
What's your idea?
2 participants
Summary
monoItemFncalls directly and keep no-body calls stuck at#prepareTerminatorCallfor annotation.kmir.mdhelper functions as total, adding fallback behavior where the return sort can represent the fallback.kmir/src/kmir/utils.pyto recognize the new stuck call shape.Testing
git diff --check -- kmir/src/kmir/kdist/mir-semantics/kmir.md kmir/src/kmir/utils.pymake buildmake checkmake test-integration TEST_ARGS="--update-expected-output"was started and then interrupted at about 17%; generated expected-output updates remain unstaged and are not included in this draft PR.Known Limitations / Follow-ups