[spectec] More functionality for the debugger

[rossberg]

This adds some more functionality to the SpecTec debugger, such as accessing the current frame and using arbitrary paths to access inner values.

@ShinWonho, you wrote the debugger, so you may want to have a look.

Btw, one other feature I'd like is the debugger stopping execution when an AL failure (such as wrong assertion) occurs, instead of just aborting execution. But I'm not sure how I would implement that.

[ShinWonho]

Thanks for adding these new features to the SpecTec debugger!

I have one small suggestion: it might be better to move the functions for accessing the store/frame/env and the print function to ds.ml. What do you think about that?

Regarding stopping the debugger when an AL assertion fails: currently the Assert instruction calls failwith when it fails, which immediately aborts execution. If we slightly modify that part, the debugger should be able to stop execution instead.

This seems fairly straightforward to implement, so I can take care of it.

[rossberg]

I have one small suggestion: it might be better to move the functions for accessing the store/frame/env and the print function to ds.ml. What do you think about that?

SGTM, I'll move those functions to ds.

Regarding stopping the debugger when an AL assertion fails: currently the Assert instruction calls failwith when it fails, which immediately aborts execution. If we slightly modify that part, the debugger should be able to stop execution instead.

This seems fairly straightforward to implement, so I can take care of it.

Cool, thanks! And ideally for other runtime failures, too, like type mismatches.

[rossberg]

@ShinWonho, I moved the access functions to Ds. I left the print functions alone, since their format seems very specific to the debugger.

[rossberg]

@ShinWonho, I'm now seeing a lot of unexpected output on CI. I modified your change such that the exception is only printed when the debugger is active, which fixed it. PTAL.

[ShinWonho]

Oh, I totally forgot to check when the debugger is inactive.
Thank you for the fix!