Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions compiler/rustc_ast/src/ast.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3700,6 +3700,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>>,
}
Expand Down
2 changes: 1 addition & 1 deletion compiler/rustc_ast_lowering/src/block.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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>>) {
Expand Down
30 changes: 23 additions & 7 deletions compiler/rustc_ast_lowering/src/contract.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand All @@ -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 {
Expand All @@ -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);
Expand All @@ -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);
Expand All @@ -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));

Expand Down Expand Up @@ -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));
Expand All @@ -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,
Expand Down
35 changes: 5 additions & 30 deletions compiler/rustc_builtin_macros/src/contracts.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
}
}

Expand All @@ -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)
}
}

Expand Down Expand Up @@ -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(
Expand Down
24 changes: 24 additions & 0 deletions compiler/rustc_parse/src/parser/expr.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down
47 changes: 35 additions & 12 deletions compiler/rustc_parse/src/parser/generics.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
let (declarations, requires) = self.parse_contract_requires()?;
let ensures = self.parse_contract_ensures()?;

if requires.is_none() && ensures.is_none() {
Ok(None)
} else {
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 precond = self.parse_expr()?;
Some(precond)
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 {
None
};
let ensures = if self.eat_keyword_noexpect(exp!(ContractEnsures).kw) {
(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.
Expand Down
17 changes: 17 additions & 0 deletions tests/ui/contracts/contracts-disabled-side-effect-declarations.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
//@ run-pass
#![feature(contracts)]
//~^ WARN the feature `contracts` is incomplete and may not be safe to use and/or cause compiler crashes [incomplete_features]

extern crate core;
use core::contracts::requires;

#[requires(*x = 0; true)]
fn buggy_add(x: &mut u32, y: u32) {
*x = *x + y;
}

fn main() {
let mut x = 10;
buggy_add(&mut x, 100);
assert_eq!(x, 110);
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
warning: the feature `contracts` is incomplete and may not be safe to use and/or cause compiler crashes
--> $DIR/contracts-disabled-side-effect-declarations.rs:2:12
|
LL | #![feature(contracts)]
| ^^^^^^^^^
|
= note: see issue #128044 <https://github.com/rust-lang/rust/issues/128044> for more information
= note: `#[warn(incomplete_features)]` on by default

warning: 1 warning emitted

Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
extern crate core;
use core::contracts::ensures;

#[ensures({*x = 0; |_ret| true})]
#[ensures(*x = 0; |_ret| true)]
fn buggy_add(x: &mut u32, y: u32) {
*x = *x + y;
}
Expand Down
19 changes: 19 additions & 0 deletions tests/ui/contracts/declared-vars-referring-to-params.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
//@ run-pass
//@ compile-flags: -Zcontract-checks=yes
#![feature(contracts)]
//~^ WARN the feature `contracts` is incomplete and may not be safe to use and/or cause compiler crashes [incomplete_features]

extern crate core;
use core::contracts::{ensures, requires};

// checks that variable declarations are lowered properly, with the ability to
// access function parameters
#[requires(let y = 2 * x; true)]
#[ensures(move |ret| { *ret == y })]
fn foo(x: u32) -> u32 {
x * 2
}

fn main() {
foo(1);
}
11 changes: 11 additions & 0 deletions tests/ui/contracts/declared-vars-referring-to-params.stderr
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
warning: the feature `contracts` is incomplete and may not be safe to use and/or cause compiler crashes
--> $DIR/declared-vars-referring-to-params.rs:3:12
|
LL | #![feature(contracts)]
| ^^^^^^^^^
|
= note: see issue #128044 <https://github.com/rust-lang/rust/issues/128044> for more information
= note: `#[warn(incomplete_features)]` on by default

warning: 1 warning emitted

17 changes: 17 additions & 0 deletions tests/ui/contracts/declared-vars-used-in-ensures.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
//@ run-pass
//@ compile-flags: -Zcontract-checks=yes
#![feature(contracts)]
//~^ WARN the feature `contracts` is incomplete and may not be safe to use and/or cause compiler crashes [incomplete_features]

extern crate core;
use core::contracts::{ensures, requires};

#[requires(let y = 1; true)]
#[ensures(move |_ret| { y == 1 })]
fn foo(x: u32) -> u32 {
x * 2
}

fn main() {
foo(1);
}
11 changes: 11 additions & 0 deletions tests/ui/contracts/declared-vars-used-in-ensures.stderr
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
warning: the feature `contracts` is incomplete and may not be safe to use and/or cause compiler crashes
--> $DIR/declared-vars-used-in-ensures.rs:3:12
|
LL | #![feature(contracts)]
| ^^^^^^^^^
|
= note: see issue #128044 <https://github.com/rust-lang/rust/issues/128044> for more information
= note: `#[warn(incomplete_features)]` on by default

warning: 1 warning emitted

19 changes: 19 additions & 0 deletions tests/ui/contracts/declared-vars-used-in-requires-and-ensures.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
//@ run-pass
//@ compile-flags: -Zcontract-checks=yes
#![feature(contracts)]
//~^ WARN the feature `contracts` is incomplete and may not be safe to use and/or cause compiler crashes [incomplete_features]

extern crate core;
use core::contracts::{ensures, requires};

// checks that variable declarations are lowered properly, with the ability to
// refer to them *both* in requires and ensures
#[requires(let y = 2 * x; y > 0)]
#[ensures(move |ret| { *ret == y })]
fn foo(x: u32) -> u32 {
x * 2
}

fn main() {
foo(1);
}
Loading
Loading