Skip to content

Commit

Permalink
Improve contracts intrisics and remove wrapper function
Browse files Browse the repository at this point in the history
1. Document the new intrinsics.
2. Make the intrinsics actually check the contract if enabled, and
   remove `contract::check_requires` function.
3. Use panic with no unwind in case contract is using to check for
   safety, we probably don't want to unwind. Following the same
   reasoning as UB checks.
  • Loading branch information
celinval authored and gitbot committed Feb 20, 2025
1 parent 435f432 commit da34e0f
Show file tree
Hide file tree
Showing 2 changed files with 23 additions and 26 deletions.
27 changes: 5 additions & 22 deletions core/src/contracts.rs
Original file line number Diff line number Diff line change
@@ -1,38 +1,21 @@
//! Unstable module containing the unstable contracts lang items and attribute macros.
#![cfg(not(bootstrap))]

#[cfg(not(bootstrap))]
pub use crate::macros::builtin::contracts_ensures as ensures;
#[cfg(not(bootstrap))]
pub use crate::macros::builtin::contracts_requires as requires;

/// Emitted by rustc as a desugaring of `#[requires(PRED)] fn foo(x: X) { ... }`
/// into: `fn foo(x: X) { check_requires(|| PRED) ... }`
#[cfg(not(bootstrap))]
#[unstable(feature = "rustc_contracts_internals", issue = "133866" /* compiler-team#759 */)]
#[lang = "contract_check_requires"]
#[track_caller]
pub fn check_requires<C: FnOnce() -> bool>(c: C) {
if core::intrinsics::contract_checks() {
assert!(core::intrinsics::contract_check_requires(c), "failed requires check");
}
}
pub use crate::macros::builtin::{contracts_ensures as ensures, contracts_requires as requires};

/// Emitted by rustc as a desugaring of `#[ensures(PRED)] fn foo() -> R { ... [return R;] ... }`
/// into: `fn foo() { let _check = build_check_ensures(|ret| PRED) ... [return _check(R);] ... }`
/// (including the implicit return of the tail expression, if any).
#[cfg(not(bootstrap))]
#[unstable(feature = "rustc_contracts_internals", issue = "133866" /* compiler-team#759 */)]
#[lang = "contract_build_check_ensures"]
#[track_caller]
pub fn build_check_ensures<Ret, C>(c: C) -> impl (FnOnce(Ret) -> Ret) + Copy
pub fn build_check_ensures<Ret, C>(cond: C) -> impl (Fn(Ret) -> Ret) + Copy
where
C: for<'a> FnOnce(&'a Ret) -> bool + Copy + 'static,
C: for<'a> Fn(&'a Ret) -> bool + Copy + 'static,
{
#[track_caller]
move |ret| {
if core::intrinsics::contract_checks() {
assert!(core::intrinsics::contract_check_ensures(&ret, c), "failed ensures check");
}
crate::intrinsics::contract_check_ensures(&ret, cond);
ret
}
}
22 changes: 18 additions & 4 deletions core/src/intrinsics/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4082,18 +4082,32 @@ pub const fn contract_checks() -> bool {
false
}

/// Check if the pre-condition `cond` has been met.
///
/// By default, if `contract_checks` is enabled, this will panic with no unwind if the condition
/// returns false.
#[cfg(not(bootstrap))]
#[unstable(feature = "rustc_contracts_internals", issue = "133866" /* compiler-team#759 */)]
#[lang = "contract_check_requires"]
#[rustc_intrinsic]
pub fn contract_check_requires<C: FnOnce() -> bool>(c: C) -> bool {
c()
pub fn contract_check_requires<C: Fn() -> bool>(cond: C) {
if contract_checks() && !cond() {
// Emit no unwind panic in case this was a safety requirement.
crate::panicking::panic_nounwind("failed requires check");
}
}

/// Check if the post-condition `cond` has been met.
///
/// By default, if `contract_checks` is enabled, this will panic with no unwind if the condition
/// returns false.
#[cfg(not(bootstrap))]
#[unstable(feature = "rustc_contracts_internals", issue = "133866" /* compiler-team#759 */)]
#[rustc_intrinsic]
pub fn contract_check_ensures<'a, Ret, C: FnOnce(&'a Ret) -> bool>(ret: &'a Ret, c: C) -> bool {
c(ret)
pub fn contract_check_ensures<'a, Ret, C: Fn(&'a Ret) -> bool>(ret: &'a Ret, cond: C) {
if contract_checks() && !cond(ret) {
crate::panicking::panic_nounwind("failed ensures check");
}
}

/// The intrinsic will return the size stored in that vtable.
Expand Down

0 comments on commit da34e0f

Please sign in to comment.