Add span information (#1088)

This PR propagates the span through the semantics, to help with
inspection/debugging either the programs or the semantics.

We do this by using a new `<currentSpan>` cell, that contains the span
of the instruction currently executing and is updated as needed in
statements and in terminators (in each terminator rule, so as not to
affect the step count - commit #2). The span is also added as part of
the information maintained for a stack frame, saved in calls and
restored on returns. So, we are able to get a location trace using the
`<currentSpan>` plus the stack.

The updated expected outputs show the new behavior, where each
configuration now contains the `<currentSpan>` cell and each
`StackFrame` contains the span.

Running this small example and stopping mid-execution:

```
  fn add(a: i32, b: i32) -> i32 {
      let c = a + b;   // line 2
      c
  }
  fn main() {
      let x = 3;
      let y = 4;
      let z = add(x, y);   // line 9
      assert!(z == 7);
  }
```
, stopping inside add while evaluating a + b gives:

- `<currentSpan>` : the a + b line (line 2, inside add)
- `<stack>` : the suspended main frame has the add(x, y) call-site span
(line 9), below it the entry frame

The trace shows add:2 -> main:9 -> entry (represented by span(0))
showing where execution is and how it got there.

Author: mariaKt

kmir/src/kmir/kast.py

@@ -286,6 +286,7 @@ def mk_call_terminator(target: int, arg_count: int) -> KInner:
                                     KApply(
                                         'constOperand(_,_,_)_BODY_ConstOperand_Span_MaybeUserTypeAnnotationIndex_MirConst',
                                         (
+                                            # synthetic span(0) sentinel (see note on the span below)
                                             KApply('span', token(0)),
                                             KApply('noUserTypeAnnotationIndex_BODY_MaybeUserTypeAnnotationIndex', ()),
                                             KApply(
@@ -312,6 +313,9 @@ def mk_call_terminator(target: int, arg_count: int) -> KInner:
                             KApply('UnwindAction::Continue', ()),
                         ),
                     ),
+                    # Synthetic call-site span for this generated entry/main-call terminator (no real source
+                    # location). Note this differs from the rt/configuration.md <currentSpan> default of
+                    # span(-1), which is the "no span yet" sentinel.
                     KApply('span', token(0)),
                 ),
             ),

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

@@ -84,11 +84,12 @@ blocks, or call another function).
 
   rule <k> #execStmts(.Statements) => .K  ... </k>
 
-  rule <k> #execStmts(STATEMENT:Statement STATEMENTS:Statements)
+  rule <k> #execStmts((statement(_, SPAN) #as STATEMENT) STATEMENTS:Statements)
          =>
            #execStmt(STATEMENT) ~> #execStmts(STATEMENTS)
          ...
        </k>
+       <currentSpan> _ => SPAN </currentSpan>
 ```
 
 `Statement` execution handles the different `StatementKind`s. Some of
@@ -158,10 +159,11 @@ function call, pushing a new stack frame and returning to a different
 block after the call returns.
 
 ```k
-  rule [termGoto]: <k> #execTerminator(terminator(terminatorKindGoto(I), _SPAN)) ~> _CONT
+  rule [termGoto]: <k> #execTerminator(terminator(terminatorKindGoto(I), SPAN)) ~> _CONT
          =>
            #execBlockIdx(I)
        </k>
+       <currentSpan> _ => SPAN </currentSpan>
 ```
 
 A `SwitchInt` terminator selects one of the blocks given as _targets_,
@@ -173,10 +175,11 @@ will be `129`.
 ```k
   syntax KItem ::= #selectBlock ( SwitchTargets , Evaluation ) [strict(2)]
 
-  rule [termSwitchInt]: <k> #execTerminator(terminator(terminatorKindSwitchInt(DISCR, TARGETS), _SPAN)) ~> _CONT
+  rule [termSwitchInt]: <k> #execTerminator(terminator(terminatorKindSwitchInt(DISCR, TARGETS), SPAN)) ~> _CONT
          =>
            #selectBlock(TARGETS, DISCR)
        </k>
+       <currentSpan> _ => SPAN </currentSpan>
 
   // These rules preserve definedness because all the same subterms show up on each side except:
   // - `branch(...)`, which is a constructor.
@@ -233,9 +236,10 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f
          <target> someBasicBlockIdx(TARGET) => NEWTARGET </target>
          <unwind> _ => UNWIND </unwind>
          <locals> ListItem(typedValue(VAL:Value, _, _)) _ => NEWLOCALS </locals>
+         <currentSpan> _ => NEWSPAN </currentSpan> // restore caller's call-site span
        //</currentFrame>
        // remaining call stack (without top frame)
-       <stack> ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK </stack>
+       <stack> ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS, NEWSPAN)) STACK => STACK </stack>
        <functions> FUNCSMAP </functions>
 
   // no value to return, skip writing
@@ -251,9 +255,10 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f
          <target> someBasicBlockIdx(TARGET) => NEWTARGET </target>
          <unwind> _ => UNWIND </unwind>
          <locals> ListItem(_:NewLocal) _ => NEWLOCALS </locals>
+         <currentSpan> _ => NEWSPAN </currentSpan> // restore caller's call-site span
        //</currentFrame>
        // remaining call stack (without top frame)
-       <stack> ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK </stack>
+       <stack> ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS, NEWSPAN)) STACK => STACK </stack>
        <functions> FUNCSMAP </functions>
 
 ```
@@ -329,13 +334,15 @@ where the returned result should go.
         => #execTerminatorCall(Ty, lookupFunction(FUNCSMAP, Ty), ARGS, DEST, TARGET, UNWIND, SPAN)
         ...
        </k>
+       <currentSpan> _ => SPAN </currentSpan>
        <functions> FUNCSMAP </functions>
 
   rule <k> #execTerminator(terminator(terminatorKindCall(operandMove(place(local(I), PROJS)), ARGS, DEST, TARGET, UNWIND), SPAN))
         => #execTerminatorCall({#projectedCallTy(TYPESMAP, I, PROJS, LOCALS)}:>Ty, lookupFunction(FUNCSMAP, {#projectedCallTy(TYPESMAP, I, PROJS, LOCALS)}:>Ty), ARGS, DEST, TARGET, UNWIND, SPAN)
         ...
        </k>
       <locals> LOCALS </locals>
+      <currentSpan> _ => SPAN </currentSpan>
       <functions> FUNCSMAP </functions>
       <types> TYPESMAP </types>
     requires isTy(#projectedCallTy(TYPESMAP, I, PROJS, LOCALS))
@@ -385,8 +392,9 @@ where the returned result should go.
          <target> OLDTARGET => TARGET </target>
          <unwind> OLDUNWIND => UNWIND </unwind>
          <locals> LOCALS </locals>
+         ... // leaves <currentSpan> unchanged: callee arg setup is related to the caller's call-site span
        </currentFrame>
-       <stack> STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK </stack>
+       <stack> STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS, SPAN)) STACK </stack>
     requires notBool isIntrinsicFunction(FUNC)
 
   // Filter check injected after every call: fires as a cut-point only when the function matches the break-on list
@@ -511,7 +519,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])
@@ -523,7 +531,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)
@@ -657,10 +665,11 @@ Otherwise the provided message is passed to a `panic!` call, ending the program
 ```k
   syntax MIRError ::= AssertError ( AssertMessage )
 
-  rule [termAssert]: <k> #execTerminator(terminator(assert(COND, EXPECTED, MSG, TARGET, _UNWIND), _SPAN)) ~> _CONT
+  rule [termAssert]: <k> #execTerminator(terminator(assert(COND, EXPECTED, MSG, TARGET, _UNWIND), SPAN)) ~> _CONT
          =>
            #expect(COND, EXPECTED, MSG) ~> #execBlockIdx(TARGET)
        </k>
+       <currentSpan> _ => SPAN </currentSpan>
 
   syntax KItem ::= #expect ( Evaluation, Bool, AssertMessage ) [strict(1)]
 
@@ -684,19 +693,21 @@ Other terminators that matter at the MIR level "Runtime" are `Drop` and `Unreach
 Drops are elaborated to Noops but still define the continuing control flow. Unreachable terminators lead to a program error.
 
 ```k
-  rule [termDrop]: <k> #execTerminator(terminator(terminatorKindDrop(_PLACE, TARGET, _UNWIND), _SPAN))
+  rule [termDrop]: <k> #execTerminator(terminator(terminatorKindDrop(_PLACE, TARGET, _UNWIND), SPAN))
          =>
            #execBlockIdx(TARGET)
         ...
        </k>
+       <currentSpan> _ => SPAN </currentSpan>
 
   syntax MIRError ::= "ReachedUnreachable"
 
-  rule [termUnreachable]: <k> #execTerminator(terminator(terminatorKindUnreachable, _SPAN))
+  rule [termUnreachable]: <k> #execTerminator(terminator(terminatorKindUnreachable, SPAN))
          =>
            ReachedUnreachable
         ...
        </k>
+       <currentSpan> _ => SPAN </currentSpan>
 ```
 
 ### Stopping on Program Errors

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

@@ -28,7 +28,8 @@ module KMIR-CONFIGURATION
                                    dest:Place,                // place to store return value
                                    target:MaybeBasicBlockIdx, // basic block to return to
                                    UnwindAction,              // action to perform on panic
-                                   locals:List)               // return val, args, local variables
+                                   locals:List,               // return val, args, local variables
+                                   span:Span)                 // call-site span of this frame
 
   configuration <kmir>
                   <k> $PGM:KItem </k>
@@ -42,6 +43,10 @@ module KMIR-CONFIGURATION
                     <target> noBasicBlockIdx </target>
                     <unwind> unwindActionUnreachable </unwind>
                     <locals> .List </locals>
+                    // span of the instruction currently executing in this frame.
+                    // span(-1) is the "no span yet" sentinel (a real Span is an interned, non-negative index).
+                    // Note: this is intentionally distinct from the span(0) synthetic entry/main-call span set in kast.py.
+                    <currentSpan> span(-1) </currentSpan>
                   </currentFrame>
                   // remaining call stack (without top frame)
                   <stack> .List </stack>

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

@@ -365,8 +365,8 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr
 
   syntax StackFrame ::= #updateStackLocal ( StackFrame, Int, Value ) [function]
 
-  rule #updateStackLocal(StackFrame(CALLER, DEST, TARGET, UNWIND, LOCALS), I, VAL)
-      => StackFrame(CALLER, DEST, TARGET, UNWIND, LOCALS[I <- typedValue(VAL, tyOfLocal(getLocal(LOCALS, I)), mutabilityMut)])
+  rule #updateStackLocal(StackFrame(CALLER, DEST, TARGET, UNWIND, LOCALS, SPAN), I, VAL)
+      => StackFrame(CALLER, DEST, TARGET, UNWIND, LOCALS[I <- typedValue(VAL, tyOfLocal(getLocal(LOCALS, I)), mutabilityMut)], SPAN)
     requires 0 <=Int I
      andBool I <Int size(LOCALS)
      andBool isTypedLocal(LOCALS[I])

kmir/src/tests/integration/data/exec-smir/allocs/array_const_compare.state

@@ -45,9 +45,12 @@
       ListItem ( typedValue ( Moved , ty ( 30 ) , mutabilityMut ) )
       ListItem ( newLocal ( ty ( 68 ) , mutabilityMut ) )
     </locals>
+    <currentSpan>
+      span ( 278 )
+    </currentSpan>
   </currentFrame>
   <stack>
-    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
+    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List , span ( 0 ) ) )
   </stack>
   <functions>
     noMap

kmir/src/tests/integration/data/exec-smir/allocs/array_nest_compare.state

@@ -61,9 +61,12 @@
       ListItem ( typedValue ( Moved , ty ( 30 ) , mutabilityMut ) )
       ListItem ( newLocal ( ty ( 84 ) , mutabilityMut ) )
     </locals>
+    <currentSpan>
+      span ( 266 )
+    </currentSpan>
   </currentFrame>
   <stack>
-    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
+    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List , span ( 0 ) ) )
   </stack>
   <functions>
     noMap

kmir/src/tests/integration/data/exec-smir/allocs/enum-two-refs-fail.state

@@ -48,6 +48,9 @@
       ListItem ( newLocal ( ty ( 25 ) , mutabilityMut ) )
       ListItem ( newLocal ( ty ( 25 ) , mutabilityMut ) )
     </locals>
+    <currentSpan>
+      span ( 145 )
+    </currentSpan>
   </currentFrame>
   <stack>
     ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( 0 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionContinue , ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) )
@@ -72,8 +75,8 @@
     ListItem ( newLocal ( ty ( 84 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 1 ) , mutabilityNot ) )
     ListItem ( newLocal ( ty ( 68 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 69 ) , mutabilityNot ) ) ) )
-    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
+    ListItem ( newLocal ( ty ( 69 ) , mutabilityNot ) ) , span ( 116 ) ) )
+    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List , span ( 0 ) ) )
   </stack>
   <functions>
     noMap

kmir/src/tests/integration/data/exec-smir/allocs/option_consts.state

@@ -108,9 +108,12 @@
       ListItem ( newLocal ( ty ( 84 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 86 ) , mutabilityMut ) )
     </locals>
+    <currentSpan>
+      span ( 374 )
+    </currentSpan>
   </currentFrame>
   <stack>
-    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
+    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List , span ( 0 ) ) )
   </stack>
   <functions>
     noMap

kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic-unchecked-runs.state

@@ -50,9 +50,12 @@
       ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Moved )
       ListItem ( Moved ) ) , ty ( 36 ) , mutabilityMut ) )
     </locals>
+    <currentSpan>
+      span ( 116 )
+    </currentSpan>
   </currentFrame>
   <stack>
-    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
+    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List , span ( 0 ) ) )
   </stack>
   <functions>
     noMap

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

@@ -63,9 +63,12 @@
       ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Moved )
       ListItem ( Moved ) ) , ty ( 29 ) , mutabilityMut ) )
     </locals>
+    <currentSpan>
+      span ( 67 )
+    </currentSpan>
   </currentFrame>
   <stack>
-    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
+    ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List , span ( 0 ) ) )
   </stack>
   <functions>
     noMap