Audit for offset intrinsic#1094
Conversation
dd4102c to
999e787
Compare
celinval
left a comment
There was a problem hiding this comment.
Just small comments. Don't worry about moving the tests to expected, but it is something I recommend for the future.
There was a problem hiding this comment.
nit: For cases like this, I recommend using the expected test suite. kani-verify-fail is very fragile.
Not a blocker though.
There was a problem hiding this comment.
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?
999e787 to
f9f9904
Compare
|
Thanks, I moved the negative tests to |
1 similar comment
|
Thanks, I moved the negative tests to |
| let src_ptr = fargs.remove(0); | ||
| let offset = fargs.remove(0); | ||
| // Check that the computation would not overflow an `isize` | ||
| let dst_ptr_of = src_ptr.clone().cast_to(Type::ssize_t()).add_overflow(offset.clone()); |
There was a problem hiding this comment.
This does integer arithmatic, not pointer arithmatic, and I think will give the wrong results
There was a problem hiding this comment.
I.e.: You should account for the pointee size.
There was a problem hiding this comment.
Right, should be getting the right results now.
celinval
left a comment
There was a problem hiding this comment.
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);
}|
Addressed all @celinval's comments, including the proposed test case. |
Description of changes:
Changes the
offsetintrinsic 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
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.