Mitigate issue with dangling pointers and memcmp (rust-lang#1526)

Author: fzaiser

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

@@ -298,6 +298,72 @@ impl<'tcx> GotocHook<'tcx> for SliceFromRawPart {
     }
 }
 
+/// This hook intercepts calls to `memcmp` and skips CBMC's pointer checks if the number of bytes to be compared is zero.
+/// See issue <https://github.com/model-checking/kani/issues/1489>
+///
+/// This compiles `memcmp(first, second, count)` to:
+/// ```c
+/// count_var = count;
+/// first_var = first;
+/// second_var = second;
+/// count_var == 0 && first_var != NULL && second_var != NULL ? 0 : memcmp(first_var, second_var, count_var)
+/// ```
+pub struct MemCmp;
+
+impl<'tcx> GotocHook<'tcx> for MemCmp {
+    fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool {
+        let name = with_no_trimmed_paths!(tcx.def_path_str(instance.def_id()));
+        name == "core::slice::cmp::memcmp" || name == "std::slice::cmp::memcmp"
+    }
+
+    fn handle(
+        &self,
+        tcx: &mut GotocCtx<'tcx>,
+        instance: Instance<'tcx>,
+        mut fargs: Vec<Expr>,
+        assign_to: Place<'tcx>,
+        target: Option<BasicBlock>,
+        span: Option<Span>,
+    ) -> Stmt {
+        let loc = tcx.codegen_span_option(span);
+        let target = target.unwrap();
+        let first = fargs.remove(0);
+        let second = fargs.remove(0);
+        let count = fargs.remove(0);
+        let (count_var, count_decl) = tcx.decl_temp_variable(count.typ().clone(), Some(count), loc);
+        let (first_var, first_decl) = tcx.decl_temp_variable(first.typ().clone(), Some(first), loc);
+        let (second_var, second_decl) =
+            tcx.decl_temp_variable(second.typ().clone(), Some(second), loc);
+        let is_count_zero = count_var.clone().is_zero();
+        // We have to ensure that the pointers are valid even if we're comparing zero bytes.
+        // According to Rust's current definition (see https://github.com/model-checking/kani/issues/1489),
+        // this means they have to be non-null and aligned.
+        // But alignment is automatically satisfied because `memcmp` takes `*const u8` pointers.
+        let is_first_ok = first_var.clone().is_nonnull();
+        let is_second_ok = second_var.clone().is_nonnull();
+        let should_skip_pointer_checks = is_count_zero.and(is_first_ok).and(is_second_ok);
+        let place_expr =
+            unwrap_or_return_codegen_unimplemented_stmt!(tcx, tcx.codegen_place(&assign_to))
+                .goto_expr;
+        let rhs = should_skip_pointer_checks.ternary(
+            Expr::int_constant(0, place_expr.typ().clone()), // zero bytes are always equal (as long as pointers are nonnull and aligned)
+            tcx.codegen_func_expr(instance, span.as_ref())
+                .call(vec![first_var, second_var, count_var]),
+        );
+        let code = place_expr.assign(rhs, loc).with_location(loc);
+        Stmt::block(
+            vec![
+                count_decl,
+                first_decl,
+                second_decl,
+                code,
+                Stmt::goto(tcx.current_fn().find_label(&target), loc),
+            ],
+            loc,
+        )
+    }
+}
+
 pub fn fn_hooks<'tcx>() -> GotocHooks<'tcx> {
     GotocHooks {
         hooks: vec![
@@ -308,6 +374,7 @@ pub fn fn_hooks<'tcx>() -> GotocHooks<'tcx> {
             Rc::new(Nondet),
             Rc::new(RustAlloc),
             Rc::new(SliceFromRawPart),
+            Rc::new(MemCmp),
         ],
     }
 }

tests/kani/MemCmpCpyZero/issue1489.rs

@@ -0,0 +1,11 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Regression test for https://github.com/model-checking/kani/issues/1489
+// Tests that memcmp and memcpy can be called with dangling pointers if the count is zero.
+
+#[kani::proof]
+fn main() {
+    // Vec::new() creates a dangling pointer
+    assert_eq!(Vec::<u8>::new(), Vec::<u8>::new());
+}