Open RyanGlScott opened 5 months ago
My assessement in https://github.com/GaloisInc/crucible/issues/1180#issue-2171350062 is slightly off. crucible-mir
no longer needs custom handles for get_unchecked{,_mut}
, as crucible-mir
now supports pointer offset operations via this code. However, this code only handles the high-level offset
function, but not the offset
intrinsic of the same name, which is what we are failing on in the example above. With that in mind, here is a minimal program that causes crux-mir
to fail with the same error:
// test.rs
#![feature(core_intrinsics)]
use std::intrinsics;
#[crux::test]
pub fn test() -> u32 {
let s: &[u32] = &[1, 2, 3, 4][..];
let ptr: *const u32 = s.as_ptr();
unsafe { *intrinsics::offset(ptr, 1) }
}
$ cabal run exe:crux-mir -- test.rs
test test/454c93d8::test[0]: [Crux] Attempting to prove verification conditions.
FAILED
failures:
---- test/454c93d8::test[0] counterexamples ----
[Crux] Found counterexample for verification goal
[Crux] test.rs:9:34: 9:37: error: in test/454c93d8::test[0]
[Crux] Translation error in test/454c93d8::test[0]: callExp: Don't know how to call core/092bc89a::intrinsics[0]::{extern#0}[0]::offset[0]::_instc5e93708b8ca6e2a[0]
[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.
It should be straightforward to extend the existing offset
override to cover this intrinsic as well.
In a similar theme, we currently have overrides for wrapping_offset
, offset_from
, and sub_ptr
, but not their corresponding intrinsics, which are arith_offset
, ptr_offset_from
, and ptr_offset_from_unsigned
, respectively. We should override these intrinsics as well.
Given this Rust code:
The following spec will crash SAW 1.1:
I used SAW to reproduce this crash (it is surprisingly difficult to reproduce using
crux-mir
), but the issue really lies incrucible-mir
. The problem is that theget_unchecked
slice-indexing function (as well as its cousin,get_unchecked_mut
) are too low-level forcrucible-mir
to handle at the moment.In the previous Rust nightly that
crucible-mir
supported (2020-03-22
), we put custom overrides in place to handle these functions—see https://github.com/GaloisInc/crucible/commit/349feee3c6229b8e4fa477ddfb555c8220a8e42d for how these were handled. Unfortunately, these overrides weren't ported over when we upgraded to the2023-01-23
nightly. I believe that porting these overrides to the more recent nightly would fix this issue. Note that nowadays, theget_unchecked{,_mut}
functions now live incore::slice::index::{impl}
rather thancore::slice::{impl}
.