Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

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

Closed
qsctr opened this issue Nov 30, 2023 · 6 comments · Fixed by #1157
Closed

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

qsctr opened this issue Nov 30, 2023 · 6 comments · Fixed by #1157
Assignees
@qsctr
Labels
crucible crux enhancement MIR Issues relating to Rust/MIR support

Comments

@qsctr
Copy link
Contributor

qsctr commented Nov 30, 2023

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 qsctr added enhancement crucible crux MIR Issues relating to Rust/MIR support labels Nov 30, 2023
@qsctr
Copy link
Contributor Author

qsctr commented Nov 30, 2023

The code in question:

crucible/crux-mir/lib/alloc/src/vec/into_iter.rs

Lines 206 to 213 in 3af4ac5

fn size_hint(&self) -> (usize, Option<usize>) {
let exact = if T::IS_ZST {
self.end.addr().wrapping_sub(self.ptr.addr())
} else {
unsafe { self.end.sub_ptr(self.ptr) }
};
(exact, Some(exact))
}

@RyanGlScott
Copy link
Contributor

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 69e92cb.

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

crucible/crux-mir/lib/alloc/src/vec/into_iter.rs

Lines 32 to 46 in 3af4ac5

pub struct IntoIter<
T,
#[unstable(feature = "allocator_api", issue = "32838")] A: Allocator = Global,
> {
pub(super) buf: NonNull<T>,
pub(super) phantom: PhantomData<T>,
pub(super) cap: usize,
// the drop impl reconstructs a RawVec from buf, cap and alloc
// to avoid dropping the allocator twice we need to wrap it into ManuallyDrop
pub(super) alloc: ManuallyDrop<A>,
pub(super) ptr: *const T,
pub(super) end: *const T, // If T is a ZST, this is actually ptr+len. This encoding is picked so that
// ptr == end is a quick test for the Iterator being empty, that works
// for both ZST and non-ZST.
}

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

@qsctr
Copy link
Contributor Author

qsctr commented Dec 9, 2023

Hmm I just noticed this line

crucible/crux-mir/lib/alloc/src/vec/into_iter.rs

Line 161 in bb50c0d

this.ptr.sub_ptr(buf)..this.end.sub_ptr(buf)

It seems like using len might not be enough, since we also need the distances to the start of the buffer

@RyanGlScott
Copy link
Contributor

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
Copy link
Contributor Author

qsctr commented Dec 12, 2023

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.

@qsctr qsctr self-assigned this Dec 12, 2023
@qsctr qsctr mentioned this issue Dec 12, 2023
Merged
@RyanGlScott
Copy link
Contributor

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@qsctr qsctr

Labels
crucible crux enhancement MIR Issues relating to Rust/MIR support
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

crux-mir: Avoid pointer arithmetic in vec::IntoIter GaloisInc/crucible
2 participants
@RyanGlScott @qsctr