Skip to content

refactor(rt): use frame ids in stack references #1056

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
Stevengre wants to merge 2 commits into from
Closed

refactor(rt): use frame ids in stack references #1056

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
5a6907e
refactor(rt): add stable stack frame ids
Stevengre Apr 7, 2026
77cb2fa
refactor(rt): use frame ids in stack references
Stevengre Apr 10, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 11 additions & 0 deletions kmir/src/kmir/kast.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -215,8 +215,19 @@ def _make_symbolic_call_config(
types: Mapping[Ty, TypeMetadata],
) -> tuple[KInner, list[KInner]]:
locals, constraints = _symbolic_locals(fn_data.args, types)
init_config = definition.init_config(KSort('GeneratedTopCell'))
_, init_subst = split_config_from(init_config)
symbolic_init_cells = (
'FRAMEID_CELL',
'ADDRESSMAP_CELL',
'NEXTADDRESS_CELL',
'EXPOSEDSET_CELL',
'GENERATEDCOUNTER_CELL',
)
symbolic_init_subst = {cell: init_subst[cell] for cell in symbolic_init_cells if cell in init_subst}
subst = Subst(
{
**symbolic_init_subst,
'K_CELL': fn_data.call_terminator,
'STACK_CELL': list_empty(), # FIXME see #560, problems matching a symbolic stack
'LOCALS_CELL': list_of(locals),
Expand Down
33 changes: 19 additions & 14 deletions kmir/src/kmir/kdist/mir-semantics/kmir.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -213,18 +213,19 @@ value is the value in local `_0`, and will go to the _destination_ in
the `LOCALS` of the caller's stack frame. Execution continues with the
context of the enclosing stack frame, at the _target_.

If the returned value is a `Reference`, its stack height must be decremented because a stack frame is popped.
NB that a stack height of `0` cannot occur here, because the compiler prevents local variable references from escaping.
References and pointers already carry stable frame ids, so returning from a call does not require
rewriting the returned value when the callee frame is popped.

If the local `_0` does not have a value (i.e., it remained uninitialised), the function returns unit and writing the value is skipped.

```k
rule [termReturnSome]: <k> #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _
=>
#setLocalValue(DEST, #decrementRef(VAL)) ~> #execBlockIdx(TARGET)
#setLocalValue(DEST, VAL) ~> #execBlockIdx(TARGET)
</k>
<currentFunc> _ => CALLER </currentFunc>
//<currentFrame>
<frameId> _ => FRAMEID </frameId>
<currentBody> _ => #getBlocks(CALLER) </currentBody>
<caller> CALLER => NEWCALLER </caller>
<dest> DEST => NEWDEST </dest>
Expand All @@ -233,7 +234,7 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f
<locals> ListItem(typedValue(VAL:Value, _, _)) _ => NEWLOCALS </locals>
//</currentFrame>
// remaining call stack (without top frame)
<stack> ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK </stack>
<stack> ListItem(StackFrame(FRAMEID, NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK </stack>

// no value to return, skip writing
rule [termReturnNone]: <k> #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _
Expand All @@ -242,6 +243,7 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f
</k>
<currentFunc> _ => CALLER </currentFunc>
//<currentFrame>
<frameId> _ => FRAMEID </frameId>
<currentBody> _ => #getBlocks(CALLER) </currentBody>
<caller> CALLER => NEWCALLER </caller>
<dest> _ => NEWDEST </dest>
Expand All @@ -250,7 +252,7 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f
<locals> ListItem(_:NewLocal) _ => NEWLOCALS </locals>
//</currentFrame>
// remaining call stack (without top frame)
<stack> ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK </stack>
<stack> ListItem(StackFrame(FRAMEID, NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK </stack>

syntax List ::= #getBlocks( Ty ) [function, total]
| #getBlocksAux( MonoItemKind ) [function, total]
Expand Down Expand Up @@ -356,14 +358,15 @@ where the returned result should go.
</k>
<currentFunc> CALLER => FTY </currentFunc>
<currentFrame>
<frameId> OLDFRAMEID => !_NEWFRAMEID:Int </frameId>
<currentBody> _ </currentBody>
<caller> OLDCALLER => CALLER </caller>
<dest> OLDDEST => DEST </dest>
<target> OLDTARGET => TARGET </target>
<unwind> OLDUNWIND => UNWIND </unwind>
<locals> LOCALS </locals>
</currentFrame>
<stack> STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK </stack>
<stack> STACK => ListItem(StackFrame(OLDFRAMEID, OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK </stack>
requires notBool isIntrinsicFunction(FUNC)
andBool notBool #functionNameMatchesEnv(getFunctionName(FUNC))

Expand All @@ -374,14 +377,15 @@ where the returned result should go.
</k>
<currentFunc> CALLER => FTY </currentFunc>
<currentFrame>
<frameId> OLDFRAMEID => !_NEWFRAMEID:Int </frameId>
<currentBody> _ </currentBody>
<caller> OLDCALLER => CALLER </caller>
<dest> OLDDEST => DEST </dest>
<target> OLDTARGET => TARGET </target>
<unwind> OLDUNWIND => UNWIND </unwind>
<locals> LOCALS </locals>
</currentFrame>
<stack> STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK </stack>
<stack> STACK => ListItem(StackFrame(OLDFRAMEID, OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK </stack>
requires notBool isIntrinsicFunction(FUNC)
andBool #functionNameMatchesEnv(getFunctionName(FUNC))

Expand Down Expand Up @@ -438,7 +442,8 @@ where the returned result should go.

The local data has to be set up for the call, which requires information about the local variables of a call. This step is separate from the above call stack setup because it needs to retrieve the locals declaration from the body. Arguments to the call are `Operands` which refer to the old locals (`OLDLOCALS` below), and the data is either _copied_ into the new locals using `#setArgs`, or it needs to be _shared_ via references.

An operand may be a `Reference` (the only way a function could access another function call's `local` variables). For this case, the stack height in the `Reference` must be incremented because a stack frame is added.
An operand may be a `Reference` (the only way a function could access another function call's `local`
variables). With frame-id-based references, argument passing forwards the reference unchanged.

```k
syntax KItem ::= #setUpCalleeData(MonoItemKind, Operands, Span)
Expand Down Expand Up @@ -495,10 +500,10 @@ An operand may be a `Reference` (the only way a function could access another fu

rule <k> #setArgFromStack(IDX, operandCopy(place(local(I), .ProjectionElems)))
=>
#setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef(getValue(CALLERLOCALS, I)))
#setLocalValue(place(local(IDX), .ProjectionElems), getValue(CALLERLOCALS, I))
...
</k>
<stack> ListItem(StackFrame(_, _, _, _, CALLERLOCALS)) _:List </stack>
<stack> ListItem(StackFrame(_, _, _, _, _, CALLERLOCALS)) _:List </stack>
requires 0 <=Int I
andBool I <Int size(CALLERLOCALS)
andBool isTypedValue(CALLERLOCALS[I])
Expand All @@ -507,10 +512,10 @@ An operand may be a `Reference` (the only way a function could access another fu
// TODO: This is not safe, need to add more checks to this.
rule <k> #setArgFromStack(IDX, operandMove(place(local(I), _)))
=>
#setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef(getValue(CALLERLOCALS, I)))
#setLocalValue(place(local(IDX), .ProjectionElems), getValue(CALLERLOCALS, I))
...
</k>
<stack> (ListItem(StackFrame(_, _, _, _, CALLERLOCALS) #as CALLERFRAME => #updateStackLocal(CALLERFRAME, I, Moved))) _:List
<stack> (ListItem(StackFrame(_, _, _, _, _, CALLERLOCALS) #as CALLERFRAME => #updateStackLocal(CALLERFRAME, I, Moved))) _:List
</stack>
requires 0 <=Int I
andBool I <Int size(CALLERLOCALS)
Expand Down Expand Up @@ -574,7 +579,7 @@ Therefore a heuristics is used here:
_SPAN
)
=>
#setLocalValue(place(local(1), .ProjectionElems), #incrementRef(getValue(LOCALS, CLOSURE)))
#setLocalValue(place(local(1), .ProjectionElems), getValue(LOCALS, CLOSURE))
~> #setTupleArgs(2, getValue(LOCALS, TUPLE)) ~> #execBlock(FIRST)
// arguments are tuple components, stored as _2 .. _n
...
Expand Down Expand Up @@ -627,7 +632,7 @@ Therefore a heuristics is used here:
rule <k> #setTupleArgs(_, .List ) => .K ... </k>

rule <k> #setTupleArgs(IDX, ListItem(VAL) REST:List)
=> #setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef(VAL)) ~> #setTupleArgs(IDX +Int 1, REST)
=> #setLocalValue(place(local(IDX), .ProjectionElems), VAL) ~> #setTupleArgs(IDX +Int 1, REST)
...
</k>
```
Expand Down
23 changes: 0 additions & 23 deletions kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,29 +51,6 @@ If nothing is removed, the list remains the same. If all elements are removed, n
rule #Ceil(range(L, A, B)) => #Ceil(L) #And #Ceil(A) #And #Ceil(B) #And {true #Equals A +Int B <=Int size(L)} [simplification]
```

The `#mapOffset` function maps `#adjustRef` over a lists of `Value`s, leaving the list length unchanged.
Definedness of the list and list elements is also guaranteed.

```k
rule size(#mapOffset(L, _)) => size(L) [simplification, preserves-definedness]

rule #Ceil(#mapOffset(L, _)[I]) => #Ceil(L) #And {true #Equals 0 <=Int I} #And {true #Equals I <Int size(L)} [simplification]

rule #Ceil(#mapOffset(L, _)) => #Ceil(L) [simplification]

rule #adjustRef(VAL:Value, 0) => VAL [simplification]

rule #adjustRef(#adjustRef(VAL, OFFSET1), OFFSET2)
=> #adjustRef(VAL, OFFSET1 +Int OFFSET2)
[simplification]

rule #mapOffset(L, 0) => L [simplification]

rule #mapOffset(#mapOffset(L, OFFSET1), OFFSET2)
=> #mapOffset(L, OFFSET1 +Int OFFSET2)
[simplification]
```

## Simplifications for `enum` Discriminants and Variant Indexes

For symbolic enum values, the variant index remains unevaluated but the original (symbolic) discriminant can be restored:
Expand Down
4 changes: 3 additions & 1 deletion kmir/src/kmir/kdist/mir-semantics/rt/configuration.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,8 @@ module KMIR-CONFIGURATION
syntax RetVal ::= return( Value )
| "noReturn"

syntax StackFrame ::= StackFrame(caller:Ty, // index of caller function
syntax StackFrame ::= StackFrame(frameId:Int, // stable id for this frame
caller:Ty, // index of caller function
dest:Place, // place to store return value
target:MaybeBasicBlockIdx, // basic block to return to
UnwindAction, // action to perform on panic
Expand All @@ -36,6 +37,7 @@ module KMIR-CONFIGURATION
<currentFunc> ty(-1) </currentFunc> // to retrieve caller
// unpacking the top frame to avoid frequent stack read/write operations
<currentFrame>
<frameId> 0 </frameId>
<currentBody> .List </currentBody>
<caller> ty(-1) </caller>
<dest> place(local(-1), .ProjectionElems)</dest>
Expand Down
Loading
Loading