diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 79afe39fd89e..75fbfe4fc307 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -296,9 +296,7 @@ impl<'tcx> GotocCtx<'tcx> { Intrinsic::AddWithOverflow => { self.codegen_op_with_overflow(BinaryOperator::OverflowResultPlus, fargs, place, loc) } - Intrinsic::ArithOffset => { - self.codegen_offset(intrinsic_str, instance, fargs, place, loc) - } + Intrinsic::ArithOffset => self.codegen_arith_offset(fargs, place, loc), Intrinsic::AssertInhabited => { self.codegen_assert_intrinsic(instance, intrinsic_str, span) } @@ -1017,51 +1015,16 @@ impl<'tcx> GotocCtx<'tcx> { /// Computes the offset from a pointer. /// - /// Note that this function handles code generation for: - /// 1. The `offset` intrinsic. - /// - /// 2. The `arith_offset` intrinsic. + /// This function handles code generation for the `arith_offset` intrinsic. /// - /// - /// Note(std): We don't check that the starting or resulting pointer stay - /// within bounds of the object they point to. Doing so causes spurious - /// failures due to the usage of these intrinsics in the standard library. - /// See for more details. - /// Also, note that this isn't a requirement for `arith_offset`, but it's - /// one of the safety conditions specified for `offset`: - /// - fn codegen_offset( - &mut self, - intrinsic: &str, - instance: Instance, - mut fargs: Vec, - p: &Place, - loc: Location, - ) -> Stmt { + /// According to the documenation, the operation is always safe. + fn codegen_arith_offset(&mut self, mut fargs: Vec, p: &Place, loc: Location) -> Stmt { let src_ptr = fargs.remove(0); let offset = fargs.remove(0); - // Check that computing `offset` in bytes would not overflow - let args = instance_args(&instance); - let ty = args.0[0].expect_ty(); - let (offset_bytes, bytes_overflow_check) = - self.count_in_bytes(offset.clone(), *ty, Type::ssize_t(), intrinsic, loc); - - // Check that the computation would not overflow an `isize` - // These checks may allow a wrapping-around behavior in CBMC: - // https://github.com/model-checking/kani/issues/1150 - let dst_ptr_of = src_ptr.clone().cast_to(Type::ssize_t()).add_overflow(offset_bytes); - let overflow_check = self.codegen_assert_assume( - dst_ptr_of.overflowed.not(), - PropertyClass::ArithmeticOverflow, - "attempt to compute offset which would overflow", - loc, - ); - - // Re-compute `dst_ptr` with standard addition to avoid conversion + // Compute `dst_ptr` with standard addition to avoid conversion let dst_ptr = src_ptr.plus(offset); - let expr_place = self.codegen_expr_to_place_stable(p, dst_ptr, loc); - Stmt::block(vec![bytes_overflow_check, overflow_check, expr_place], loc) + self.codegen_expr_to_place_stable(p, dst_ptr, loc) } /// ptr_offset_from returns the offset between two pointers diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 14e012aac76b..e5396468a1f3 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -420,6 +420,13 @@ impl<'tcx> GotocCtx<'tcx> { // https://doc.rust-lang.org/std/primitive.pointer.html#method.offset // These checks may allow a wrapping-around behavior in CBMC: // https://github.com/model-checking/kani/issues/1150 + // Note(std): We don't check that the starting or resulting pointer stay + // within bounds of the object they point to. Doing so causes spurious + // failures due to the usage of these intrinsics in the standard library. + // See for more details. + // Note that this is one of the safety conditions for `offset`: + // + let overflow_res = ce1.clone().cast_to(Type::ssize_t()).add_overflow(offset_bytes); let overflow_check = self.codegen_assert_assume( overflow_res.overflowed.not(), diff --git a/tests/expected/arith-offset-overflow/expected b/tests/expected/arith-offset-overflow/expected index 72ded2ac24c1..34c886c358cb 100644 --- a/tests/expected/arith-offset-overflow/expected +++ b/tests/expected/arith-offset-overflow/expected @@ -1,2 +1 @@ -FAILURE\ -attempt to compute offset which would overflow \ No newline at end of file +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/arith-offset-overflow/main.rs b/tests/expected/arith-offset-overflow/main.rs index 0a5f3bce348b..b91a17edb69c 100644 --- a/tests/expected/arith-offset-overflow/main.rs +++ b/tests/expected/arith-offset-overflow/main.rs @@ -1,8 +1,9 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Checks that `arith_offset` fails if the offset computation would -// result in an arithmetic overflow +// Checks that `arith_offset` succeeds even if the offset computation would +// result in an arithmetic overflow as it uses wrapping: +// https://doc.rust-lang.org/std/intrinsics/fn.arith_offset.html #![feature(core_intrinsics)] use std::intrinsics::arith_offset; diff --git a/tests/expected/offset-overflow/expected b/tests/expected/offset-overflow/expected index bcf0242f9e9d..9613638bf8f9 100644 --- a/tests/expected/offset-overflow/expected +++ b/tests/expected/offset-overflow/expected @@ -1,2 +1,2 @@ FAILURE\ -attempt to compute number in bytes which would overflow +attempt to compute offset which would overflow diff --git a/tests/expected/offset-overflow/main.rs b/tests/expected/offset-overflow/main.rs index 43f294848012..fc9f36b9cc5d 100644 --- a/tests/expected/offset-overflow/main.rs +++ b/tests/expected/offset-overflow/main.rs @@ -8,13 +8,12 @@ use std::intrinsics::offset; #[kani::proof] fn test_offset_overflow() { - let a: [i32; 3] = [1, 2, 3]; - let ptr: *const i32 = a.as_ptr(); + let s: &str = "123"; + let ptr: *const u8 = s.as_ptr(); - // a value that when multiplied by the size of i32 (i.e. 4 bytes) - // would overflow `isize` - let count: isize = isize::MAX / 4 + 1; unsafe { - let _d = offset(ptr, count); + // This should fail because adding `isize::MAX` to `ptr` would overflow + // `isize` + let _d = offset(ptr, isize::MAX); } } diff --git a/tests/expected/ptr-offset-overflow/expected b/tests/expected/ptr-offset-overflow-bytes/expected similarity index 100% rename from tests/expected/ptr-offset-overflow/expected rename to tests/expected/ptr-offset-overflow-bytes/expected diff --git a/tests/expected/ptr-offset-overflow/main.rs b/tests/expected/ptr-offset-overflow-bytes/main.rs similarity index 100% rename from tests/expected/ptr-offset-overflow/main.rs rename to tests/expected/ptr-offset-overflow-bytes/main.rs diff --git a/tests/expected/wrapping-offset-bytes-overflow/expected b/tests/expected/wrapping-offset-bytes-overflow/expected index 449c4dae7bf9..34c886c358cb 100644 --- a/tests/expected/wrapping-offset-bytes-overflow/expected +++ b/tests/expected/wrapping-offset-bytes-overflow/expected @@ -1,2 +1 @@ -FAILURE\ -arith_offset: attempt to compute number in bytes which would overflow \ No newline at end of file +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/wrapping-offset-bytes-overflow/main.rs b/tests/expected/wrapping-offset-bytes-overflow/main.rs index edbe310d21cc..81a3fadecaf8 100644 --- a/tests/expected/wrapping-offset-bytes-overflow/main.rs +++ b/tests/expected/wrapping-offset-bytes-overflow/main.rs @@ -2,7 +2,9 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // Check that an offset (computed with `wrapping_offset`) that overflows an -// `isize::MAX` triggers a verification failure. +// `isize::MAX` does NOT trigger a verification failure as the operation is +// always safe: +// https://doc.rust-lang.org/std/primitive.pointer.html#method.wrapping_offset use std::convert::TryInto; #[kani::proof]