Skip to content

Commit f0c7ab6

Browse files
pnkfelixcelinval
authored andcommitted
attribute-based contract syntax that desugars into the internal AST extensions added earlier.
1 parent ba21ceb commit f0c7ab6

File tree

9 files changed

+326
-0
lines changed

9 files changed

+326
-0
lines changed
Lines changed: 172 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,172 @@
1+
#![allow(unused_imports, unused_variables)]
2+
3+
use rustc_ast::token;
4+
use rustc_ast::tokenstream::{DelimSpacing, DelimSpan, Spacing, TokenStream, TokenTree};
5+
use rustc_errors::ErrorGuaranteed;
6+
use rustc_expand::base::{AttrProcMacro, ExtCtxt};
7+
use rustc_span::Span;
8+
use rustc_span::symbol::{Ident, Symbol, kw, sym};
9+
10+
pub(crate) struct ExpandRequires;
11+
12+
pub(crate) struct ExpandEnsures;
13+
14+
impl AttrProcMacro for ExpandRequires {
15+
fn expand<'cx>(
16+
&self,
17+
ecx: &'cx mut ExtCtxt<'_>,
18+
span: Span,
19+
annotation: TokenStream,
20+
annotated: TokenStream,
21+
) -> Result<TokenStream, ErrorGuaranteed> {
22+
expand_requires_tts(ecx, span, annotation, annotated)
23+
}
24+
}
25+
26+
impl AttrProcMacro for ExpandEnsures {
27+
fn expand<'cx>(
28+
&self,
29+
ecx: &'cx mut ExtCtxt<'_>,
30+
span: Span,
31+
annotation: TokenStream,
32+
annotated: TokenStream,
33+
) -> Result<TokenStream, ErrorGuaranteed> {
34+
expand_ensures_tts(ecx, span, annotation, annotated)
35+
}
36+
}
37+
38+
fn expand_injecting_circa_where_clause(
39+
_ecx: &mut ExtCtxt<'_>,
40+
attr_span: Span,
41+
annotated: TokenStream,
42+
inject: impl FnOnce(&mut Vec<TokenTree>) -> Result<(), ErrorGuaranteed>,
43+
) -> Result<TokenStream, ErrorGuaranteed> {
44+
let mut new_tts = Vec::with_capacity(annotated.len());
45+
let mut cursor = annotated.into_trees();
46+
47+
// Find the `fn name<G,...>(x:X,...)` and inject the AST contract forms right after
48+
// the formal parameters (and return type if any).
49+
while let Some(tt) = cursor.next_ref() {
50+
new_tts.push(tt.clone());
51+
if let TokenTree::Token(tok, _) = tt
52+
&& tok.is_ident_named(kw::Fn)
53+
{
54+
break;
55+
}
56+
}
57+
58+
// Found the `fn` keyword, now find the formal parameters.
59+
//
60+
// FIXME: can this fail if you have parentheticals in a generics list, like `fn foo<F: Fn(X) -> Y>` ?
61+
while let Some(tt) = cursor.next_ref() {
62+
new_tts.push(tt.clone());
63+
64+
if let TokenTree::Delimited(_, _, token::Delimiter::Parenthesis, _) = tt {
65+
break;
66+
}
67+
if let TokenTree::Token(token::Token { kind: token::TokenKind::Semi, .. }, _) = tt {
68+
panic!("contract attribute applied to fn without parameter list.");
69+
}
70+
}
71+
72+
// There *might* be a return type declaration (and figuring out where that ends would require
73+
// parsing an arbitrary type expression, e.g. `-> Foo<args ...>`
74+
//
75+
// Instead of trying to figure that out, scan ahead and look for the first occurence of a
76+
// `where`, a `{ ... }`, or a `;`.
77+
//
78+
// FIXME: this might still fall into a trap for something like `-> Ctor<T, const { 0 }>`. I
79+
// *think* such cases must be under a Delimited (e.g. `[T; { N }]` or have the braced form
80+
// prefixed by e.g. `const`, so we should still be able to filter them out without having to
81+
// parse the type expression itself. But rather than try to fix things with hacks like that,
82+
// time might be better spent extending the attribute expander to suport tt-annotation atop
83+
// ast-annotated, which would be an elegant way to sidestep all of this.
84+
let mut opt_next_tt = cursor.next_ref();
85+
while let Some(next_tt) = opt_next_tt {
86+
if let TokenTree::Token(tok, _) = next_tt
87+
&& tok.is_ident_named(kw::Where)
88+
{
89+
break;
90+
}
91+
if let TokenTree::Delimited(_, _, token::Delimiter::Brace, _) = next_tt {
92+
break;
93+
}
94+
if let TokenTree::Token(token::Token { kind: token::TokenKind::Semi, .. }, _) = next_tt {
95+
break;
96+
}
97+
98+
// for anything else, transcribe the tt and keep looking.
99+
new_tts.push(next_tt.clone());
100+
opt_next_tt = cursor.next_ref();
101+
continue;
102+
}
103+
104+
// At this point, we've transcribed everything from the `fn` through the formal parameter list
105+
// and return type declaration, (if any), but `tt` itself has *not* been transcribed.
106+
//
107+
// Now inject the AST contract form.
108+
//
109+
// FIXME: this kind of manual token tree munging does not have significant precedent among
110+
// rustc builtin macros, probably because most builtin macros use direct AST manipulation to
111+
// accomplish similar goals. But since our attributes need to take arbitrary expressions, and
112+
// our attribute infrastructure does not yet support mixing a token-tree annotation with an AST
113+
// annotated, we end up doing token tree manipulation.
114+
inject(&mut new_tts)?;
115+
116+
// Above we injected the internal AST requires/ensures contruct. Now copy over all the other
117+
// token trees.
118+
if let Some(tt) = opt_next_tt {
119+
new_tts.push(tt.clone());
120+
}
121+
while let Some(tt) = cursor.next_ref() {
122+
new_tts.push(tt.clone());
123+
}
124+
125+
Ok(TokenStream::new(new_tts))
126+
}
127+
128+
fn expand_requires_tts(
129+
_ecx: &mut ExtCtxt<'_>,
130+
attr_span: Span,
131+
annotation: TokenStream,
132+
annotated: TokenStream,
133+
) -> Result<TokenStream, ErrorGuaranteed> {
134+
expand_injecting_circa_where_clause(_ecx, attr_span, annotated, |new_tts| {
135+
new_tts.push(TokenTree::Token(
136+
token::Token::from_ast_ident(Ident::new(kw::RustcContractRequires, attr_span)),
137+
Spacing::Joint,
138+
));
139+
new_tts.push(TokenTree::Token(
140+
token::Token::new(token::TokenKind::OrOr, attr_span),
141+
Spacing::Alone,
142+
));
143+
new_tts.push(TokenTree::Delimited(
144+
DelimSpan::from_single(attr_span),
145+
DelimSpacing::new(Spacing::JointHidden, Spacing::JointHidden),
146+
token::Delimiter::Parenthesis,
147+
annotation,
148+
));
149+
Ok(())
150+
})
151+
}
152+
153+
fn expand_ensures_tts(
154+
_ecx: &mut ExtCtxt<'_>,
155+
attr_span: Span,
156+
annotation: TokenStream,
157+
annotated: TokenStream,
158+
) -> Result<TokenStream, ErrorGuaranteed> {
159+
expand_injecting_circa_where_clause(_ecx, attr_span, annotated, |new_tts| {
160+
new_tts.push(TokenTree::Token(
161+
token::Token::from_ast_ident(Ident::new(kw::RustcContractEnsures, attr_span)),
162+
Spacing::Joint,
163+
));
164+
new_tts.push(TokenTree::Delimited(
165+
DelimSpan::from_single(attr_span),
166+
DelimSpacing::new(Spacing::JointHidden, Spacing::JointHidden),
167+
token::Delimiter::Parenthesis,
168+
annotation,
169+
));
170+
Ok(())
171+
})
172+
}

compiler/rustc_builtin_macros/src/lib.rs

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -55,6 +55,7 @@ mod trace_macros;
5555

5656
pub mod asm;
5757
pub mod cmdline_attrs;
58+
pub mod contracts;
5859
pub mod proc_macro_harness;
5960
pub mod standard_library_imports;
6061
pub mod test_harness;
@@ -139,4 +140,8 @@ pub fn register_builtin_macros(resolver: &mut dyn ResolverExpand) {
139140

140141
let client = proc_macro::bridge::client::Client::expand1(proc_macro::quote);
141142
register(sym::quote, SyntaxExtensionKind::Bang(Box::new(BangProcMacro { client })));
143+
let requires = SyntaxExtensionKind::Attr(Box::new(contracts::ExpandRequires));
144+
register(sym::contracts_requires, requires);
145+
let ensures = SyntaxExtensionKind::Attr(Box::new(contracts::ExpandEnsures));
146+
register(sym::contracts_ensures, ensures);
142147
}

compiler/rustc_span/src/symbol.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -686,6 +686,8 @@ symbols! {
686686
contract_check_ensures,
687687
contract_check_requires,
688688
contract_checks,
689+
contracts_ensures,
690+
contracts_requires,
689691
convert_identity,
690692
copy,
691693
copy_closures,

library/core/src/contracts.rs

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,10 @@
11
//! Unstable module containing the unstable contracts lang items and attribute macros.
22
3+
#[cfg(not(bootstrap))]
4+
pub use crate::macros::builtin::contracts_ensures as ensures;
5+
#[cfg(not(bootstrap))]
6+
pub use crate::macros::builtin::contracts_requires as requires;
7+
38
/// Emitted by rustc as a desugaring of `#[requires(PRED)] fn foo(x: X) { ... }`
49
/// into: `fn foo(x: X) { check_requires(|| PRED) ... }`
510
#[cfg(not(bootstrap))]

library/core/src/macros/mod.rs

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1766,6 +1766,32 @@ pub(crate) mod builtin {
17661766
/* compiler built-in */
17671767
}
17681768

1769+
/// Attribute macro applied to a function to give it a post-condition.
1770+
///
1771+
/// The attribute carries an argument token-tree which is
1772+
/// eventually parsed as a unary closure expression that is
1773+
/// invoked on a reference to the return value.
1774+
#[cfg(not(bootstrap))]
1775+
#[unstable(feature = "rustc_contracts", issue = "none")]
1776+
#[allow_internal_unstable(core_intrinsics)]
1777+
#[rustc_builtin_macro]
1778+
pub macro contracts_ensures($item:item) {
1779+
/* compiler built-in */
1780+
}
1781+
1782+
/// Attribute macro applied to a function to give it a precondition.
1783+
///
1784+
/// The attribute carries an argument token-tree which is
1785+
/// eventually parsed as an boolean expression with access to the
1786+
/// function's formal parameters
1787+
#[cfg(not(bootstrap))]
1788+
#[unstable(feature = "rustc_contracts", issue = "none")]
1789+
#[allow_internal_unstable(core_intrinsics)]
1790+
#[rustc_builtin_macro]
1791+
pub macro contracts_requires($item:item) {
1792+
/* compiler built-in */
1793+
}
1794+
17691795
/// Attribute macro applied to a function to register it as a handler for allocation failure.
17701796
///
17711797
/// See also [`std::alloc::handle_alloc_error`](../../../std/alloc/fn.handle_alloc_error.html).
Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
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+
#[core::contracts::requires(x.baz > 0)]
22+
#[core::contracts::ensures(|ret| *ret > 100)]
23+
fn nest(x: Baz) -> i32
24+
{
25+
loop {
26+
return x.baz + 50;
27+
}
28+
}
29+
30+
struct Baz { baz: i32 }
31+
32+
const BAZ_PASS_PRE_POST: Baz = Baz { baz: 100 };
33+
#[cfg(any(unchk_fail_post, chk_fail_post))]
34+
const BAZ_FAIL_POST: Baz = Baz { baz: 10 };
35+
#[cfg(any(unchk_fail_pre, chk_fail_pre))]
36+
const BAZ_FAIL_PRE: Baz = Baz { baz: -10 };
37+
38+
fn main() {
39+
assert_eq!(nest(BAZ_PASS_PRE_POST), 150);
40+
#[cfg(any(unchk_fail_pre, chk_fail_pre))]
41+
nest(BAZ_FAIL_PRE);
42+
#[cfg(any(unchk_fail_post, chk_fail_post))]
43+
nest(BAZ_FAIL_POST);
44+
}
Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
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+
#[core::contracts::requires(x.baz > 0)]
22+
#[core::contracts::ensures(|ret| *ret > 100)]
23+
fn tail(x: Baz) -> i32
24+
{
25+
x.baz + 50
26+
}
27+
28+
struct Baz { baz: i32 }
29+
30+
const BAZ_PASS_PRE_POST: Baz = Baz { baz: 100 };
31+
#[cfg(any(unchk_fail_post, chk_fail_post))]
32+
const BAZ_FAIL_POST: Baz = Baz { baz: 10 };
33+
#[cfg(any(unchk_fail_pre, chk_fail_pre))]
34+
const BAZ_FAIL_PRE: Baz = Baz { baz: -10 };
35+
36+
fn main() {
37+
assert_eq!(tail(BAZ_PASS_PRE_POST), 150);
38+
#[cfg(any(unchk_fail_pre, chk_fail_pre))]
39+
tail(BAZ_FAIL_PRE);
40+
#[cfg(any(unchk_fail_post, chk_fail_post))]
41+
tail(BAZ_FAIL_POST);
42+
}
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
//@ run-pass
2+
//@ compile-flags: -Zcontract-checks=yes
3+
#![feature(rustc_contracts)]
4+
5+
#[core::contracts::ensures(|ret| *ret > 0)]
6+
fn outer() -> i32 {
7+
let inner_closure = || -> i32 { 0 };
8+
inner_closure();
9+
10
10+
}
11+
12+
fn main() {
13+
outer();
14+
}
Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
//@ run-pass
2+
//@ compile-flags: -Zcontract-checks=yes
3+
#![feature(rustc_contracts)]
4+
5+
struct Outer { outer: std::cell::Cell<i32> }
6+
7+
#[core::contracts::requires(x.outer.get() > 0)]
8+
fn outer(x: Outer) {
9+
let inner_closure = || { };
10+
x.outer.set(0);
11+
inner_closure();
12+
}
13+
14+
fn main() {
15+
outer(Outer { outer: 1.into() });
16+
}

0 commit comments

Comments
 (0)