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

[carolynzech]

Problem

Right now, -Z autoharness implies -Z function-contracts, since it will generate contract harnesses for contracts it finds without you explicitly opting in. It does not, however, imply -Z loop-contracts, so if you don't provide that flag you can unwind until you hit the default loop bound, and you don't prove the contract. This behavior is inconsistent and confusing.

Solution

Autoharness is already unstable, so it feels redundant to make people opt in to instability on top of instability. Instead, just make -Z autoharness imply -Z function-contracts and -Z loop-contracts.

Alternative

Alternatively, we could make -Z autoharness imply neither of these options, and skip functions with contracts altogether / generate standard harnesses for them. But I fear even with warnings, users wouldn't notice we did this, and erroneously conclude that we've proven their contracts. If they're already opting into the unstable autoharness feature, I think we can safely assume they are okay with instability and turn -Z function-contracts and -Z loop-contracts on by default.

Towards #3832

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[tautschnig]

1. Is this documented in all the necessary places?
2. I don't really know of a reason why someone would not want to enable these features, but if such a use case ever comes along: how would we do it?

[carolynzech]

Is this documented in all the necessary places?

I forgot to update the book. That's now done. I also removed the limitation about loop contracts, which I fixed in a previous PR.

I don't really know of a reason why someone would not want to enable these features, but if such a use case ever comes along: how would we do it?

Assuming that we ever wanted to support the "Alternative" behavior from the PR description, we would:

1. Revert this PR (which would make -Z loop-contracts required to pass explicitly again)
2. Change the compiler s.t. -Z function-contracts is explicitly required by adding logic like this (psuedocode):

// `fns_to_verify` contains all the functions eligible for automatic harnesses
for fn_to_verify in fns_to_verify {
  if has_function_contract(fn_to_verify) {
    if is_enabled(UnstableFeature::FunctionContracts) {
      generate_automatic_contract_harness(fn_to_verify);
      continue;
    } else {
      tcx.dcx.warn(format!("
        Found {fn_to_verify} which has a function contract, but -Z function-contracts wasn't supplied;
        generating a standard harness instead.
      "));
    }
    generate_standard_harness(fn_to_verify);
}

i.e., generate a contract harness iff the user opted into the feature, otherwise, generate a standard harness. You could also change this pseudocode to skip over functions with contracts entirely if that was the desired alternate behavior.

[carolynzech]

More specifically, the constructor of FunctionWithContractPass:

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

Lines 345 to 360 in 946263e

	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::AllFns)
	&& !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(),
	)

instantiates the pass for a given harness so that check_fn equals the target of the automatic harness.

Then, we call FunctionWithContractPass:transform on every function in our reachability analysis, which ends up here:

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

Lines 473 to 480 in 946263e

	kani_attributes.has_contract().then(|| {
	let fn_def_id = rustc_internal::internal(tcx, fn_def.def_id());
	if self.check_fn == Some(fn_def_id) {
	if kani_attributes.has_recursion() {
	ContractMode::RecursiveCheck
	} else {
	ContractMode::SimpleCheck
	}

meaning that if a given function

1. actually has a contract (kani_attributes.has_contract()) and
2. is the target of our harness (self.check_fn == Some(fn_def_id))

we'll replace its body with the "check" closure to check the contract.

To implement the alternative behavior, we'd have to change this logic to only use the "check" closure if it meets the above criteria and the user actually wants automatic harnesses to target contracts. I imagine I'd do this by changing the FunctionWithContractPass constructor logic to instantiate check_fn to None if -Z function-contracts wasn't passed.