Skip to content

Add span information#1088

Open
mariaKt wants to merge 3 commits into
masterfrom
mk/span-info
Open

Add span information#1088
mariaKt wants to merge 3 commits into
masterfrom
mk/span-info

Conversation

@mariaKt

@mariaKt mariaKt commented Jun 15, 2026

Copy link
Copy Markdown
Collaborator

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.

@mariaKt mariaKt requested review from dkcumming and ehildenb June 15, 2026 23:38
Comment on lines 45 to +46
<locals> .List </locals>
<currentSpan> span(-1) </currentSpan> // span of the instruction currently executing in this frame

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe th edefault could be .Span instead of span(-1), and it could be a MaybeSpan? But this also looks fine, just a though. Feel free to merge it either way.

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I thought that .Span would be if Span was a List sort to indicate an empty list, or do we do this otherwise? Wouldn't we need to change the defintion of Span to do this? Currently it is:

syntax Span ::= span(Int) [group(mir-int), symbol(span)] 

where the group(mir-int) indicates that we have we have an wrapped / interned integer. Span on the stable-mir side looks like this:

#[derive(Clone, Copy, PartialEq, Eq, Serialize)]
pub struct Span(usize);

It feels like we shouldn't change it but I am not confident on that. If there is a better way to do things I am definitely for it.

@dkcumming dkcumming left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I left a response to Everett's comment. Otherwise all good except that I think the value of the sentinel should be noted to be different to what we are using in kast.py, I don't think that is bad just flagging it.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants