Merge branch 'main' into toolchain

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

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<HarnessResult>,
  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)

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"
 )

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]

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));
+ }
+}

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);
+ }
+}

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

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

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`

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
+}

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)]\
+| ^^^^^^^^^^^^^^

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<T: Default>() {
+ foo();
+}

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]\

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

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",

tools/compiletest/src/main.rs

@@ -349,7 +349,7 @@ fn collect_tests_from_dir(
  tests: &mut Vec<test::TestDescAndFn>,
 ) -> 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)? {

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)