conflicting requirements: diagnostics vs logic

[oli-obk]

Just like the rust compiler miri is getting more complicated and tracking more data in order to improve its diagnostics. @rust-lang/wg-diagnostics has been working on improving the situation, but the big hammer we always wanted has been out of reach due to lack of resources.

Now, miri is a quite a bit smaller than rustc and its entanglement with diagnostics not as strong yet.

My proposal is basically to implement a version of #17 that allows rerunning after a failure, but this time tracking data without caring abot speed (note:speed is not the goal here, simplicity is). This requires a few things:

• recording nondeterministic input in disable-isolation mode
• make parts of miri generic over the additional data that should be tracked and reported
  • this will allow us to move the tracking part into its very own module and possibly even crate. I'd hope we'd be able to isolate all memory model logic into a crate that then gets used by the crate that applies extra tracking. A separate binary could be supplied that will just throw unhelpful gibberish at you, but uses only the memory model logic without any of the convenience things we added for usability.

[RalfJung]

That sounds very complicated, can't we "just" to good ol' "split the code into different files"?

[oli-obk]

We can, but you'll still end up with random fields that are only useful for diagnostics in the non-diagnostics code.

It's not more complicated that the machine split, although arguably that is complicated

[RalfJung]

Yeah, there's some extra (opaque) state that needs to be carried around. That seems easy though, we have experience with that with all the Extra types we already have.

[oli-obk]

Stashing this idea for now. It doesn't seem too problematic looking at the motivating PR #2030