Audit for arith_offset intrinsic (rust-lang#1228)

* Implement `arith_offset` with `codegen_offset`

* Extend `codegen_offset` args with `intrinsic`

* Add tests for `arith_offset`/`wrapping_offset`

* Improve documentation for `codegen_offset`

* Link issue and extend comment

Author: adpaco-aws

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

@@ -383,7 +383,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
         match intrinsic {
             "add_with_overflow" => codegen_op_with_overflow!(add_overflow),
-            "arith_offset" => unstable_codegen!(codegen_wrapping_op!(plus)),
+            "arith_offset" => self.codegen_offset(intrinsic, instance, fargs, p, loc),
             "assert_inhabited" => self.codegen_assert_intrinsic(instance, intrinsic, span),
             "assert_uninit_valid" => self.codegen_assert_intrinsic(instance, intrinsic, span),
             "assert_zero_valid" => self.codegen_assert_intrinsic(instance, intrinsic, span),
@@ -562,7 +562,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 "https://github.com/model-checking/kani/issues/1025"
             ),
             "needs_drop" => codegen_intrinsic_const!(),
-            "offset" => self.codegen_offset(instance, fargs, p, loc),
+            "offset" => self.codegen_offset(intrinsic, 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)),
@@ -992,10 +992,24 @@ impl<'tcx> GotocCtx<'tcx> {
         Stmt::block(vec![src_align_check, dst_align_check, overflow_check, copy_expr], loc)
     }
 
-    /// Computes the offset from a pointer
-    /// https://doc.rust-lang.org/std/intrinsics/fn.offset.html
+    /// Computes the offset from a pointer.
+    ///
+    /// Note that this function handles code generation for:
+    ///  1. The `offset` intrinsic.
+    ///     https://doc.rust-lang.org/std/intrinsics/fn.offset.html
+    ///  2. The `arith_offset` intrinsic.
+    ///     https://doc.rust-lang.org/std/intrinsics/fn.arith_offset.html
+    ///
+    /// 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 https://github.com/model-checking/kani/issues/1233 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`:
+    /// https://doc.rust-lang.org/std/primitive.pointer.html#safety-2
     fn codegen_offset(
         &mut self,
+        intrinsic: &str,
         instance: Instance<'tcx>,
         mut fargs: Vec<Expr>,
         p: &Place<'tcx>,
@@ -1007,7 +1021,7 @@ impl<'tcx> GotocCtx<'tcx> {
         // Check that computing `offset` in bytes would not overflow
         let ty = self.monomorphize(instance.substs.type_at(0));
         let (offset_bytes, bytes_overflow_check) =
-            self.count_in_bytes(offset.clone(), ty, Type::ssize_t(), "offset", loc);
+            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:

tests/expected/arith-offset-i32-fail/expected

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

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

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

tests/expected/arith-offset-overflow/expected

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

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

@@ -0,0 +1,17 @@
+// 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
+#![feature(core_intrinsics)]
+use std::intrinsics::arith_offset;
+
+#[kani::proof]
+fn test_arith_offset_overflow() {
+    let s: &str = "123";
+    let ptr: *const u8 = s.as_ptr();
+
+    unsafe {
+        let _ = arith_offset(ptr, isize::MAX);
+    }
+}

tests/expected/arith-offset-u8-fail/expected

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

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

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

tests/expected/wrapping-offset-bytes-overflow/expected

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

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

@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// 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.
+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.wrapping_offset((max_offset + 1).try_into().unwrap());
+    assert_eq!(v_100, v_wrap);
+    assert_eq!(*v_100, *v_wrap);
+}

tests/kani/Intrinsics/ArithOffset/offset_i32_ok.rs

@@ -0,0 +1,31 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `arith_offset` returns the expected addresses
+#![feature(core_intrinsics)]
+use std::intrinsics::arith_offset;
+
+#[kani::proof]
+fn test_arith_offset() {
+    let arr: [i32; 3] = [1, 2, 3];
+    let ptr: *const i32 = arr.as_ptr();
+
+    unsafe {
+        assert_eq!(*arith_offset(ptr, 0), 1);
+        assert_eq!(*arith_offset(ptr, 1), 2);
+        assert_eq!(*arith_offset(ptr, 2), 3);
+        assert_eq!(*arith_offset(ptr, 2).sub(1), 2);
+
+        // This wouldn't be okay because it's
+        // more than one byte past the object
+        // let x = *arith_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!(*arith_offset(other_ptr, 0), 2);
+        assert_eq!(*arith_offset(other_ptr, 1), 3);
+        assert_eq!(*arith_offset(other_ptr, 1).sub(1), 2);
+    }
+}

tests/kani/Intrinsics/ArithOffset/offset_u8_ok.rs

@@ -0,0 +1,31 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `arith_offset` returns the expected addresses
+#![feature(core_intrinsics)]
+use std::intrinsics::arith_offset;
+
+#[kani::proof]
+fn test_arith_offset() {
+    let s: &str = "123";
+    let ptr: *const u8 = s.as_ptr();
+
+    unsafe {
+        assert_eq!(*arith_offset(ptr, 0) as char, '1');
+        assert_eq!(*arith_offset(ptr, 1) as char, '2');
+        assert_eq!(*arith_offset(ptr, 2) as char, '3');
+        assert_eq!(*arith_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 = *arith_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!(*arith_offset(other_ptr, 0) as char, '2');
+        assert_eq!(*arith_offset(other_ptr, 1) as char, '3');
+        assert_eq!(*arith_offset(other_ptr, 1).sub(1) as char, '2');
+    }
+}