Audit for offset intrinsic

[adpaco-aws]

Description of changes:

Changes the offset intrinsic to use addition with overflow to detect overflow, but computes the actual destination pointer with regular addition. This fixes spurious failures that appeared when offsets were negative or being substracted.

In addition, standard pointer checks cover the case where the pointer is dereferenced outside the object bounds. I've observed that this works as expected: One byte past the object is fine, more than that is not. 5 test cases included.

Resolved issues:

Resolves #1082
Part of #727

Call-outs:

Testing:

• How is this change tested? Adds 5 test cases.

• Is this a refactor change? No.

Checklist

• Each commit message has a non-empty body, explaining why the change was made
• Methods or procedures are documented
• Regression or unit tests are included, or existing tests cover the modified code
• My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[celinval]

Just small comments. Don't worry about moving the tests to expected, but it is something I recommend for the future.

[celinval]

nit: For cases like this, I recommend using the expected test suite. kani-verify-fail is very fragile.

Not a blocker though.

[celinval]

I would prefer if we don't delete this one in favor of things that call the intrinsic directly. This is actually closer to what the user code would look like. Can you please just rename it?

[adpaco-aws]

Thanks, I moved the negative tests to expected and restored the "fixme" test (sorry about that).

[adpaco-aws]

Thanks, I moved the negative tests to expected and restored the "fixme" test (sorry about that).

[danielsn]

This does integer arithmatic, not pointer arithmatic, and I think will give the wrong results

[celinval]

I.e.: You should account for the pointee size.

[adpaco-aws]

Right, should be getting the right results now.

[celinval]

Can you add a test that exercise the new check? Something like:

/// Check that an offset that overflow an isize::MAX triggers a verification failure.
#[kani::proof]
unsafe fn check_wrap_offset() {
        let v : &[u128] = &[0; 200];
        let v_100 : *const u128 = &v[100];
        let max_offset = usize::MAX / std::mem::size_of::<u128>();
        let v_wrap : *const u128 = v_100.offset((max_offset + 1).try_into().unwrap());
        assert_eq!(v_100, v_wrap);
        assert_eq!(*v_100, *v_wrap);
}

[danielsn]

Approved modulo @celinval comments

[adpaco-aws]

Addressed all @celinval's comments, including the proposed test case.