`crux_mir`: Iterating over 0-length `Vec` fails with `tried to subtract pointers into different arrays`

[qsctr]

When SAW is run on the following function with count = 0

fn sum(count: u32) -> u32 {
    let mut v1 = vec![];
    (0..count).for_each(|i| v1.push(i));
    let mut sum = 0;
    for i in v1 {
        sum += i;
    }
    sum
}

enable_experimental;

m <- mir_load_module "target/wasm32-unknown-unknown/debug/deps/scratch-c883c2110759b0e9.linked-mir.json";

let sum_spec count = do {
  mir_execute_func [mir_term {{ `count : [32] }}];
  mir_return (mir_term {{ sum [0..<count] : [32] }});
};

mir_verify m "scratch::sum" [] false (sum_spec 0) z3;

it fails with

[08:31:21.039] Loading file "/home/bretton/Documents/scratch/test_alloc.saw"
[08:31:22.457] Verifying scratch/aace4ee0::sum[0] ...
[08:31:22.465] Simulating scratch/aace4ee0::sum[0] ...
[08:31:22.470] Stack trace:
"mir_verify" (/home/bretton/Documents/scratch/test_alloc.saw:10:1-10:11)
Symbolic execution failed.
Abort due to assertion failure:
  ./lib/alloc/src/vec/into_iter.rs:210:39: 210:47: error: in alloc/0621aa31::vec[0]::into_iter[0]::{impl#5}[0]::size_hint[0]::_inst793e6cb55b43c40a[0]
  tried to subtract pointers into different arrays

We might need to do something similar to 69e92cb.

[qsctr]

The code in question: https://github.com/GaloisInc/crucible/blob/3af4ac55ccc4ae4b30388d068936fc9a2fbfb85d/crux-mir/lib/alloc/src/vec/into_iter.rs#L206-L213

[RyanGlScott]

A version of the test case that only requires crux-mir:

fn sum(count: u32) -> u32 {
    let mut v1 = vec![];
    (0..count).for_each(|i| v1.push(i));
    let mut sum = 0;
    for i in v1 {
        sum += i;
    }
    sum
}

#[crux::test]
fn f() -> u32 {
    sum(0)
}

$ cabal run exe:crux-mir -- test.rs 
test test/028c4489::f[0]: [Crux] Attempting to prove verification conditions.
FAILED

failures:

---- test/028c4489::f[0] counterexamples ----
[Crux] Found counterexample for verification goal
[Crux]   ./lib/alloc/src/vec/into_iter.rs:210:39: 210:47: error: in alloc/bb1eeb3b::vec[0]::into_iter[0]::{impl#5}[0]::size_hint[0]::_inst793e6cb55b43c40a[0]
[Crux]   tried to subtract pointers into different arrays

[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.

We might need to do something similar to https://github.com/GaloisInc/crucible/commit/69e92cb7c9db05610b4660b31edd7ebfad1d19e8.

Indeed. Currently, vec::IntoIter is defined as:

https://github.com/GaloisInc/crucible/blob/3af4ac55ccc4ae4b30388d068936fc9a2fbfb85d/crux-mir/lib/alloc/src/vec/into_iter.rs#L32-L46

We likely need to add a len: usize field, similarly to the len fields that 69e92cb7c9db05610b4660b31edd7ebfad1d19e8 added for slice::Iter and slice::IterMut.

[qsctr]

Hmm I just noticed this line https://github.com/GaloisInc/crucible/blob/bb50c0d16922e13d6358ce9abc7042ed13feccab/crux-mir/lib/alloc/src/vec/into_iter.rs#L161 It seems like using len might not be enough, since we also need the distances to the start of the buffer

[RyanGlScott]

Good point. That being said, I'm unclear if we really need to patch into_vecdeque() (the function in which this code lives) to make the original example work, so it might suffice to leave that function unchanged for now.

[qsctr]

Yeah I don't think it's needed for the original example. I just meant that if we wanted to fix everything in the file, we would need to add more stuff at some point.

[RyanGlScott]

Certainly. But no need to let perfect be the enemy of good. The current set of patches in our vendored copy of the Rust standard libraries is almost certainly incomplete, so we're not breaking new ground here.