contracts: added lang items that act as hooks for rustc-injected code to invoke.

see test for an example of the kind of injected code that is anticipated here.
This commit is contained in:
Felix S. Klock II 2024-12-02 21:16:35 +00:00 committed by Celina G. Val
parent bcb8565f30
commit 777def87d5
5 changed files with 90 additions and 0 deletions

View file

@ -418,6 +418,10 @@ language_item_table! {
String, sym::String, string, Target::Struct, GenericRequirement::None;
CStr, sym::CStr, c_str, Target::Struct, GenericRequirement::None;
// Experimental lang items for implementing contract pre- and post-condition checking.
ContractBuildCheckEnsures, sym::contract_build_check_ensures, contract_build_check_ensures_fn, Target::Fn, GenericRequirement::None;
ContractCheckRequires, sym::contract_check_requires, contract_check_requires_fn, Target::Fn, GenericRequirement::None;
}
pub enum GenericRequirement {

View file

@ -676,6 +676,7 @@ symbols! {
const_ty_placeholder: "<const_ty>",
constant,
constructor,
contract_build_check_ensures,
contract_check_ensures,
contract_check_requires,
contract_checks,

View file

@ -0,0 +1,33 @@
//! Unstable module containing the unstable contracts lang items and attribute macros.
/// 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", issue = "none" /* 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");
}
}
/// 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", issue = "none" /* compiler-team#759 */)]
#[lang = "contract_build_check_ensures"]
#[track_caller]
pub fn build_check_ensures<Ret, C>(c: C) -> impl (FnOnce(Ret) -> Ret) + Copy
where
C: for<'a> FnOnce(&'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");
}
ret
}
}

View file

@ -114,6 +114,7 @@
#![feature(bstr)]
#![feature(bstr_internals)]
#![feature(const_carrying_mul_add)]
#![feature(closure_track_caller)]
#![feature(const_eval_select)]
#![feature(core_intrinsics)]
#![feature(coverage_attribute)]
@ -246,6 +247,10 @@ pub mod autodiff {
pub use crate::macros::builtin::autodiff;
}
#[cfg(not(bootstrap))]
#[unstable(feature = "rustc_contracts", issue = "none")]
pub mod contracts;
#[unstable(feature = "cfg_match", issue = "115585")]
pub use crate::macros::cfg_match;

View file

@ -0,0 +1,47 @@
//@ revisions: unchk_pass unchk_fail_pre unchk_fail_post chk_pass chk_fail_pre chk_fail_post
//
//@ [unchk_pass] run-pass
//@ [unchk_fail_pre] run-pass
//@ [unchk_fail_post] run-pass
//@ [chk_pass] run-pass
//
//@ [chk_fail_pre] run-fail
//@ [chk_fail_post] run-fail
//
//@ [unchk_pass] compile-flags: -Zcontract-checks=no
//@ [unchk_fail_pre] compile-flags: -Zcontract-checks=no
//@ [unchk_fail_post] compile-flags: -Zcontract-checks=no
//
//@ [chk_pass] compile-flags: -Zcontract-checks=yes
//@ [chk_fail_pre] compile-flags: -Zcontract-checks=yes
//@ [chk_fail_post] compile-flags: -Zcontract-checks=yes
#![feature(rustc_contracts)]
fn foo(x: Baz) -> i32 {
core::contracts::check_requires(|| x.baz > 0);
let injected_checker = {
core::contracts::build_check_ensures(|ret| *ret > 100)
};
let ret = x.baz + 50;
injected_checker(ret)
}
struct Baz { baz: i32 }
const BAZ_PASS_PRE_POST: Baz = Baz { baz: 100 };
#[cfg(any(unchk_fail_post, chk_fail_post))]
const BAZ_FAIL_POST: Baz = Baz { baz: 10 };
#[cfg(any(unchk_fail_pre, chk_fail_pre))]
const BAZ_FAIL_PRE: Baz = Baz { baz: -10 };
fn main() {
assert_eq!(foo(BAZ_PASS_PRE_POST), 150);
#[cfg(any(unchk_fail_pre, chk_fail_pre))]
foo(BAZ_FAIL_PRE);
#[cfg(any(unchk_fail_post, chk_fail_post))]
foo(BAZ_FAIL_POST);
}