Skip to content

feat(rt): stabilize pointer cast address allocation #1003

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

Draft
Stevengre wants to merge 4 commits into
base: master
Choose a base branch
from
Draft

feat(rt): stabilize pointer cast address allocation #1003

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
3b012b9
fix(test): isolate concurrent smir json outputs
Stevengre Apr 2, 2026
ca20a13
test(prove): add cross-frame pointer cast reproducer
Stevengre Apr 2, 2026
b97ec0f
refactor(rt): add stable stack frame ids
Stevengre Apr 7, 2026
6f65b2c
feat(rt): implement pointer cast address allocation
Stevengre Apr 7, 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
25 changes: 15 additions & 10 deletions kmir/src/kmir/cargo.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@
import os
import shutil
import subprocess
import tempfile
from functools import cached_property
from pathlib import Path
from typing import TYPE_CHECKING
Expand Down Expand Up @@ -180,16 +181,20 @@ def cargo_get_smir_json(
command.append(str(rs_file.resolve()))

cwd = cwd or Path.cwd()
smir_json_result = cwd / rs_file.with_suffix('.smir.json').name
run_process_2(command, cwd=cwd)
json_smir = json.loads(smir_json_result.read_text())
_LOGGER.info(f'Loaded: {smir_json_result}')
if save_smir:
_LOGGER.info(f'SMIR JSON available at: {smir_json_result}')
else:
smir_json_result.unlink()
_LOGGER.info(f'Deleted: {smir_json_result}')
return json_smir
smir_name = rs_file.with_suffix('.smir.json').name
with tempfile.TemporaryDirectory(prefix=f'{rs_file.stem}.smir.', dir=cwd) as temp_dir:
workdir = Path(temp_dir)
smir_json_result = workdir / smir_name
run_process_2(command, cwd=workdir)
json_smir = json.loads(smir_json_result.read_text())
_LOGGER.info(f'Loaded: {smir_json_result}')
if save_smir:
saved_smir = cwd / smir_name
shutil.move(smir_json_result, saved_smir)
_LOGGER.info(f'SMIR JSON available at: {saved_smir}')
else:
_LOGGER.info(f'Deleted with temporary directory: {smir_json_result}')
return json_smir


def stable_mir_json() -> Path:
Expand Down
10 changes: 10 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,18 @@ 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',
)
subst = Subst(
{
**{cell: init_subst[cell] for cell in symbolic_init_cells},
'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
16 changes: 10 additions & 6 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 @@ -225,6 +225,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> 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 @@ -498,7 +502,7 @@ An operand may be a `Reference` (the only way a function could access another fu
#setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef(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 @@ -510,7 +514,7 @@ An operand may be a `Reference` (the only way a function could access another fu
#setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef(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
10 changes: 9 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 @@ -19,12 +19,15 @@ requires "./value.md"
module KMIR-CONFIGURATION
imports INT-SYNTAX
imports BOOL-SYNTAX
imports MAP
imports SET
imports RT-VALUE-SYNTAX

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 +39,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 All @@ -45,6 +49,10 @@ module KMIR-CONFIGURATION
</currentFrame>
// remaining call stack (without top frame)
<stack> .List </stack>
// address allocation model for pointer-to-integer casts
<addressMap> .Map </addressMap>
<nextAddress> 4096 </nextAddress>
<exposedSet> .Set </exposedSet>
</kmir>
```

Expand Down
Loading
Loading