Audit for ptr_offset_from
#1099
Conversation
| @@ -873,6 +874,7 @@ impl Expr { | |||
| (lhs.typ == rhs.typ && lhs.typ.is_integer()) | |||
| || (lhs.typ.is_pointer() && rhs.typ.is_integer()) | |||
| } | |||
| ROk => lhs.typ.is_pointer() && rhs.typ.is_c_size_t(), | |||
There was a problem hiding this comment.
I'm not sure ROk is properly classed as a binary operator
There was a problem hiding this comment.
In my first attempt I declared it as a unary operator but CBMC complained that two arguments were expected for __CPROVER_r/w_ok, so that is why I implemented this. I can remove if it's going to be a blocker.
There was a problem hiding this comment.
My concern had been more whether we should think of it as a binop, or as a CBMC intrinsic. But we can merge this PR and have a separate ticket to track that. #1111
| let cast_src_ptr = src_ptr.clone().cast_to(Type::ssize_t()); | ||
| let offset = cast_dst_ptr.sub_overflow(cast_src_ptr); | ||
| let overflow_check = self.codegen_assert( | ||
| offset.overflowed.not(), |
There was a problem hiding this comment.
does this cause performance problems
There was a problem hiding this comment.
I couldn't come up with a test for this overflow check and then I realized it's wrong. The overflow check has to be done for the distance in bytes, which is what we do now. An expected test for the overflow case is included.
| @@ -878,26 +878,28 @@ impl<'tcx> GotocCtx<'tcx> { | |||
| /// https://doc.rust-lang.org/std/intrinsics/fn.ptr_offset_from.html | |||
There was a problem hiding this comment.
There are a bunch of checks, and we're only checking some of them
Both the starting and other pointer must be either in bounds or one byte past the end of the same [allocated object](https://doc.rust-lang.org/std/ptr/index.html#allocated-object).
Both pointers must be derived from a pointer to the same object. (See below for an example.)
The distance between the pointers, in bytes, must be an exact multiple of the size of T.
The distance between the pointers, in bytes, cannot overflow an isize.
The distance being in bounds cannot rely on “wrapping around” the address space.
| ], | ||
| loc, | ||
| ) | ||
| // Check that the computation would not overflow an `isize` |
There was a problem hiding this comment.
Why did you remove the same_object check
There was a problem hiding this comment.
The same_object check is being done by CBMC by default. I converted the test we already had for it into an expected test so we ensure the "same object violation" stays there.
adpaco-aws
force-pushed
the
offset_from-audit
branch
from
fb81d6a to
58e78bc
Compare
|
Please check the most recent version, there are 4 tests now for this intrinsic. |
adpaco-aws
force-pushed
the
offset_from-audit
branch
from
7a6049d to
fe16fa1
Compare
Description of changes:
Adds an arithmetic overflow check for
ptr_offset_fromand removes the__CPROVER_same_objectcheck because CBMC applies it to the arithmetic operation by default.As with
offset, I had concerns because there were no checks for the pointers staying within bounds of the object. So I added__CPROVER_r_okirep expression and used it, just to find that a bunch of regressions fail.Resolved issues:
Part of #727
Call-outs:
Testing:
How is this change tested? Existing tests.
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.