diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 25bc0cbe8ad1..0e22fc3d4570 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/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,6 +281,9 @@ 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)); @@ -287,6 +291,7 @@ impl CodegenBackend for GotocCodegenBackend { } } units.store_modifies(&modifies_instances); + units.store_loop_contracts(&loop_contracts_instances); units.write_metadata(&queries, tcx); } ReachabilityType::Tests => { diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index 176268022f34..ec95f7e908cd 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/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 } } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 7d63315e1e13..ecc91e8a3116 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/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( diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index ebb12f7656b6..072528f9a765 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/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); diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index c92b20cf49d6..67d32b0079c4 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/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, } } diff --git a/kani-driver/src/call_goto_instrument.rs b/kani-driver/src/call_goto_instrument.rs index 4ec363655491..6825392e3309 100644 --- a/kani-driver/src/call_goto_instrument.rs +++ b/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 = 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(), diff --git a/tests/expected/loop-contract/multiple_loops.rs b/tests/expected/loop-contract/multiple_loops.rs index 8baf1f251b4c..8c844eee2f95 100644 --- a/tests/expected/loop-contract/multiple_loops.rs +++ b/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();