Apply loop contracts only if there exists some usage

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -263,6 +263,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
@@ -280,13 +281,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

@@ -573,6 +573,9 @@ impl GotocHook for LoopInvariantRegister {
     ) -> Stmt {
         let loc = gcx.codegen_span_stable(span);
         let func_exp = gcx.codegen_func_expr(instance, loc);
+
+        gcx.has_loop_contracts = true;
+
         // Add `free(0)` to make sure the body of `free` won't be dropped to
         // satisfy the requirement of DFCC.
         Stmt::block(

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

@@ -37,12 +37,7 @@ impl KaniSession {
             self.goto_sanity_check(output)?;
         }
 
-        let is_loop_contracts_enabled = self
-            .args
-            .common_args
-            .unstable_features
-            .contains(kani_metadata::UnstableFeature::LoopContracts);
-        self.instrument_contracts(harness, is_loop_contracts_enabled, output)?;
+        self.instrument_contracts(harness, output)?;
 
         if self.args.checks.undefined_function_on() {
             self.add_library(output)?;
@@ -172,18 +167,17 @@ impl KaniSession {
     pub fn instrument_contracts(
         &self,
         harness: &HarnessMetadata,
-        is_loop_contracts_enabled: bool,
         file: &Path,
     ) -> Result<()> {
         // Do nothing if neither loop contracts nor function contracts is enabled.
-        if !is_loop_contracts_enabled && harness.contract.is_none() {
+        if !harness.has_loop_contracts && harness.contract.is_none() {
             return Ok(());
         }
 
         let mut args: Vec<OsString> =
             vec!["--dfcc".into(), (&harness.mangled_name).into(), "--no-malloc-may-fail".into()];
 
-        if is_loop_contracts_enabled {
+        if harness.has_loop_contracts {
             args.append(&mut vec![
                 "--apply-loop-contracts".into(),
                 "--loop-contracts-no-unwind".into(),

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();