diff --git a/crucible-mir/CHANGELOG.md b/crucible-mir/CHANGELOG.md index 0e5085815..7d5096b55 100644 --- a/crucible-mir/CHANGELOG.md +++ b/crucible-mir/CHANGELOG.md @@ -1,3 +1,8 @@ +# next -- TBA + +* Fix a bug in which `crucible-mir` would fail to parse MIR JSON code involving + casts from array references to pointers. + # 0.2 -- 2024-02-05 * `crucible-mir` now supports the `nightly-2023-01-23` Rust toolchain. Some of diff --git a/crucible-mir/src/Mir/JSON.hs b/crucible-mir/src/Mir/JSON.hs index 618c18810..3006838c2 100644 --- a/crucible-mir/src/Mir/JSON.hs +++ b/crucible-mir/src/Mir/JSON.hs @@ -407,6 +407,7 @@ instance FromJSON CastKind where -- https://github.com/GaloisInc/crucible/issues/1223 Just (String "PointerExposeAddress") -> pure Misc Just (String "PointerFromExposedAddress") -> pure Misc + Just (String "Pointer(ArrayToPointer)") -> pure Misc Just (String "DynStar") -> pure Misc Just (String "IntToInt") -> pure Misc Just (String "FloatToInt") -> pure Misc diff --git a/crux-mir/test/conc_eval/ptr/coerce_array_to_pointer.rs b/crux-mir/test/conc_eval/ptr/coerce_array_to_pointer.rs new file mode 100644 index 000000000..7e138e80c --- /dev/null +++ b/crux-mir/test/conc_eval/ptr/coerce_array_to_pointer.rs @@ -0,0 +1,20 @@ +type T = u64; +const COUNT: usize = 16; + +pub fn output_array(src: &[T; COUNT], dst: *mut T) { + unsafe { + std::ptr::copy(src as *const T, dst, COUNT); + } +} + +#[cfg_attr(crux, crux::test)] +pub fn crux_test() -> T { + let src: &[T; COUNT] = &[42; COUNT]; + let dst: &mut [T; COUNT] = &mut [0; COUNT]; + output_array(src, dst as *mut T); + dst[0] +} + +pub fn main() { + println!("{:?}", crux_test()); +}