crux-mir doesn't handle byte -> char casts

[sauclovian-g]

crux-mir doesn't handle byte -> char casts. This came up in Formal VerSo. It isn't a problematic conversion so it seems reasonable to just implement it.

[sauclovian-g]

(crux-mir? crucible-mir? actually the latter, not entirely clear on the exact difference/boundary between them)

[RyanGlScott]

(crux-mir? crucible-mir? actually the latter, not entirely clear on the exact difference/boundary between them)

crucible-mir is the underlying symbolic execution machinery for MIR code, and crux-mir is a standalone tool built on top of crucible-mir meant for simulating Rust programs with inline assertions. SAW also depends on crucible-mir, but it does not depend on crux-mir.

[RyanGlScott]

Here is a test case that demonstrates the issue using crux-mir:

pub fn b() -> u8 {
    97
}

#[crux::test]
pub fn test() -> char {
    b() as char
}

$ cabal run exe:crux-mir -- test.rs 
test test/2604af8f::test[0]: [Crux] Attempting to prove verification conditions.
FAILED

failures:

---- test/2604af8f::test[0] counterexamples ----
[Crux] Found counterexample for verification goal
[Crux]   test.rs:7:5: 7:16: error: in test/2604af8f::test[0]
[Crux]   Translation error in test/2604af8f::test[0]: unimplemented cast: Misc
[Crux]     ty: TyUint B8
[Crux]     as: TyChar

[Crux-MIR] ---- FINAL RESULTS ----
[Crux] Goal status:
[Crux]   Total: 1
[Crux]   Proved: 0
[Crux]   Disproved: 1
[Crux]   Incomplete: 0
[Crux]   Unknown: 0
[Crux] Overall status: Invalid.