Codegen unimplemented for fat pointer operations for now (#1084)

This mitigates #327 and #675

Author: celinval

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

@@ -42,6 +42,23 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
+    /// This function codegen comparison for fat pointers.
+    /// We currently don't support this. See issue #327 for more information.
+    fn codegen_comparison_fat_ptr(
+        &mut self,
+        op: &BinOp,
+        left: &Operand<'tcx>,
+        right: &Operand<'tcx>,
+    ) -> Expr {
+        debug!(?op, ?left, ?right, "codegen_comparison_fat_ptr");
+        self.codegen_unimplemented(
+            &format!("Fat pointer comparison '{:?}'", op),
+            Type::Bool,
+            Location::None,
+            "https://github.com/model-checking/kani/issues/327",
+        )
+    }
+
     fn codegen_unchecked_scalar_binop(
         &mut self,
         op: &BinOp,
@@ -311,7 +328,11 @@ impl<'tcx> GotocCtx<'tcx> {
                 self.codegen_unchecked_scalar_binop(op, e1, e2)
             }
             BinOp::Eq | BinOp::Lt | BinOp::Le | BinOp::Ne | BinOp::Ge | BinOp::Gt => {
-                self.codegen_comparison(op, e1, e2)
+                if self.is_ref_of_unsized(self.operand_ty(e1)) {
+                    self.codegen_comparison_fat_ptr(op, e1, e2)
+                } else {
+                    self.codegen_comparison(op, e1, e2)
+                }
             }
             // https://doc.rust-lang.org/std/primitive.pointer.html#method.offset
             BinOp::Offset => {

tests/cargo-kani/percent-encoding/Cargo.toml

@@ -0,0 +1,13 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "check_percent_encode"
+version = "0.1.0"
+edition = "2021"
+
+
+[dependencies]
+percent-encoding = "2.1.0"
+
+[package.metadata.kani.flags]
+only-codegen = true

tests/cargo-kani/percent-encoding/src/lib.rs

@@ -0,0 +1,10 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+use percent_encoding::{utf8_percent_encode, NON_ALPHANUMERIC};
+
+#[kani::proof]
+pub fn check_encoding() {
+    let hello = utf8_percent_encode("hello world", NON_ALPHANUMERIC);
+    assert_eq!(hello.to_string(), "hello%20world");
+}

tests/expected/unsupported-fatptr-comparison/expected

@@ -0,0 +1,25 @@
+Checking harness check_slice_ptr...
+Status: FAILURE\
+Description: "Fat pointer comparison 'Lt' is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/327"
+
+Status: UNDETERMINED\
+Description: "Fat pointer comparison 'Le' is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/327"
+
+Status: UNDETERMINED\
+Description: "Fat pointer comparison 'Gt' is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/327"
+
+Status: UNDETERMINED\
+Description: "Fat pointer comparison 'Ge' is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/327"
+
+Status: UNDETERMINED\
+Description: "Fat pointer comparison 'Ne' is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/327"
+
+Status: UNDETERMINED\
+Description: "Fat pointer comparison 'Eq' is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/327"
+
+Failed Checks: Fat pointer comparison 'Lt' is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/327
+
+
+Checking harness check_dyn_ptr...
+
+Failed Checks: Fat pointer comparison 'Lt' is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/327

tests/expected/unsupported-fatptr-comparison/ptr_comparison.rs

@@ -0,0 +1,37 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Test relation comparison of fat pointers to slices.
+use std::cmp::*;
+
+/// Check comparison operators for two different elements.
+fn compare<T: ?Sized>(smaller: *const T, bigger: *const T) {
+    // Check relation operations that should return true.
+    assert!(smaller < bigger);
+    assert!(smaller <= bigger);
+    assert!(bigger > smaller);
+    assert!(bigger >= smaller);
+    assert!(bigger != smaller);
+    assert!(!(bigger == smaller));
+}
+
+#[kani::proof]
+fn check_slice_ptr() {
+    let array = [[0u8, 2]; 10];
+    let first_ptr: *const [u8] = &array[0];
+    let second_ptr: *const [u8] = &array[5];
+
+    compare(first_ptr, second_ptr);
+}
+
+trait Dummy {}
+impl Dummy for u8 {}
+
+#[kani::proof]
+fn check_dyn_ptr() {
+    let array = [0u8; 10];
+    let first_ptr: *const dyn Dummy = &array[0];
+    let second_ptr: *const dyn Dummy = &array[5];
+
+    compare(first_ptr, second_ptr);
+}

tests/kani/PointerComparison/fixme_ptr_comparison.rs

@@ -0,0 +1,105 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Test relation comparison of fat pointers to slices.
+use std::cmp::*;
+
+/// Check comparison operators for two different elements.
+fn compare_diff<T: ?Sized>(smaller: *const T, bigger: *const T) {
+    // Check Ord::cmp().
+    assert_eq!(smaller.cmp(&bigger), Ordering::Less);
+    assert_eq!(bigger.cmp(&smaller), Ordering::Greater);
+
+    // Check relation operations that should return true.
+    assert!(smaller < bigger);
+    assert!(smaller <= bigger);
+    assert!(bigger > smaller);
+    assert!(bigger >= smaller);
+    assert!(bigger != smaller);
+
+    // Check relation operations that should return false.
+    assert!(!(smaller > bigger));
+    assert!(!(smaller >= bigger));
+    assert!(!(bigger <= smaller));
+    assert!(!(bigger < smaller));
+    assert!(!(bigger == smaller));
+    assert!(!(std::ptr::eq(bigger, smaller)));
+
+    // Check Ord::{max, min}.
+    assert_eq!(smaller.min(bigger), smaller);
+    assert_eq!(smaller.max(bigger), bigger);
+    assert_eq!(bigger.min(smaller), smaller);
+    assert_eq!(bigger.max(smaller), bigger);
+}
+
+/// Check comparison operators for the same object.
+fn compare_equal<T: ?Sized>(object: *const T) {
+    // Check Ord::cmp().
+    assert_eq!(object.cmp(&object), Ordering::Equal);
+
+    // Check relation operations that should return true.
+    assert!(object <= object);
+    assert!(object >= object);
+    assert!(object == object);
+
+    // Check relation operations that should return false.
+    assert!(!(object > object));
+    assert!(!(object < object));
+    assert!(!(object != object));
+
+    // Check Ord::{max, min}.
+    assert_eq!(object.min(object), object);
+    assert_eq!(object.max(object), object);
+}
+
+/// Check clamp operation.
+fn check_clamp<T: ?Sized>(object: *const T, smaller: *const T, bigger: *const T) {
+    assert_eq!(object.clamp(smaller, bigger), object);
+    assert_eq!(object.clamp(smaller, object), object);
+    assert_eq!(object.clamp(object, bigger), object);
+
+    assert_eq!(object.clamp(bigger, bigger), bigger);
+    assert_eq!(object.clamp(smaller, smaller), smaller);
+}
+
+#[cfg_attr(kani, kani::proof)]
+fn check_thin_ptr() {
+    let array = [0u8; 10];
+    let first_ptr: *const u8 = &array[0];
+    let second_ptr: *const u8 = &array[5];
+
+    compare_diff(first_ptr, second_ptr);
+    compare_equal(first_ptr);
+    check_clamp(&array[5], &array[0], &array[9]);
+}
+
+#[cfg_attr(kani, kani::proof)]
+fn check_slice_ptr() {
+    let array = [[0u8, 2]; 10];
+    let first_ptr: *const [u8] = &array[0];
+    let second_ptr: *const [u8] = &array[5];
+
+    compare_diff(first_ptr, second_ptr);
+    compare_equal(first_ptr);
+    check_clamp::<[u8]>(&array[5], &array[0], &array[9]);
+}
+
+trait Dummy {}
+impl Dummy for u8 {}
+
+#[cfg_attr(kani, kani::proof)]
+fn check_dyn_ptr() {
+    let array = [0u8; 10];
+    let first_ptr: *const dyn Dummy = &array[0];
+    let second_ptr: *const dyn Dummy = &array[5];
+
+    compare_diff(first_ptr, second_ptr);
+    compare_equal(first_ptr);
+    check_clamp::<dyn Dummy>(&array[5], &array[0], &array[9]);
+}
+
+// Allow us to run usign rustc.
+fn main() {
+    check_thin_ptr();
+    check_slice_ptr();
+}

tests/kani/PointerOffset/fixme_overflow_ptr.rs

@@ -0,0 +1,12 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[kani::proof]
+fn check_thin_ptr() {
+    let array = [0, 1, 2, 3, 4, 5, 6];
+    let second_ptr: *const i32 = &array[3];
+    unsafe {
+        let before = second_ptr.sub(1);
+        assert_eq!(*before, 2);
+    }
+}