Pointer outside object bounds in iterator examples

[adpaco-aws]

The following code from the "Rust by Example" book:

// compile-flags: --edition 2018
// rmc-flags: --cbmc-args --unwind 4
#![allow(unused)]
pub fn main() {
    let vec1 = vec![1, 2, 3];
    let vec2 = vec![4, 5, 6];

    // `iter()` for vecs yields `&i32`. Destructure to `i32`.
    println!("2 in vec1: {}", vec1.iter()     .any(|&x| x == 2));
    // `into_iter()` for vecs yields `i32`. No destructuring required.
    println!("2 in vec2: {}", vec2.into_iter().any(| x| x == 2));

    let array1 = [1, 2, 3];
    let array2 = [4, 5, 6];

    // `iter()` for arrays yields `&i32`.
    println!("2 in array1: {}", array1.iter()     .any(|&x| x == 2));
    // `into_iter()` for arrays unusually yields `&i32`.
    println!("2 in array2: {}", array2.into_iter().any(|&x| x == 2));
}

fails to verify with

[std::ptr::const_ptr::<impl *const T>::offset_from.pointer_primitives.4] line 391 pointer outside object bounds in POINTER_OBJECT(var_11): FAILURE
[std::ptr::const_ptr::<impl *const T>::offset_from.pointer_primitives.8] line 391 pointer outside object bounds in POINTER_OBJECT(var_12): FAILURE
VERIFICATION FAILED

Not sure if #356 has anything to do, the error is quite different.

[zhassan-aws]

This is a smaller example that triggers the same spurious failure:

fn main() {
    let v: Vec<u8> = vec![5, 5, 5];
    for x in v {
        assert!(x == 5);
    }
    
}

This appears to be caused by CBMC's --pointer-primitive-check. Running the following commands:

rmc-rustc -Z symbol-mangling-version=v0 -Z symbol_table_passes= -Z human_readable_cgu_names --cfg=rmc -o test3.o test3.rs
symtab2gb test3.symtab.json --out test3.symtab.json.out
goto-cc --function main test3.symtab.json.out /home/ubuntu/git/rmc/library/rmc/rmc_lib.c -o test3.goto
goto-instrument --add-library test3.goto test3.goto
goto-instrument --generate-function-body-options assert-false --generate-function-body ".*" --drop-unused-functions test3.goto test3.goto
cbmc --bounds-check --pointer-check --pointer-primitive-check --conversion-check --div-by-zero-check --float-overflow-check --nan-check --pointer-overflow-check --undefined-shift-check --unwinding-assertions --object-bits 16 --unwind 5 --function main test3.goto

but without --pointer-primitive-check in the CBMC command doesn't produce any failures. The line that the failure points to is this one (in rmc/library/core/src/ptr/const_ptr.rs):

#[stable(feature = "ptr_offset_from", since = "1.47.0")]
    #[rustc_const_unstable(feature = "const_ptr_offset_from", issue = "41079")]
    #[inline]
    pub const unsafe fn offset_from(self, origin: *const T) -> isize
    where
        T: Sized,
    {
        let pointee_size = mem::size_of::<T>();
        assert!(0 < pointee_size && pointee_size <= isize::MAX as usize);
        // SAFETY: the caller must uphold the safety contract for `ptr_offset_from`.
        unsafe { intrinsics::ptr_offset_from(self, origin) } // <-------------------------- 
    }

[celinval]

This is a duplicate of #556. Both are issues with pointer primitive checks happening inside const_ptr::offset_from.