From 95afb374232ad0dc4008b0ae1d9fcd37b379e6a8 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Thu, 7 Nov 2024 16:51:07 -0600 Subject: [PATCH 1/4] Apply loop contracts only if there exists some usage --- .../src/codegen_cprover_gotoc/compiler_interface.rs | 5 +++++ .../src/codegen_cprover_gotoc/context/goto_ctx.rs | 3 +++ .../src/codegen_cprover_gotoc/overrides/hooks.rs | 3 +++ kani-compiler/src/kani_middle/codegen_units.rs | 7 +++++++ kani-compiler/src/kani_middle/metadata.rs | 2 ++ kani-driver/src/call_goto_instrument.rs | 12 +++--------- tests/expected/loop-contract/multiple_loops.rs | 8 ++++++++ 7 files changed, 31 insertions(+), 9 deletions(-) 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(); From fbf71aef72b1700c2ef4300b39c4e3ab0286469c Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Thu, 7 Nov 2024 16:59:29 -0600 Subject: [PATCH 2/4] Fix format --- kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs | 2 +- kani-driver/src/call_goto_instrument.rs | 6 +----- kani_metadata/src/harness.rs | 2 ++ tests/expected/loop-contract/multiple_loops.rs | 2 +- 4 files changed, 5 insertions(+), 7 deletions(-) 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 ec95f7e908cd..6fd9da651002 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -105,7 +105,7 @@ impl<'tcx> GotocCtx<'tcx> { unsupported_constructs: FxHashMap::default(), concurrent_constructs: FxHashMap::default(), transformer, - has_loop_contracts: false + has_loop_contracts: false, } } } diff --git a/kani-driver/src/call_goto_instrument.rs b/kani-driver/src/call_goto_instrument.rs index 6825392e3309..8f4eb150ff7b 100644 --- a/kani-driver/src/call_goto_instrument.rs +++ b/kani-driver/src/call_goto_instrument.rs @@ -164,11 +164,7 @@ impl KaniSession { } /// Apply annotated function contracts and loop contracts with goto-instrument. - pub fn instrument_contracts( - &self, - harness: &HarnessMetadata, - file: &Path, - ) -> Result<()> { + pub fn instrument_contracts(&self, harness: &HarnessMetadata, file: &Path) -> Result<()> { // Do nothing if neither loop contracts nor function contracts is enabled. if !harness.has_loop_contracts && harness.contract.is_none() { return Ok(()); diff --git a/kani_metadata/src/harness.rs b/kani_metadata/src/harness.rs index 426cf8d9e960..6932b15dc1a7 100644 --- a/kani_metadata/src/harness.rs +++ b/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, + /// 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. diff --git a/tests/expected/loop-contract/multiple_loops.rs b/tests/expected/loop-contract/multiple_loops.rs index 8c844eee2f95..b99278d32b43 100644 --- a/tests/expected/loop-contract/multiple_loops.rs +++ b/tests/expected/loop-contract/multiple_loops.rs @@ -47,7 +47,7 @@ fn simple_while_loops() { /// Check that `loop-contracts` works correctly for harness /// without loop contracts. #[kani::proof] -fn no_loop_harness(){ +fn no_loop_harness() { let x = 2; assert!(x == 2); } From 94862d4d5f45bbd6ff83d7d99cc6fa977ed0bbe9 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Thu, 7 Nov 2024 17:49:58 -0600 Subject: [PATCH 3/4] Add a test without loop contracts enabled --- .../codegen_cprover_gotoc/overrides/hooks.rs | 8 ++++++- kani-driver/src/call_goto_instrument.rs | 19 +++++++++++++---- kani-driver/src/metadata.rs | 1 + .../loop-contract/multiple_loops.expected | 1 + .../simple_while_loop_not_enabled.expected | 2 ++ .../simple_while_loop_not_enabled.rs | 21 +++++++++++++++++++ 6 files changed, 47 insertions(+), 5 deletions(-) create mode 100644 tests/expected/loop-contract/simple_while_loop_not_enabled.expected create mode 100644 tests/expected/loop-contract/simple_while_loop_not_enabled.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index ecc91e8a3116..a1f32bad223b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -567,7 +567,7 @@ impl GotocHook for LoopInvariantRegister { gcx: &mut GotocCtx, instance: Instance, fargs: Vec, - _assign_to: &Place, + assign_to: &Place, target: Option, span: Span, ) -> Stmt { @@ -583,6 +583,12 @@ impl GotocHook for LoopInvariantRegister { BuiltinFn::Free .call(vec![Expr::pointer_constant(0, Type::void_pointer())], loc) .as_stmt(loc), + 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)), ), diff --git a/kani-driver/src/call_goto_instrument.rs b/kani-driver/src/call_goto_instrument.rs index 8f4eb150ff7b..09b8cbb18fc8 100644 --- a/kani-driver/src/call_goto_instrument.rs +++ b/kani-driver/src/call_goto_instrument.rs @@ -37,7 +37,13 @@ impl KaniSession { self.goto_sanity_check(output)?; } - self.instrument_contracts(harness, output)?; + let is_loop_contracts_enabled = self + .args + .common_args + .unstable_features + .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() { self.add_library(output)?; @@ -164,16 +170,21 @@ impl KaniSession { } /// Apply annotated function contracts and loop contracts with goto-instrument. - pub fn instrument_contracts(&self, harness: &HarnessMetadata, file: &Path) -> Result<()> { + 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 !harness.has_loop_contracts && harness.contract.is_none() { + if !is_loop_contracts_enabled && harness.contract.is_none() { return Ok(()); } let mut args: Vec = vec!["--dfcc".into(), (&harness.mangled_name).into(), "--no-malloc-may-fail".into()]; - if harness.has_loop_contracts { + if is_loop_contracts_enabled { args.append(&mut vec![ "--apply-loop-contracts".into(), "--loop-contracts-no-unwind".into(), diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs index 174ce55187a6..94a5393408d3 100644 --- a/kani-driver/src/metadata.rs +++ b/kani-driver/src/metadata.rs @@ -223,6 +223,7 @@ pub mod tests { attributes, goto_file: model_file, contract: Default::default(), + has_loop_contracts: false, } } diff --git a/tests/expected/loop-contract/multiple_loops.expected b/tests/expected/loop-contract/multiple_loops.expected index 34c886c358cb..5d63471c6fa8 100644 --- a/tests/expected/loop-contract/multiple_loops.expected +++ b/tests/expected/loop-contract/multiple_loops.expected @@ -1 +1,2 @@ VERIFICATION:- SUCCESSFUL +Complete - 2 successfully verified harnesses, 0 failures, 2 total. diff --git a/tests/expected/loop-contract/simple_while_loop_not_enabled.expected b/tests/expected/loop-contract/simple_while_loop_not_enabled.expected new file mode 100644 index 000000000000..c0356572717d --- /dev/null +++ b/tests/expected/loop-contract/simple_while_loop_not_enabled.expected @@ -0,0 +1,2 @@ +Unwinding loop +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/loop-contract/simple_while_loop_not_enabled.rs b/tests/expected/loop-contract/simple_while_loop_not_enabled.rs new file mode 100644 index 000000000000..71851f7d875b --- /dev/null +++ b/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); +} From deef703f50638956b41995b12494fe3dc496c930 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Thu, 7 Nov 2024 18:51:07 -0600 Subject: [PATCH 4/4] Handle hook for loop contracts register function when loop contracts didsabled --- .../codegen_cprover_gotoc/overrides/hooks.rs | 56 ++++++++++++------- 1 file changed, 37 insertions(+), 19 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index a1f32bad223b..74c39c45ed74 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -576,25 +576,43 @@ impl GotocHook for LoopInvariantRegister { 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( - vec![ - BuiltinFn::Free - .call(vec![Expr::pointer_constant(0, Type::void_pointer())], loc) - .as_stmt(loc), - 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, - ) + 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, + ) + } } }