Skip to content

Commit 56ab47c

Browse files
StevengreStevengre
committed
refactor(rt): add stable stack frame ids
1 parent cdd73ac commit 56ab47c

82 files changed

Lines changed: 526 additions & 199 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎kmir/src/kmir/kast.py‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -215,8 +215,11 @@ def _make_symbolic_call_config(
215215
types: Mapping[Ty, TypeMetadata],
216216
) -> tuple[KInner, list[KInner]]:
217217
locals, constraints = _symbolic_locals(fn_data.args, types)
218+
init_config = definition.init_config(KSort('GeneratedTopCell'))
219+
_, init_subst = split_config_from(init_config)
218220
subst = Subst(
219221
{
222+
**init_subst,
220223
'K_CELL': fn_data.call_terminator,
221224
'STACK_CELL': list_empty(), # FIXME see #560, problems matching a symbolic stack
222225
'LOCALS_CELL': list_of(locals),

‎kmir/src/kmir/kdist/mir-semantics/kmir.md‎

Lines changed: 10 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -225,6 +225,7 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f
225225
</k>
226226
<currentFunc> _ => CALLER </currentFunc>
227227
//<currentFrame>
228+
<frameId> _ => FRAMEID </frameId>
228229
<currentBody> _ => #getBlocks(CALLER) </currentBody>
229230
<caller> CALLER => NEWCALLER </caller>
230231
<dest> DEST => NEWDEST </dest>
@@ -233,7 +234,7 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f
233234
<locals> ListItem(typedValue(VAL:Value, _, _)) _ => NEWLOCALS </locals>
234235
//</currentFrame>
235236
// remaining call stack (without top frame)
236-
<stack> ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK </stack>
237+
<stack> ListItem(StackFrame(FRAMEID, NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK </stack>
237238
238239
// no value to return, skip writing
239240
rule [termReturnNone]: <k> #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _
@@ -242,6 +243,7 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f
242243
</k>
243244
<currentFunc> _ => CALLER </currentFunc>
244245
//<currentFrame>
246+
<frameId> _ => FRAMEID </frameId>
245247
<currentBody> _ => #getBlocks(CALLER) </currentBody>
246248
<caller> CALLER => NEWCALLER </caller>
247249
<dest> _ => NEWDEST </dest>
@@ -250,7 +252,7 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f
250252
<locals> ListItem(_:NewLocal) _ => NEWLOCALS </locals>
251253
//</currentFrame>
252254
// remaining call stack (without top frame)
253-
<stack> ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK </stack>
255+
<stack> ListItem(StackFrame(FRAMEID, NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK </stack>
254256
255257
syntax List ::= #getBlocks( Ty ) [function, total]
256258
| #getBlocksAux( MonoItemKind ) [function, total]
@@ -356,14 +358,15 @@ where the returned result should go.
356358
</k>
357359
<currentFunc> CALLER => FTY </currentFunc>
358360
<currentFrame>
361+
<frameId> OLDFRAMEID => !_NEWFRAMEID:Int </frameId>
359362
<currentBody> _ </currentBody>
360363
<caller> OLDCALLER => CALLER </caller>
361364
<dest> OLDDEST => DEST </dest>
362365
<target> OLDTARGET => TARGET </target>
363366
<unwind> OLDUNWIND => UNWIND </unwind>
364367
<locals> LOCALS </locals>
365368
</currentFrame>
366-
<stack> STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK </stack>
369+
<stack> STACK => ListItem(StackFrame(OLDFRAMEID, OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK </stack>
367370
requires notBool isIntrinsicFunction(FUNC)
368371
andBool notBool #functionNameMatchesEnv(getFunctionName(FUNC))
369372
@@ -374,14 +377,15 @@ where the returned result should go.
374377
</k>
375378
<currentFunc> CALLER => FTY </currentFunc>
376379
<currentFrame>
380+
<frameId> OLDFRAMEID => !_NEWFRAMEID:Int </frameId>
377381
<currentBody> _ </currentBody>
378382
<caller> OLDCALLER => CALLER </caller>
379383
<dest> OLDDEST => DEST </dest>
380384
<target> OLDTARGET => TARGET </target>
381385
<unwind> OLDUNWIND => UNWIND </unwind>
382386
<locals> LOCALS </locals>
383387
</currentFrame>
384-
<stack> STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK </stack>
388+
<stack> STACK => ListItem(StackFrame(OLDFRAMEID, OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK </stack>
385389
requires notBool isIntrinsicFunction(FUNC)
386390
andBool #functionNameMatchesEnv(getFunctionName(FUNC))
387391
@@ -498,7 +502,7 @@ An operand may be a `Reference` (the only way a function could access another fu
498502
#setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef(getValue(CALLERLOCALS, I)))
499503
...
500504
</k>
501-
<stack> ListItem(StackFrame(_, _, _, _, CALLERLOCALS)) _:List </stack>
505+
<stack> ListItem(StackFrame(_, _, _, _, _, CALLERLOCALS)) _:List </stack>
502506
requires 0 <=Int I
503507
andBool I <Int size(CALLERLOCALS)
504508
andBool isTypedValue(CALLERLOCALS[I])
@@ -510,7 +514,7 @@ An operand may be a `Reference` (the only way a function could access another fu
510514
#setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef(getValue(CALLERLOCALS, I)))
511515
...
512516
</k>
513-
<stack> (ListItem(StackFrame(_, _, _, _, CALLERLOCALS) #as CALLERFRAME => #updateStackLocal(CALLERFRAME, I, Moved))) _:List
517+
<stack> (ListItem(StackFrame(_, _, _, _, _, CALLERLOCALS) #as CALLERFRAME => #updateStackLocal(CALLERFRAME, I, Moved))) _:List
514518
</stack>
515519
requires 0 <=Int I
516520
andBool I <Int size(CALLERLOCALS)

‎kmir/src/kmir/kdist/mir-semantics/rt/configuration.md‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,8 @@ module KMIR-CONFIGURATION
2424
syntax RetVal ::= return( Value )
2525
| "noReturn"
2626
27-
syntax StackFrame ::= StackFrame(caller:Ty, // index of caller function
27+
syntax StackFrame ::= StackFrame(frameId:Int, // stable id for this frame
28+
caller:Ty, // index of caller function
2829
dest:Place, // place to store return value
2930
target:MaybeBasicBlockIdx, // basic block to return to
3031
UnwindAction, // action to perform on panic
@@ -36,6 +37,7 @@ module KMIR-CONFIGURATION
3637
<currentFunc> ty(-1) </currentFunc> // to retrieve caller
3738
// unpacking the top frame to avoid frequent stack read/write operations
3839
<currentFrame>
40+
<frameId> 0 </frameId>
3941
<currentBody> .List </currentBody>
4042
<caller> ty(-1) </caller>
4143
<dest> place(local(-1), .ProjectionElems)</dest>

‎kmir/src/kmir/kdist/mir-semantics/rt/data.md‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -362,8 +362,8 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr
362362
363363
syntax StackFrame ::= #updateStackLocal ( StackFrame, Int, Value ) [function]
364364
365-
rule #updateStackLocal(StackFrame(CALLER, DEST, TARGET, UNWIND, LOCALS), I, VAL)
366-
=> StackFrame(CALLER, DEST, TARGET, UNWIND, LOCALS[I <- typedValue(VAL, tyOfLocal(getLocal(LOCALS, I)), mutabilityMut)])
365+
rule #updateStackLocal(StackFrame(FRAMEID, CALLER, DEST, TARGET, UNWIND, LOCALS), I, VAL)
366+
=> StackFrame(FRAMEID, CALLER, DEST, TARGET, UNWIND, LOCALS[I <- typedValue(VAL, tyOfLocal(getLocal(LOCALS, I)), mutabilityMut)])
367367
requires 0 <=Int I
368368
andBool I <Int size(LOCALS)
369369
andBool isTypedLocal(LOCALS[I])

‎kmir/src/tests/integration/data/crate-tests/single-bin/single_exe::a_module::twice.expected‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11

22
┌─ 1 (root, init)
33
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
4+
│ function: main
45
│
56
│ (44 steps)
67
├─ 3 (split)

‎kmir/src/tests/integration/data/crate-tests/single-bin/single_exe::main.expected‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11

22
┌─ 1 (root, init)
33
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
4+
│ function: main
45
│
56
│ (228 steps)
67
├─ 3 (terminal)

‎kmir/src/tests/integration/data/crate-tests/single-dylib/small_test_dylib::add.expected‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11

22
┌─ 1 (root, init)
33
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
4+
│ function: main
45
│
56
│ (35 steps)
67
├─ 3 (split)

‎kmir/src/tests/integration/data/crate-tests/single-lib/small_test_lib::testing::test_add_in_range.expected‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11

22
┌─ 1 (root, init)
33
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
4+
│ function: main
45
│
56
│ (114 steps)
67
├─ 3 (split)

‎kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,9 @@
11

22
┌─ 1 (root, init)
33
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
4+
│ function: main
45
│
5-
│ (737 steps)
6+
│ (736 steps)
67
├─ 3 (terminal)
78
│ #EndProgram ~> .K
89
│

‎kmir/src/tests/integration/data/crate-tests/two-crate-dylib/crate2::test_crate1_with.expected‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11

22
┌─ 1 (root, init)
33
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
4+
│ function: main
45
│
56
│ (216 steps)
67
├─ 3 (terminal)

0 commit comments

Comments
 (0)