Skip to content

Commit d1c9f09

Browse files
fmeasegitbot
authored and
gitbot
committed
Rollup merge of rust-lang#128045 - pnkfelix:rustc-contracts, r=oli-obk
#[contracts::requires(...)] + #[contracts::ensures(...)] cc rust-lang#128044 Updated contract support: attribute syntax for preconditions and postconditions, implemented via a series of desugarings that culminates in: 1. a compile-time flag (`-Z contract-checks`) that, similar to `-Z ub-checks`, attempts to ensure that the decision of enabling/disabling contract checks is delayed until the end user program is compiled, 2. invocations of lang-items that handle invoking the precondition, building a checker for the post-condition, and invoking that post-condition checker at the return sites for the function, and 3. intrinsics for the actual evaluation of pre- and post-condition predicates that third-party verification tools can intercept and reinterpret for their own purposes (e.g. creating shims of behavior that abstract away the function body and replace it solely with the pre- and post-conditions). Known issues: * My original intent, as described in the MCP (rust-lang/compiler-team#759) was to have a rustc-prefixed attribute namespace (like rustc_contracts::requires). But I could not get things working when I tried to do rewriting via a rustc-prefixed builtin attribute-macro. So for now it is called `contracts::requires`. * Our attribute macro machinery does not provide direct support for attribute arguments that are parsed like rust expressions. I spent some time trying to add that (e.g. something that would parse the attribute arguments as an AST while treating the remainder of the items as a token-tree), but its too big a lift for me to undertake. So instead I hacked in something approximating that goal, by semi-trivially desugaring the token-tree attribute contents into internal AST constucts. This may be too fragile for the long-term. * (In particular, it *definitely* breaks when you try to add a contract to a function like this: `fn foo1(x: i32) -> S<{ 23 }> { ... }`, because its token-tree based search for where to inject the internal AST constructs cannot immediately see that the `{ 23 }` is within a generics list. I think we can live for this for the short-term, i.e. land the work, and continue working on it while in parallel adding a new attribute variant that takes a token-tree attribute alongside an AST annotation, which would completely resolve the issue here.) * the *intent* of `-Z contract-checks` is that it behaves like `-Z ub-checks`, in that we do not prematurely commit to including or excluding the contract evaluation in upstream crates (most notably, `core` and `std`). But the current test suite does not actually *check* that this is the case. Ideally the test suite would be extended with a multi-crate test that explores the matrix of enabling/disabling contracts on both the upstream lib and final ("leaf") bin crates.
2 parents 86a08cf + 5d134c6 commit d1c9f09

File tree

4 files changed

+98
-0
lines changed

4 files changed

+98
-0
lines changed

Diff for: core/src/contracts.rs

+21
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
//! Unstable module containing the unstable contracts lang items and attribute macros.
2+
#![cfg(not(bootstrap))]
3+
4+
pub use crate::macros::builtin::{contracts_ensures as ensures, contracts_requires as requires};
5+
6+
/// Emitted by rustc as a desugaring of `#[ensures(PRED)] fn foo() -> R { ... [return R;] ... }`
7+
/// into: `fn foo() { let _check = build_check_ensures(|ret| PRED) ... [return _check(R);] ... }`
8+
/// (including the implicit return of the tail expression, if any).
9+
#[unstable(feature = "contracts_internals", issue = "128044" /* compiler-team#759 */)]
10+
#[lang = "contract_build_check_ensures"]
11+
#[track_caller]
12+
pub fn build_check_ensures<Ret, C>(cond: C) -> impl (Fn(Ret) -> Ret) + Copy
13+
where
14+
C: for<'a> Fn(&'a Ret) -> bool + Copy + 'static,
15+
{
16+
#[track_caller]
17+
move |ret| {
18+
crate::intrinsics::contract_check_ensures(&ret, cond);
19+
ret
20+
}
21+
}

Diff for: core/src/intrinsics/mod.rs

+46
Original file line numberDiff line numberDiff line change
@@ -4064,6 +4064,52 @@ pub const unsafe fn const_deallocate(_ptr: *mut u8, _size: usize, _align: usize)
40644064
// Runtime NOP
40654065
}
40664066

4067+
/// Returns whether we should perform contract-checking at runtime.
4068+
///
4069+
/// This is meant to be similar to the ub_checks intrinsic, in terms
4070+
/// of not prematurely commiting at compile-time to whether contract
4071+
/// checking is turned on, so that we can specify contracts in libstd
4072+
/// and let an end user opt into turning them on.
4073+
#[cfg(not(bootstrap))]
4074+
#[rustc_const_unstable(feature = "contracts_internals", issue = "128044" /* compiler-team#759 */)]
4075+
#[unstable(feature = "contracts_internals", issue = "128044" /* compiler-team#759 */)]
4076+
#[inline(always)]
4077+
#[rustc_intrinsic]
4078+
pub const fn contract_checks() -> bool {
4079+
// FIXME: should this be `false` or `cfg!(contract_checks)`?
4080+
4081+
// cfg!(contract_checks)
4082+
false
4083+
}
4084+
4085+
/// Check if the pre-condition `cond` has been met.
4086+
///
4087+
/// By default, if `contract_checks` is enabled, this will panic with no unwind if the condition
4088+
/// returns false.
4089+
#[cfg(not(bootstrap))]
4090+
#[unstable(feature = "contracts_internals", issue = "128044" /* compiler-team#759 */)]
4091+
#[lang = "contract_check_requires"]
4092+
#[rustc_intrinsic]
4093+
pub fn contract_check_requires<C: Fn() -> bool>(cond: C) {
4094+
if contract_checks() && !cond() {
4095+
// Emit no unwind panic in case this was a safety requirement.
4096+
crate::panicking::panic_nounwind("failed requires check");
4097+
}
4098+
}
4099+
4100+
/// Check if the post-condition `cond` has been met.
4101+
///
4102+
/// By default, if `contract_checks` is enabled, this will panic with no unwind if the condition
4103+
/// returns false.
4104+
#[cfg(not(bootstrap))]
4105+
#[unstable(feature = "contracts_internals", issue = "128044" /* compiler-team#759 */)]
4106+
#[rustc_intrinsic]
4107+
pub fn contract_check_ensures<'a, Ret, C: Fn(&'a Ret) -> bool>(ret: &'a Ret, cond: C) {
4108+
if contract_checks() && !cond(ret) {
4109+
crate::panicking::panic_nounwind("failed ensures check");
4110+
}
4111+
}
4112+
40674113
/// The intrinsic will return the size stored in that vtable.
40684114
///
40694115
/// # Safety

Diff for: core/src/lib.rs

+5
Original file line numberDiff line numberDiff line change
@@ -113,6 +113,7 @@
113113
#![feature(bigint_helper_methods)]
114114
#![feature(bstr)]
115115
#![feature(bstr_internals)]
116+
#![feature(closure_track_caller)]
116117
#![feature(const_carrying_mul_add)]
117118
#![feature(const_eval_select)]
118119
#![feature(core_intrinsics)]
@@ -247,6 +248,10 @@ pub mod autodiff {
247248
pub use crate::macros::builtin::autodiff;
248249
}
249250

251+
#[cfg(not(bootstrap))]
252+
#[unstable(feature = "contracts", issue = "128044")]
253+
pub mod contracts;
254+
250255
#[unstable(feature = "cfg_match", issue = "115585")]
251256
pub use crate::macros::cfg_match;
252257

Diff for: core/src/macros/mod.rs

+26
Original file line numberDiff line numberDiff line change
@@ -1777,6 +1777,32 @@ pub(crate) mod builtin {
17771777
/* compiler built-in */
17781778
}
17791779

1780+
/// Attribute macro applied to a function to give it a post-condition.
1781+
///
1782+
/// The attribute carries an argument token-tree which is
1783+
/// eventually parsed as a unary closure expression that is
1784+
/// invoked on a reference to the return value.
1785+
#[cfg(not(bootstrap))]
1786+
#[unstable(feature = "contracts", issue = "128044")]
1787+
#[allow_internal_unstable(contracts_internals)]
1788+
#[rustc_builtin_macro]
1789+
pub macro contracts_ensures($item:item) {
1790+
/* compiler built-in */
1791+
}
1792+
1793+
/// Attribute macro applied to a function to give it a precondition.
1794+
///
1795+
/// The attribute carries an argument token-tree which is
1796+
/// eventually parsed as an boolean expression with access to the
1797+
/// function's formal parameters
1798+
#[cfg(not(bootstrap))]
1799+
#[unstable(feature = "contracts", issue = "128044")]
1800+
#[allow_internal_unstable(contracts_internals)]
1801+
#[rustc_builtin_macro]
1802+
pub macro contracts_requires($item:item) {
1803+
/* compiler built-in */
1804+
}
1805+
17801806
/// Attribute macro applied to a function to register it as a handler for allocation failure.
17811807
///
17821808
/// See also [`std::alloc::handle_alloc_error`](../../../std/alloc/fn.handle_alloc_error.html).

0 commit comments

Comments
 (0)