crucible-mir: Make translation errors non-fatal

[RyanGlScott]

Consider the following program:

pub fn f() -> u32 {
    42
}

pub fn g() {
    panic!("Don't run me")
}

It is conceivable that we would want to verify f in SAW but not g. Despite this, if you load this program's MIR JSON into SAW using mir_load_module, it will crash before you even have a chance to verify any functions:

[12:54:23.144] Loading file "/home/ryanscott/Documents/Hacking/Haskell/saw-script/test.saw"
[12:54:23.180] standalone use of `dyn` is not supported: TyDynamic core/73237d41::any[0]::Any[0]::_trait646b6cc91b1abac7[0]
CallStack (from HasCallStack):
  error, called at src/Mir/TransTy.hs:228:25 in crucible-mir-0.1-inplace:Mir.TransTy
  tyToRepr, called at src/Mir/Trans.hs:868:12 in crucible-mir-0.1-inplace:Mir.Trans
  evalCast', called at src/Mir/Trans.hs:936:5 in crucible-mir-0.1-inplace:Mir.Trans
  evalCast, called at src/Mir/Trans.hs:993:30 in crucible-mir-0.1-inplace:Mir.Trans
  evalRval, called at src/Mir/Trans.hs:1219:11 in crucible-mir-0.1-inplace:Mir.Trans
  transStatement, called at src/Mir/Trans.hs:1685:68 in crucible-mir-0.1-inplace:Mir.Trans
  translateBlockBody, called at src/Mir/Trans.hs:1694:28 in crucible-mir-0.1-inplace:Mir.Trans
  registerBlock, called at src/Mir/Trans.hs:1734:10 in crucible-mir-0.1-inplace:Mir.Trans
  genFn, called at src/Mir/Trans.hs:1780:24 in crucible-mir-0.1-inplace:Mir.Trans
  transDefine, called at src/Mir/Trans.hs:2237:30 in crucible-mir-0.1-inplace:Mir.Trans
  transCollection, called at src/Mir/ParseTranslate.hs:76:26 in crucible-mir-0.1-inplace:Mir.ParseTranslate
  translateMIR, called at src/SAWScript/Crucible/MIR/Builtins.hs:358:11 in saw-script-1.0.0.99-inplace:SAWScript.Crucible.MIR.Builtins

Ultimately, the issue lies in the fact that crucible-mir crashes when translating g into a Crucible CFG, even if that CFG is never simulated. This is a poor experience for SAW users, as it means that functions unrelated to the verification effort can prevent the code from being loaded into SAW, and the only workaround at present is to comment out large chunks of code.

When crucible-mir encounters a situation like this, it should not crash, but instead emit a CFG that errors when simulated. This is the behavior of crucible-mir's mirFail function, and the fact that crucible-mir crashes on this program is the result of using error instead of mirFail here:

crucible/crucible-mir/src/Mir/TransTy.hs

Lines 225 to 228 in 0d26e4a

	-- We don't support unsized rvalues. Currently we error only for standalone
	-- standalone (i.e., not under `TyRef`/`TyRawPtr`) use of `TyDynamic` - we
	-- should do the same for TySlice and TyStr as well.
	M.TyDynamic _trait -> error $ unwords ["standalone use of `dyn` is not supported:", show t0]

We should replace error with mirFail here, which would likely fix the issue at hand. We should also audit other uses of error in MirGenerator-adjacent code to make sure that similar issues are prevented.

A secondary goal is to make crucible-mir be able to successfully translate code involving panic!. Doing so would require figuring out which function(s) in panic!'s chain of macro-expanded function calls needs to be overridden. For the time being, a workaround is to use unimplemented! instead of panic!.

[spernsteiner]

In general I agree with changing error to mirFail wherever we can. But I'm surprised to see this particular error being hit. "Standalone use of dyn" should mean that it saw a local of type dyn Foo, which is normally illegal - dyn Foo unsized, so it can only be manipulated through a pointer like &dyn Foo. We should investigate whether this error is coming from code in the standard library that's using the unstable "unsized locals" feature, and if so, whether we can patch it out.