search

model-checking / kani

Kani Rust Verifier
https://model-checking.github.io/kani
Apache License 2.0
2.27k stars 95 forks source link

Disallow side effects in contract expressions #3213

Open pi314mm opened 6 months ago

pi314mm commented 6 months ago

Currently, function contracts allow for arbitrary expressions, including ones that allow for potential side effects. This could result in a statement that modifies the input arguments to a function before running the function on those arguments, or modifying the result or input arguments after the computation has passed.

This is likely related to #2909. This showcases an infinite loop as a side effect resulting in a contract being vacuously true.

The problem with side effects within the function contracts is that it blurs the abstraction of the contract macros, as it requires the user to reason about the kani::assert statements that the contract macros compile to. The arguments are no longer being directly fed in and out of the function, but rather there are precomputations and postcomputations which could have side effects. To truly maintain the proper abstraction of these macros, the pre and post computations must be pure.

jsalzbergedu commented 6 months ago

I think only allowing const fn in the function contracts would be a good fit. const fn disallows arbitrary looping and disallows side effects that cannot be evaluated at compile time.

EDIT: const fn allows while true. We would need to do both this and some looping restriction.

celinval commented 5 months ago

I think only allowing const fn in the function contracts would be a good fit. const fn disallows arbitrary looping and disallows side effects that cannot be evaluated at compile time.

EDIT: const fn allows while true. We would need to do both this and some looping restriction.

That's a great idea. I worry that this might be too restrictive though.

celinval commented 5 months ago

I wonder if we can at least wrap everything into an Fn closure like the one being added in #3307. That will ensure that the contract expressions cannot mutably capture their environment.