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.
This commit is contained in:
Dawid Lachowicz
2025-07-11 15:34:40 +01:00
parent a41214f9bd
commit aeae085dc3
27 changed files with 326 additions and 62 deletions

View File

@@ -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 {

View File

@@ -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.