Add free(0) to codegen of loop contracts (#3637)

Add `free(0)` to the codegen result of loop contracts to avoid dropping
the body of `free`, which is required by DFCC.

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

Author: qinheping

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

@@ -573,9 +573,19 @@ impl GotocHook for LoopInvariantRegister {
     ) -> Stmt {
         let loc = gcx.codegen_span_stable(span);
         let func_exp = gcx.codegen_func_expr(instance, loc);
-
-        Stmt::goto(bb_label(target.unwrap()), loc)
-            .with_loop_contracts(func_exp.call(fargs).cast_to(Type::CInteger(CIntType::Bool)))
+        // Add `free(0)` to make sure the body of `free` won't be dropped to
+        // satisfy the requirement of DFCC.
+        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).with_loop_contracts(
+                    func_exp.call(fargs).cast_to(Type::CInteger(CIntType::Bool)),
+                ),
+            ],
+            loc,
+        )
     }
 }
 

tests/expected/loop-contract/count_zero.rs

@@ -27,9 +27,5 @@ const fn count_zero(slice: &[u8]) -> usize {
 
 #[kani::proof]
 pub fn check_counter() {
-    // Needed to avoid having `free` be removed as unused function. This is
-    // because DFCC contract enforcement assumes that a definition for `free`
-    // exists.
-    let _ = Box::new(10);
     assert_eq!(count_zero(&[1, 2, 3]), 0)
 }

tests/expected/loop-contract/memchar_naive.rs

@@ -13,10 +13,6 @@
 
 #[kani::proof]
 fn memchar_naive_harness() {
-    // Needed to avoid having `free` be removed as unused function. This is
-    // because DFCC contract enforcement assumes that a definition for `free`
-    // exists.
-    let _ = Box::new(10);
     let text = [1, 2, 3, 4, 5];
     let x = 5;
     let mut i = 0;

tests/expected/loop-contract/multiple_loops.rs

@@ -44,10 +44,6 @@ fn simple_while_loops() {
 
 #[kani::proof]
 fn multiple_loops_harness() {
-    // Needed to avoid having `free` be removed as unused function. This is
-    // because DFCC contract enforcement assumes that a definition for `free`
-    // exists.
-    let _ = Box::new(10);
     multiple_loops();
     simple_while_loops();
 }

tests/expected/loop-contract/simple_while_loop.rs

@@ -9,12 +9,7 @@
 #![feature(proc_macro_hygiene)]
 
 #[kani::proof]
-#[kani::solver(kissat)]
 fn simple_while_loop_harness() {
-    // Needed to avoid having `free` be removed as unused function. This is
-    // because DFCC contract enforcement assumes that a definition for `free`
-    // exists.
-    let _ = Box::new(10);
     let mut x: u8 = kani::any_where(|i| *i >= 2);
 
     #[kani::loop_invariant(x >= 2)]

tests/expected/loop-contract/small_slice_eq.rs

@@ -44,10 +44,6 @@ unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool {
 
 #[kani::proof]
 fn small_slice_eq_harness() {
-    // Needed to avoid having `free` be removed as unused function. This is
-    // because DFCC contract enforcement assumes that a definition for `free`
-    // exists.
-    let _ = Box::new(10);
     const ARR_SIZE: usize = 2000;
     let x: [u8; ARR_SIZE] = kani::any();
     let y: [u8; ARR_SIZE] = kani::any();