Address comments and use integer addition in offset

I decided to add a new test, and I bumped into issue model-checking#1150.
Thus, I updated our model to use integer arithmetic operations instead
of CBMC pointer arithmetic.

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

@@ -38,7 +38,7 @@ pub enum PropertyClass {
     /// Overflow panics that can be generated by Intrisics.
     /// NOTE: Not all uses of this are found by rust-analyzer because of the use of macros. Try grep instead.
     ///
-    /// SPECIAL BEHAVIOR: Same as SafetyCheck.
+    /// SPECIAL BEHAVIOR: Same as SafetyCheck. TODO: Replace this with `SafetyCheck`.
     ArithmeticOverflow,
     /// The Rust `assume` instrinsic is `assert`'d by Kani, and gets this property class.
     ///
@@ -69,11 +69,11 @@ pub enum PropertyClass {
     Assertion,
     /// Another intrinsic check.
     ///
-    /// SPECIAL BEHAVIOR: Same as SafetyCheck
+    /// SPECIAL BEHAVIOR: Same as SafetyCheck. TODO: Replace this with `SafetyCheck`.
     ExactDiv,
     /// Another intrinsic check.
     ///
-    /// SPECIAL BEHAVIOR: Same as SafetyCheck
+    /// SPECIAL BEHAVIOR: Same as SafetyCheck. TODO: Replace this with `SafetyCheck`.
     FiniteCheck,
     /// Checks added by Kani compiler to determine whether a property (e.g.
     /// `PropertyClass::Assertion` or `PropertyClass:Cover`) is reachable

kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs

@@ -155,12 +155,29 @@ impl GotocHook for UnsupportedCheck {
         &self,
         gcx: &mut GotocCtx,
         _instance: Instance,
-        fargs: Vec<Expr>,
+        mut fargs: Vec<Expr>,
         _assign_to: &Place,
         target: Option<BasicBlockIdx>,
         span: Span,
     ) -> Stmt {
-        check_hook(PropertyClass::UnsupportedConstruct, gcx, fargs, target, span)
+        assert_eq!(fargs.len(), 2);
+        let msg = fargs.pop().unwrap();
+        let cond = fargs.pop().unwrap().cast_to(Type::bool());
+        let msg = gcx.extract_const_message(&msg).unwrap();
+        let target = target.unwrap();
+        let caller_loc = gcx.codegen_caller_span_stable(span);
+        Stmt::block(
+            vec![
+                gcx.codegen_assert_assume(
+                    cond,
+                    PropertyClass::UnsupportedConstruct,
+                    &msg,
+                    caller_loc,
+                ),
+                Stmt::goto(bb_label(target), caller_loc),
+            ],
+            caller_loc,
+        )
     }
 }
 
@@ -174,15 +191,28 @@ impl GotocHook for SafetyCheck {
         &self,
         gcx: &mut GotocCtx,
         _instance: Instance,
-        fargs: Vec<Expr>,
+        mut fargs: Vec<Expr>,
         _assign_to: &Place,
         target: Option<BasicBlockIdx>,
         span: Span,
     ) -> Stmt {
-        check_hook(PropertyClass::SafetyCheck, gcx, fargs, target, span)
+        assert_eq!(fargs.len(), 2);
+        let msg = fargs.pop().unwrap();
+        let cond = fargs.pop().unwrap().cast_to(Type::bool());
+        let msg = gcx.extract_const_message(&msg).unwrap();
+        let target = target.unwrap();
+        let caller_loc = gcx.codegen_caller_span_stable(span);
+        Stmt::block(
+            vec![
+                gcx.codegen_assert_assume(cond, PropertyClass::SafetyCheck, &msg, caller_loc),
+                Stmt::goto(bb_label(target), caller_loc),
+            ],
+            caller_loc,
+        )
     }
 }
 
+// TODO: Remove this and replace occurrences with `SanityCheck`.
 struct Check;
 impl GotocHook for Check {
     fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
@@ -207,15 +237,10 @@ impl GotocHook for Check {
 
         let (msg, reach_stmt) = gcx.codegen_reachability_check(msg, span);
 
-        // Since `cond` might have side effects, assign it to a temporary
-        // variable so that it's evaluated once, then assert and assume it
-        // TODO: I don't think `cond` can have side effects, this is MIR, it's going to be temps
-        let (tmp, decl) = gcx.decl_temp_variable(cond.typ().clone(), Some(cond), caller_loc);
         Stmt::block(
             vec![
                 reach_stmt,
-                decl,
-                gcx.codegen_assert(tmp, PropertyClass::Assertion, &msg, caller_loc),
+                gcx.codegen_assert(cond, PropertyClass::Assertion, &msg, caller_loc),
                 Stmt::goto(bb_label(target), caller_loc),
             ],
             caller_loc,
@@ -755,25 +780,3 @@ impl GotocHooks {
         }
     }
 }
-
-fn check_hook(
-    prop_class: PropertyClass,
-    gcx: &mut GotocCtx,
-    mut fargs: Vec<Expr>,
-    target: Option<BasicBlockIdx>,
-    span: Span,
-) -> Stmt {
-    assert_eq!(fargs.len(), 2);
-    let msg = fargs.pop().unwrap();
-    let cond = fargs.pop().unwrap().cast_to(Type::bool());
-    let msg = gcx.extract_const_message(&msg).unwrap();
-    let target = target.unwrap();
-    let caller_loc = gcx.codegen_caller_span_stable(span);
-    Stmt::block(
-        vec![
-            gcx.codegen_assert_assume(cond, prop_class, &msg, caller_loc),
-            Stmt::goto(bb_label(target), caller_loc),
-        ],
-        caller_loc,
-    )
-}

library/kani_core/src/models.rs

@@ -57,7 +57,11 @@ macro_rules! generate_models {
                     let (byte_offset, overflow) = offset.overflowing_mul(t_size);
                     kani::safety_check(!overflow, "Offset in bytes overflows isize");
                     let orig_ptr = ptr.to_const_ptr();
-                    let new_ptr = orig_ptr.wrapping_byte_offset(byte_offset);
+                    // NOTE: For CBMC, using the pointer addition can have unexpected behavior
+                    // when the offset is higher than the object bits since it will wrap around.
+                    // TODO: Use `wrapping_byte_offset` once we fix:
+                    //       https://github.com/model-checking/kani/issues/1150
+                    let new_ptr = orig_ptr.addr().wrapping_add_signed(byte_offset) as *const T;
                     kani::safety_check(
                         kani::mem::same_allocation_internal(orig_ptr, new_ptr),
                         "Offset result and original pointer must point to the same allocation",
@@ -104,7 +108,7 @@ macro_rules! generate_models {
                     if let Ok(val) = self.try_into() {
                         val
                     } else {
-                        kani::safety_check(false, "Offset in bytes overflow isize");
+                        kani::safety_check(false, "Offset value overflows isize");
                         unreachable!();
                     }
                 }

tests/expected/offset-bounds-check/offset_usize.expected

@@ -0,0 +1,10 @@
+SUMMARY:\
+ ** 5 of
+Failed Checks: Offset in bytes overflows isize
+Failed Checks: Offset result and original pointer must point to the same allocation
+Failed Checks: Offset value overflows isize
+Failed Checks: "This should fail for delta `1`"
+Failed Checks: "This should fail for delta `0`"
+
+Verification failed for - check_intrinsic_args
+Complete - 0 successfully verified harnesses, 1 failures, 1 total.

tests/expected/offset-bounds-check/offset_usize.rs

@@ -0,0 +1,18 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Check different violations that can be triggered when providing an usize offset
+//! with a type that has size > 1.
+
+#![feature(core_intrinsics)]
+use std::intrinsics::offset;
+use std::ptr::addr_of;
+
+#[kani::proof]
+fn check_intrinsic_args() {
+    let array = [0u32];
+    let delta: usize = kani::any();
+    let new = unsafe { offset(addr_of!(array), delta) };
+    assert!(delta <= 1, "Expected 0 and 1 to be the only safe values for offset");
+    assert_eq!(new, &array, "This should fail for delta `1`");
+    assert_ne!(new, &array, "This should fail for delta `0`");
+}

tests/expected/offset-invalid-args/invalid_offset_ty.expected

@@ -0,0 +1 @@
+Cannot offset by non-isize type u32

tests/expected/offset-invalid-args/invalid_offset_ty.rs

@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Check Kani output if the arguments provided to the offset intrinsic are incorrect.
+
+#![feature(core_intrinsics)]
+use std::intrinsics::offset;
+use std::ptr::addr_of;
+
+/// The rust compiler currently ICE.
+#[kani::proof]
+fn check_intrinsic_args() {
+    let array = [0];
+    let delta: u32 = kani::any();
+    let new = unsafe { offset(addr_of!(array), delta) };
+    assert_ne!(new, &array)
+}

tests/expected/offset-invalid-args/invalid_args.rs → tests/expected/offset-invalid-args/non_ptr_arg.rs

@@ -9,7 +9,7 @@ use std::intrinsics::offset;
 #[kani::proof]
 fn check_intrinsic_args() {
     let array = [0];
-    let delta: u32 = kani::any();
+    let delta: usize = kani::any();
     let new = unsafe { offset(&array, delta) };
     assert_ne!(new, &array)
 }