From fd39cfcde191c438193e254164dbe9459b389469 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 8 Oct 2024 19:29:04 -0700 Subject: [PATCH] Fix the computation of the number of bytes of a pointer offset --- .../codegen_cprover_gotoc/codegen/rvalue.rs | 2 +- .../offset-from-bytes-overflow/expected | 2 +- tests/expected/offset-overflow/expected | 2 +- tests/expected/ptr-offset-overflow/expected | 5 ++++ tests/expected/ptr-offset-overflow/main.rs | 27 +++++++++++++++++++ 5 files changed, 35 insertions(+), 3 deletions(-) create mode 100644 tests/expected/ptr-offset-overflow/expected create mode 100644 tests/expected/ptr-offset-overflow/main.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 7a4594a181e3..14e012aac76b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -410,7 +410,7 @@ impl<'tcx> GotocCtx<'tcx> { // Check that computing `offset` in bytes would not overflow let (offset_bytes, bytes_overflow_check) = self.count_in_bytes( ce2.clone().cast_to(Type::ssize_t()), - ty, + pointee_type_stable(ty).unwrap(), Type::ssize_t(), "offset", loc, diff --git a/tests/expected/offset-from-bytes-overflow/expected b/tests/expected/offset-from-bytes-overflow/expected index 9613638bf8f9..bcf0242f9e9d 100644 --- a/tests/expected/offset-from-bytes-overflow/expected +++ b/tests/expected/offset-from-bytes-overflow/expected @@ -1,2 +1,2 @@ FAILURE\ -attempt to compute offset which would overflow +attempt to compute number in bytes which would overflow diff --git a/tests/expected/offset-overflow/expected b/tests/expected/offset-overflow/expected index 72ded2ac24c1..bcf0242f9e9d 100644 --- a/tests/expected/offset-overflow/expected +++ b/tests/expected/offset-overflow/expected @@ -1,2 +1,2 @@ FAILURE\ -attempt to compute offset which would overflow \ No newline at end of file +attempt to compute number in bytes which would overflow diff --git a/tests/expected/ptr-offset-overflow/expected b/tests/expected/ptr-offset-overflow/expected new file mode 100644 index 000000000000..ad33ce91dabb --- /dev/null +++ b/tests/expected/ptr-offset-overflow/expected @@ -0,0 +1,5 @@ +std::ptr::const_ptr::::offset.arithmetic_overflow\ +Status: FAILURE\ +Description: "offset: attempt to compute number in bytes which would overflow" + +VERIFICATION:- FAILED diff --git a/tests/expected/ptr-offset-overflow/main.rs b/tests/expected/ptr-offset-overflow/main.rs new file mode 100644 index 000000000000..d2877addb923 --- /dev/null +++ b/tests/expected/ptr-offset-overflow/main.rs @@ -0,0 +1,27 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test checks that Kani detects the overflow in pointer offset + +use std::convert::TryFrom; + +struct Foo { + arr: [i32; 4096], +} + +#[cfg_attr(kani, kani::proof)] +fn main() { + let f = Foo { arr: [0; 4096] }; + assert_eq!(std::mem::size_of::(), 16384); + // a large enough count that causes `count * size_of::()` to overflow + // `isize` without overflowing `usize` + let count: usize = 562949953421320; + // the `unwrap` ensures that it indeed doesn't overflow `usize` + let bytes = count.checked_mul(std::mem::size_of::()).unwrap(); + // ensure that it overflows `isize`: + assert!(isize::try_from(bytes).is_err()); + + let ptr: *const Foo = &f as *const Foo; + // this should fail because `count * size_of::` overflows `isize` + let _p = unsafe { ptr.offset(count as isize) }; +}