Skip to content

Commit aeae085

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 a41214f commit aeae085

27 files changed

+325
-61
lines changed

compiler/rustc_ast/src/ast.rs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3700,6 +3700,9 @@ pub struct TraitImplHeader {
37003700

37013701
#[derive(Clone, Encodable, Decodable, Debug, Default, Walkable)]
37023702
pub struct FnContract {
3703+
/// Declarations of variables accessible both in the `requires` and
3704+
/// `ensures` clauses.
3705+
pub declarations: ThinVec<Stmt>,
37033706
pub requires: Option<Box<Expr>>,
37043707
pub ensures: Option<Box<Expr>>,
37053708
}

compiler/rustc_ast_lowering/src/block.rs

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

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

compiler/rustc_ast_lowering/src/contract.rs

Lines changed: 23 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,11 @@ impl<'a, 'hir> LoweringContext<'a, 'hir> {
1818
body: impl FnOnce(&mut Self) -> rustc_hir::Expr<'hir>,
1919
contract: &rustc_ast::FnContract,
2020
) -> rustc_hir::Expr<'hir> {
21+
// The order in which things are lowered is important! I.e to
22+
// refer to variables in contract_decls from postcond/precond,
23+
// we must lower it first!
24+
let contract_decls = self.lower_stmts(&contract.declarations).0;
25+
2126
match (&contract.requires, &contract.ensures) {
2227
(Some(req), Some(ens)) => {
2328
// Lower the fn contract, which turns:
@@ -27,6 +32,7 @@ impl<'a, 'hir> LoweringContext<'a, 'hir> {
2732
// into:
2833
//
2934
// let __postcond = if contract_checks {
35+
// CONTRACT_DECLARATIONS;
3036
// contract_check_requires(PRECOND);
3137
// Some(|ret_val| POSTCOND)
3238
// } else {
@@ -45,8 +51,11 @@ impl<'a, 'hir> LoweringContext<'a, 'hir> {
4551
let precond = self.lower_precond(req);
4652
let postcond_checker = self.lower_postcond_checker(ens);
4753

48-
let contract_check =
49-
self.lower_contract_check_with_postcond(Some(precond), postcond_checker);
54+
let contract_check = self.lower_contract_check_with_postcond(
55+
contract_decls,
56+
Some(precond),
57+
postcond_checker,
58+
);
5059

5160
let wrapped_body =
5261
self.wrap_body_with_contract_check(body, contract_check, postcond_checker.span);
@@ -68,15 +77,15 @@ impl<'a, 'hir> LoweringContext<'a, 'hir> {
6877
// let ret = { body };
6978
//
7079
// if contract_checks {
80+
// CONTRACT_DECLARATIONS;
7181
// contract_check_ensures(__postcond, ret)
7282
// } else {
7383
// ret
7484
// }
7585
// }
76-
7786
let postcond_checker = self.lower_postcond_checker(ens);
7887
let contract_check =
79-
self.lower_contract_check_with_postcond(None, postcond_checker);
88+
self.lower_contract_check_with_postcond(contract_decls, None, postcond_checker);
8089

8190
let wrapped_body =
8291
self.wrap_body_with_contract_check(body, contract_check, postcond_checker.span);
@@ -91,12 +100,13 @@ impl<'a, 'hir> LoweringContext<'a, 'hir> {
91100
//
92101
// {
93102
// if contracts_checks {
103+
// CONTRACT_DECLARATIONS;
94104
// contract_requires(PRECOND);
95105
// }
96106
// body
97107
// }
98108
let precond = self.lower_precond(req);
99-
let precond_check = self.lower_contract_check_just_precond(precond);
109+
let precond_check = self.lower_contract_check_just_precond(contract_decls, precond);
100110

101111
let body = self.arena.alloc(body(self));
102112

@@ -145,9 +155,12 @@ impl<'a, 'hir> LoweringContext<'a, 'hir> {
145155

146156
fn lower_contract_check_just_precond(
147157
&mut self,
158+
contract_decls: &'hir [rustc_hir::Stmt<'hir>],
148159
precond: rustc_hir::Stmt<'hir>,
149160
) -> rustc_hir::Stmt<'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

152165
let then_block_stmts = self.block_all(precond.span, stmts, None);
153166
let then_block = self.arena.alloc(self.expr_block(&then_block_stmts));
@@ -164,10 +177,13 @@ impl<'a, 'hir> LoweringContext<'a, 'hir> {
164177

165178
fn lower_contract_check_with_postcond(
166179
&mut self,
180+
contract_decls: &'hir [rustc_hir::Stmt<'hir>],
167181
precond: Option<rustc_hir::Stmt<'hir>>,
168182
postcond_checker: &'hir rustc_hir::Expr<'hir>,
169183
) -> &'hir rustc_hir::Expr<'hir> {
170-
let stmts = self.arena.alloc_from_iter(precond.into_iter());
184+
let stmts = self
185+
.arena
186+
.alloc_from_iter(contract_decls.into_iter().map(|d| *d).chain(precond.into_iter()));
171187
let span = match precond {
172188
Some(precond) => precond.span,
173189
None => postcond_checker.span,

compiler/rustc_builtin_macros/src/contracts.rs

Lines changed: 5 additions & 30 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

@@ -130,42 +130,17 @@ fn expand_contract_clause(
130130
Ok(new_tts)
131131
}
132132

133-
fn expand_requires_tts(
133+
fn expand_contract_clause_tts(
134134
ecx: &mut ExtCtxt<'_>,
135135
attr_span: Span,
136136
annotation: TokenStream,
137137
annotated: TokenStream,
138+
clause_keyword: rustc_span::Symbol,
138139
) -> Result<TokenStream, ErrorGuaranteed> {
139140
let feature_span = ecx.with_def_site_ctxt(attr_span);
140141
expand_contract_clause(ecx, attr_span, annotated, |new_tts| {
141142
new_tts.push_tree(TokenTree::Token(
142-
token::Token::from_ast_ident(Ident::new(kw::ContractRequires, feature_span)),
143-
Spacing::Joint,
144-
));
145-
new_tts.push_tree(TokenTree::Token(
146-
token::Token::new(token::TokenKind::OrOr, attr_span),
147-
Spacing::Alone,
148-
));
149-
new_tts.push_tree(TokenTree::Delimited(
150-
DelimSpan::from_single(attr_span),
151-
DelimSpacing::new(Spacing::JointHidden, Spacing::JointHidden),
152-
token::Delimiter::Brace,
153-
annotation,
154-
));
155-
Ok(())
156-
})
157-
}
158-
159-
fn expand_ensures_tts(
160-
ecx: &mut ExtCtxt<'_>,
161-
attr_span: Span,
162-
annotation: TokenStream,
163-
annotated: TokenStream,
164-
) -> Result<TokenStream, ErrorGuaranteed> {
165-
let feature_span = ecx.with_def_site_ctxt(attr_span);
166-
expand_contract_clause(ecx, attr_span, annotated, |new_tts| {
167-
new_tts.push_tree(TokenTree::Token(
168-
token::Token::from_ast_ident(Ident::new(kw::ContractEnsures, feature_span)),
143+
token::Token::from_ast_ident(Ident::new(clause_keyword, feature_span)),
169144
Spacing::Joint,
170145
));
171146
new_tts.push_tree(TokenTree::Delimited(

compiler/rustc_parse/src/parser/expr.rs

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

4039+
pub(crate) fn mk_unit_expr(&self, span: Span) -> Box<Expr> {
4040+
self.mk_expr(span, ExprKind::Tup(Default::default()))
4041+
}
4042+
4043+
pub(crate) fn mk_closure_expr(&self, span: Span, body: Box<Expr>) -> Box<Expr> {
4044+
self.mk_expr(
4045+
span,
4046+
ast::ExprKind::Closure(Box::new(ast::Closure {
4047+
binder: rustc_ast::ClosureBinder::NotPresent,
4048+
constness: rustc_ast::Const::No,
4049+
movability: rustc_ast::Movability::Movable,
4050+
capture_clause: rustc_ast::CaptureBy::Ref,
4051+
coroutine_kind: None,
4052+
fn_decl: Box::new(rustc_ast::FnDecl {
4053+
inputs: Default::default(),
4054+
output: rustc_ast::FnRetTy::Default(span),
4055+
}),
4056+
fn_arg_span: span,
4057+
fn_decl_span: span,
4058+
body,
4059+
})),
4060+
)
4061+
}
4062+
40394063
/// Create expression span ensuring the span of the parent node
40404064
/// is larger than the span of lhs and rhs, including the attributes.
40414065
fn mk_expr_sp(&self, lhs: &Box<Expr>, lhs_span: Span, op_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
@@ -312,25 +312,48 @@ impl<'a> Parser<'a> {
312312
/// Parses an experimental fn contract
313313
/// (`contract_requires(WWW) contract_ensures(ZZZ)`)
314314
pub(super) fn parse_contract(&mut self) -> PResult<'a, Option<Box<ast::FnContract>>> {
315-
let requires = if self.eat_keyword_noexpect(exp!(ContractRequires).kw) {
315+
let (declarations, requires) = self.parse_contract_requires()?;
316+
let ensures = self.parse_contract_ensures()?;
317+
318+
if requires.is_none() && ensures.is_none() {
319+
Ok(None)
320+
} else {
321+
Ok(Some(Box::new(ast::FnContract { declarations, requires, ensures })))
322+
}
323+
}
324+
325+
fn parse_contract_requires(
326+
&mut self,
327+
) -> PResult<'a, (ThinVec<rustc_ast::Stmt>, Option<Box<rustc_ast::Expr>>)> {
328+
Ok(if self.eat_keyword_noexpect(exp!(ContractRequires).kw) {
316329
self.psess.gated_spans.gate(sym::contracts_internals, self.prev_token.span);
317-
let precond = self.parse_expr()?;
318-
Some(precond)
330+
let mut decls_and_precond = self.parse_block()?;
331+
332+
let precond = match decls_and_precond.stmts.pop() {
333+
Some(precond) => match precond.kind {
334+
rustc_ast::StmtKind::Expr(expr) => expr,
335+
// Insert dummy node that will be rejected by typechecker to
336+
// avoid reinventing an error
337+
_ => self.mk_unit_expr(decls_and_precond.span),
338+
},
339+
None => self.mk_unit_expr(decls_and_precond.span),
340+
};
341+
let precond = self.mk_closure_expr(precond.span, precond);
342+
let decls = decls_and_precond.stmts;
343+
(decls, Some(precond))
319344
} else {
320-
None
321-
};
322-
let ensures = if self.eat_keyword_noexpect(exp!(ContractEnsures).kw) {
345+
(Default::default(), None)
346+
})
347+
}
348+
349+
fn parse_contract_ensures(&mut self) -> PResult<'a, Option<Box<rustc_ast::Expr>>> {
350+
Ok(if self.eat_keyword_noexpect(exp!(ContractEnsures).kw) {
323351
self.psess.gated_spans.gate(sym::contracts_internals, self.prev_token.span);
324352
let postcond = self.parse_expr()?;
325353
Some(postcond)
326354
} else {
327355
None
328-
};
329-
if requires.is_none() && ensures.is_none() {
330-
Ok(None)
331-
} else {
332-
Ok(Some(Box::new(ast::FnContract { requires, ensures })))
333-
}
356+
})
334357
}
335358

336359
/// 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)