Skip to content

Commit

Permalink
crucible-mir: Properly parse ArrayToPointer casts
Browse files Browse the repository at this point in the history
Although `crucible-mir` had support for translating these sorts of casts
(`ArrayToPointer` casts), it did not parse them properly. This patch ensures
that `ArrayToPointer` casts are parsed as `Misc`, which allows them to be
handled by the code in `Mir.Trans`.

Fixes #1224.
  • Loading branch information
RyanGlScott committed Jul 18, 2024
1 parent 2909c22 commit edddf4b
Show file tree
Hide file tree
Showing 3 changed files with 26 additions and 0 deletions.
5 changes: 5 additions & 0 deletions crucible-mir/CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -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
Expand Down
1 change: 1 addition & 0 deletions crucible-mir/src/Mir/JSON.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
20 changes: 20 additions & 0 deletions crux-mir/test/conc_eval/ptr/coerce_array_to_pointer.rs
Original file line number Diff line number Diff line change
@@ -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());
}

0 comments on commit edddf4b

Please sign in to comment.