Add panics_if precondition to express panic-freedom
#4230
Conversation
Implements a solution towards model-checking#3567, following up on the RFC discussion in model-checking#3893.
github-actions
bot
added
Z-EndToEndBenchCI
| @@ -29,6 +29,12 @@ impl<'a> ContractConditionsHandler<'a> { | |||
| #(#body_stmts)* | |||
| }) | |||
| } | |||
| ContractConditionsData::PanicsIf { attr } => { | |||
| quote!({ | |||
| kani::assume(!(#attr)); | |||
There was a problem hiding this comment.
Could we instead name that clause may_panic_if ? the current encoding checks that the function does not panic when the negation of the condition holds, not that it panics when the condition holds. The function may or may not panic when this condition does not hold.
Suggestion: add two clauses:
-
no_panic_if(P), specifies panic-freedom conditions (passes if function does not panic whenever the condition holds)- verified by checking that function does not panic under
kani::assume(P); - or by checking that when function panics then !P held initially on inputs
- verified by checking that function does not panic under
-
panic_if(Q): specifies panic conditions (passes if function panics whenever the condition holds)- verified by checking that function panics under
kani::assume(Q);- or by check that when function does not panics then !Q held initially on inputs
- verified by checking that function panics under
-
consistency check: assert!(!P || !Q); (are the conditions disjoint?)
-
completeness check : assert!(P || Q); (are we covering the whole input space?)
-
if both consistency and completeness hold we have a partition of the input domain
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.
Implements a solution towards #3567, following up on the RFC discussion in #3893.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.