Audit for offset intrinsic (rust-lang#1094)

Author: adpaco-aws

docs/src/rust-feature-support.md

@@ -371,7 +371,7 @@ nearbyintf32 | No | |
 nearbyintf64 | No | |
 needs_drop | Yes | |
 nontemporal_store | No | |
-offset | Partial | Missing undefined behavior checks |
+offset | Yes | |
 powf32 | No | |
 powf64 | No | |
 powif32 | No | |

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

@@ -513,7 +513,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 "https://github.com/model-checking/kani/issues/1025"
             ),
             "needs_drop" => codegen_intrinsic_const!(),
-            "offset" => codegen_op_with_overflow_check!(add_overflow),
+            "offset" => self.codegen_offset(instance, fargs, p, loc),
             "powf32" => unstable_codegen!(codegen_simple_intrinsic!(Powf)),
             "powf64" => unstable_codegen!(codegen_simple_intrinsic!(Pow)),
             "powif32" => unstable_codegen!(codegen_simple_intrinsic!(Powif)),
@@ -868,6 +868,44 @@ impl<'tcx> GotocCtx<'tcx> {
         Stmt::atomic_block(vec![skip_stmt], loc)
     }
 
+    /// Computes the offset from a pointer
+    /// https://doc.rust-lang.org/std/intrinsics/fn.offset.html
+    fn codegen_offset(
+        &mut self,
+        instance: Instance<'tcx>,
+        mut fargs: Vec<Expr>,
+        p: &Place<'tcx>,
+        loc: Location,
+    ) -> Stmt {
+        let src_ptr = fargs.remove(0);
+        let offset = fargs.remove(0);
+
+        // Check that computing `bytes` would not overflow
+        let ty = self.monomorphize(instance.substs.type_at(0));
+        let layout = self.layout_of(ty);
+        let size = Expr::int_constant(layout.size.bytes(), Type::ssize_t());
+        let bytes = offset.clone().mul_overflow(size);
+        let bytes_overflow_check = self.codegen_assert(
+            bytes.overflowed.not(),
+            PropertyClass::ArithmeticOverflow,
+            "attempt to compute offset in bytes which would overflow",
+            loc,
+        );
+
+        // Check that the computation would not overflow an `isize`
+        let dst_ptr_of = src_ptr.clone().cast_to(Type::ssize_t()).add_overflow(bytes.result);
+        let overflow_check = self.codegen_assert(
+            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
+        let dst_ptr = src_ptr.plus(offset);
+        let expr_place = self.codegen_expr_to_place(p, dst_ptr);
+        Stmt::block(vec![bytes_overflow_check, overflow_check, expr_place], loc)
+    }
+
     /// ptr_offset_from returns the offset between two pointers
     /// https://doc.rust-lang.org/std/intrinsics/fn.ptr_offset_from.html
     fn codegen_ptr_offset_from(

tests/expected/offset-bytes-overflow/expected

@@ -0,0 +1,2 @@
+FAILURE\
+attempt to compute offset in bytes which would overflow

tests/expected/offset-bytes-overflow/main.rs

@@ -0,0 +1,15 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that an offset that overflows an `isize::MAX` triggers a verification failure.
+use std::convert::TryInto;
+
+#[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);
+}

tests/expected/offset-i32-fail/expected

@@ -0,0 +1,2 @@
+FAILURE\
+dereference failure: pointer outside object bounds

tests/expected/offset-i32-fail/main.rs

@@ -0,0 +1,17 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that the pointer computed with `offset` causes a failure if it's
+// dereferenced outside the object bounds
+#![feature(core_intrinsics)]
+use std::intrinsics::offset;
+
+#[kani::proof]
+fn test_offset() {
+    let arr: [i32; 3] = [1, 2, 3];
+    let ptr: *const i32 = arr.as_ptr();
+
+    unsafe {
+        let x = *offset(ptr, 3);
+    }
+}

tests/expected/offset-overflow/expected

@@ -0,0 +1,2 @@
+FAILURE\
+attempt to compute offset which would overflow

tests/expected/offset-overflow/main.rs

@@ -0,0 +1,17 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `offset` fails if the offset computation would
+// result in an arithmetic overflow
+#![feature(core_intrinsics)]
+use std::intrinsics::offset;
+
+#[kani::proof]
+fn test_offset_overflow() {
+    let s: &str = "123";
+    let ptr: *const u8 = s.as_ptr();
+
+    unsafe {
+        let _ = offset(ptr, isize::MAX);
+    }
+}

tests/expected/offset-u8-fail/expected

@@ -0,0 +1,2 @@
+FAILURE\
+dereference failure: pointer outside object bounds

tests/expected/offset-u8-fail/main.rs

@@ -0,0 +1,17 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that the pointer computed with `offset` causes a failure if it's
+// dereferenced outside the object bounds
+#![feature(core_intrinsics)]
+use std::intrinsics::offset;
+
+#[kani::proof]
+fn test_offset() {
+    let s: &str = "123";
+    let ptr: *const u8 = s.as_ptr();
+
+    unsafe {
+        let x = *offset(ptr, 4) as char;
+    }
+}

tests/kani/Intrinsics/Offset/offset_i32_ok.rs

@@ -0,0 +1,31 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `offset` returns the expected addresses
+#![feature(core_intrinsics)]
+use std::intrinsics::offset;
+
+#[kani::proof]
+fn test_offset() {
+    let arr: [i32; 3] = [1, 2, 3];
+    let ptr: *const i32 = arr.as_ptr();
+
+    unsafe {
+        assert_eq!(*offset(ptr, 0), 1);
+        assert_eq!(*offset(ptr, 1), 2);
+        assert_eq!(*offset(ptr, 2), 3);
+        assert_eq!(*offset(ptr, 2).sub(1), 2);
+
+        // This wouldn't be okay because it's
+        // more than one byte past the object
+        // let x = *offset(ptr, 3);
+
+        // Check that the results are the same with a pointer
+        // that goes 1 element behind the original one
+        let other_ptr: *const i32 = ptr.add(1);
+
+        assert_eq!(*offset(other_ptr, 0), 2);
+        assert_eq!(*offset(other_ptr, 1), 3);
+        assert_eq!(*offset(other_ptr, 1).sub(1), 2);
+    }
+}

tests/kani/Intrinsics/Offset/offset_u8_ok.rs

@@ -0,0 +1,31 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `offset` returns the expected addresses
+#![feature(core_intrinsics)]
+use std::intrinsics::offset;
+
+#[kani::proof]
+fn test_offset() {
+    let s: &str = "123";
+    let ptr: *const u8 = s.as_ptr();
+
+    unsafe {
+        assert_eq!(*offset(ptr, 0) as char, '1');
+        assert_eq!(*offset(ptr, 1) as char, '2');
+        assert_eq!(*offset(ptr, 2) as char, '3');
+        assert_eq!(*offset(ptr, 2).sub(1) as char, '2');
+
+        // This is okay because it's one byte past the object,
+        // but there is nothing we can assert about it
+        let x = *offset(ptr, 3);
+
+        // Check that the results are the same with a pointer
+        // that goes 1 element behind the original one
+        let other_ptr: *const u8 = ptr.add(1);
+
+        assert_eq!(*offset(other_ptr, 0) as char, '2');
+        assert_eq!(*offset(other_ptr, 1) as char, '3');
+        assert_eq!(*offset(other_ptr, 1).sub(1) as char, '2');
+    }
+}