crucible-mir: Properly parse ArrayToPointer casts

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

crucible-mir/src/Mir/JSON.hs

@@ -403,9 +403,11 @@ instance FromJSON CastKind where
                                                Just (String "Pointer(MutToConstPointer)") -> pure MutToConstPointer
                                                Just (String "UnsizeVtable") -> UnsizeVtable <$> v .: "vtable"
                                                -- TODO: actually plumb this information through if it is relevant
-                                                --      instead of using Misc
+                                               -- instead of using Misc. See
+                                               -- 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

crucible-mir/src/Mir/Mir.hs

@@ -459,7 +459,7 @@ data Vtable = Vtable
     }
     deriving (Show, Eq, Ord, Generic)
 
--- TODO: add other castkinds (see json)
+-- TODO: add other castkinds (see https://github.com/GaloisInc/crucible/issues/1223)
 data CastKind =
     Misc
   | ReifyFnPointer

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());
+}