Audit for ptr_offset_from (rust-lang#1099)

Author: adpaco-aws

cprover_bindings/src/goto_program/expr.rs

@@ -181,6 +181,7 @@ pub enum BinaryOperand {
     OverflowMult,
     OverflowPlus,
     Plus,
+    ROk,
     Rol,
     Ror,
     Shl,
@@ -873,6 +874,7 @@ impl Expr {
                 (lhs.typ == rhs.typ && lhs.typ.is_integer())
                     || (lhs.typ.is_pointer() && rhs.typ.is_integer())
             }
+            ROk => lhs.typ.is_pointer() && rhs.typ.is_c_size_t(),
         }
     }
 
@@ -914,6 +916,7 @@ impl Expr {
             IeeeFloatEqual | IeeeFloatNotequal => Type::bool(),
             // Overflow flags
             OverflowMinus | OverflowMult | OverflowPlus => Type::bool(),
+            ROk => Type::bool(),
         }
     }
     /// self op right;
@@ -1072,6 +1075,11 @@ impl Expr {
     pub fn ror(self, e: Expr) -> Expr {
         self.binop(Ror, e)
     }
+
+    /// `__CPROVER_r_ok(self, e)`
+    pub fn r_ok(self, e: Expr) -> Expr {
+        self.binop(ROk, e)
+    }
 }
 
 /// Constructors for self operations

cprover_bindings/src/irep/to_irep.rs

@@ -76,6 +76,7 @@ impl ToIrepId for BinaryOperand {
             BinaryOperand::OverflowMult => IrepId::OverflowMult,
             BinaryOperand::OverflowPlus => IrepId::OverflowPlus,
             BinaryOperand::Plus => IrepId::Plus,
+            BinaryOperand::ROk => IrepId::ROk,
             BinaryOperand::Rol => IrepId::Rol,
             BinaryOperand::Ror => IrepId::Ror,
             BinaryOperand::Shl => IrepId::Shl,

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

@@ -523,7 +523,7 @@ impl<'tcx> GotocCtx<'tcx> {
             "pref_align_of" => codegen_intrinsic_const!(),
             "ptr_guaranteed_eq" => codegen_ptr_guaranteed_cmp!(eq),
             "ptr_guaranteed_ne" => codegen_ptr_guaranteed_cmp!(neq),
-            "ptr_offset_from" => self.codegen_ptr_offset_from(fargs, p, loc),
+            "ptr_offset_from" => self.codegen_ptr_offset_from(instance, fargs, p, loc),
             "raw_eq" => self.codegen_intrinsic_raw_eq(instance, fargs, p, loc),
             "rintf32" => codegen_unimplemented_intrinsic!(
                 "https://github.com/model-checking/kani/issues/1025"
@@ -905,26 +905,34 @@ impl<'tcx> GotocCtx<'tcx> {
     /// https://doc.rust-lang.org/std/intrinsics/fn.ptr_offset_from.html
     fn codegen_ptr_offset_from(
         &mut self,
+        instance: Instance<'tcx>,
         mut fargs: Vec<Expr>,
         p: &Place<'tcx>,
         loc: Location,
     ) -> Stmt {
-        let a = fargs.remove(0);
-        let b = fargs.remove(0);
-        let pointers_to_same_object = a.clone().same_object(b.clone());
+        let dst_ptr = fargs.remove(0);
+        let src_ptr = fargs.remove(0);
 
-        Stmt::block(
-            vec![
-                self.codegen_assert(
-                    pointers_to_same_object,
-                    PropertyClass::PointerOffset,
-                    "ptr_offset_from: pointers point to same object",
-                    loc.clone(),
-                ),
-                self.codegen_expr_to_place(p, a.sub(b)),
-            ],
+        // Compute the offset with standard substraction using `isize`
+        let cast_dst_ptr = dst_ptr.clone().cast_to(Type::ssize_t());
+        let cast_src_ptr = src_ptr.clone().cast_to(Type::ssize_t());
+        let offset = cast_dst_ptr.sub(cast_src_ptr);
+
+        // Check that computing `offset_bytes` would not overflow an `isize`
+        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 offset_bytes = offset.clone().mul_overflow(size);
+        let overflow_check = self.codegen_assert(
+            offset_bytes.overflowed.not(),
+            PropertyClass::ArithmeticOverflow,
+            "attempt to compute offset in bytes which would overflow",
             loc,
-        )
+        );
+
+        // Re-compute the offset with standard substraction (no casts this time)
+        let offset_expr = self.codegen_expr_to_place(p, dst_ptr.sub(src_ptr));
+        Stmt::block(vec![overflow_check, offset_expr], loc)
     }
 
     /// A transmute is a bitcast from the argument type to the return type.

tests/expected/intrinsics/offset-same-object/expected

@@ -0,0 +1,2 @@
+FAILURE\
+"same object violation"

tests/kani/PointerOffset/Unstable/main_fail.rs renamed to tests/expected/intrinsics/offset-same-object/main.rs

@@ -1,7 +1,8 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-verify-fail
 
+// Checks that `ptr_offset_from` fails if the object that the arguments
+// point to are not the same.
 #![feature(core_intrinsics)]
 use std::intrinsics::ptr_offset_from;
 
@@ -12,11 +13,6 @@ fn main() {
     let ptr1: *const i32 = &a[1];
     let ptr2: *const i32 = &b[3];
     unsafe {
-        // Offset operations result in Undefined Behavior if
-        // some conditions are violated. More info at:
-        // https://doc.rust-lang.org/std/primitive.pointer.html#method.offset_from
-        // In particular, the below call to `ptr_offset_from` is expected
-        // to fail because `ptr1` and `ptr2` point to different objects.
         let offset = ptr_offset_from(ptr2, ptr1);
     }
 }

tests/expected/offset-from-bytes-overflow/expected

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

tests/expected/offset-from-bytes-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
+
+// Check that an offset computed with `offset_from` triggers a verification failure
+// if it overflows an `isize` in bytes.
+use std::convert::TryInto;
+
+#[kani::proof]
+fn main() {
+    let v: &[u128] = &[0; 200];
+    let v_100: *const u128 = &v[100];
+    let max_offset = usize::MAX / std::mem::size_of::<u128>();
+    unsafe {
+        let v_wrap: *const u128 = v_100.add((max_offset + 1).try_into().unwrap());
+        let _ = v_wrap.offset_from(v_100) == 2;
+    }
+}