Add span information

[mariaKt]

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.

[ehildenb]

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.

[dkcumming]

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.

[mariaKt]

I think @ehildenb meant noSpan, not .Span (MaybeSpan already has someSpan/noSpan), and that way no changes are needed in any sort. But, I decided against it while writing this, because making a MaybeSpan means wrapping every write as someSpan(span(N)), and the same for the stack field. It seemed more verbose and heavier for no gain, since span(-1) is already unambiguous. I added a comment documenting it, but I can change it if you want.

[dkcumming]

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.

[mariaKt]

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.

I added comments explaining the difference between these, in both files.