Autoharness: Harness Generation Improvements

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -42,8 +42,8 @@ use rustc_session::config::{CrateType, OutputFilenames, OutputType};
 use rustc_session::output::out_filename;
 use rustc_smir::rustc_internal;
 use rustc_target::spec::PanicStrategy;
+use stable_mir::CrateDef;
 use stable_mir::mir::mono::{Instance, MonoItem};
-use stable_mir::{CrateDef, DefId};
 use std::any::Any;
 use std::collections::BTreeMap;
 use std::fmt::Write;
@@ -212,6 +212,27 @@ impl GotocCodegenBackend {
 
         (gcx, items, contract_info)
     }
+
+    /// Given a contract harness, get the DefId of its target.
+    /// For manual harnesses, extract it from the #[proof_for_contract] attribute.
+    /// For automatic harnesses, extract the target from the harness's GenericArgs.
+    fn target_def_id_for_harness(
+        &self,
+        tcx: TyCtxt,
+        harness: &Instance,
+        is_automatic_harness: bool,
+    ) -> Option<InternalDefId> {
+        if is_automatic_harness {
+            let kind = harness.args().0[0].expect_ty().kind();
+            let (fn_to_verify_def, _) = kind.fn_def().unwrap();
+            let def_id = fn_to_verify_def.def_id();
+            let attrs = KaniAttributes::for_def_id(tcx, def_id);
+            if attrs.has_contract() { Some(rustc_internal::internal(tcx, def_id)) } else { None }
+        } else {
+            let harness_attrs = KaniAttributes::for_def_id(tcx, harness.def.def_id());
+            harness_attrs.interpret_for_contract_attribute().map(|(_, id, _)| id)
+        }
+    }
 }
 
 impl CodegenBackend for GotocCodegenBackend {
@@ -275,8 +296,9 @@ impl CodegenBackend for GotocCodegenBackend {
                         for harness in &unit.harnesses {
                             let transformer = BodyTransformation::new(&queries, tcx, &unit);
                             let model_path = units.harness_model_path(*harness).unwrap();
+                            let is_automatic_harness = units.is_automatic_harness(harness);
                             let contract_metadata =
-                                contract_metadata_for_harness(tcx, harness.def.def_id());
+                                self.target_def_id_for_harness(tcx, harness, is_automatic_harness);
                             let (gcx, items, contract_info) = self.codegen_items(
                                 tcx,
                                 &[MonoItem::Fn(*harness)],
@@ -453,11 +475,6 @@ impl ArchiveBuilderBuilder for ArArchiveBuilderBuilder {
     }
 }
 
-fn contract_metadata_for_harness(tcx: TyCtxt, def_id: DefId) -> Option<InternalDefId> {
-    let attrs = KaniAttributes::for_def_id(tcx, def_id);
-    attrs.interpret_for_contract_attribute().map(|(_, id, _)| id)
-}
-
 fn check_target(session: &Session) {
     // The requirement below is needed to build a valid CBMC machine model
     // in function `machine_model_from_session` from

kani-compiler/src/kani_middle/codegen_units.rs

@@ -97,7 +97,7 @@ impl CodegenUnits {
                         chosen: chosen.iter().map(|func| func.name()).collect::<BTreeSet<_>>(),
                         skipped,
                     })
-                    .expect("Initializing the autoharness metdata failed");
+                    .expect("Initializing the autoharness metadata failed");
 
                 let automatic_harnesses = get_all_automatic_harnesses(
                     tcx,
@@ -133,6 +133,10 @@ impl CodegenUnits {
         self.units.iter()
     }
 
+    pub fn is_automatic_harness(&self, harness: &Harness) -> bool {
+        self.harness_info.get(harness).is_some_and(|md| md.is_automatically_generated)
+    }
+
     /// We store which instance of modifies was generated.
     pub fn store_modifies(&mut self, harness_modifies: &[(Harness, AssignsContract)]) {
         for (harness, modifies) in harness_modifies {
@@ -340,7 +344,12 @@ fn get_all_automatic_harnesses(
                 &GenericArgs(vec![GenericArgKind::Type(fn_to_verify.ty())]),
             )
             .unwrap();
-            let metadata = gen_automatic_proof_metadata(tcx, &base_filename, &fn_to_verify);
+            let metadata = gen_automatic_proof_metadata(
+                tcx,
+                &base_filename,
+                &fn_to_verify,
+                harness.mangled_name(),
+            );
             (harness, metadata)
         })
         .collect::<HashMap<_, _>>()

kani-compiler/src/kani_middle/metadata.rs

@@ -112,12 +112,13 @@ pub fn gen_contracts_metadata(
 /// Generate metadata for automatically generated harnesses.
 /// For now, we just use the data from the function we are verifying; since we only generate one automatic harness per function,
 /// 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),
+/// TODO: 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.
 pub fn gen_automatic_proof_metadata(
     tcx: TyCtxt,
     base_name: &Path,
     fn_to_verify: &Instance,
+    harness_mangled_name: String,
 ) -> HarnessMetadata {
     let def = fn_to_verify.def;
     let pretty_name = fn_to_verify.name();
@@ -137,8 +138,10 @@ pub fn gen_automatic_proof_metadata(
     };
 
     HarnessMetadata {
+        // pretty_name is what gets displayed to the user, and that should be the name of the function being verified, hence using fn_to_verify name
         pretty_name,
-        mangled_name,
+        // We pass --function mangled_name to CBMC to select the entry point, which should be the mangled name of the automatic harness intrinsic
+        mangled_name: harness_mangled_name,
         crate_name: def.krate().name,
         original_file: loc.filename,
         original_start_line: loc.start_line,

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

@@ -7,21 +7,24 @@
 //! then transform its body to be a harness for that function.
 
 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};
+use crate::kani_middle::kani_functions::{KaniHook, KaniIntrinsic, KaniModel};
 use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction};
 use crate::kani_middle::transform::{TransformPass, TransformationType};
 use crate::kani_queries::QueryDb;
 use rustc_middle::ty::TyCtxt;
+use stable_mir::CrateDef;
 use stable_mir::mir::mono::Instance;
-use stable_mir::mir::{Body, Operand, Place, TerminatorKind};
-use stable_mir::ty::{FnDef, GenericArgKind, GenericArgs};
+use stable_mir::mir::{Body, Mutability, Operand, Place, TerminatorKind};
+use stable_mir::ty::{FnDef, GenericArgKind, GenericArgs, RigidTy, Ty};
 use tracing::debug;
 
 #[derive(Debug)]
 pub struct AutomaticHarnessPass {
     /// The FnDef of KaniModel::Any
     kani_any: FnDef,
+    init_contracts_hook: Instance,
     /// All of the automatic harness Instances that we generated in the CodegenUnits constructor
     automatic_harnesses: Vec<Instance>,
 }
@@ -37,6 +40,9 @@ impl AutomaticHarnessPass {
         let kani_fns = query_db.kani_functions();
         let harness_intrinsic = *kani_fns.get(&KaniIntrinsic::AutomaticHarness.into()).unwrap();
         let kani_any = *kani_fns.get(&KaniModel::Any.into()).unwrap();
+        let init_contracts_hook = *kani_fns.get(&KaniHook::InitContracts.into()).unwrap();
+        let init_contracts_hook =
+            Instance::resolve(init_contracts_hook, &GenericArgs(vec![])).unwrap();
         let automatic_harnesses = unit
             .harnesses
             .iter()
@@ -46,7 +52,7 @@ impl AutomaticHarnessPass {
                 def == harness_intrinsic
             })
             .collect::<Vec<_>>();
-        Self { kani_any, automatic_harnesses }
+        Self { kani_any, init_contracts_hook, automatic_harnesses }
     }
 }
 
@@ -65,7 +71,7 @@ impl TransformPass for AutomaticHarnessPass {
         matches!(query_db.args().reachability_analysis, ReachabilityType::AllFns)
     }
 
-    fn transform(&mut self, _tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) {
+    fn transform(&mut self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) {
         debug!(function=?instance.name(), "AutomaticHarnessPass::transform");
 
         if !self.automatic_harnesses.contains(&instance) {
@@ -83,6 +89,23 @@ impl TransformPass for AutomaticHarnessPass {
         harness_body.clear_body(TerminatorKind::Return);
         let mut source = SourceInstruction::Terminator { bb: 0 };
 
+        // Contract harnesses need a free(NULL) statement, c.f. kani_core::init_contracts().
+        let attrs = KaniAttributes::for_def_id(tcx, def.def_id());
+        if attrs.has_contract() {
+            let ret_local = harness_body.new_local(
+                Ty::from_rigid_kind(RigidTy::Tuple(vec![])),
+                source.span(harness_body.blocks()),
+                Mutability::Not,
+            );
+            harness_body.insert_call(
+                &self.init_contracts_hook,
+                &mut source,
+                InsertPosition::Before,
+                vec![],
+                Place::from(ret_local),
+            );
+        }
+
         let mut arg_locals = vec![];
 
         // For each argument of `fn_to_verify`, create a nondeterministic value of its type

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

@@ -350,12 +350,11 @@ impl FunctionWithContractPass {
                     && !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();
+                    let (fn_to_verify_def, _) = kind.fn_def().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())),
+                        Some(rustc_internal::internal(tcx, fn_to_verify_def.def_id())),
                         HashSet::default(),
                     )
                 } else {

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

@@ -1,17 +1,21 @@
-Kani generated automatic harnesses for 5 function(s):
-+--------------------------------+
-| Selected Function              |
-+================================+
-| should_fail::max               |
-|--------------------------------|
-| should_pass::div               |
-|--------------------------------|
-| should_pass::has_loop_contract |
-|--------------------------------|
-| should_pass::has_recursion_gcd |
-|--------------------------------|
-| should_pass::unchecked_mul     |
-+--------------------------------+
+Kani generated automatic harnesses for 7 function(s):
++---------------------------------------------+
+| Selected Function                           |
++=============================================+
+| should_fail::max                            |
+|---------------------------------------------|
+| should_pass::alignment::Alignment           |
+|---------------------------------------------|
+| should_pass::alignment::Alignment::as_usize |
+|---------------------------------------------|
+| should_pass::div                            |
+|---------------------------------------------|
+| should_pass::has_loop_contract              |
+|---------------------------------------------|
+| should_pass::has_recursion_gcd              |
+|---------------------------------------------|
+| should_pass::unchecked_mul                  |
++---------------------------------------------+
 
 Skipped Functions: None. Kani generated automatic harnesses for all functions in the available crate(s).
 
@@ -37,23 +41,37 @@ arithmetic_overflow\
 	 - Status: SUCCESS\
 	 - Description: "attempt to compute `unchecked_mul` which would overflow"
 
+Autoharness: Checking function should_pass::alignment::Alignment::as_usize's contract against all possible inputs...
+
+should_pass::alignment::Alignment::as_usize\
+	 - Status: SUCCESS\
+	 - Description: "Rust intrinsic assumption failed"
+
+should_pass::alignment::Alignment::as_usize\
+	 - Status: SUCCESS\
+	 - Description: "|result| result.is_power_of_two()"
+
 Manual Harness Summary:
 No proof harnesses (functions with #[kani::proof]) were found to verify.
 
 Autoharness Summary:
-+--------------------------------+-----------------------------+---------------------+
-| Selected Function              | Kind of Automatic Harness   | Verification Result |
-+====================================================================================+
-| should_pass::div               | #[kani::proof_for_contract] | Success             |
-|--------------------------------+-----------------------------+---------------------|
-| should_pass::has_loop_contract | #[kani::proof]              | Success             |
-|--------------------------------+-----------------------------+---------------------|
-| should_pass::has_recursion_gcd | #[kani::proof_for_contract] | Success             |
-|--------------------------------+-----------------------------+---------------------|
-| should_pass::unchecked_mul     | #[kani::proof_for_contract] | Success             |
-|--------------------------------+-----------------------------+---------------------|
-| should_fail::max               | #[kani::proof_for_contract] | Failure             |
-+--------------------------------+-----------------------------+---------------------+
++---------------------------------------------+-----------------------------+---------------------+
+| Selected Function                           | Kind of Automatic Harness   | Verification Result |
++=================================================================================================+
+| should_pass::alignment::Alignment           | #[kani::proof]              | Success             |
+|---------------------------------------------+-----------------------------+---------------------|
+| should_pass::alignment::Alignment::as_usize | #[kani::proof_for_contract] | Success             |
+|---------------------------------------------+-----------------------------+---------------------|
+| should_pass::div                            | #[kani::proof_for_contract] | Success             |
+|---------------------------------------------+-----------------------------+---------------------|
+| should_pass::has_loop_contract              | #[kani::proof]              | Success             |
+|---------------------------------------------+-----------------------------+---------------------|
+| should_pass::has_recursion_gcd              | #[kani::proof_for_contract] | Success             |
+|---------------------------------------------+-----------------------------+---------------------|
+| should_pass::unchecked_mul                  | #[kani::proof_for_contract] | Success             |
+|---------------------------------------------+-----------------------------+---------------------|
+| should_fail::max                            | #[kani::proof_for_contract] | Failure             |
++---------------------------------------------+-----------------------------+---------------------+
 Note that `kani autoharness` sets default --harness-timeout of 60s and --default-unwind of 20.
 If verification failed because of timing out or too low of an unwinding bound, try passing larger values for these arguments (or, if possible, writing a loop contract).
-Complete - 4 successfully verified functions, 1 failures, 5 total.
+Complete - 6 successfully verified functions, 1 failures, 7 total.

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

@@ -46,6 +46,90 @@ mod should_pass {
     unsafe fn unchecked_mul(left: u8, rhs: u8) -> u8 {
         unsafe { left.unchecked_mul(rhs) }
     }
+
+    // Check that we can create automatic harnesses for more complex situtations, i.e.,
+    // functions with contracts that reference nested data structures that derive Arbitrary.
+    mod alignment {
+        // FIXME: Note that since this is a tuple struct, we generate an extra harness for the Alignment constructor,
+        // c.f. https://github.com/model-checking/kani/issues/3832#issuecomment-2730580836
+        #[derive(kani::Arbitrary)]
+        pub struct Alignment(AlignmentEnum);
+
+        #[derive(kani::Arbitrary)]
+        enum AlignmentEnum {
+            _Align1Shl0 = 1 << 0,
+            _Align1Shl1 = 1 << 1,
+            _Align1Shl2 = 1 << 2,
+            _Align1Shl3 = 1 << 3,
+            _Align1Shl4 = 1 << 4,
+            _Align1Shl5 = 1 << 5,
+            _Align1Shl6 = 1 << 6,
+            _Align1Shl7 = 1 << 7,
+            _Align1Shl8 = 1 << 8,
+            _Align1Shl9 = 1 << 9,
+            _Align1Shl10 = 1 << 10,
+            _Align1Shl11 = 1 << 11,
+            _Align1Shl12 = 1 << 12,
+            _Align1Shl13 = 1 << 13,
+            _Align1Shl14 = 1 << 14,
+            _Align1Shl15 = 1 << 15,
+            _Align1Shl16 = 1 << 16,
+            _Align1Shl17 = 1 << 17,
+            _Align1Shl18 = 1 << 18,
+            _Align1Shl19 = 1 << 19,
+            _Align1Shl20 = 1 << 20,
+            _Align1Shl21 = 1 << 21,
+            _Align1Shl22 = 1 << 22,
+            _Align1Shl23 = 1 << 23,
+            _Align1Shl24 = 1 << 24,
+            _Align1Shl25 = 1 << 25,
+            _Align1Shl26 = 1 << 26,
+            _Align1Shl27 = 1 << 27,
+            _Align1Shl28 = 1 << 28,
+            _Align1Shl29 = 1 << 29,
+            _Align1Shl30 = 1 << 30,
+            _Align1Shl31 = 1 << 31,
+            _Align1Shl32 = 1 << 32,
+            _Align1Shl33 = 1 << 33,
+            _Align1Shl34 = 1 << 34,
+            _Align1Shl35 = 1 << 35,
+            _Align1Shl36 = 1 << 36,
+            _Align1Shl37 = 1 << 37,
+            _Align1Shl38 = 1 << 38,
+            _Align1Shl39 = 1 << 39,
+            _Align1Shl40 = 1 << 40,
+            _Align1Shl41 = 1 << 41,
+            _Align1Shl42 = 1 << 42,
+            _Align1Shl43 = 1 << 43,
+            _Align1Shl44 = 1 << 44,
+            _Align1Shl45 = 1 << 45,
+            _Align1Shl46 = 1 << 46,
+            _Align1Shl47 = 1 << 47,
+            _Align1Shl48 = 1 << 48,
+            _Align1Shl49 = 1 << 49,
+            _Align1Shl50 = 1 << 50,
+            _Align1Shl51 = 1 << 51,
+            _Align1Shl52 = 1 << 52,
+            _Align1Shl53 = 1 << 53,
+            _Align1Shl54 = 1 << 54,
+            _Align1Shl55 = 1 << 55,
+            _Align1Shl56 = 1 << 56,
+            _Align1Shl57 = 1 << 57,
+            _Align1Shl58 = 1 << 58,
+            _Align1Shl59 = 1 << 59,
+            _Align1Shl60 = 1 << 60,
+            _Align1Shl61 = 1 << 61,
+            _Align1Shl62 = 1 << 62,
+            _Align1Shl63 = 1 << 63,
+        }
+
+        impl Alignment {
+            #[kani::ensures(|result| result.is_power_of_two())]
+            pub fn as_usize(self) -> usize {
+                self.0 as usize
+            }
+        }
+    }
 }
 
 mod should_fail {