From dd26362479ca9f57445f66187ea33d6a70ced534 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Wed, 18 Sep 2024 15:08:13 -0400 Subject: [PATCH 1/3] Call `check_proof_attribute` for contract harnesses (#3522) Kani enforces that `[kani::proof]` attribute is not applied to generic functions. We do not currently enforce this restriction on contract harnesses. When the compiler [searches for harnesses to verify](https://github.com/model-checking/kani/blob/dba8f3926a61025f5078de787ebd8d21278333ca/kani-compiler/src/kani_middle/codegen_units.rs#L63), it only looks at monomorphized functions. Thus, currently a user can write this code: ```rust #[kani::requires(true)] fn foo() {} #[kani::proof_for_contract(foo)] fn check_foo() { foo() } ``` and get "No proof harnesses (functions with #[kani::proof]) were found to verify." In the case where a user is running many harnesses, they may not notice that Kani skipped the harness. For example, we currently have [this harness](https://github.com/model-checking/verify-rust-std/blob/149f6dd5409fac01a983d7b98c51d51666c74e45/library/core/src/ptr/unique.rs#L288) in the standard library, which doesn't actually run. (PR to fix is [here](https://github.com/model-checking/verify-rust-std/pull/86)). After this PR merges, the code snippet above would instead error with: ```rust error: the '#[kani::proof_for_contract]' attribute cannot be applied to generic functions --> src/lib.rs:4:1 | 4 | #[kani::proof_for_contract(foo)] | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | = note: this error originates in the attribute macro `kani::proof_for_contract` (in Nightly builds, run with -Z macro-backtrace for more info) error: aborting due to 1 previous error ``` 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/kani_middle/attributes.rs | 27 +++++++++++++++----- tests/ui/invalid-contract-harness/expected | 17 ++++++++++++ tests/ui/invalid-contract-harness/invalid.rs | 25 ++++++++++++++++++ tests/ui/invalid-harnesses/expected | 2 +- tests/ui/mir-linker/generic-harness/expected | 2 +- 5 files changed, 65 insertions(+), 8 deletions(-) create mode 100644 tests/ui/invalid-contract-harness/expected create mode 100644 tests/ui/invalid-contract-harness/invalid.rs diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 9a3ff7c1d6a6..86e97f633dfb 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -358,7 +358,7 @@ impl<'tcx> KaniAttributes<'tcx> { ); } expect_single(self.tcx, kind, &attrs); - attrs.iter().for_each(|attr| self.check_proof_attribute(attr)) + attrs.iter().for_each(|attr| self.check_proof_attribute(kind, attr)) } KaniAttributeKind::Unstable => attrs.iter().for_each(|attr| { let _ = UnstableAttribute::try_from(*attr).map_err(|err| err.report(self.tcx)); @@ -370,6 +370,7 @@ impl<'tcx> KaniAttributes<'tcx> { ); } expect_single(self.tcx, kind, &attrs); + attrs.iter().for_each(|attr| self.check_proof_attribute(kind, attr)) } KaniAttributeKind::StubVerified => { expect_single(self.tcx, kind, &attrs); @@ -583,15 +584,29 @@ impl<'tcx> KaniAttributes<'tcx> { } /// Check that if this item is tagged with a proof_attribute, it is a valid harness. - fn check_proof_attribute(&self, proof_attribute: &Attribute) { + fn check_proof_attribute(&self, kind: KaniAttributeKind, proof_attribute: &Attribute) { let span = proof_attribute.span; let tcx = self.tcx; - expect_no_args(tcx, KaniAttributeKind::Proof, proof_attribute); + if let KaniAttributeKind::Proof = kind { + expect_no_args(tcx, kind, proof_attribute); + } + if tcx.def_kind(self.item) != DefKind::Fn { - tcx.dcx().span_err(span, "the `proof` attribute can only be applied to functions"); + tcx.dcx().span_err( + span, + format!( + "the '#[kani::{}]' attribute can only be applied to functions", + kind.as_ref() + ), + ); } else if tcx.generics_of(self.item).requires_monomorphization(tcx) { - tcx.dcx() - .span_err(span, "the `proof` attribute cannot be applied to generic functions"); + tcx.dcx().span_err( + span, + format!( + "the '#[kani::{}]' attribute cannot be applied to generic functions", + kind.as_ref() + ), + ); } else { let instance = Instance::mono(tcx, self.item); if !super::fn_abi(tcx, instance).args.is_empty() { diff --git a/tests/ui/invalid-contract-harness/expected b/tests/ui/invalid-contract-harness/expected new file mode 100644 index 000000000000..1e07c4ca4b16 --- /dev/null +++ b/tests/ui/invalid-contract-harness/expected @@ -0,0 +1,17 @@ +error: only one '#[kani::proof_for_contract]' attribute is allowed per harness\ +invalid.rs:\ +|\ +| #[kani::proof_for_contract(foo)]\ +| ^^^^^^^^^^^^^^ + +error: functions used as harnesses cannot have any arguments\ +invalid.rs:\ +|\ +| #[kani::proof_for_contract(foo)] +| ^^^^^^^^^^^^^^ + +error: the '#[kani::proof_for_contract]' attribute cannot be applied to generic functions\ +invalid.rs:\ +|\ +| #[kani::proof_for_contract(foo)]\ +| ^^^^^^^^^^^^^^ diff --git a/tests/ui/invalid-contract-harness/invalid.rs b/tests/ui/invalid-contract-harness/invalid.rs new file mode 100644 index 000000000000..e30382e3c602 --- /dev/null +++ b/tests/ui/invalid-contract-harness/invalid.rs @@ -0,0 +1,25 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +// This test is to check Kani's error handling of invalid usages of the `proof_for_contract` harness. +// We also ensure that all errors and warnings are printed in one compilation. + +#[kani::requires(true)] +fn foo() {} + +#[kani::proof_for_contract(foo)] +#[kani::proof_for_contract(foo)] +fn multiple_proof_annotations() { + foo(); +} + +#[kani::proof_for_contract(foo)] +fn proof_with_arg(arg: bool) { + foo(); +} + +#[kani::proof_for_contract(foo)] +fn generic_harness() { + foo(); +} diff --git a/tests/ui/invalid-harnesses/expected b/tests/ui/invalid-harnesses/expected index 7def51a0d85a..265af44a1685 100644 --- a/tests/ui/invalid-harnesses/expected +++ b/tests/ui/invalid-harnesses/expected @@ -10,7 +10,7 @@ invalid.rs:\ | #[kani::proof] | ^^^^^^^^^^^^^^ -error: the `proof` attribute cannot be applied to generic functions\ +error: the '#[kani::proof]' attribute cannot be applied to generic functions\ invalid.rs:\ |\ | #[kani::proof]\ diff --git a/tests/ui/mir-linker/generic-harness/expected b/tests/ui/mir-linker/generic-harness/expected index 0798bb9e99a3..176ca1a5b7db 100644 --- a/tests/ui/mir-linker/generic-harness/expected +++ b/tests/ui/mir-linker/generic-harness/expected @@ -1 +1 @@ -error: the `proof` attribute cannot be applied to generic functions +error: the '#[kani::proof]' attribute cannot be applied to generic functions From 27cee8b71d8e82d86e04d315534d1677d2744716 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Wed, 18 Sep 2024 16:11:23 -0400 Subject: [PATCH 2/3] Add tests for issue 3009 (#3526) Kani v0.55 no longer has the overly broad span issue reported in #3009. I suspect that our shift (#3363) from functions to closures for contracts allows rustc to produce better error messages. Add tests to prevent regression in the future. Resolves #3009 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .../function-contracts/non_bool_contracts.expected | 11 +++++++++++ tests/ui/function-contracts/non_bool_contracts.rs | 13 +++++++++++++ 2 files changed, 24 insertions(+) create mode 100644 tests/ui/function-contracts/non_bool_contracts.expected create mode 100644 tests/ui/function-contracts/non_bool_contracts.rs diff --git a/tests/ui/function-contracts/non_bool_contracts.expected b/tests/ui/function-contracts/non_bool_contracts.expected new file mode 100644 index 000000000000..a6d7704330db --- /dev/null +++ b/tests/ui/function-contracts/non_bool_contracts.expected @@ -0,0 +1,11 @@ +| +| #[kani::requires(a + b)] +| -----------------^^^^^-- +| | | +| | expected `bool`, found `u64` +| arguments to this function are incorrect +| + +| +| #[kani::ensures(|result| a % *result && b % *result == 0 && *result != 0)] +| ^^^^^^^^^^^ expected `bool`, found `u64` \ No newline at end of file diff --git a/tests/ui/function-contracts/non_bool_contracts.rs b/tests/ui/function-contracts/non_bool_contracts.rs new file mode 100644 index 000000000000..e192e625cac3 --- /dev/null +++ b/tests/ui/function-contracts/non_bool_contracts.rs @@ -0,0 +1,13 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +// This tests that Kani reports the "ideal" error message when contracts are non-boolean expressions +// By "ideal," we mean that the error spans are as narrow as possible +// (c.f. https://github.com/model-checking/kani/issues/3009) + +#[kani::requires(a + b)] +#[kani::ensures(|result| a % *result && b % *result == 0 && *result != 0)] +fn gcd(a: u64, b: u64) -> u64 { + 0 +} From f1221b1b25e9e2896a9dfef48768cabc677b0ef6 Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Fri, 20 Sep 2024 11:40:16 -0400 Subject: [PATCH 3/3] Fix storing coverage data in cargo projects (#3527) This PR changes the condition we use to decide where to store the coverage data resulting from a coverage-enabled verification run. The previous condition would otherwise cause Kani to crash at the end of the run in some cases: ``` Source-based code coverage results: src/pair.rs (pair::Pair::new) * 6:5 - 8:6 COVERED src/pair.rs (pair::Pair::sum) * 9:5 - 11:6 COVERED src/pair.rs (pair::kani_tests::test_one_plus_two) * 29:5 - 32:6 COVERED Verification Time: 0.083455205s thread 'main' panicked at kani-driver/src/coverage/cov_session.rs:70:43: called `Option::unwrap()` on a `None` value note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace ``` The PR also adds a new `cargo-coverage` mode to `compiletest` which runs `cargo kani` with the source-based coverage feature enabled. This ensures that coverage-enabled `cargo kani` runs are also being tested, and will also be helpful for testing the upcoming coverage tool (#3121) with cargo packages. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- kani-driver/src/coverage/cov_session.rs | 4 +-- scripts/kani-regression.sh | 1 + tests/cargo-coverage/simple-lib/Cargo.toml | 10 ++++++ tests/cargo-coverage/simple-lib/src/lib.rs | 25 ++++++++++++++ tests/cargo-coverage/simple-lib/src/pair.rs | 33 +++++++++++++++++++ .../simple-lib/test_one_plus_two.expected | 10 ++++++ .../simple-lib/test_sum.expected | 10 ++++++ tools/compiletest/src/common.rs | 3 ++ tools/compiletest/src/main.rs | 8 +++-- tools/compiletest/src/runtest.rs | 33 +++++++++++++++++-- 10 files changed, 131 insertions(+), 6 deletions(-) create mode 100644 tests/cargo-coverage/simple-lib/Cargo.toml create mode 100644 tests/cargo-coverage/simple-lib/src/lib.rs create mode 100644 tests/cargo-coverage/simple-lib/src/pair.rs create mode 100644 tests/cargo-coverage/simple-lib/test_one_plus_two.expected create mode 100644 tests/cargo-coverage/simple-lib/test_sum.expected diff --git a/kani-driver/src/coverage/cov_session.rs b/kani-driver/src/coverage/cov_session.rs index df82d982bd72..bf6b34d3cd0b 100644 --- a/kani-driver/src/coverage/cov_session.rs +++ b/kani-driver/src/coverage/cov_session.rs @@ -18,7 +18,7 @@ impl KaniSession { /// Note: Currently, coverage mappings are not included due to technical /// limitations. But this is where we should save them. pub fn save_coverage_metadata(&self, project: &Project, stamp: &String) -> Result<()> { - if self.args.target_dir.is_some() { + if project.input.is_none() { self.save_coverage_metadata_cargo(project, stamp) } else { self.save_coverage_metadata_standalone(project, stamp) @@ -97,7 +97,7 @@ impl KaniSession { results: &Vec, stamp: &String, ) -> Result<()> { - if self.args.target_dir.is_some() { + if project.input.is_none() { self.save_coverage_results_cargo(results, stamp) } else { self.save_coverage_results_standalone(project, results, stamp) diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index b1de293d533c..bd6b04d7386e 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -60,6 +60,7 @@ TESTS=( "cargo-ui cargo-kani" "script-based-pre exec" "coverage coverage-based" + "cargo-coverage cargo-coverage" "kani-docs cargo-kani" "kani-fixme kani-fixme" ) diff --git a/tests/cargo-coverage/simple-lib/Cargo.toml b/tests/cargo-coverage/simple-lib/Cargo.toml new file mode 100644 index 000000000000..23f843337dc7 --- /dev/null +++ b/tests/cargo-coverage/simple-lib/Cargo.toml @@ -0,0 +1,10 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "simple-lib" +version = "0.1.0" +edition = "2018" + +[dependencies] + +[workspace] diff --git a/tests/cargo-coverage/simple-lib/src/lib.rs b/tests/cargo-coverage/simple-lib/src/lib.rs new file mode 100644 index 000000000000..f5f23c6a2acb --- /dev/null +++ b/tests/cargo-coverage/simple-lib/src/lib.rs @@ -0,0 +1,25 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +pub mod pair; +pub use pair::Pair; + +#[cfg(test)] +mod tests { + #[test] + fn it_works() { + assert_eq!(2 + 2, 4); + } +} + +#[cfg(kani)] +mod kani_tests { + use super::*; + + #[kani::proof] + fn test_sum() { + let a: u64 = kani::any(); + let b: u64 = kani::any(); + let p = Pair::new(a, b); + assert!(p.sum() == a.wrapping_add(b)); + } +} diff --git a/tests/cargo-coverage/simple-lib/src/pair.rs b/tests/cargo-coverage/simple-lib/src/pair.rs new file mode 100644 index 000000000000..0201156c4225 --- /dev/null +++ b/tests/cargo-coverage/simple-lib/src/pair.rs @@ -0,0 +1,33 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +pub struct Pair(pub u64, pub u64); + +impl Pair { + pub fn new(a: u64, b: u64) -> Self { + Pair(a, b) + } + pub fn sum(&self) -> u64 { + self.0.wrapping_add(self.1) + } +} + +#[cfg(test)] +mod tests { + use super::*; + #[test] + fn one_plus_two() { + let p = Pair::new(1, 2); + assert_eq!(p.sum(), 3); + } +} + +#[cfg(kani)] +mod kani_tests { + use super::*; + + #[kani::proof] + fn test_one_plus_two() { + let p = Pair::new(1, 2); + assert!(p.sum() == 3); + } +} diff --git a/tests/cargo-coverage/simple-lib/test_one_plus_two.expected b/tests/cargo-coverage/simple-lib/test_one_plus_two.expected new file mode 100644 index 000000000000..6010f6fe7b3d --- /dev/null +++ b/tests/cargo-coverage/simple-lib/test_one_plus_two.expected @@ -0,0 +1,10 @@ +Source-based code coverage results: + +src/pair.rs (pair::Pair::new)\ + * 6:5 - 8:6 COVERED + +src/pair.rs (pair::Pair::sum)\ + * 9:5 - 11:6 COVERED + +src/pair.rs (pair::kani_tests::test_one_plus_two)\ + * 29:5 - 32:6 COVERED diff --git a/tests/cargo-coverage/simple-lib/test_sum.expected b/tests/cargo-coverage/simple-lib/test_sum.expected new file mode 100644 index 000000000000..ea1bd5ad3a62 --- /dev/null +++ b/tests/cargo-coverage/simple-lib/test_sum.expected @@ -0,0 +1,10 @@ +Source-based code coverage results: + +src/lib.rs (kani_tests::test_sum)\ + * 19:5 - 24:6 COVERED + +src/pair.rs (pair::Pair::new)\ + * 6:5 - 8:6 COVERED + +src/pair.rs (pair::Pair::sum)\ + * 9:5 - 11:6 COVERED diff --git a/tools/compiletest/src/common.rs b/tools/compiletest/src/common.rs index 99ec78bef693..d5c4ccf3c116 100644 --- a/tools/compiletest/src/common.rs +++ b/tools/compiletest/src/common.rs @@ -17,6 +17,7 @@ use test::ColorConfig; pub enum Mode { Kani, KaniFixme, + CargoCoverage, CargoKani, CargoKaniTest, // `cargo kani --tests`. This is temporary and should be removed when s2n-quic moves --tests to `Cargo.toml`. CoverageBased, @@ -34,6 +35,7 @@ impl FromStr for Mode { "cargo-kani" => Ok(CargoKani), "cargo-kani-test" => Ok(CargoKaniTest), "coverage-based" => Ok(CoverageBased), + "cargo-coverage" => Ok(CargoCoverage), "exec" => Ok(Exec), "expected" => Ok(Expected), "stub-tests" => Ok(Stub), @@ -47,6 +49,7 @@ impl fmt::Display for Mode { let s = match *self { Kani => "kani", KaniFixme => "kani-fixme", + CargoCoverage => "cargo-coverage", CargoKani => "cargo-kani", CargoKaniTest => "cargo-kani-test", CoverageBased => "coverage-based", diff --git a/tools/compiletest/src/main.rs b/tools/compiletest/src/main.rs index 94cbd561aa51..dd1284d7a3c9 100644 --- a/tools/compiletest/src/main.rs +++ b/tools/compiletest/src/main.rs @@ -349,7 +349,7 @@ fn collect_tests_from_dir( tests: &mut Vec, ) -> io::Result<()> { match config.mode { - Mode::CargoKani | Mode::CargoKaniTest => { + Mode::CargoCoverage | Mode::CargoKani | Mode::CargoKaniTest => { collect_expected_tests_from_dir(config, dir, relative_dir_path, inputs, tests) } Mode::Exec => collect_exec_tests_from_dir(config, dir, relative_dir_path, inputs, tests), @@ -378,7 +378,11 @@ fn collect_expected_tests_from_dir( // output directory corresponding to each to avoid race conditions during // the testing phase. We immediately return after adding the tests to avoid // treating `*.rs` files as tests. - assert!(config.mode == Mode::CargoKani || config.mode == Mode::CargoKaniTest); + assert!( + config.mode == Mode::CargoCoverage + || config.mode == Mode::CargoKani + || config.mode == Mode::CargoKaniTest + ); let has_cargo_toml = dir.join("Cargo.toml").exists(); for file in fs::read_dir(dir)? { diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index c8387c691296..c6575db17819 100644 --- a/tools/compiletest/src/runtest.rs +++ b/tools/compiletest/src/runtest.rs @@ -8,7 +8,7 @@ use crate::common::KaniFailStep; use crate::common::{output_base_dir, output_base_name}; use crate::common::{ - CargoKani, CargoKaniTest, CoverageBased, Exec, Expected, Kani, KaniFixme, Stub, + CargoCoverage, CargoKani, CargoKaniTest, CoverageBased, Exec, Expected, Kani, KaniFixme, Stub, }; use crate::common::{Config, TestPaths}; use crate::header::TestProps; @@ -74,6 +74,7 @@ impl<'test> TestCx<'test> { match self.config.mode { Kani => self.run_kani_test(), KaniFixme => self.run_kani_test(), + CargoCoverage => self.run_cargo_coverage_test(), CargoKani => self.run_cargo_kani_test(false), CargoKaniTest => self.run_cargo_kani_test(true), CoverageBased => self.run_expected_coverage_test(), @@ -313,7 +314,7 @@ impl<'test> TestCx<'test> { self.compose_and_run(kani) } - /// Run coverage based output for kani on a single file + /// Run Kani with coverage enabled on a single source file fn run_kani_with_coverage(&self) -> ProcRes { let mut kani = Command::new("kani"); if !self.props.compile_flags.is_empty() { @@ -329,6 +330,34 @@ impl<'test> TestCx<'test> { self.compose_and_run(kani) } + /// Run Kani with coverage enabled on a cargo package + fn run_cargo_coverage_test(&self) { + // We create our own command for the same reasons listed in `run_kani_test` method. + let mut cargo = Command::new("cargo"); + // We run `cargo` on the directory where we found the `*.expected` file + let parent_dir = self.testpaths.file.parent().unwrap(); + // The name of the function to test is the same as the stem of `*.expected` file + let function_name = self.testpaths.file.file_stem().unwrap().to_str().unwrap(); + cargo + .arg("kani") + .arg("--coverage") + .arg("-Zsource-coverage") + .arg("--target-dir") + .arg(self.output_base_dir().join("target")) + .current_dir(parent_dir); + + if "expected" != self.testpaths.file.file_name().unwrap() { + cargo.args(["--harness", function_name]); + } + cargo.args(&self.config.extra_args); + + let proc_res = self.compose_and_run(cargo); + self.verify_output(&proc_res, &self.testpaths.file); + + // TODO: We should probably be checking the exit status somehow + // See https://github.com/model-checking/kani/issues/1895 + } + /// Runs an executable file and: /// * Checks the expected output if an expected file is specified /// * Checks the exit code (assumed to be 0 by default)