Skip to content

Commit 777def8

Browse files
pnkfelixcelinval
authored andcommitted
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.
1 parent bcb8565 commit 777def8

File tree

5 files changed

+90
-0
lines changed

5 files changed

+90
-0
lines changed

compiler/rustc_hir/src/lang_items.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -418,6 +418,10 @@ language_item_table! {
418418

419419
String, sym::String, string, Target::Struct, GenericRequirement::None;
420420
CStr, sym::CStr, c_str, Target::Struct, GenericRequirement::None;
421+
422+
// Experimental lang items for implementing contract pre- and post-condition checking.
423+
ContractBuildCheckEnsures, sym::contract_build_check_ensures, contract_build_check_ensures_fn, Target::Fn, GenericRequirement::None;
424+
ContractCheckRequires, sym::contract_check_requires, contract_check_requires_fn, Target::Fn, GenericRequirement::None;
421425
}
422426

423427
pub enum GenericRequirement {

compiler/rustc_span/src/symbol.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -676,6 +676,7 @@ symbols! {
676676
const_ty_placeholder: "<const_ty>",
677677
constant,
678678
constructor,
679+
contract_build_check_ensures,
679680
contract_check_ensures,
680681
contract_check_requires,
681682
contract_checks,

library/core/src/contracts.rs

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
//! Unstable module containing the unstable contracts lang items and attribute macros.
2+
3+
/// Emitted by rustc as a desugaring of `#[requires(PRED)] fn foo(x: X) { ... }`
4+
/// into: `fn foo(x: X) { check_requires(|| PRED) ... }`
5+
#[cfg(not(bootstrap))]
6+
#[unstable(feature = "rustc_contracts", issue = "none" /* compiler-team#759 */)]
7+
#[lang = "contract_check_requires"]
8+
#[track_caller]
9+
pub fn check_requires<C: FnOnce() -> bool>(c: C) {
10+
if core::intrinsics::contract_checks() {
11+
assert!(core::intrinsics::contract_check_requires(c), "failed requires check");
12+
}
13+
}
14+
15+
/// Emitted by rustc as a desugaring of `#[ensures(PRED)] fn foo() -> R { ... [return R;] ... }`
16+
/// into: `fn foo() { let _check = build_check_ensures(|ret| PRED) ... [return _check(R);] ... }`
17+
/// (including the implicit return of the tail expression, if any).
18+
#[cfg(not(bootstrap))]
19+
#[unstable(feature = "rustc_contracts", issue = "none" /* compiler-team#759 */)]
20+
#[lang = "contract_build_check_ensures"]
21+
#[track_caller]
22+
pub fn build_check_ensures<Ret, C>(c: C) -> impl (FnOnce(Ret) -> Ret) + Copy
23+
where
24+
C: for<'a> FnOnce(&'a Ret) -> bool + Copy + 'static,
25+
{
26+
#[track_caller]
27+
move |ret| {
28+
if core::intrinsics::contract_checks() {
29+
assert!(core::intrinsics::contract_check_ensures(&ret, c), "failed ensures check");
30+
}
31+
ret
32+
}
33+
}

library/core/src/lib.rs

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -114,6 +114,7 @@
114114
#![feature(bstr)]
115115
#![feature(bstr_internals)]
116116
#![feature(const_carrying_mul_add)]
117+
#![feature(closure_track_caller)]
117118
#![feature(const_eval_select)]
118119
#![feature(core_intrinsics)]
119120
#![feature(coverage_attribute)]
@@ -246,6 +247,10 @@ pub mod autodiff {
246247
pub use crate::macros::builtin::autodiff;
247248
}
248249

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

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
1+
//@ revisions: unchk_pass unchk_fail_pre unchk_fail_post chk_pass chk_fail_pre chk_fail_post
2+
//
3+
//@ [unchk_pass] run-pass
4+
//@ [unchk_fail_pre] run-pass
5+
//@ [unchk_fail_post] run-pass
6+
//@ [chk_pass] run-pass
7+
//
8+
//@ [chk_fail_pre] run-fail
9+
//@ [chk_fail_post] run-fail
10+
//
11+
//@ [unchk_pass] compile-flags: -Zcontract-checks=no
12+
//@ [unchk_fail_pre] compile-flags: -Zcontract-checks=no
13+
//@ [unchk_fail_post] compile-flags: -Zcontract-checks=no
14+
//
15+
//@ [chk_pass] compile-flags: -Zcontract-checks=yes
16+
//@ [chk_fail_pre] compile-flags: -Zcontract-checks=yes
17+
//@ [chk_fail_post] compile-flags: -Zcontract-checks=yes
18+
19+
#![feature(rustc_contracts)]
20+
21+
fn foo(x: Baz) -> i32 {
22+
core::contracts::check_requires(|| x.baz > 0);
23+
24+
let injected_checker = {
25+
core::contracts::build_check_ensures(|ret| *ret > 100)
26+
};
27+
28+
let ret = x.baz + 50;
29+
injected_checker(ret)
30+
}
31+
32+
struct Baz { baz: i32 }
33+
34+
35+
const BAZ_PASS_PRE_POST: Baz = Baz { baz: 100 };
36+
#[cfg(any(unchk_fail_post, chk_fail_post))]
37+
const BAZ_FAIL_POST: Baz = Baz { baz: 10 };
38+
#[cfg(any(unchk_fail_pre, chk_fail_pre))]
39+
const BAZ_FAIL_PRE: Baz = Baz { baz: -10 };
40+
41+
fn main() {
42+
assert_eq!(foo(BAZ_PASS_PRE_POST), 150);
43+
#[cfg(any(unchk_fail_pre, chk_fail_pre))]
44+
foo(BAZ_FAIL_PRE);
45+
#[cfg(any(unchk_fail_post, chk_fail_post))]
46+
foo(BAZ_FAIL_POST);
47+
}

0 commit comments

Comments
 (0)