Skip to content

Commit 68621b6

Browse files
committed
Add contract variable declarations
Contract variables can be declared in the `requires` clause and can be referenced both in `requires` and `ensures`, subject to usual borrow checking rules. This allows any setup common to both the `requires` and `ensures` clauses to only be done once.
1 parent b606b49 commit 68621b6

28 files changed

+338
-65
lines changed

compiler/rustc_ast/src/ast.rs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3774,6 +3774,9 @@ pub struct Impl {
37743774

37753775
#[derive(Clone, Encodable, Decodable, Debug, Default, Walkable)]
37763776
pub struct FnContract {
3777+
/// Declarations of variables accessible both in the [requires] and
3778+
/// [ensures] clauses.
3779+
pub declarations: ThinVec<Stmt>,
37773780
pub requires: Option<P<Expr>>,
37783781
pub ensures: Option<P<Expr>>,
37793782
}

compiler/rustc_ast_lowering/src/block.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ impl<'a, 'hir> LoweringContext<'a, 'hir> {
2626
hir::Block { hir_id, stmts, expr, rules, span: self.lower_span(b.span), targeted_by_break }
2727
}
2828

29-
fn lower_stmts(
29+
pub(super) fn lower_stmts(
3030
&mut self,
3131
mut ast_stmts: &[Stmt],
3232
) -> (&'hir [hir::Stmt<'hir>], Option<&'hir hir::Expr<'hir>>) {

compiler/rustc_ast_lowering/src/contract.rs

Lines changed: 23 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,11 @@ impl<'a, 'hir> LoweringContext<'a, 'hir> {
66
body: impl FnOnce(&mut Self) -> rustc_hir::Expr<'hir>,
77
contract: &rustc_ast::FnContract,
88
) -> rustc_hir::Expr<'hir> {
9+
// The order in which things are lowered is important! I.e to
10+
// refer to variables in contract_decls from postcond/precond,
11+
// we must lower it first!
12+
let contract_decls = self.lower_stmts(&contract.declarations).0;
13+
914
match (&contract.requires, &contract.ensures) {
1015
(Some(req), Some(ens)) => {
1116
// Lower the fn contract, which turns:
@@ -16,6 +21,7 @@ impl<'a, 'hir> LoweringContext<'a, 'hir> {
1621
//
1722
// {
1823
// let __postcond = if contracts_checks() {
24+
// CONTRACT_DECLARATIONS;
1925
// contract_check_requires(PRECOND);
2026
// Some(|ret_val| POSTCOND)
2127
// } else {
@@ -27,8 +33,11 @@ impl<'a, 'hir> LoweringContext<'a, 'hir> {
2733
let precond = self.lower_precond(req);
2834
let postcond_checker = self.lower_postcond_checker(ens);
2935

30-
let contract_check =
31-
self.lower_contract_check_with_postcond(Some(precond), postcond_checker);
36+
let contract_check = self.lower_contract_check_with_postcond(
37+
contract_decls,
38+
Some(precond),
39+
postcond_checker,
40+
);
3241

3342
let wrapped_body =
3443
self.wrap_body_with_contract_check(body, contract_check, postcond_checker.span);
@@ -43,16 +52,13 @@ impl<'a, 'hir> LoweringContext<'a, 'hir> {
4352
//
4453
// {
4554
// let __postcond = if contracts_check() {
55+
// CONTRACT_DECLARATIONS;
4656
// Some(|ret_val| POSTCOND)
4757
// } else {
4858
// None
4959
// };
50-
// __postcond({ body })
51-
// }
52-
53-
let postcond_checker = self.lower_postcond_checker(ens);
5460
let contract_check =
55-
self.lower_contract_check_with_postcond(None, postcond_checker);
61+
self.lower_contract_check_with_postcond(contract_decls, None, postcond_checker);
5662

5763
let wrapped_body =
5864
self.wrap_body_with_contract_check(body, contract_check, postcond_checker.span);
@@ -67,12 +73,13 @@ impl<'a, 'hir> LoweringContext<'a, 'hir> {
6773
//
6874
// {
6975
// if contracts_check() {
76+
// CONTRACT_DECLARATIONS;
7077
// contract_requires(PRECOND);
7178
// }
7279
// body
7380
// }
7481
let precond = self.lower_precond(req);
75-
let precond_check = self.lower_contract_check_just_precond(precond);
82+
let precond_check = self.lower_contract_check_just_precond(contract_decls, precond);
7683

7784
let body = self.arena.alloc(body(self));
7885

@@ -121,9 +128,12 @@ impl<'a, 'hir> LoweringContext<'a, 'hir> {
121128

122129
fn lower_contract_check_just_precond(
123130
&mut self,
131+
contract_decls: &'hir [rustc_hir::Stmt<'hir>],
124132
precond: rustc_hir::Stmt<'hir>,
125133
) -> rustc_hir::Stmt<'hir> {
126-
let stmts = self.arena.alloc_from_iter([precond].into_iter());
134+
let stmts = self
135+
.arena
136+
.alloc_from_iter(contract_decls.into_iter().map(|d| *d).chain([precond].into_iter()));
127137

128138
let then_block_stmts = self.block_all(precond.span, stmts, None);
129139
let then_block = self.arena.alloc(self.expr_block(&then_block_stmts));
@@ -144,10 +154,13 @@ impl<'a, 'hir> LoweringContext<'a, 'hir> {
144154

145155
fn lower_contract_check_with_postcond(
146156
&mut self,
157+
contract_decls: &'hir [rustc_hir::Stmt<'hir>],
147158
precond: Option<rustc_hir::Stmt<'hir>>,
148159
postcond_checker: &'hir rustc_hir::Expr<'hir>,
149160
) -> &'hir rustc_hir::Expr<'hir> {
150-
let stmts = self.arena.alloc_from_iter(precond.into_iter());
161+
let stmts = self
162+
.arena
163+
.alloc_from_iter(contract_decls.into_iter().map(|d| *d).chain(precond.into_iter()));
151164
let span = match precond {
152165
Some(precond) => precond.span,
153166
None => postcond_checker.span,

compiler/rustc_builtin_macros/src/contracts.rs

Lines changed: 6 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ impl AttrProcMacro for ExpandRequires {
1717
annotation: TokenStream,
1818
annotated: TokenStream,
1919
) -> Result<TokenStream, ErrorGuaranteed> {
20-
expand_requires_tts(ecx, span, annotation, annotated)
20+
expand_contract_clause_tts(ecx, span, annotation, annotated, kw::ContractRequires)
2121
}
2222
}
2323

@@ -29,7 +29,7 @@ impl AttrProcMacro for ExpandEnsures {
2929
annotation: TokenStream,
3030
annotated: TokenStream,
3131
) -> Result<TokenStream, ErrorGuaranteed> {
32-
expand_ensures_tts(ecx, span, annotation, annotated)
32+
expand_contract_clause_tts(ecx, span, annotation, annotated, kw::ContractEnsures)
3333
}
3434
}
3535

@@ -122,48 +122,23 @@ fn expand_contract_clause(
122122
Ok(new_tts)
123123
}
124124

125-
fn expand_requires_tts(
125+
fn expand_contract_clause_tts(
126126
ecx: &mut ExtCtxt<'_>,
127127
attr_span: Span,
128128
annotation: TokenStream,
129129
annotated: TokenStream,
130+
clause_keyword: rustc_span::Symbol,
130131
) -> Result<TokenStream, ErrorGuaranteed> {
131132
let feature_span = ecx.with_def_site_ctxt(attr_span);
132133
expand_contract_clause(ecx, attr_span, annotated, |new_tts| {
133134
new_tts.push_tree(TokenTree::Token(
134-
token::Token::from_ast_ident(Ident::new(kw::ContractRequires, feature_span)),
135-
Spacing::Joint,
136-
));
137-
new_tts.push_tree(TokenTree::Token(
138-
token::Token::new(token::TokenKind::OrOr, attr_span),
139-
Spacing::Alone,
140-
));
141-
new_tts.push_tree(TokenTree::Delimited(
142-
DelimSpan::from_single(attr_span),
143-
DelimSpacing::new(Spacing::JointHidden, Spacing::JointHidden),
144-
token::Delimiter::Parenthesis,
145-
annotation,
146-
));
147-
Ok(())
148-
})
149-
}
150-
151-
fn expand_ensures_tts(
152-
ecx: &mut ExtCtxt<'_>,
153-
attr_span: Span,
154-
annotation: TokenStream,
155-
annotated: TokenStream,
156-
) -> Result<TokenStream, ErrorGuaranteed> {
157-
let feature_span = ecx.with_def_site_ctxt(attr_span);
158-
expand_contract_clause(ecx, attr_span, annotated, |new_tts| {
159-
new_tts.push_tree(TokenTree::Token(
160-
token::Token::from_ast_ident(Ident::new(kw::ContractEnsures, feature_span)),
135+
token::Token::from_ast_ident(Ident::new(clause_keyword, feature_span)),
161136
Spacing::Joint,
162137
));
163138
new_tts.push_tree(TokenTree::Delimited(
164139
DelimSpan::from_single(attr_span),
165140
DelimSpacing::new(Spacing::JointHidden, Spacing::JointHidden),
166-
token::Delimiter::Parenthesis,
141+
token::Delimiter::Brace,
167142
annotation,
168143
));
169144
Ok(())

compiler/rustc_parse/src/parser/expr.rs

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3999,6 +3999,30 @@ impl<'a> Parser<'a> {
39993999
self.mk_expr(span, ExprKind::Err(guar))
40004000
}
40014001

4002+
pub(crate) fn mk_unit_expr(&self, span: Span) -> P<Expr> {
4003+
self.mk_expr(span, ExprKind::Tup(Default::default()))
4004+
}
4005+
4006+
pub(crate) fn mk_closure_expr(&self, span: Span, body: P<Expr>) -> P<Expr> {
4007+
self.mk_expr(
4008+
span,
4009+
ast::ExprKind::Closure(Box::new(ast::Closure {
4010+
binder: rustc_ast::ClosureBinder::NotPresent,
4011+
constness: rustc_ast::Const::No,
4012+
movability: rustc_ast::Movability::Movable,
4013+
capture_clause: rustc_ast::CaptureBy::Ref,
4014+
coroutine_kind: None,
4015+
fn_decl: Box::new(rustc_ast::FnDecl {
4016+
inputs: Default::default(),
4017+
output: rustc_ast::FnRetTy::Default(span),
4018+
}),
4019+
fn_arg_span: span,
4020+
fn_decl_span: span,
4021+
body,
4022+
})),
4023+
)
4024+
}
4025+
40024026
/// Create expression span ensuring the span of the parent node
40034027
/// is larger than the span of lhs and rhs, including the attributes.
40044028
fn mk_expr_sp(&self, lhs: &P<Expr>, lhs_span: Span, rhs_span: Span) -> Span {

compiler/rustc_parse/src/parser/generics.rs

Lines changed: 35 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -311,25 +311,48 @@ impl<'a> Parser<'a> {
311311
pub(super) fn parse_contract(
312312
&mut self,
313313
) -> PResult<'a, Option<rustc_ast::ptr::P<ast::FnContract>>> {
314-
let requires = if self.eat_keyword_noexpect(exp!(ContractRequires).kw) {
314+
let (declarations, requires) = self.parse_contract_requires()?;
315+
let ensures = self.parse_contract_ensures()?;
316+
317+
if requires.is_none() && ensures.is_none() {
318+
Ok(None)
319+
} else {
320+
Ok(Some(rustc_ast::ptr::P(ast::FnContract { declarations, requires, ensures })))
321+
}
322+
}
323+
324+
fn parse_contract_requires(
325+
&mut self,
326+
) -> PResult<'a, (ThinVec<rustc_ast::Stmt>, Option<Box<rustc_ast::Expr>>)> {
327+
Ok(if self.eat_keyword_noexpect(exp!(ContractRequires).kw) {
315328
self.psess.gated_spans.gate(sym::contracts_internals, self.prev_token.span);
316-
let precond = self.parse_expr()?;
317-
Some(precond)
329+
let mut decls_and_precond = self.parse_block()?;
330+
331+
let precond = match decls_and_precond.stmts.pop() {
332+
Some(precond) => match precond.kind {
333+
rustc_ast::StmtKind::Expr(expr) => expr,
334+
// Insert dummy node that will be rejected by typechecker to
335+
// avoid reinventing an error
336+
_ => self.mk_unit_expr(decls_and_precond.span),
337+
},
338+
None => self.mk_unit_expr(decls_and_precond.span),
339+
};
340+
let precond = self.mk_closure_expr(precond.span, precond);
341+
let decls = decls_and_precond.stmts;
342+
(decls, Some(precond))
318343
} else {
319-
None
320-
};
321-
let ensures = if self.eat_keyword_noexpect(exp!(ContractEnsures).kw) {
344+
(Default::default(), None)
345+
})
346+
}
347+
348+
fn parse_contract_ensures(&mut self) -> PResult<'a, Option<Box<rustc_ast::Expr>>> {
349+
Ok(if self.eat_keyword_noexpect(exp!(ContractEnsures).kw) {
322350
self.psess.gated_spans.gate(sym::contracts_internals, self.prev_token.span);
323351
let postcond = self.parse_expr()?;
324352
Some(postcond)
325353
} else {
326354
None
327-
};
328-
if requires.is_none() && ensures.is_none() {
329-
Ok(None)
330-
} else {
331-
Ok(Some(rustc_ast::ptr::P(ast::FnContract { requires, ensures })))
332-
}
355+
})
333356
}
334357

335358
/// Parses an optional where-clause.
Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
//@ run-pass
2+
#![feature(contracts)]
3+
//~^ WARN the feature `contracts` is incomplete and may not be safe to use and/or cause compiler crashes [incomplete_features]
4+
5+
extern crate core;
6+
use core::contracts::requires;
7+
8+
#[requires(*x = 0; true)]
9+
fn buggy_add(x: &mut u32, y: u32) {
10+
*x = *x + y;
11+
}
12+
13+
fn main() {
14+
let mut x = 10;
15+
buggy_add(&mut x, 100);
16+
assert_eq!(x, 110);
17+
}
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
warning: the feature `contracts` is incomplete and may not be safe to use and/or cause compiler crashes
2+
--> $DIR/contracts-disabled-side-effect-declarations.rs:2:12
3+
|
4+
LL | #![feature(contracts)]
5+
| ^^^^^^^^^
6+
|
7+
= note: see issue #128044 <https://github.com/rust-lang/rust/issues/128044> for more information
8+
= note: `#[warn(incomplete_features)]` on by default
9+
10+
warning: 1 warning emitted
11+

tests/ui/contracts/contracts-disabled-side-effect-ensures.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
extern crate core;
66
use core::contracts::ensures;
77

8-
#[ensures({*x = 0; |_ret| true})]
8+
#[ensures(*x = 0; |_ret| true)]
99
fn buggy_add(x: &mut u32, y: u32) {
1010
*x = *x + y;
1111
}
Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
//@ run-pass
2+
//@ compile-flags: -Zcontract-checks=yes
3+
#![feature(contracts)]
4+
//~^ WARN the feature `contracts` is incomplete and may not be safe to use and/or cause compiler crashes [incomplete_features]
5+
6+
extern crate core;
7+
use core::contracts::{ensures, requires};
8+
9+
// checks that variable declarations are lowered properly, with the ability to
10+
// access function parameters
11+
#[requires(let y = 2 * x; true)]
12+
#[ensures(move |ret| { *ret == y })]
13+
fn foo(x: u32) -> u32 {
14+
x * 2
15+
}
16+
17+
fn main() {
18+
foo(1);
19+
}

0 commit comments

Comments
 (0)