Closed sauclovian-g closed 3 days ago
(crux-mir? crucible-mir? actually the latter, not entirely clear on the exact difference/boundary between them)
(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
.
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.
Fixed by #1191.
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.