Autoharness: enable function-contracts and loop-contracts features by default

docs/src/reference/experimental/autoharness.md

@@ -29,14 +29,20 @@ Autoharness: Checking function foo against all possible inputs...
 <VERIFICATION RESULTS>
 ```
 
-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...
 <VERIFICATION RESULTS>
 ```
 
+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).

kani-driver/src/args/mod.rs

@@ -146,7 +146,7 @@ pub enum StandaloneSubcommand {
     VerifyStd(Box<std_args::VerifyStdArgs>),
     /// List contracts and harnesses.
     List(Box<list_args::StandaloneListArgs>),
-    /// 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<autoharness_args::StandaloneAutoharnessArgs>),
 }
 
@@ -177,7 +177,7 @@ pub enum CargoKaniSubcommand {
     /// List contracts and harnesses.
     List(Box<list_args::CargoListArgs>),
 
-    /// 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<autoharness_args::CargoAutoharnessArgs>),
 }
 

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.

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

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.

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

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

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