Remove empty box creation from contracts impl (#3233)

There seems to be an issue in CBMC contracts implementation that it
assumes that `free` must have a body. However, slicing can remove `free`
body if the harness does not allocate anything.

diffblue/cbmc#8317

We used to create an empty Box before to force `free` to be in scope.
Instead, just invoke `free(NULL)` which is a no-op.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Co-authored-by: Jaisurya Nanduri <[email protected]>

Author: celinval

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

@@ -458,6 +458,45 @@ impl GotocHook for UntrackedDeref {
     }
 }
 
+struct InitContracts;
+
+/// CBMC contracts currently has a limitation where `free` has to be in scope.
+/// However, if there is no dynamic allocation in the harness, slicing removes `free` from the
+/// scope.
+///
+/// Thus, this function will basically translate into:
+/// ```c
+/// // This is a no-op.
+/// free(NULL);
+/// ```
+impl GotocHook for InitContracts {
+    fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
+        matches_function(tcx, instance.def, "KaniInitContracts")
+    }
+
+    fn handle(
+        &self,
+        gcx: &mut GotocCtx,
+        _instance: Instance,
+        fargs: Vec<Expr>,
+        _assign_to: &Place,
+        target: Option<BasicBlockIdx>,
+        span: Span,
+    ) -> Stmt {
+        assert_eq!(fargs.len(), 0,);
+        let loc = gcx.codegen_span_stable(span);
+        Stmt::block(
+            vec![
+                BuiltinFn::Free
+                    .call(vec![Expr::pointer_constant(0, Type::void_pointer())], loc)
+                    .as_stmt(loc),
+                Stmt::goto(bb_label(target.unwrap()), loc),
+            ],
+            loc,
+        )
+    }
+}
+
 pub fn fn_hooks() -> GotocHooks {
     GotocHooks {
         hooks: vec![
@@ -472,6 +511,7 @@ pub fn fn_hooks() -> GotocHooks {
             Rc::new(RustAlloc),
             Rc::new(MemCmp),
             Rc::new(UntrackedDeref),
+            Rc::new(InitContracts),
         ],
     }
 }

library/kani/src/internal.rs

@@ -76,3 +76,17 @@ impl<'a, T> Pointer<'a> for *mut T {
 pub fn untracked_deref<T>(_: &T) -> T {
     todo!()
 }
+
+/// CBMC contracts currently has a limitation where `free` has to be in scope.
+/// However, if there is no dynamic allocation in the harness, slicing removes `free` from the
+/// scope.
+///
+/// Thus, this function will basically translate into:
+/// ```c
+/// // This is a no-op.
+/// free(NULL);
+/// ```
+#[inline(never)]
+#[doc(hidden)]
+#[rustc_diagnostic_item = "KaniInitContracts"]
+pub fn init_contracts() {}

library/kani_macros/src/sysroot/contracts/mod.rs

@@ -294,7 +294,7 @@ pub fn proof_for_contract(attr: TokenStream, item: TokenStream) -> TokenStream {
         #[kanitool::proof_for_contract = stringify!(#args)]
         #(#attrs)*
         #vis #sig {
-            let _ = std::boxed::Box::new(0_usize);
+            kani::internal::init_contracts();
             #block
         }
     )