refactor(kmir): simplify terminator call setup

.gitignore

@@ -4,6 +4,7 @@ __pycache__/
 /deps/.stable-mir-json
 /.vscode/
 kmir/src/tests/integration/data/**/target
+tmp/
 .DS_Store
 proof/
-/result*
+/result*

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

@@ -1050,6 +1050,8 @@ Literal arrays are also built using this RValue.
 
 
   // #readOperands accumulates a list of `TypedLocal` values from operands
+  syntax KResult ::= List
+
   syntax KItem ::= #readOperands ( Operands )
                  | #readOperandsAux( List , Operands )
                  | #readOn( List, Operands )

kmir/src/kmir/testing/fixtures.py

@@ -20,14 +20,16 @@ def pytest_configure(config) -> None:
     sys.setrecursionlimit(1000000)
 
 
-def _normalize_symbol_hashes(text: str) -> str:
-    """Normalize rustc symbol hash suffixes that drift across builds/environments."""
+def _normalize_unstable_snapshot_values(text: str) -> str:
+    """Normalize values in proof snapshots that drift across builds/environments."""
     # Normalize mangled symbol hashes, including generic names with `$` and `.`.
     # Keep trailing `E` when present; truncated variants may omit it.
     text = re.sub(r'(_ZN[0-9A-Za-z_$.]+17h)[0-9a-fA-F]+E', r'\1<hash>E', text)
     text = re.sub(r'(_ZN[0-9A-Za-z_$.]+17h)[0-9a-fA-F]+', r'\1<hash>', text)
     # Normalize demangled hash suffixes (`...::h<hex>`).
     text = re.sub(r'(::h)[0-9a-fA-F]{8,}', r'\1<hash>', text)
+    # Normalize call target type identifiers that can shift when linked crate metadata changes.
+    text = re.sub(r'(#prepareTerminatorCall \( ty \( )\d+( \) ,)', r'\1<type-id>\2', text)
     return text
 
 
@@ -37,14 +39,13 @@ def assert_or_update_show_output(
     if path_replacements:
         for old, new in path_replacements.items():
             actual_text = actual_text.replace(old, new)
-    # Normalize rustc symbol hash suffixes that can drift across builds/environments.
-    actual_text = _normalize_symbol_hashes(actual_text)
+    actual_text = _normalize_unstable_snapshot_values(actual_text)
     if update:
         expected_file.write_text(actual_text)
     else:
         assert expected_file.is_file()
         expected_text = expected_file.read_text()
-        expected_text = _normalize_symbol_hashes(expected_text)
+        expected_text = _normalize_unstable_snapshot_values(expected_text)
         if actual_text != expected_text:
             diff = '\n'.join(
                 unified_diff(

kmir/src/kmir/utils.py

@@ -289,21 +289,22 @@ def _extract_alloc_id(operands: KInner) -> int | None:
 
 
 def _annotate_nobody_function(k_cell: KInner, smir_info: SMIRInfo) -> list[str]:
-    """If the k cell is `#setUpCalleeData` for a `noBody` callee, return annotation lines with decoded info."""
+    """If the k cell is a pending call to a `noBody` callee, return annotation lines with decoded info."""
 
     from .alloc import Allocation, AllocId, AllocInfo, Memory
     from .linker import _demangle
 
-    setup_call_label = '#setUpCalleeData(_,_,_)_KMIR-CONTROL-FLOW_KItem_MonoItemKind_Operands_Span'
+    prepare_call_label = '#prepareTerminatorCall(_,_,_,_,_,_,_)_KMIR-CONTROL-FLOW_KItem_Ty_MonoItemKind_Operands_Place_MaybeBasicBlockIdx_UnwindAction_Span'
 
     annotations: list[str] = []
 
     match k_cell:
         case KSequence(items=(KApply(label=KLabel(name=label_name), args=args), *_)) | KApply(
             label=KLabel(name=label_name), args=args
-        ) if (label_name == setup_call_label):
+        ) if (label_name == prepare_call_label):
             match args:
                 case [
+                    _,
                     KApply(
                         label=KLabel(name='MonoItemKind::MonoItemFn'),
                         args=[
@@ -313,6 +314,9 @@ def _annotate_nobody_function(k_cell: KInner, smir_info: SMIRInfo) -> list[str]:
                         ],
                     ),
                     operands,
+                    _,
+                    _,
+                    _,
                     KApply(label=KLabel(name='span'), args=[KToken(token=span_str)]),
                 ]:
                     def_id = int(def_id_str)

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

@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (44 steps)
+│  (55 steps)
 ├─ 3 (split)
 │   #expect ( BoolVal ( notBool ARG_UINT1:Int +Int ARG_UINT1:Int &Int 18446744073709
 ┃

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

@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (228 steps)
+│  (243 steps)
 ├─ 3 (terminal)
 │   #EndProgram ~> .K
 │

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

@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (35 steps)
+│  (41 steps)
 ├─ 3 (split)
 │   #expect ( BoolVal ( notBool ARG_UINT1:Int +Int ARG_UINT2:Int &Int 18446744073709
 ┃

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

@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (114 steps)
+│  (127 steps)
 ├─ 3 (split)
 │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) )
 ┃
@@ -14,9 +14,9 @@
 ┃  ├─ 4
 ┃  │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) )
 ┃  │
-┃  │  (6 steps)
+┃  │  (5 steps)
 ┃  └─ 6 (stuck, leaf)
-┃      #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN3std7process4exit17h<hash>
+┃      #prepareTerminatorCall ( ty ( <type-id> ) , monoItemFn ( ... name: symbol ( "_ZN3std7pr
 ┃
 ┗━━┓ subst: .Subst
    ┃ constraint:
@@ -25,7 +25,7 @@
    ├─ 5
    │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) )
    │
-   │  (182 steps)
+   │  (188 steps)
    ├─ 7 (terminal)
    │   #EndProgram ~> .K
    │

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

@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (737 steps)
+│  (800 steps)
 ├─ 3 (terminal)
 │   #EndProgram ~> .K
 │

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

@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (216 steps)
+│  (239 steps)
 ├─ 3 (terminal)
 │   #EndProgram ~> .K
 │

kmir/src/tests/integration/data/exec-smir/call-with-args/closure-call.state

@@ -34,15 +34,14 @@
       ListItem ( typedValue ( Integer ( 32 , 32 , false ) , ty ( 25 ) , mutabilityNot ) )
       ListItem ( typedValue ( thunk ( #decodeConstant ( constantKindZeroSized , ty ( 30 ) , typeInfoVoidType ) ) , ty ( 30 ) , mutabilityNot ) )
       ListItem ( typedValue ( Integer ( 32 , 32 , false ) , ty ( 25 ) , mutabilityNot ) )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 4 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 31 ) , mutabilityMut ) )
-      ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 32 , false ) ) ) , ty ( 26 ) , mutabilityMut ) )
+      ListItem ( typedValue ( Moved , ty ( 31 ) , mutabilityMut ) )
+      ListItem ( typedValue ( Moved , ty ( 26 ) , mutabilityMut ) )
       ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 32 , false ) )
       ListItem ( Integer ( 32 , 32 , false ) ) ) , ty ( 32 ) , mutabilityNot ) )
       ListItem ( typedValue ( thunk ( #decodeConstant ( constantKindZeroSized , ty ( 33 ) , typeInfoVoidType ) ) , ty ( 33 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 1 ) , mutabilityNot ) )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 9 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 34 ) , mutabilityMut ) )
-      ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 32 , false ) )
-      ListItem ( Integer ( 32 , 32 , false ) ) ) , ty ( 32 ) , mutabilityMut ) )
+      ListItem ( typedValue ( Moved , ty ( 34 ) , mutabilityMut ) )
+      ListItem ( typedValue ( Moved , ty ( 32 ) , mutabilityMut ) )
     </locals>
   </currentFrame>
   <stack>

kmir/src/tests/integration/data/exec-smir/call-with-args/main-a-b-with-int.state

@@ -1,19 +1,21 @@
 <kmir>
   <k>
-    #execBlock ( basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 63 ) ) ) ) ~> .K
+    operandConstant ( constOperand (... span: span ( 57 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x0b\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 2 ) , mutability: mutabilityMut ) ) , ty: ty ( 28 ) , id: mirConstId ( 12 ) ) ) ) ~> #readOn ( ListItem ( Integer ( 10 , 64 , false ) ) , .Operands ) ~> #freezer#execTerminatorCall(_,_,_,_,_,_,_,_,_,_)_KMIR-CONTROL-FLOW_KItem_String_Body_Operands_List_KItem_Ty_Place_MaybeBasicBlockIdx_UnwindAction_Span4_ ( "b" ~> .K , body (... blocks: basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 63 ) ) )  .BasicBlocks , locals: localDecl (... ty: ty ( 1 ) , span: span ( 64 ) , mut: mutabilityMut )  localDecl (... ty: ty ( 26 ) , span: span ( 65 ) , mut: mutabilityNot )  localDecl (... ty: ty ( 28 ) , span: span ( 66 ) , mut: mutabilityNot )  .LocalDecls , argCount: 2 , varDebugInfo: varDebugInfo (... name: symbol ( "_s" ) , sourceInfo: sourceInfo (... span: span ( 65 ) , scope: sourceScope ( 0 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) , argumentIndex: someInt ( 1 ) )  varDebugInfo (... name: symbol ( "_t" ) , sourceInfo: sourceInfo (... span: span ( 66 ) , scope: sourceScope ( 0 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) , argumentIndex: someInt ( 2 ) )  .VarDebugInfos , spreadArg: noLocal , span: span ( 67 ) ) ~> .K , operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) )  operandConstant ( constOperand (... span: span ( 57 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x0b\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 2 ) , mutability: mutabilityMut ) ) , ty: ty ( 28 ) , id: mirConstId ( 12 ) ) ) )  .Operands ~> .K , ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Integer ( 10 , 64 , false ) , ty ( 26 ) , mutabilityNot ) ) ~> .K , ty ( 27 ) ~> .K , place (... local: local ( 0 ) , projection: .ProjectionElems ) ~> .K , someBasicBlockIdx ( basicBlockIdx ( 1 ) ) ~> .K , unwindActionContinue ~> .K , span ( 58 ) ~> .K ) ~> .K
   </k>
   <retVal>
     noReturn
   </retVal>
   <currentFunc>
-    ty ( 27 )
+    ty ( 25 )
   </currentFunc>
   <currentFrame>
     <currentBody>
-      ListItem ( basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 63 ) ) ) )
+      ListItem ( basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 56 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 27 ) , id: mirConstId ( 11 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) )  operandConstant ( constOperand (... span: span ( 57 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x0b\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 2 ) , mutability: mutabilityMut ) ) , ty: ty ( 28 ) , id: mirConstId ( 12 ) ) ) )  .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 58 ) ) ) )
+      ListItem ( basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 59 ) ) ) )
     </currentBody>
     <caller>
-      ty ( 25 )
+      ty ( -1 )
     </caller>
     <dest>
       place (... local: local ( 0 ) , projection: .ProjectionElems )
@@ -27,12 +29,9 @@
     <locals>
       ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) )
       ListItem ( typedValue ( Integer ( 10 , 64 , false ) , ty ( 26 ) , mutabilityNot ) )
-      ListItem ( typedValue ( Integer ( 11 , 16 , true ) , ty ( 28 ) , mutabilityNot ) )
     </locals>
   </currentFrame>
   <stack>
-    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( 0 ) , projection: .ProjectionElems ) , someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwindActionContinue , ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) )
-    ListItem ( typedValue ( Integer ( 10 , 64 , false ) , ty ( 26 ) , mutabilityNot ) ) ) )
     ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( 0 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionContinue , ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) ) ) )
     ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
   </stack>

kmir/src/tests/integration/data/exec-smir/enum/enum.state

@@ -1,6 +1,6 @@
 <kmir>
   <k>
-    #selectBlock ( switchTargets (... branches: branch ( 89 , basicBlockIdx ( 7 ) )  branch ( 90 , basicBlockIdx ( 6 ) )  .Branches , otherwise: basicBlockIdx ( 5 ) ) , operandMove ( place (... local: local ( 11 ) , projection: .ProjectionElems ) ) ) ~> .K
+    Integer ( 9090 , 0 , false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 11 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindSwitchInt (... discr: operandMove ( place (... local: local ( 11 ) , projection: .ProjectionElems ) ) , targets: switchTargets (... branches: branch ( 89 , basicBlockIdx ( 7 ) )  branch ( 90 , basicBlockIdx ( 6 ) )  .Branches , otherwise: basicBlockIdx ( 5 ) ) ) , span: span ( 69 ) ) ) ~> .K
   </k>
   <retVal>
     noReturn
@@ -47,7 +47,7 @@
       ListItem ( newLocal ( ty ( 16 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 28 ) , mutabilityNot ) )
       ListItem ( typedValue ( Moved , ty ( 6 ) , mutabilityMut ) )
-      ListItem ( typedValue ( Integer ( 9090 , 0 , false ) , ty ( 29 ) , mutabilityMut ) )
+      ListItem ( newLocal ( ty ( 29 ) , mutabilityMut ) )
       ListItem ( newLocal ( ty ( 26 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 28 ) , mutabilityMut ) )
     </locals>

kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.state

@@ -1,19 +1,20 @@
 <kmir>
   <k>
-    #execTerminator ( terminator (... kind: terminatorKindReturn , span: span ( 65 ) ) ) ~> .K
+    #readOperandsAux ( .List , .Operands ) ~> #freezer#execTerminatorCall(_,_,_,_,_,_,_,_,_,_)_KMIR-CONTROL-FLOW_KItem_String_Body_Operands_List_KItem_Ty_Place_MaybeBasicBlockIdx_UnwindAction_Span4_ ( "b" ~> .K , body (... blocks: basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 60 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 27 ) , id: mirConstId ( 11 ) ) ) ) , args: .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 61 ) ) )  basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 62 ) ) )  .BasicBlocks , locals: localDecl (... ty: ty ( 1 ) , span: span ( 63 ) , mut: mutabilityMut )  .LocalDecls , argCount: 0 , varDebugInfo: .VarDebugInfos , spreadArg: noLocal , span: span ( 64 ) ) ~> .K , .Operands ~> .K , ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) ) ~> .K , ty ( 26 ) ~> .K , place (... local: local ( 0 ) , projection: .ProjectionElems ) ~> .K , someBasicBlockIdx ( basicBlockIdx ( 1 ) ) ~> .K , unwindActionContinue ~> .K , span ( 56 ) ~> .K ) ~> .K
   </k>
   <retVal>
     noReturn
   </retVal>
   <currentFunc>
-    ty ( 27 )
+    ty ( 25 )
   </currentFunc>
   <currentFrame>
     <currentBody>
-      ListItem ( basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 65 ) ) ) )
+      ListItem ( basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 55 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 26 ) , id: mirConstId ( 10 ) ) ) ) , args: .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 56 ) ) ) )
+      ListItem ( basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 57 ) ) ) )
     </currentBody>
     <caller>
-      ty ( 26 )
+      ty ( -1 )
     </caller>
     <dest>
       place (... local: local ( 0 ) , projection: .ProjectionElems )
@@ -29,8 +30,6 @@
     </locals>
   </currentFrame>
   <stack>
-    ListItem ( StackFrame ( ty ( 25 ) , place (... local: local ( 0 ) , projection: .ProjectionElems ) , someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwindActionContinue , ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) ) ) )
-    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( 0 ) , projection: .ProjectionElems ) , someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwindActionContinue , ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) ) ) )
     ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( 0 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionContinue , ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) ) ) )
     ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
   </stack>