crucible-mir: Re-implement overrides for get_unchecked slice indexing

[RyanGlScott]

Given this Rust code:

fn bar(bytes: &[u8]) -> u32 {
    return 0u32;
}

pub fn foo(arr: &[u8; 4]) -> u32 {
    bar(&arr[0..4])
}

The following spec will crash SAW 1.1:

enable_experimental;

let ref_to_fresh n ty = do {
    x <- mir_fresh_var n ty;
    r <- mir_alloc ty;
    mir_points_to r (mir_term x);
    return (x, r);
};

let foo_spec = do {
    (x, r_x) <- ref_to_fresh "x" (mir_array 4 mir_u8);
    mir_execute_func [r_x];
};

m <- mir_load_module "test.linked-mir.json";
mir_verify m "test::foo" [] false foo_spec z3;

$ ~/Software/saw-1.1/bin/saw test.saw
[11:57:58.326] Loading file "/home/ryanscott/Documents/Hacking/SAW/test.saw"
[11:57:58.332] Verifying test/d9b5c637::foo[0] ...
[11:57:58.340] Simulating test/d9b5c637::foo[0] ...
[11:57:58.341] Stack trace:
"mir_verify" (/home/ryanscott/Documents/Hacking/SAW/test.saw:16:1-16:11)
Symbolic execution failed.
Abort due to assertion failure:
  /home/ryanscott/.rustup/toolchains/nightly-2023-01-23-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:473:43: 473:48 !/home/ryanscott/.rustup/toolchains/nightly-2023-01-23-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/index.rs:386:54: 386:69: error: in core/73237d41::slice[0]::index[0]::{impl#4}[0]::get_unchecked[0]::_instaddce72e1232152c[0]
  Translation error in core/73237d41::slice[0]::index[0]::{impl#4}[0]::get_unchecked[0]::_instaddce72e1232152c[0]: callExp: Don't know how to call core/73237d41::intrinsics[0]::{extern#0}[0]::offset[0]::_instaddce72e1232152c[0]

I used SAW to reproduce this crash (it is surprisingly difficult to reproduce using crux-mir), but the issue really lies in crucible-mir. The problem is that the get_unchecked slice-indexing function (as well as its cousin, get_unchecked_mut) are too low-level for crucible-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 349feee for how these were handled. Unfortunately, these overrides weren't ported over when we upgraded to the 2023-01-23 nightly. I believe that porting these overrides to the more recent nightly would fix this issue. Note that nowadays, the get_unchecked{,_mut} functions now live in core::slice::index::{impl} rather than core::slice::{impl}.

[RyanGlScott]

My assessement in #1180 (comment) 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.