-
Notifications
You must be signed in to change notification settings - Fork 13k
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Improve contracts intrisics and remove wrapper function
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
Showing
7 changed files
with
57 additions
and
72 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
37 changes: 25 additions & 12 deletions
37
tests/ui/contracts/internal_machinery/contract-intrinsics.rs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,23 +1,36 @@ | ||
//@ run-pass | ||
//@ revisions: yes no none | ||
//@ [yes] compile-flags: -Zcontract-checks=yes | ||
//@ [no] compile-flags: -Zcontract-checks=no | ||
//@ revisions: default unchk_pass chk_pass chk_fail_ensures chk_fail_requires | ||
// | ||
//@ [default] run-pass | ||
//@ [unchk_pass] run-pass | ||
//@ [chk_pass] run-pass | ||
//@ [chk_fail_requires] run-fail | ||
//@ [chk_fail_ensures] run-fail | ||
// | ||
//@ [unchk_pass] compile-flags: -Zcontract-checks=no | ||
//@ [chk_pass] compile-flags: -Zcontract-checks=yes | ||
//@ [chk_fail_requires] compile-flags: -Zcontract-checks=yes | ||
//@ [chk_fail_ensures] compile-flags: -Zcontract-checks=yes | ||
#![feature(cfg_contract_checks, rustc_contracts_internals, core_intrinsics)] | ||
|
||
fn main() { | ||
#[cfg(none)] // default: disabled | ||
#[cfg(any(default, unchk_pass))] // default: disabled | ||
assert_eq!(core::intrinsics::contract_checks(), false); | ||
|
||
#[cfg(yes)] // explicitly enabled | ||
#[cfg(chk_pass)] // explicitly enabled | ||
assert_eq!(core::intrinsics::contract_checks(), true); | ||
|
||
#[cfg(no)] // explicitly disabled | ||
assert_eq!(core::intrinsics::contract_checks(), false); | ||
// always pass | ||
core::intrinsics::contract_check_requires(|| true); | ||
|
||
assert_eq!(core::intrinsics::contract_check_requires(|| true), true); | ||
assert_eq!(core::intrinsics::contract_check_requires(|| false), false); | ||
// fail if enabled | ||
#[cfg(any(default, unchk_pass, chk_fail_requires))] | ||
core::intrinsics::contract_check_requires(|| false); | ||
|
||
let doubles_to_two = { let old = 2; move |ret| ret + ret == old }; | ||
assert_eq!(core::intrinsics::contract_check_ensures(&1, doubles_to_two), true); | ||
assert_eq!(core::intrinsics::contract_check_ensures(&2, doubles_to_two), false); | ||
// Always pass | ||
core::intrinsics::contract_check_ensures(&1, doubles_to_two); | ||
|
||
// Fail if enabled | ||
#[cfg(any(default, unchk_pass, chk_fail_ensures))] | ||
core::intrinsics::contract_check_ensures(&2, doubles_to_two); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters