Add span information#1088
Open
mariaKt wants to merge 3 commits into
Open
Conversation
ehildenb
approved these changes
Jun 19, 2026
Comment on lines
45
to
+46
| <locals> .List </locals> | ||
| <currentSpan> span(-1) </currentSpan> // span of the instruction currently executing in this frame |
Member
There was a problem hiding this comment.
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.
Collaborator
There was a problem hiding this comment.
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.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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 eachStackFramecontains the span.Running this small example and stopping mid-execution:
, 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 frameThe trace shows add:2 -> main:9 -> entry (represented by span(0)) showing where execution is and how it got there.