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..87a8050b2 100644 --- a/crucible-mir/src/Mir/JSON.hs +++ b/crucible-mir/src/Mir/JSON.hs @@ -401,6 +401,7 @@ instance FromJSON CastKind where Just (String "Pointer(UnsafeFnPointer)") -> pure UnsafeFnPointer Just (String "Pointer(Unsize)") -> pure Unsize Just (String "Pointer(MutToConstPointer)") -> pure MutToConstPointer + Just (String "Pointer(ArrayToPointer)") -> pure ArrayToPointer Just (String "UnsizeVtable") -> UnsizeVtable <$> v .: "vtable" -- TODO: actually plumb this information through if it is relevant -- instead of using Misc. See diff --git a/crucible-mir/src/Mir/Mir.hs b/crucible-mir/src/Mir/Mir.hs index 95b25fff5..0e372fc19 100644 --- a/crucible-mir/src/Mir/Mir.hs +++ b/crucible-mir/src/Mir/Mir.hs @@ -468,6 +468,7 @@ data CastKind = | Unsize | UnsizeVtable VtableName | MutToConstPointer + | ArrayToPointer deriving (Show,Eq, Ord, Generic) data Constant = Constant Ty ConstVal diff --git a/crucible-mir/src/Mir/Trans.hs b/crucible-mir/src/Mir/Trans.hs index d03cbfdbc..bfc923a93 100644 --- a/crucible-mir/src/Mir/Trans.hs +++ b/crucible-mir/src/Mir/Trans.hs @@ -868,7 +868,7 @@ evalCast' ck ty1 e ty2 = do -> return $ MirExp (MirReferenceRepr tpr) (getSlicePtr e') -- *const [T; N] -> *const T (get first element) - (M.Misc, M.TyRawPtr (M.TyArray t1 _) m1, M.TyRawPtr t2 m2) + (M.ArrayToPointer, M.TyRawPtr (M.TyArray t1 _) m1, M.TyRawPtr t2 m2) | t1 == t2, m1 == m2, MirExp (MirReferenceRepr (MirVectorRepr tpr)) e' <- e -> MirExp (MirReferenceRepr tpr) <$> subindexRef tpr e' (R.App $ usizeLit 0) 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()); +}