Add unstable option prove-safety-only

[tautschnig]

Compute verification results under the assumption that no panic occurs. This enables safety verification, i.e., proving the absence of undefined behavior without being distracted by panics which Kani, otherwise, also reports as verification failures. #4230 was an efforts towards the same goal, but required manual annotation of the conditions under which a panic may occur (and may hide undefined behavior when either the given specifications are too broad or when undefined behavior arises on a path to a panic).

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

[carolynzech]

Can you provide motivation in the PR description? I'm mainly interested in what you think the use cases are for this feature.

[tautschnig]

Can you provide motivation in the PR description? I'm mainly interested in what you think the use cases are for this feature.

Good point :-) Done!

[zhassan-aws]

LGTM. I'm a bit unsure about the option name. I can't think of a better name though.

[carolynzech]

LGTM. I'm a bit unsure about the option name. I can't think of a better name though.

@zhassan-aws, @tautschnig and I spoke about this offline and I was thinking prove-safety-only, since assume-no-panic implies (to me) that we only mean panic!.

We also spoke offline about how I'd like to see more tests about how this impacts safety verification and user-defined assertions--looking at all callsites of codegen_assert_assume, there's ones like

kani/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

Lines 68 to 76 in 313f9b1

	// Codegen an assertion failure since vtable comparison is not stable.
	let ret_type = Type::Bool;
	let body = vec![
	self.codegen_assert_assume_false(
	PropertyClass::SafetyCheck,
	format!("Reached unstable vtable comparison '{op:?}'").as_str(),
	loc,
	),
	ret_type.nondet().as_stmt(loc).with_location(loc),

that give me pause, since it seems like then we'll be assuming a safety condition holds? I'll admit I'm not entirely clear on why we call codegen_assert in some cases and codegen_assert_assume in others, so the fact that this PR only needs to change one is also confusing to me.

[tautschnig]

We also spoke offline about how I'd like to see more tests about how this impacts safety verification and user-defined assertions--looking at all callsites of codegen_assert_assume, there's ones like [...] that give me pause, since it seems like then we'll be assuming a safety condition holds? I'll admit I'm not entirely clear on why we call codegen_assert in some cases and codegen_assert_assume in others, so the fact that this PR only needs to change one is also confusing to me.

The key here are the changes in #3860: the PropertyClass will tell us whether we are dealing with a panic or possible undefined behavior. The example you listed above is a SafetyCheck, so --prove-safety-only will retain the assertion.