Apply loop contracts only if there exists some usage (#3694)

In this PR, we detect the usage of loop contracts, and apply loop
contracts with goto-instrument only if there exists some usage of loop
contracts in the codegen unit.

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

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -256,6 +256,7 @@ impl CodegenBackend for GotocCodegenBackend {
                 ReachabilityType::Harnesses => {
                     let mut units = CodegenUnits::new(&queries, tcx);
                     let mut modifies_instances = vec![];
+                    let mut loop_contracts_instances = vec![];
                     // Cross-crate collecting of all items that are reachable from the crate harnesses.
                     for unit in units.iter() {
                         // We reset the body cache for now because each codegen unit has different
@@ -273,13 +274,17 @@ impl CodegenBackend for GotocCodegenBackend {
                                 contract_metadata,
                                 transformer,
                             );
+                            if gcx.has_loop_contracts {
+                                loop_contracts_instances.push(*harness);
+                            }
                             results.extend(gcx, items, None);
                             if let Some(assigns_contract) = contract_info {
                                 modifies_instances.push((*harness, assigns_contract));
                             }
                         }
                     }
                     units.store_modifies(&modifies_instances);
+                    units.store_loop_contracts(&loop_contracts_instances);
                     units.write_metadata(&queries, tcx);
                 }
                 ReachabilityType::Tests => {

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

@@ -74,6 +74,8 @@ pub struct GotocCtx<'tcx> {
     pub concurrent_constructs: UnsupportedConstructs,
     /// The body transformation agent.
     pub transformer: BodyTransformation,
+    /// If there exist some usage of loop contracts int context.
+    pub has_loop_contracts: bool,
 }
 
 /// Constructor
@@ -103,6 +105,7 @@ impl<'tcx> GotocCtx<'tcx> {
             unsupported_constructs: FxHashMap::default(),
             concurrent_constructs: FxHashMap::default(),
             transformer,
+            has_loop_contracts: false,
         }
     }
 }

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

@@ -567,25 +567,52 @@ impl GotocHook for LoopInvariantRegister {
         gcx: &mut GotocCtx,
         instance: Instance,
         fargs: Vec<Expr>,
-        _assign_to: &Place,
+        assign_to: &Place,
         target: Option<BasicBlockIdx>,
         span: Span,
     ) -> Stmt {
         let loc = gcx.codegen_span_stable(span);
         let func_exp = gcx.codegen_func_expr(instance, loc);
-        // 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,
-        )
+
+        gcx.has_loop_contracts = true;
+
+        if gcx.queries.args().unstable_features.contains(&"loop-contracts".to_string()) {
+            // When loop-contracts is enabled, codegen
+            // free(0)
+            // goto target --- with loop contracts annotated.
+
+            // 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,
+            )
+        } else {
+            // When loop-contracts is not enabled, codegen
+            // assign_to = true
+            // goto target
+            Stmt::block(
+                vec![
+                    unwrap_or_return_codegen_unimplemented_stmt!(
+                        gcx,
+                        gcx.codegen_place_stable(assign_to, loc)
+                    )
+                    .goto_expr
+                    .assign(Expr::c_true(), loc),
+                    Stmt::goto(bb_label(target.unwrap()), loc).with_loop_contracts(
+                        func_exp.call(fargs).cast_to(Type::CInteger(CIntType::Bool)),
+                    ),
+                ],
+                loc,
+            )
+        }
     }
 }
 

kani-compiler/src/kani_middle/codegen_units.rs

@@ -91,6 +91,13 @@ impl CodegenUnits {
         }
     }
 
+    /// We flag that the harness contains usage of loop contracts.
+    pub fn store_loop_contracts(&mut self, harnesses: &[Harness]) {
+        for harness in harnesses {
+            self.harness_info.get_mut(harness).unwrap().has_loop_contracts = true;
+        }
+    }
+
     /// Write compilation metadata into a file.
     pub fn write_metadata(&self, queries: &QueryDb, tcx: TyCtxt) {
         let metadata = self.generate_metadata(tcx);

kani-compiler/src/kani_middle/metadata.rs

@@ -38,6 +38,7 @@ pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) ->
         // TODO: This no longer needs to be an Option.
         goto_file: Some(model_file),
         contract: Default::default(),
+        has_loop_contracts: false,
     }
 }
 
@@ -108,5 +109,6 @@ pub fn gen_test_metadata(
         // TODO: This no longer needs to be an Option.
         goto_file: Some(model_file),
         contract: Default::default(),
+        has_loop_contracts: false,
     }
 }

kani-driver/src/call_goto_instrument.rs

@@ -41,7 +41,8 @@ impl KaniSession {
             .args
             .common_args
             .unstable_features
-            .contains(kani_metadata::UnstableFeature::LoopContracts);
+            .contains(kani_metadata::UnstableFeature::LoopContracts)
+            && harness.has_loop_contracts;
         self.instrument_contracts(harness, is_loop_contracts_enabled, output)?;
 
         if self.args.checks.undefined_function_on() {

kani-driver/src/metadata.rs

@@ -223,6 +223,7 @@ pub mod tests {
             attributes,
             goto_file: model_file,
             contract: Default::default(),
+            has_loop_contracts: false,
         }
     }
 

kani_metadata/src/harness.rs

@@ -36,6 +36,8 @@ pub struct HarnessMetadata {
     pub attributes: HarnessAttributes,
     /// A CBMC-level assigns contract that should be enforced when running this harness.
     pub contract: Option<AssignsContract>,
+    /// If the harness contains some usage of loop contracts.
+    pub has_loop_contracts: bool,
 }
 
 /// The attributes added by the user to control how a harness is executed.

tests/expected/loop-contract/multiple_loops.expected

@@ -1 +1,2 @@
 VERIFICATION:- SUCCESSFUL
+Complete - 2 successfully verified harnesses, 0 failures, 2 total.

tests/expected/loop-contract/multiple_loops.rs

@@ -44,6 +44,14 @@ fn simple_while_loops() {
     assert!(x == 2);
 }
 
+/// Check that `loop-contracts` works correctly for harness
+/// without loop contracts.
+#[kani::proof]
+fn no_loop_harness() {
+    let x = 2;
+    assert!(x == 2);
+}
+
 #[kani::proof]
 fn multiple_loops_harness() {
     multiple_loops();

tests/expected/loop-contract/simple_while_loop_not_enabled.expected

@@ -0,0 +1,2 @@
+Unwinding loop
+VERIFICATION:- SUCCESSFUL

tests/expected/loop-contract/simple_while_loop_not_enabled.rs

@@ -0,0 +1,21 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags:
+
+//! Check if the harness can be proved when loop contracts is not enabled.
+
+#![feature(stmt_expr_attributes)]
+#![feature(proc_macro_hygiene)]
+
+#[kani::proof]
+fn simple_while_loop_harness() {
+    let mut x: u8 = 10;
+
+    #[kani::loop_invariant(x >= 2)]
+    while x > 2 {
+        x = x - 1;
+    }
+
+    assert!(x == 2);
+}