Rollup merge of #144444 - dawidl022:contracts/variable-scoping-rebased, r=jackh726
Contract variable declarations This change adds contract variables that 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. In particular, one future use case would be for [Fulminate](https://dl.acm.org/doi/10.1145/3704879)-like ownership assertions in contracts, that are essentially side-effects, and executing them twice would alter the semantics of the contract. As of this change, `requires` can now be an arbitrary sequence of statements, with the final expression being of type `bool`. They are executed in sequence as expected, before checking if the final `bool` expression holds. This PR depends on rust-lang/rust#144438 (which has now been merged). Contracts tracking issue: https://github.com/rust-lang/rust/issues/128044 **Other changes introduced**: - Contract macros now wrap the content in braces to produce blocks, meaning there's no need to wrap the content in `{}` when using multiple statements. The change is backwards compatible, in that wrapping the content in `{}` still works as before. The macros also now treat `requires` and `ensures` uniformally, meaning the `requires` closure is built inside the parser, as opposed to in the macro. **Known limiatations**: - Contracts with variable declarations are subject to the regular borrow checking rules, and the way contracts are currently lowered limits the usefulness of contract variable declarations. Consider the below example: ```rust #[requires(let init_x = *x; true)] #[ensures(move |_| *x == 2 * init_x)] fn double_in_place(x: &mut i32) { *x *= 2; } ``` We have used the new variable declarations feature to remember the initial value pointed to by `x`, however, moving `x` into the `ensures` does not pass the borrow checker, meaning the above function contract is illegal. Ideally, something like the above should be expressable in contracts.
This commit is contained in:
@@ -3680,6 +3680,9 @@ pub struct TraitImplHeader {
|
||||
|
||||
#[derive(Clone, Encodable, Decodable, Debug, Default, Walkable)]
|
||||
pub struct FnContract {
|
||||
/// Declarations of variables accessible both in the `requires` and
|
||||
/// `ensures` clauses.
|
||||
pub declarations: ThinVec<Stmt>,
|
||||
pub requires: Option<Box<Expr>>,
|
||||
pub ensures: Option<Box<Expr>>,
|
||||
}
|
||||
|
||||
@@ -27,7 +27,7 @@ impl<'a, 'hir> LoweringContext<'a, 'hir> {
|
||||
hir::Block { hir_id, stmts, expr, rules, span: self.lower_span(b.span), targeted_by_break }
|
||||
}
|
||||
|
||||
fn lower_stmts(
|
||||
pub(super) fn lower_stmts(
|
||||
&mut self,
|
||||
mut ast_stmts: &[Stmt],
|
||||
) -> (&'hir [hir::Stmt<'hir>], Option<&'hir hir::Expr<'hir>>) {
|
||||
|
||||
@@ -18,6 +18,11 @@ impl<'a, 'hir> LoweringContext<'a, 'hir> {
|
||||
body: impl FnOnce(&mut Self) -> rustc_hir::Expr<'hir>,
|
||||
contract: &rustc_ast::FnContract,
|
||||
) -> rustc_hir::Expr<'hir> {
|
||||
// The order in which things are lowered is important! I.e to
|
||||
// refer to variables in contract_decls from postcond/precond,
|
||||
// we must lower it first!
|
||||
let contract_decls = self.lower_stmts(&contract.declarations).0;
|
||||
|
||||
match (&contract.requires, &contract.ensures) {
|
||||
(Some(req), Some(ens)) => {
|
||||
// Lower the fn contract, which turns:
|
||||
@@ -27,6 +32,7 @@ impl<'a, 'hir> LoweringContext<'a, 'hir> {
|
||||
// into:
|
||||
//
|
||||
// let __postcond = if contract_checks {
|
||||
// CONTRACT_DECLARATIONS;
|
||||
// contract_check_requires(PRECOND);
|
||||
// Some(|ret_val| POSTCOND)
|
||||
// } else {
|
||||
@@ -45,8 +51,11 @@ impl<'a, 'hir> LoweringContext<'a, 'hir> {
|
||||
let precond = self.lower_precond(req);
|
||||
let postcond_checker = self.lower_postcond_checker(ens);
|
||||
|
||||
let contract_check =
|
||||
self.lower_contract_check_with_postcond(Some(precond), postcond_checker);
|
||||
let contract_check = self.lower_contract_check_with_postcond(
|
||||
contract_decls,
|
||||
Some(precond),
|
||||
postcond_checker,
|
||||
);
|
||||
|
||||
let wrapped_body =
|
||||
self.wrap_body_with_contract_check(body, contract_check, postcond_checker.span);
|
||||
@@ -68,15 +77,15 @@ impl<'a, 'hir> LoweringContext<'a, 'hir> {
|
||||
// let ret = { body };
|
||||
//
|
||||
// if contract_checks {
|
||||
// CONTRACT_DECLARATIONS;
|
||||
// contract_check_ensures(__postcond, ret)
|
||||
// } else {
|
||||
// ret
|
||||
// }
|
||||
// }
|
||||
|
||||
let postcond_checker = self.lower_postcond_checker(ens);
|
||||
let contract_check =
|
||||
self.lower_contract_check_with_postcond(None, postcond_checker);
|
||||
self.lower_contract_check_with_postcond(contract_decls, None, postcond_checker);
|
||||
|
||||
let wrapped_body =
|
||||
self.wrap_body_with_contract_check(body, contract_check, postcond_checker.span);
|
||||
@@ -91,12 +100,13 @@ impl<'a, 'hir> LoweringContext<'a, 'hir> {
|
||||
//
|
||||
// {
|
||||
// if contracts_checks {
|
||||
// CONTRACT_DECLARATIONS;
|
||||
// contract_requires(PRECOND);
|
||||
// }
|
||||
// body
|
||||
// }
|
||||
let precond = self.lower_precond(req);
|
||||
let precond_check = self.lower_contract_check_just_precond(precond);
|
||||
let precond_check = self.lower_contract_check_just_precond(contract_decls, precond);
|
||||
|
||||
let body = self.arena.alloc(body(self));
|
||||
|
||||
@@ -145,9 +155,12 @@ impl<'a, 'hir> LoweringContext<'a, 'hir> {
|
||||
|
||||
fn lower_contract_check_just_precond(
|
||||
&mut self,
|
||||
contract_decls: &'hir [rustc_hir::Stmt<'hir>],
|
||||
precond: rustc_hir::Stmt<'hir>,
|
||||
) -> rustc_hir::Stmt<'hir> {
|
||||
let stmts = self.arena.alloc_from_iter([precond].into_iter());
|
||||
let stmts = self
|
||||
.arena
|
||||
.alloc_from_iter(contract_decls.into_iter().map(|d| *d).chain([precond].into_iter()));
|
||||
|
||||
let then_block_stmts = self.block_all(precond.span, stmts, None);
|
||||
let then_block = self.arena.alloc(self.expr_block(&then_block_stmts));
|
||||
@@ -164,10 +177,13 @@ impl<'a, 'hir> LoweringContext<'a, 'hir> {
|
||||
|
||||
fn lower_contract_check_with_postcond(
|
||||
&mut self,
|
||||
contract_decls: &'hir [rustc_hir::Stmt<'hir>],
|
||||
precond: Option<rustc_hir::Stmt<'hir>>,
|
||||
postcond_checker: &'hir rustc_hir::Expr<'hir>,
|
||||
) -> &'hir rustc_hir::Expr<'hir> {
|
||||
let stmts = self.arena.alloc_from_iter(precond.into_iter());
|
||||
let stmts = self
|
||||
.arena
|
||||
.alloc_from_iter(contract_decls.into_iter().map(|d| *d).chain(precond.into_iter()));
|
||||
let span = match precond {
|
||||
Some(precond) => precond.span,
|
||||
None => postcond_checker.span,
|
||||
|
||||
@@ -17,7 +17,7 @@ impl AttrProcMacro for ExpandRequires {
|
||||
annotation: TokenStream,
|
||||
annotated: TokenStream,
|
||||
) -> Result<TokenStream, ErrorGuaranteed> {
|
||||
expand_requires_tts(ecx, span, annotation, annotated)
|
||||
expand_contract_clause_tts(ecx, span, annotation, annotated, kw::ContractRequires)
|
||||
}
|
||||
}
|
||||
|
||||
@@ -29,7 +29,7 @@ impl AttrProcMacro for ExpandEnsures {
|
||||
annotation: TokenStream,
|
||||
annotated: TokenStream,
|
||||
) -> Result<TokenStream, ErrorGuaranteed> {
|
||||
expand_ensures_tts(ecx, span, annotation, annotated)
|
||||
expand_contract_clause_tts(ecx, span, annotation, annotated, kw::ContractEnsures)
|
||||
}
|
||||
}
|
||||
|
||||
@@ -130,42 +130,17 @@ fn expand_contract_clause(
|
||||
Ok(new_tts)
|
||||
}
|
||||
|
||||
fn expand_requires_tts(
|
||||
fn expand_contract_clause_tts(
|
||||
ecx: &mut ExtCtxt<'_>,
|
||||
attr_span: Span,
|
||||
annotation: TokenStream,
|
||||
annotated: TokenStream,
|
||||
clause_keyword: rustc_span::Symbol,
|
||||
) -> Result<TokenStream, ErrorGuaranteed> {
|
||||
let feature_span = ecx.with_def_site_ctxt(attr_span);
|
||||
expand_contract_clause(ecx, attr_span, annotated, |new_tts| {
|
||||
new_tts.push_tree(TokenTree::Token(
|
||||
token::Token::from_ast_ident(Ident::new(kw::ContractRequires, feature_span)),
|
||||
Spacing::Joint,
|
||||
));
|
||||
new_tts.push_tree(TokenTree::Token(
|
||||
token::Token::new(token::TokenKind::OrOr, attr_span),
|
||||
Spacing::Alone,
|
||||
));
|
||||
new_tts.push_tree(TokenTree::Delimited(
|
||||
DelimSpan::from_single(attr_span),
|
||||
DelimSpacing::new(Spacing::JointHidden, Spacing::JointHidden),
|
||||
token::Delimiter::Brace,
|
||||
annotation,
|
||||
));
|
||||
Ok(())
|
||||
})
|
||||
}
|
||||
|
||||
fn expand_ensures_tts(
|
||||
ecx: &mut ExtCtxt<'_>,
|
||||
attr_span: Span,
|
||||
annotation: TokenStream,
|
||||
annotated: TokenStream,
|
||||
) -> Result<TokenStream, ErrorGuaranteed> {
|
||||
let feature_span = ecx.with_def_site_ctxt(attr_span);
|
||||
expand_contract_clause(ecx, attr_span, annotated, |new_tts| {
|
||||
new_tts.push_tree(TokenTree::Token(
|
||||
token::Token::from_ast_ident(Ident::new(kw::ContractEnsures, feature_span)),
|
||||
token::Token::from_ast_ident(Ident::new(clause_keyword, feature_span)),
|
||||
Spacing::Joint,
|
||||
));
|
||||
new_tts.push_tree(TokenTree::Delimited(
|
||||
|
||||
@@ -4036,6 +4036,30 @@ impl<'a> Parser<'a> {
|
||||
self.mk_expr(span, ExprKind::Err(guar))
|
||||
}
|
||||
|
||||
pub(crate) fn mk_unit_expr(&self, span: Span) -> Box<Expr> {
|
||||
self.mk_expr(span, ExprKind::Tup(Default::default()))
|
||||
}
|
||||
|
||||
pub(crate) fn mk_closure_expr(&self, span: Span, body: Box<Expr>) -> Box<Expr> {
|
||||
self.mk_expr(
|
||||
span,
|
||||
ast::ExprKind::Closure(Box::new(ast::Closure {
|
||||
binder: rustc_ast::ClosureBinder::NotPresent,
|
||||
constness: rustc_ast::Const::No,
|
||||
movability: rustc_ast::Movability::Movable,
|
||||
capture_clause: rustc_ast::CaptureBy::Ref,
|
||||
coroutine_kind: None,
|
||||
fn_decl: Box::new(rustc_ast::FnDecl {
|
||||
inputs: Default::default(),
|
||||
output: rustc_ast::FnRetTy::Default(span),
|
||||
}),
|
||||
fn_arg_span: span,
|
||||
fn_decl_span: span,
|
||||
body,
|
||||
})),
|
||||
)
|
||||
}
|
||||
|
||||
/// Create expression span ensuring the span of the parent node
|
||||
/// is larger than the span of lhs and rhs, including the attributes.
|
||||
fn mk_expr_sp(&self, lhs: &Box<Expr>, lhs_span: Span, op_span: Span, rhs_span: Span) -> Span {
|
||||
|
||||
@@ -312,25 +312,48 @@ impl<'a> Parser<'a> {
|
||||
/// Parses an experimental fn contract
|
||||
/// (`contract_requires(WWW) contract_ensures(ZZZ)`)
|
||||
pub(super) fn parse_contract(&mut self) -> PResult<'a, Option<Box<ast::FnContract>>> {
|
||||
let requires = if self.eat_keyword_noexpect(exp!(ContractRequires).kw) {
|
||||
self.psess.gated_spans.gate(sym::contracts_internals, self.prev_token.span);
|
||||
let precond = self.parse_expr()?;
|
||||
Some(precond)
|
||||
let (declarations, requires) = self.parse_contract_requires()?;
|
||||
let ensures = self.parse_contract_ensures()?;
|
||||
|
||||
if requires.is_none() && ensures.is_none() {
|
||||
Ok(None)
|
||||
} else {
|
||||
None
|
||||
};
|
||||
let ensures = if self.eat_keyword_noexpect(exp!(ContractEnsures).kw) {
|
||||
Ok(Some(Box::new(ast::FnContract { declarations, requires, ensures })))
|
||||
}
|
||||
}
|
||||
|
||||
fn parse_contract_requires(
|
||||
&mut self,
|
||||
) -> PResult<'a, (ThinVec<rustc_ast::Stmt>, Option<Box<rustc_ast::Expr>>)> {
|
||||
Ok(if self.eat_keyword_noexpect(exp!(ContractRequires).kw) {
|
||||
self.psess.gated_spans.gate(sym::contracts_internals, self.prev_token.span);
|
||||
let mut decls_and_precond = self.parse_block()?;
|
||||
|
||||
let precond = match decls_and_precond.stmts.pop() {
|
||||
Some(precond) => match precond.kind {
|
||||
rustc_ast::StmtKind::Expr(expr) => expr,
|
||||
// Insert dummy node that will be rejected by typechecker to
|
||||
// avoid reinventing an error
|
||||
_ => self.mk_unit_expr(decls_and_precond.span),
|
||||
},
|
||||
None => self.mk_unit_expr(decls_and_precond.span),
|
||||
};
|
||||
let precond = self.mk_closure_expr(precond.span, precond);
|
||||
let decls = decls_and_precond.stmts;
|
||||
(decls, Some(precond))
|
||||
} else {
|
||||
(Default::default(), None)
|
||||
})
|
||||
}
|
||||
|
||||
fn parse_contract_ensures(&mut self) -> PResult<'a, Option<Box<rustc_ast::Expr>>> {
|
||||
Ok(if self.eat_keyword_noexpect(exp!(ContractEnsures).kw) {
|
||||
self.psess.gated_spans.gate(sym::contracts_internals, self.prev_token.span);
|
||||
let postcond = self.parse_expr()?;
|
||||
Some(postcond)
|
||||
} else {
|
||||
None
|
||||
};
|
||||
if requires.is_none() && ensures.is_none() {
|
||||
Ok(None)
|
||||
} else {
|
||||
Ok(Some(Box::new(ast::FnContract { requires, ensures })))
|
||||
}
|
||||
})
|
||||
}
|
||||
|
||||
/// Parses an optional where-clause.
|
||||
|
||||
Reference in New Issue
Block a user