Remove 'static bound on contract ensures closure

[dawidl022]

The 'static bound on the closure of build_check_ensures prevented some patterns of contracts from type checking, without a clear reason for doing so. As such, this change removes the 'static bound.

While working on the proposal for owned and block for contracts, I came across a pattern that was rejected by type checker while attempting to specify std::ptr::write:

#![feature(core_intrinsics)]#![feature(contracts)]use core::contracts::{requires, ensures};use core::intrinsics;use std::mem::MaybeUninit;fnowned<T>(p:*constT) -> T{// Stub implementation for ownership assertion. Ignore this.unsafe{ std::ptr::read(p)}}#[requires(owned::<MaybeUninit<T>>(dst as*const _);true)]#[ensures(move |_| { owned::<T>(dst);true})]pubunsafefnwrite<T>(dst:*mutT,src:T){unsafe{
intrinsics::write_via_move(dst, src)}}

error[E0310]: the parameter type `T` may not live long enough
--> src/main.rs:13:1
|
13 | #[ensures(move |_| { owned::<T>(dst); true })]
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
| |
| the parameter type `T` must be valid for the static lifetime...
| ...so that the type `T` will meet its required lifetime bounds
|
help: consider adding an explicit lifetime bound
|
14 | pub unsafe fn write<T: 'static>(dst: *mut T, src: T) {
| +++++++++
For more information about this error, try `rustc --explain E0310`.

Eventually, I was able to track down the issue to a trait bound in core::contracts::build_check_ensures, which puts a 'static bound on the ensures closure. Remvoing the 'static bound allows the above contract to type-check, and additionally removes the need for the move in the ensures closure.

I have reduced the problem down to some minimal reproducible examples, which I included as part of this change as regression tests. The error messages for the regression tests before the change were as follows:

error: lifetime may not live long enough
--> /Users/dawidl022/Development/rust/tests/ui/contracts/ensures-lifetime.rs:14:1
|
LL | #[ensures(|_| { x; true })]
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^ requires that `'1` must outlive `'static`
LL | pub fn noop<T>(x: &T) {}
| - let's call the lifetime of this reference `'1`
error[E0597]: `x` does not live long enough
--> /Users/dawidl022/Development/rust/tests/ui/contracts/ensures-lifetime.rs:14:17
|
LL | #[ensures(|_| { x; true })]
| ----------------^----------
| | | |
| | | borrowed value does not live long enough
| | value captured here
| requires that `x` is borrowed for `'static`
LL | pub fn noop<T>(x: &T) {}
| - - `x` dropped here while still borrowed
| |
| binding `x` declared here
|
note: requirement that the value outlives `'static` introduced here
--> /rustc/FAKE_PREFIX/library/core/src/contracts.rs:21:34
error: lifetime may not live long enough
--> /Users/dawidl022/Development/rust/tests/ui/contracts/ensures-lifetime.rs:17:1
|
LL | #[ensures(move |_| { x; true })]
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ requires that `'1` must outlive `'static`
LL | pub fn noop_mv<T>(x: &T) {}
| - let's call the lifetime of this reference `'1`
error[E0310]: the parameter type `T` may not live long enough
--> /Users/dawidl022/Development/rust/tests/ui/contracts/ensures-lifetime.rs:20:1
|
LL | #[ensures(|_| { x; true })]
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
| |
| the parameter type `T` must be valid for the static lifetime...
| ...so that the type `T` will meet its required lifetime bounds
|
help: consider adding an explicit lifetime bound
|
LL | pub fn noop_ptr<T: 'static>(x: *const T) {}
| +++++++++
error[E0310]: the parameter type `T` may not live long enough
--> /Users/dawidl022/Development/rust/tests/ui/contracts/ensures-lifetime.rs:20:1
|
LL | #[ensures(|_| { x; true })]
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
| |
| the parameter type `T` must be valid for the static lifetime...
| ...so that the type `T` will meet its required lifetime bounds
|
= note: duplicate diagnostic emitted due to `-Z deduplicate-diagnostics=no`
help: consider adding an explicit lifetime bound
|
LL | pub fn noop_ptr<T: 'static>(x: *const T) {}
| +++++++++
error[E0310]: the parameter type `T` may not live long enough
--> /Users/dawidl022/Development/rust/tests/ui/contracts/ensures-lifetime.rs:20:1
|
LL | #[ensures(|_| { x; true })]
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
| |
| the parameter type `T` must be valid for the static lifetime...
| ...so that the type `T` will meet its required lifetime bounds
|
= note: duplicate diagnostic emitted due to `-Z deduplicate-diagnostics=no`
help: consider adding an explicit lifetime bound
|
LL | pub fn noop_ptr<T: 'static>(x: *const T) {}
| +++++++++
error[E0597]: `x` does not live long enough
--> /Users/dawidl022/Development/rust/tests/ui/contracts/ensures-lifetime.rs:20:17
|
LL | #[ensures(|_| { x; true })]
| ----------------^----------
| | | |
| | | borrowed value does not live long enough
| | value captured here
| requires that `x` is borrowed for `'static`
LL | pub fn noop_ptr<T>(x: *const T) {}
| - - `x` dropped here while still borrowed
| |
| binding `x` declared here
|
note: requirement that the value outlives `'static` introduced here
--> /rustc/FAKE_PREFIX/library/core/src/contracts.rs:21:34
error[E0310]: the parameter type `T` may not live long enough
--> /Users/dawidl022/Development/rust/tests/ui/contracts/ensures-lifetime.rs:23:1
|
LL | #[ensures(move |_| { x; true })]
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
| |
| the parameter type `T` must be valid for the static lifetime...
| ...so that the type `T` will meet its required lifetime bounds
|
help: consider adding an explicit lifetime bound
|
LL | pub fn noop_ptr_mv<T: 'static>(x: *const T) {}
| +++++++++
error: aborting due to 8 previous errors; 1 warning emitted
Some errors have detailed explanations: E0310, E0597.
For more information about an error, try `rustc --explain E0310`.
------------------------------------------
---- [ui] tests/ui/contracts/ensures-lifetime.rs stdout end ----
failures:
[ui] tests/ui/contracts/ensures-lifetime.rs

@celinval are you aware of any reason why the 'static bound was put on build_check_ensures in the first place?

I have checked that the contracts in #136578 and #147148 still type check with this change.

Contracts tracking issue: #128044

[rustbot]

r? @davidtwco

rustbot has assigned @davidtwco.
They will have a look at your PR within the next two weeks and either review your PR or reassign to another reviewer.

Use r? to explicitly pick a reviewer

[chenyukang]

you may add #![allow(incomplete_features)] to suppress this warning.

[dawidl022]

Thanks for pointing this out! So far all the other contract UI tests have included this warning in the stderr, so I followed that pattern.

[tautschnig]

Brilliant, this will enable adding a lot more contracts that #147148 currently has commented out.

[celinval]

@dawidl022, I don't recall why the build ensures had 'static. I can see if I can find my notes when @pnkfelix handed contacts over to me.

[davidtwco]

r? @celinval

@bors delegate=celinval

[bors]

✌️ @celinval, you can now approve this pull request!

If @davidtwco told you to "r=me" after making some further change, please make that change, then do @bors r=@davidtwco

[celinval]

I couldn't find any notes on this, but I took a closer look at it. I believe the reason why there's a 'static is because we haven't decided yet whether ensures should run before or after dropping local variables.

Removing the 'static would allow ensures clauses that rely on local variables being alive by the time ensures run.

[dawidl022]

Removing the 'static would allow ensures clauses that rely on local variables being alive by the time ensures run.

Wouldn't these local variables really just be function parameters? The way contracts are scoped, they can only refer to
parameters, not other "regular" local variables. Also, the type system prevents us from returning with a reference to any local variable (as we would have a dangling reference), so we wouldn't be able to talk about those in the contract anyways.

It seems to me that it should be fine for the ensures clause to reference parameters. Do you have any problematic examples in mind?

[celinval]

Yes, at least in theory. You are correct, that without 'static, only function parameters would be available, but do we want to verify what happens when they get dropped? I created a thread to discuss this further: https://rust-lang.zulipchat.com/#narrow/channel/544080-t-lang.2Fcontracts/topic/Order.20of.20evaluation.20between.20ensures.20and.20dropping.20parameters

[dawidl022]

but do we want to verify what happens when they get dropped

I think that is a valid concern to raise.

Nonetheless, I'm not sure 'static is the best way to implement this. The separation logic I'm used to indeed does not permit you to reference local variables or function parameters in the postcondition. However, one can create copies of values held in parameters in the precondition, store them in contract variables (as implemented in #144444) and then refer to them in the postcondition. So for raw pointers in particular, which are Copy, I would expect that pattern to work:

#[requires(let dst_ptr = dst; owned::<MaybeUninit<T>>(dst_ptr as *const _); true)]
#[ensures(move |_| { owned::<T>(dst_ptr); true })]
pub unsafe fn write<T>(dst: *mut T, src: T) {
unsafe {
intrinsics::write_via_move(dst, src)
}
}

However, I get the same type error:

error[E0310]: the parameter type `T` may not live long enough
--> src/main.rs:14:1
|
14 | #[ensures(move |_| { owned::<T>(dst_ptr); true })]
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
| |
| the parameter type `T` must be valid for the static lifetime...
| ...so that the type `T` will meet its required lifetime bounds
|
help: consider adding an explicit lifetime bound
|
15 | pub unsafe fn write<T: 'static>(dst: *mut T, src: T) {
| +++++++++

[celinval]

I'm not saying it is great, but what I'm saying is that if we remove the 'static at this point, contracts will start accepting ensures clauses that assume the parameters are alive. Which I am not convinced is desirable.

If you change the signature of owned to:

fnowned<T>(p:*const()) -> T{// Stub implementation for ownership assertion. Ignore this. unsafe{ std::ptr::read(p as*constT)}}

I believe you should be able to use the following contract:

#[ensures({let ptr = dst as*const(); move |_| { owned::<T>(ptr);true}})]

This is not very ergonomic, and makes contracts with generic parameters harder.

Do you have any other suggestion that we could implement to reject parameters in ensure clauses and remove the 'static constraint? Given the current implementation, the other options I can think about would require extra runtime logic, which I think is less desirable than 'static. For example, we could add a layer of indirection or add to the preamble a variable reassignment that would force the parameters to be dropped before invoking ensures.

[dawidl022]

If you change the signature of owned to:

Thank you! I was not aware of this workaround.

Do you have any other suggestion that we could implement to reject parameters in ensure clauses and remove the 'static constraint?

I'm not sure how easy it is to implement, but we could remove the lexical scope of function parameters from the ensures clause. I feel it would be a bit challanging, since we still want access to variables declared in the requires clause.

[dawidl022]

but we could remove the lexical scope of function parameters from the ensures clause.

I realise this would not prevent users from creating references to parameters in the requires clause and then using them in the ensures clause, which also would require the parameters to still be alive when the ensures clause runs.

[dawidl022]

The borrow checker would flag any borrow-rule violations, so e.g. if we did decide that the ensures clause runs
after local variables are dropped, then the borrow checker would complain if we did reference parameters in the ensures clause. However, I understand that having 'static there right now is a way of preventing the later change to be a breaking change:

because we haven't decided yet whether ensures should run before or after dropping local variables.

[dawidl022]

@celinval May we please move forward with this change?

I understand the concerns regarding the assumption of parameters being alive in the ensures clause. However, resolving this issue fully is non-trivial, and will require some design, discussions and planning.

In the meantime, I suggest we allow the ensures clause to type-check in agreement with the behaviour of how contracts are implemented - that the ensures clause does indeed run before the function returns, and so we can assume parameters (that have not been dropped as part of the function) are still alive. The borrow checker should be abe to handle any violations, and I think having more ergonomic contracts will facilitate experimentation on #149213.

[celinval]

@dawidl022, I was wondering if we could change contracts implementation to add one layer of indirection, and do the following:

If contracts is disabled:

fnfunc(args:Args) -> Ret{iffalse{
<precond>;
<build_post>;let ret = func(args);
<postcode>(&ret);
ret
}else{
<body>
}}

If contracts enabled:

fnfunc(args:Args) -> Ret{
<precond>;
<build_post>;let ret = move | | { body }();
<postcode>(&ret);
ret
}

[celinval]

I don't think we should accept invalid contracts in favor of a slightly better ergonomic. The experiment is not blocked on this, is it?

[dawidl022]

I was wondering if we could change contracts implementation to add one layer of indirection, and do the following:

@celinval what would be the advantages/rationale for the lowering you suggested?

How does it compare to the lowering proposed in the re-architecture section of your document? Could we go straight for the latter instead?

[celinval]

I was wondering if we could change contracts implementation to add one layer of indirection, and do the following:

@celinval what would be the advantages/rationale for the lowering you suggested?

How does it compare to the lowering proposed in the re-architecture section of your document? Could we go straight for the latter instead?

The only advantage would be to unblock you earlier. It would still be temporary

[apiraino]

removing t-compiler since this looks like t-llibs

@rustbot label -t-compiler