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

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