From eb3484465a6d93d69e4d87584323c0095db209d4 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Fri, 11 Apr 2025 22:27:33 -0400 Subject: [PATCH 1/2] enable -Zfunction-contracts and -Zloop-contracts when -Zautoharness is supplied --- kani-driver/src/args/mod.rs | 4 ++-- kani-driver/src/autoharness/mod.rs | 3 +++ kani_metadata/src/unstable.rs | 9 +++++++++ .../cargo_autoharness_contracts/contracts.sh | 2 +- tests/script-based-pre/cargo_autoharness_list/list.sh | 2 +- .../termination_timeout.sh | 2 +- .../termination_unwind.sh | 2 +- 7 files changed, 18 insertions(+), 6 deletions(-) diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 76fbc626d113..be198df73c25 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -146,7 +146,7 @@ pub enum StandaloneSubcommand { VerifyStd(Box), /// List contracts and harnesses. List(Box), - /// Scan the input file for functions eligible for automatic (i.e., harness-free) verification and verify them. + /// Create and run harnesses automatically for eligible functions. Implies -Z function-contracts and -Z loop-contracts. Autoharness(Box), } @@ -177,7 +177,7 @@ pub enum CargoKaniSubcommand { /// List contracts and harnesses. List(Box), - /// Scan the crate for functions eligible for automatic (i.e., harness-free) verification and verify them. + /// Create and run harnesses automatically for eligible functions. Implies -Z function-contracts and -Z loop-contracts. Autoharness(Box), } diff --git a/kani-driver/src/autoharness/mod.rs b/kani-driver/src/autoharness/mod.rs index 498a8d3e94fe..15ada39332d3 100644 --- a/kani-driver/src/autoharness/mod.rs +++ b/kani-driver/src/autoharness/mod.rs @@ -7,6 +7,7 @@ use crate::args::Timeout; use crate::args::autoharness_args::{ CargoAutoharnessArgs, CommonAutoharnessArgs, StandaloneAutoharnessArgs, }; +use crate::args::common::UnstableFeature; use crate::call_cbmc::VerificationStatus; use crate::call_single_file::to_rustc_arg; use crate::harness_runner::HarnessResult; @@ -151,6 +152,8 @@ impl KaniSession { /// Enable autoharness mode. pub fn enable_autoharness(&mut self) { self.auto_harness = true; + self.args.common_args.unstable_features.enable_feature(UnstableFeature::FunctionContracts); + self.args.common_args.unstable_features.enable_feature(UnstableFeature::LoopContracts); } /// Add the compiler arguments specific to the `autoharness` subcommand. diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs index a901f11b357d..f72c53b91e57 100644 --- a/kani_metadata/src/unstable.rs +++ b/kani_metadata/src/unstable.rs @@ -142,4 +142,13 @@ impl EnabledUnstableFeatures { pub fn contains(&self, feature: UnstableFeature) -> bool { self.enabled_unstable_features.contains(&feature) } + + /// Enable an additional unstable feature. + /// Note that this enables an unstable feature that the user did not pass on the command line, so this function should be called with caution. + /// At time of writing, the only use is to enable -Z function-contracts and -Z loop-contracts when the autoharness subcommand is running. + pub fn enable_feature(&mut self, feature: UnstableFeature) { + if !self.contains(feature) { + self.enabled_unstable_features.push(feature); + } + } } diff --git a/tests/script-based-pre/cargo_autoharness_contracts/contracts.sh b/tests/script-based-pre/cargo_autoharness_contracts/contracts.sh index d4c93fcd828d..34e177be9134 100755 --- a/tests/script-based-pre/cargo_autoharness_contracts/contracts.sh +++ b/tests/script-based-pre/cargo_autoharness_contracts/contracts.sh @@ -2,7 +2,7 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -cargo kani autoharness -Z autoharness -Z function-contracts -Z loop-contracts +cargo kani autoharness -Z autoharness # We expect verification to fail, so the above command will produce an exit status of 1 # However, we don't want the test to fail because of that exit status; we only want it to fail if the expected file doesn't match # So, exit with a status code of 0 explicitly. diff --git a/tests/script-based-pre/cargo_autoharness_list/list.sh b/tests/script-based-pre/cargo_autoharness_list/list.sh index 7deb9a0667cc..bf02eeb0276b 100755 --- a/tests/script-based-pre/cargo_autoharness_list/list.sh +++ b/tests/script-based-pre/cargo_autoharness_list/list.sh @@ -2,4 +2,4 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -cargo kani autoharness -Z autoharness --list -Z list -Z function-contracts +cargo kani autoharness -Z autoharness --list -Z list diff --git a/tests/script-based-pre/cargo_autoharness_termination_timeout/termination_timeout.sh b/tests/script-based-pre/cargo_autoharness_termination_timeout/termination_timeout.sh index 65f949b65ad3..db4a99f8be09 100755 --- a/tests/script-based-pre/cargo_autoharness_termination_timeout/termination_timeout.sh +++ b/tests/script-based-pre/cargo_autoharness_termination_timeout/termination_timeout.sh @@ -2,4 +2,4 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -cargo kani autoharness -Z autoharness -Z function-contracts +cargo kani autoharness -Z autoharness diff --git a/tests/script-based-pre/cargo_autoharness_termination_unwind/termination_unwind.sh b/tests/script-based-pre/cargo_autoharness_termination_unwind/termination_unwind.sh index 78df727def41..b197c0b1e077 100755 --- a/tests/script-based-pre/cargo_autoharness_termination_unwind/termination_unwind.sh +++ b/tests/script-based-pre/cargo_autoharness_termination_unwind/termination_unwind.sh @@ -4,4 +4,4 @@ # Set the timeout to 5m to ensure that the gcd_recursion test gets killed because of the unwind bound # and not because CBMC times out. -cargo kani autoharness -Z autoharness -Z function-contracts --harness-timeout 5m -Z unstable-options +cargo kani autoharness -Z autoharness --harness-timeout 5m -Z unstable-options From 5befe360554d77cd1c3bc2f70d91bdc2927a2d3b Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 14 Apr 2025 17:38:06 -0400 Subject: [PATCH 2/2] update book --- docs/src/reference/experimental/autoharness.md | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/docs/src/reference/experimental/autoharness.md b/docs/src/reference/experimental/autoharness.md index 67f46a9abf47..34d69da13738 100644 --- a/docs/src/reference/experimental/autoharness.md +++ b/docs/src/reference/experimental/autoharness.md @@ -29,14 +29,20 @@ Autoharness: Checking function foo against all possible inputs... ``` -However, if Kani detects that `foo` has a [contract](./contracts.md), it will instead generate a `#[kani::proof_for_contract]` harness and verify the contract: +However, if Kani detects that `foo` has a [function contract](./contracts.md), it will instead generate a `#[kani::proof_for_contract]` harness and verify the contract: ``` Autoharness: Checking function foo's contract against all possible inputs... ``` +Similarly, Kani will detect the presence of [loop contracts](./loop-contracts.md) and verify them. + +Thus, `-Z autoharness` implies `-Z function-contracts` and `-Z loop-contracts`, i.e., opting into the experimental +autoharness feature means that you are also opting into the function contracts and loop contracts features. + Kani generates and runs these harnesses internally—the user only sees the verification results. +### Options The `autoharness` subcommand has options `--include-function` and `--exclude-function` to include and exclude particular functions. These flags look for partial matches against the fully qualified name of a function. @@ -112,8 +118,3 @@ Failed Checks: x and y are equal VERIFICATION:- FAILED ``` - -### Loop Contracts -If a function contains a loop with a loop contract, Kani will detect the presence of a loop contract and verify that contract. -If, however, the loop does not have a contract, then there is currently no way to specify an unwinding bound for the function, meaning that Kani may hang as it tries to unwind the loop. -We recommend using the `--exclude-function` option to exclude any functions that have this issue (or `--harness-timeout` to bail after attempting verification for some amount of time). \ No newline at end of file