crucible-mir-comp uses what4 `getCurrentProgramLoc` but not `setCurrentProgramLoc`

[sauclovian-g]

It could be that I'm missing something; however, there are four uses of W4.getCurrentProgramLoc in crucible-mir-comp and no uses of W4.setCurrentProgramLoc, and as best I can tell it doesn't call any of the higher-level things in SAW that would do that for it.

This seems unlikely to produce useful results.

Probably it should either load up the W4 current location, or not use the feature and just pass positions around.

[RyanGlScott]

Looking in just the crucible-mir-comp source code is unlikely to give a complete picture. This is because crucible-mir-comp is effectively an extension of crucible-mir, so crucible-mir-comp inherits crucible-mir's position tracking. For instance, crucible-mir sets the current program locations quite a few places in Mir.Trans (see the calls to setPosition here).

That being said, it's possible that there are some opportunities to make the current position more precise in crucible-mir-comp that we're not taking. Is there an example you have in mind of an error message that could be improved this way?

[sauclovian-g]

As far as I know we have zero test coverage for any of the errors these positions might flow to, so I have no idea. I just noticed this and it seemed broken. If it's not, just close the issue... maybe I can stuff some comments about it into #3291.

[RyanGlScott]

Every failing proof goal that crux-mir and crux-mir-comp reports includes Rust source positions that are put in place via crucible-mir's uses of setPosition. In this sense, every test case in the crux-mir-comp test suite exercises crucible-mir's error position tracking.

There is an additional question of whether these failing proof goals could be made more precise by leveraging additional information from crucible-mir-comp. It's plausible that this is the case, although I don't have a specific example on hand of a program whose error message could be improved this way. My inclination would be to close this issue (since it's unclear if it's actionable in its current state) and instead open a more targeted one if we find an error message whose source position is unhelpfully vague.