contract harnesses support

kani-compiler/src/kani_middle/codegen_units.rs

@@ -8,7 +8,7 @@
 //! according to their stub configuration.
 
 use crate::args::ReachabilityType;
-use crate::kani_middle::attributes::is_proof_harness;
+use crate::kani_middle::attributes::{KaniAttributes, is_proof_harness};
 use crate::kani_middle::kani_functions::{KaniIntrinsic, KaniModel};
 use crate::kani_middle::metadata::{
     gen_automatic_proof_metadata, gen_contracts_metadata, gen_proof_metadata,
@@ -73,22 +73,35 @@ impl CodegenUnits {
             }
             ReachabilityType::Automatic => {
                 let mut all_harnesses = get_all_manual_harnesses(tcx, base_filename);
+                let mut units = group_by_stubs(tcx, &all_harnesses);
+                validate_units(tcx, &units);
+
                 let kani_fns = queries.kani_functions();
-                let any_inst = kani_fns.get(&KaniModel::Any.into()).unwrap();
-                let verifiable_fns = filter_crate_items(tcx, |_, instance: Instance| -> bool {
-                    is_eligible_for_automatic_harness(tcx, instance, *any_inst)
-                });
                 let kani_harness_intrinsic =
                     kani_fns.get(&KaniIntrinsic::AutomaticHarness.into()).unwrap();
+                let kani_any_inst = kani_fns.get(&KaniModel::Any.into()).unwrap();
+                let verifiable_fns = filter_crate_items(tcx, |_, instance: Instance| -> bool {
+                    is_eligible_for_automatic_harness(tcx, instance, *kani_any_inst)
+                });
                 let automatic_harnesses = get_all_automatic_harnesses(
                     tcx,
                     verifiable_fns,
                     *kani_harness_intrinsic,
                     base_filename,
                 );
+                // We generate one contract harness per function under contract, so each harness is in its own unit,
+                // and these harnesses have no stubs.
+                units.extend(
+                    automatic_harnesses
+                        .iter()
+                        .map(|(harness, _)| CodegenUnit {
+                            harnesses: vec![*harness],
+                            stubs: HashMap::default(),
+                        })
+                        .collect::<Vec<_>>(),
+                );
                 all_harnesses.extend(automatic_harnesses);
-                let units = group_by_stubs(tcx, &all_harnesses);
-                validate_units(tcx, &units);
+                // No need to validate the units again because validation only checks stubs, and we haven't added any stubs.
                 debug!(?units, "CodegenUnits::new");
                 CodegenUnits { units, harness_info: all_harnesses, crate_info }
             }
@@ -113,7 +126,15 @@ impl CodegenUnits {
     /// We flag that the harness contains usage of loop contracts.
     pub fn store_loop_contracts(&mut self, harnesses: &[Harness]) {
         for harness in harnesses {
-            self.harness_info.get_mut(harness).unwrap().has_loop_contracts = true;
+            let metadata = self.harness_info.get_mut(harness).unwrap();
+            metadata.has_loop_contracts = true;
+            // If we're generating this harness automatically and we encounter a loop contract,
+            // ensure that the HarnessKind is updated to be a contract harness
+            // targeting the function to verify.
+            if metadata.is_automatically_generated {
+                metadata.attributes.kind =
+                    HarnessKind::ProofForContract { target_fn: metadata.pretty_name.clone() }
+            }
         }
     }
 
@@ -315,16 +336,11 @@ fn get_all_automatic_harnesses(
 }
 
 /// Determine whether `instance` is eligible for automatic verification.
-/// `instance` is eligible iff:
-///   1. It is not a harness,
-///   2. It has a non-empty body,
-///   3. It is not an associated item of a Kani trait implementation (e.g., a kani::any implementation)
-///   4. All of its arguments implement Arbitrary
 fn is_eligible_for_automatic_harness(tcx: TyCtxt, instance: Instance, any_inst: FnDef) -> bool {
+    // `instance` is ineligble if it is a harness or has an nonexistent/empty body
     if is_proof_harness(tcx, instance) || !instance.has_body() {
         return false;
     }
-    // Don't generate a harness for functions with empty bodies.
     let body = instance.body().unwrap();
     if body.blocks.is_empty()
         || (body.blocks[0].statements.is_empty()
@@ -333,14 +349,20 @@ fn is_eligible_for_automatic_harness(tcx: TyCtxt, instance: Instance, any_inst:
         return false;
     }
 
-    // Don't generate harnesses for associated items of Kani trait implementations.
-    // FIXME -- find a less hardcoded way of doing this (perhaps upstream PR to StableMIR).
-    if instance.name().contains("kani::Arbitrary") || instance.name().contains("kani::Invariant") {
+    // `instance` is ineligble if it is an associated item of a Kani trait implementation,
+    // or part of Kani contract instrumentation.
+    // FIXME -- find a less hardcoded way of checking the former condition (perhaps upstream PR to StableMIR).
+    if instance.name().contains("kani::Arbitrary")
+        || instance.name().contains("kani::Invariant")
+        || KaniAttributes::for_instance(tcx, instance)
+            .fn_marker()
+            .is_some_and(|m| m.as_str() == "kani_contract_mode")
+    {
         return false;
     }
 
-    // Each non-generic argument of instance must implement Arbitrary.
-    // FIXME -- this will only find Arbitrary implementations for types whose Arbitrary
+    // Each non-generic argument of `instance`` must implement Arbitrary.
+    // FIXME -- this is sound but not complete, since it will only work for types whose Arbitrary
     // implementations have an inner call to kani::any, which not all implementations (e.g. PhantomPinned) do.
     body.arg_locals().iter().all(|arg| {
         let kani_any_body =

kani-compiler/src/kani_middle/metadata.rs

@@ -90,9 +90,8 @@ pub fn gen_contracts_metadata(tcx: TyCtxt) -> Vec<ContractedFunction> {
 /// the metdata from that function uniquely identifies the harness.
 /// In future iterations of this feature, we will likely have multiple harnesses for a single function (e.g., for generic functions),
 /// in which case HarnessMetadata will need to change further to differentiate between those harnesses.
-/// TODO Instead of just generating HarnessKind::Proof, generate HarnessKind::ProofForContract if fn_to_verify has a contract.
 pub fn gen_automatic_proof_metadata(
-    _tcx: TyCtxt,
+    tcx: TyCtxt,
     base_name: &Path,
     fn_to_verify: &Instance,
 ) -> HarnessMetadata {
@@ -105,14 +104,21 @@ pub fn gen_automatic_proof_metadata(
     let file_stem = format!("{}_{mangled_name}", base_name.file_stem().unwrap().to_str().unwrap());
     let model_file = base_name.with_file_name(file_stem).with_extension(ArtifactType::SymTabGoto);
 
+    let kani_attributes = KaniAttributes::for_instance(tcx, *fn_to_verify);
+    let harness_kind = if kani_attributes.has_contract() {
+        HarnessKind::ProofForContract { target_fn: pretty_name.clone() }
+    } else {
+        HarnessKind::Proof
+    };
+
     HarnessMetadata {
         pretty_name,
         mangled_name,
         crate_name: def.krate().name,
         original_file: loc.filename,
         original_start_line: loc.start_line,
         original_end_line: loc.end_line,
-        attributes: HarnessAttributes::new(HarnessKind::Proof),
+        attributes: HarnessAttributes::new(harness_kind),
         // TODO: This no longer needs to be an Option.
         goto_file: Some(model_file),
         contract: Default::default(),

kani-compiler/src/kani_middle/transform/contracts.rs

@@ -1,6 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! This module contains code related to the MIR-to-MIR pass to enable contracts.
+use crate::args::ReachabilityType;
 use crate::kani_middle::attributes::KaniAttributes;
 use crate::kani_middle::codegen_units::CodegenUnit;
 use crate::kani_middle::kani_functions::{KaniIntrinsic, KaniModel};
@@ -341,13 +342,34 @@ impl FunctionWithContractPass {
     /// verifying.
     pub fn new(tcx: TyCtxt, queries: &QueryDb, unit: &CodegenUnit) -> FunctionWithContractPass {
         if let Some(harness) = unit.harnesses.first() {
-            let attrs = KaniAttributes::for_instance(tcx, *harness);
-            let check_fn = attrs.interpret_for_contract_attribute().map(|(_, def_id, _)| def_id);
-            let replace_fns: HashSet<_> = attrs
-                .interpret_stub_verified_attribute()
-                .iter()
-                .map(|(_, def_id, _)| *def_id)
-                .collect();
+            let (check_fn, replace_fns) = {
+                let harness_generic_args = harness.args().0;
+                // Manual harnesses have no arguments, so if there are generic arguments,
+                // we know this is an automatic harness
+                if matches!(queries.args().reachability_analysis, ReachabilityType::Automatic)
+                    && !harness_generic_args.is_empty()
+                {
+                    let kind = harness.args().0[0].expect_ty().kind();
+                    let (def, args) = kind.fn_def().unwrap();
+                    let fn_to_verify = Instance::resolve(def, &args).unwrap();
+                    // For automatic harnesses, the target is the function to verify,
+                    // and stubs are empty.
+                    (
+                        Some(rustc_internal::internal(tcx, fn_to_verify.def.def_id())),
+                        HashSet::default(),
+                    )
+                } else {
+                    let attrs = KaniAttributes::for_instance(tcx, *harness);
+                    let check_fn =
+                        attrs.interpret_for_contract_attribute().map(|(_, def_id, _)| def_id);
+                    let replace_fns: HashSet<_> = attrs
+                        .interpret_stub_verified_attribute()
+                        .iter()
+                        .map(|(_, def_id, _)| *def_id)
+                        .collect();
+                    (check_fn, replace_fns)
+                }
+            };
             let run_contract_fn =
                 queries.kani_functions().get(&KaniModel::RunContract.into()).copied();
             assert!(run_contract_fn.is_some(), "Failed to find Kani run contract function");

tests/script-based-pre/cargo_autoverify_contracts_fixme/Cargo.toml → tests/script-based-pre/cargo_autoverify_contracts/Cargo.toml

@@ -1,5 +1,5 @@
 [package]
-name = "cargo_autoverify_contracts_fixme"
+name = "cargo_autoverify_contracts"
 version = "0.1.0"
 edition = "2024"
 

tests/script-based-pre/cargo_autoverify_contracts/contracts.expected

@@ -0,0 +1,19 @@
+Checking function should_fail::max against all possible inputs...
+assertion\
+	 - Status: FAILURE\
+	 - Description: "|result : &u32| *result == x"
+
+Checking function should_pass::has_loop_contract against all possible inputs...
+should_pass::has_loop_contract.assertion\
+	 - Status: SUCCESS\
+	 - Description: "assertion failed: x == 2"
+
+Checking function should_pass::has_recursion_gcd against all possible inputs...
+assertion\
+	 - Status: SUCCESS\
+	 - Description: "|result : &u8| *result != 0 && x % *result == 0 && y % *result == 0"
+
+Checking function should_pass::div against all possible inputs...
+
+Verification failed for - should_fail::max
+Complete - 3 successfully verified harnesses, 1 failures, 4 total.

tests/script-based-pre/cargo_autoverify_contracts/contracts.sh

@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+cargo kani autoverify -Z unstable-options -Z function-contracts -Z loop-contracts
+# 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.
+exit 0;

tests/script-based-pre/cargo_autoverify_contracts/src/lib.rs

@@ -0,0 +1,50 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Test that the autoverify subcommand correctly verifies contracts,
+// i.e., that it detects the presence of a contract and generates a contract
+// harness instead of a standard harness.
+
+#![feature(stmt_expr_attributes)]
+#![feature(proc_macro_hygiene)]
+
+mod should_pass {
+    #[kani::requires(divisor != 0)]
+    fn div(dividend: u32, divisor: u32) -> u32 {
+        dividend / divisor
+    }
+
+    #[kani::requires(x != 0 && y != 0)]
+    #[kani::ensures(|result : &u8| *result != 0 && x % *result == 0 && y % *result == 0)]
+    #[kani::recursion]
+    fn has_recursion_gcd(x: u8, y: u8) -> u8 {
+        let mut max = x;
+        let mut min = y;
+        if min > max {
+            let val = max;
+            max = min;
+            min = val;
+        }
+
+        let res = max % min;
+        if res == 0 { min } else { has_recursion_gcd(min, res) }
+    }
+
+    fn has_loop_contract() {
+        let mut x: u8 = kani::any_where(|i| *i >= 2);
+
+        #[kani::loop_invariant(x >= 2)]
+        while x > 2 {
+            x = x - 1;
+        }
+
+        assert!(x == 2);
+    }
+}
+
+mod should_fail {
+    #[kani::ensures(|result : &u32| *result == x)]
+    fn max(x: u32, y: u32) -> u32 {
+        if x > y { x } else { y }
+    }
+}

tests/script-based-pre/cargo_autoverify_loops_fixme/src/lib.rs

@@ -1,28 +1,39 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zautomatic-harnesses
-
-#![feature(stmt_expr_attributes)]
-#![feature(proc_macro_hygiene)]
 
 // Test that automatic harnesses terminate on functions with loops.
 
 // Since foo()'s arguments implement Arbitrary, we will attempt to verify it,
 // and enter an infinite loop.
-// Instead, we should just skip this function, perhaps printing a message to the user that we skipped it.
+// Unclear what the best solution to this problem is; perhaps this is just a known limitation
+// and the user needs to specify some command line flag to skip this function,
+// or we can conservatively skip functions with loops that don't have loop contracts.
 fn infinite_loop() {
     loop {}
 }
 
-// Shouldn't skip this function -- it has a loop, but since it also has a loop contract,
-// we can generate a contract harness for it and be assured that the proof will terminate.
-fn has_loop_contract() {
-    let mut x: u8 = kani::any_where(|i| *i >= 2);
+/// Euclid's algorithm for calculating the GCD of two numbers
+#[kani::requires(x != 0 && y != 0)]
+#[kani::ensures(|result : &u8| *result != 0 && x % *result == 0 && y % *result == 0)]
+fn gcd(mut x: u8, mut y: u8) -> u8 {
+    (x, y) = (if x > y { x } else { y }, if x > y { y } else { x });
+    loop {
+        let res = x % y;
+        if res == 0 {
+            return y;
+        }
 
-    #[kani::loop_invariant(x >= 2)]
-    while x > 2 {
-        x = x - 1;
+        x = y;
+        y = res;
     }
+}
 
-    assert!(x == 2);
+// Since we can specify an unwinding bound in a manual harness,
+// the proof will terminate.
+// Automatic harnesses, however, do not support unwinding bounds,
+// so the proof does not terminate.
+#[kani::proof_for_contract(gcd)]
+#[kani::unwind(12)]
+fn gcd_harness() {
+    gcd(kani::any(), kani::any());
 }