From c64575219fc672f3884a2e965f5f1438c7d2033c Mon Sep 17 00:00:00 2001
From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
Date: Wed, 9 Oct 2024 08:55:32 -0700
Subject: [PATCH] Fix the computation of the number of bytes of a pointer
 offset (#3584)

This PR fixes the logic that computes the number of bytes of a pointer
offset. The logic was incorrectly using the size of the pointer as
opposed to the size of the pointee.

This fixes the soundness issue in #3582 (but not the spurious failures).

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
 .../codegen_cprover_gotoc/codegen/rvalue.rs   |  2 +-
 .../offset-from-bytes-overflow/expected       |  2 +-
 tests/expected/offset-overflow/expected       |  2 +-
 tests/expected/offset-overflow/main.rs        |  9 ++++---
 tests/expected/ptr-offset-overflow/expected   |  5 ++++
 tests/expected/ptr-offset-overflow/main.rs    | 27 +++++++++++++++++++
 6 files changed, 41 insertions(+), 6 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/offset-overflow/main.rs b/tests/expected/offset-overflow/main.rs
index 55b79df854cc..43f294848012 100644
--- a/tests/expected/offset-overflow/main.rs
+++ b/tests/expected/offset-overflow/main.rs
@@ -8,10 +8,13 @@ use std::intrinsics::offset;
 
 #[kani::proof]
 fn test_offset_overflow() {
-    let s: &str = "123";
-    let ptr: *const u8 = s.as_ptr();
+    let a: [i32; 3] = [1, 2, 3];
+    let ptr: *const i32 = a.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, isize::MAX / 8);
+        let _d = offset(ptr, count);
     }
 }
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::<impl *const Foo>::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::<Foo>(), 16384);
+    // a large enough count that causes `count * size_of::<Foo>()` 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::<Foo>()).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::<Foo>` overflows `isize`
+    let _p = unsafe { ptr.offset(count as isize) };
+}