Skip to content

Commit 2dda231

Browse files
authored
Rollup merge of #144444 - dawidl022:contracts/variable-scoping-rebased, r=jackh726
Contract variable declarations This change adds contract variables that can be declared in the `requires` clause and can be referenced both in `requires` and `ensures`, subject to usual borrow checking rules. This allows any setup common to both the `requires` and `ensures` clauses to only be done once. In particular, one future use case would be for [Fulminate](https://dl.acm.org/doi/10.1145/3704879)-like ownership assertions in contracts, that are essentially side-effects, and executing them twice would alter the semantics of the contract. As of this change, `requires` can now be an arbitrary sequence of statements, with the final expression being of type `bool`. They are executed in sequence as expected, before checking if the final `bool` expression holds. This PR depends on rust-lang/rust#144438 (which has now been merged). Contracts tracking issue: rust-lang/rust#128044 **Other changes introduced**: - Contract macros now wrap the content in braces to produce blocks, meaning there's no need to wrap the content in `{}` when using multiple statements. The change is backwards compatible, in that wrapping the content in `{}` still works as before. The macros also now treat `requires` and `ensures` uniformally, meaning the `requires` closure is built inside the parser, as opposed to in the macro. **Known limiatations**: - Contracts with variable declarations are subject to the regular borrow checking rules, and the way contracts are currently lowered limits the usefulness of contract variable declarations. Consider the below example: ```rust #[requires(let init_x = *x; true)] #[ensures(move |_| *x == 2 * init_x)] fn double_in_place(x: &mut i32) { *x *= 2; } ``` We have used the new variable declarations feature to remember the initial value pointed to by `x`, however, moving `x` into the `ensures` does not pass the borrow checker, meaning the above function contract is illegal. Ideally, something like the above should be expressable in contracts.
2 parents 09bdb28 + ca3def1 commit 2dda231

File tree

0 file changed

+0
-0
lines changed

    0 file changed

    +0
    -0
    lines changed

    0 commit comments

    Comments
     (0)