Replace the hook for realloc with a C implementation (rust-lang#1088)

Co-authored-by:
Daniel Schwartz-Narbonne

Author: zhassan-aws

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

@@ -548,47 +548,6 @@ impl<'tcx> GotocHook<'tcx> for RustDealloc {
     }
 }
 
-struct RustRealloc;
-
-impl<'tcx> GotocHook<'tcx> for RustRealloc {
-    fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool {
-        let name = tcx.symbol_name(instance).name.to_string();
-        name == "__rust_realloc"
-    }
-
-    fn handle(
-        &self,
-        tcx: &mut GotocCtx<'tcx>,
-        _instance: Instance<'tcx>,
-        mut fargs: Vec<Expr>,
-        assign_to: Option<Place<'tcx>>,
-        target: Option<BasicBlock>,
-        span: Option<Span>,
-    ) -> Stmt {
-        let loc = tcx.codegen_span_option(span);
-        let p = assign_to.unwrap();
-        let target = target.unwrap();
-        let ptr = fargs.remove(0).cast_to(Type::void_pointer());
-        fargs.remove(0); // old_size
-        fargs.remove(0); // align
-        let size = fargs.remove(0);
-        Stmt::block(
-            vec![
-                unwrap_or_return_codegen_unimplemented_stmt!(tcx, tcx.codegen_place(&p))
-                    .goto_expr
-                    .assign(
-                        BuiltinFn::Realloc
-                            .call(vec![ptr, size], loc.clone())
-                            .cast_to(Type::unsigned_int(8).to_pointer()),
-                        loc.clone(),
-                    ),
-                Stmt::goto(tcx.current_fn().find_label(&target), loc.clone()),
-            ],
-            loc,
-        )
-    }
-}
-
 struct RustAllocZeroed;
 
 impl<'tcx> GotocHook<'tcx> for RustAllocZeroed {
@@ -680,7 +639,6 @@ pub fn fn_hooks<'tcx>() -> GotocHooks<'tcx> {
             Rc::new(RustAlloc),
             Rc::new(RustAllocZeroed),
             Rc::new(RustDealloc),
-            Rc::new(RustRealloc),
             Rc::new(SliceFromRawPart),
         ],
     }

library/kani/kani_lib.c

@@ -1,2 +1,36 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#include <assert.h>
+#include <stddef.h>
+#include <stdint.h>
+#include <stdlib.h>
+#include <string.h>
+
+// This is a C implementation of the __rust_realloc function that has the following signature:
+//     fn __rust_realloc(ptr: *mut u8, old_size: usize, align: usize, new_size: usize) -> *mut u8;
+// This low-level function is called by std::alloc:realloc, and its
+// implementation is provided by the compiler backend, so we need to provide an
+// implementation for it to prevent verification failure due to missing function
+// definition.
+// For safety, refer to the documentation of GlobalAlloc::realloc:
+// https://doc.rust-lang.org/std/alloc/trait.GlobalAlloc.html#method.realloc
+uint8_t *__rust_realloc(uint8_t *ptr, size_t old_size, size_t align, size_t new_size)
+{
+    // Passing a NULL pointer is undefined behavior
+    __CPROVER_assert(ptr != 0, "realloc called with a null pointer");
+    __CPROVER_assume(ptr != 0);
+
+    // Passing a new_size of 0 is undefined behavior
+    __CPROVER_assert(new_size > 0, "realloc called with a size of 0");
+    __CPROVER_assume(new_size > 0);
+
+    uint8_t *result = malloc(new_size);
+    if (result) {
+        size_t bytes_to_copy = new_size < old_size ? new_size : old_size;
+        memcpy(result, ptr, bytes_to_copy);
+        free(ptr);
+    }
+
+    return result;
+}

tests/expected/realloc/null/expected

@@ -0,0 +1,4 @@
+Status: FAILURE\
+Description: "realloc called with a null pointer"
+
+VERIFICATION:- FAILED

tests/expected/realloc/null/main.rs

@@ -0,0 +1,16 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Calling realloc with a null pointer fails
+
+use std::alloc::{realloc, Layout};
+
+#[kani::proof]
+fn main() {
+    unsafe {
+        let layout = Layout::array::<i32>(0).unwrap();
+        let ptr: *const u8 = std::ptr::null();
+
+        let _ptr = realloc(ptr as *mut u8, layout, 12);
+    }
+}

tests/expected/realloc/shrink/expected

@@ -0,0 +1,4 @@
+Status: FAILURE\
+Description: "dereference failure: pointer outside object bounds"
+
+VERIFICATION:- FAILED

tests/expected/realloc/shrink/main.rs

@@ -0,0 +1,35 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Use realloc to shrink the size of the allocated block and make sure
+// out-of-bound accesses result in verification failure
+
+use std::alloc::{alloc, dealloc, realloc, Layout};
+
+#[kani::proof]
+fn main() {
+    unsafe {
+        let mut len = 5;
+        let mut layout = Layout::array::<i16>(len).unwrap();
+        let ptr = alloc(layout);
+
+        *(ptr as *mut i16) = 5557;
+        *(ptr as *mut i16).offset(1) = 381;
+        *(ptr as *mut i16).offset(2) = -782;
+        *(ptr as *mut i16).offset(3) = -1294;
+        *(ptr as *mut i16).offset(4) = 22222;
+
+        // realloc to a smaller size (2 i16 elements = 4 bytes)
+        let ptr = realloc(ptr as *mut u8, layout, 4);
+        len = 2;
+        layout = Layout::array::<i16>(len).unwrap();
+
+        // the first two elements should remain intact
+        assert_eq!(*(ptr as *mut i16), 5557);
+        assert_eq!(*(ptr as *mut i16).offset(1), 381);
+        // this should be an invalid memory access
+        let _x = *(ptr as *mut i16).offset(2);
+
+        dealloc(ptr, layout);
+    }
+}

tests/expected/realloc/zero_size/expected

@@ -0,0 +1,4 @@
+Status: FAILURE\
+Description: "realloc called with a size of 0"
+
+VERIFICATION:- FAILED

tests/expected/realloc/zero_size/main.rs

@@ -0,0 +1,20 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Calling realloc with a size of zero fails
+
+use std::alloc::{alloc, realloc, Layout};
+
+#[kani::proof]
+fn main() {
+    unsafe {
+        let layout = Layout::array::<i32>(3).unwrap();
+        let ptr = alloc(layout);
+
+        *(ptr as *mut i32) = 888;
+        *(ptr as *mut i32).offset(1) = 777;
+        *(ptr as *mut i32).offset(2) = -432;
+
+        let _ptr = realloc(ptr as *mut u8, layout, 0);
+    }
+}

tests/kani/Realloc/two_reallocs.rs

@@ -0,0 +1,38 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Perform two reallocs in a row and make sure the data is properly copied
+
+use std::alloc::{alloc, dealloc, realloc, Layout};
+
+#[kani::proof]
+fn main() {
+    unsafe {
+        let mut len = 4;
+        let mut layout = Layout::array::<u16>(len).unwrap();
+        let mut sz = layout.size();
+        let ptr = alloc(layout);
+
+        *(ptr as *mut u16) = 551;
+        *(ptr as *mut u16).offset(1) = 12;
+        *(ptr as *mut u16).offset(2) = 8928;
+        *(ptr as *mut u16).offset(3) = 499;
+
+        sz *= 2;
+        let ptr = realloc(ptr as *mut u8, layout, sz);
+        len *= 2;
+        layout = Layout::array::<u16>(len).unwrap();
+
+        sz *= 2;
+        let ptr = realloc(ptr as *mut u8, layout, sz);
+        len *= 2;
+        layout = Layout::array::<u16>(len).unwrap();
+
+        assert_eq!(*(ptr as *mut u16), 551);
+        assert_eq!(*(ptr as *mut u16).offset(1), 12);
+        assert_eq!(*(ptr as *mut u16).offset(2), 8928);
+        assert_eq!(*(ptr as *mut u16).offset(3), 499);
+
+        dealloc(ptr, layout);
+    }
+}

tests/kani/Vectors/fixme_702.rs renamed to tests/kani/Vectors/push.rs

@@ -1,7 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Failing example from https://github.com/model-checking/kani/issues/702
 // Push 5 elements to force the vector to resize, then check that the values were correctly copied.
 #[kani::proof]
 fn main() {