Rollup merge of #128045 - pnkfelix:rustc-contracts, r=oli-obk
#[contracts::requires(...)] + #[contracts::ensures(...)] cc https://github.com/rust-lang/rust/issues/128044 Updated contract support: attribute syntax for preconditions and postconditions, implemented via a series of desugarings that culminates in: 1. a compile-time flag (`-Z contract-checks`) that, similar to `-Z ub-checks`, attempts to ensure that the decision of enabling/disabling contract checks is delayed until the end user program is compiled, 2. invocations of lang-items that handle invoking the precondition, building a checker for the post-condition, and invoking that post-condition checker at the return sites for the function, and 3. intrinsics for the actual evaluation of pre- and post-condition predicates that third-party verification tools can intercept and reinterpret for their own purposes (e.g. creating shims of behavior that abstract away the function body and replace it solely with the pre- and post-conditions). Known issues: * My original intent, as described in the MCP (https://github.com/rust-lang/compiler-team/issues/759) was to have a rustc-prefixed attribute namespace (like rustc_contracts::requires). But I could not get things working when I tried to do rewriting via a rustc-prefixed builtin attribute-macro. So for now it is called `contracts::requires`. * Our attribute macro machinery does not provide direct support for attribute arguments that are parsed like rust expressions. I spent some time trying to add that (e.g. something that would parse the attribute arguments as an AST while treating the remainder of the items as a token-tree), but its too big a lift for me to undertake. So instead I hacked in something approximating that goal, by semi-trivially desugaring the token-tree attribute contents into internal AST constucts. This may be too fragile for the long-term. * (In particular, it *definitely* breaks when you try to add a contract to a function like this: `fn foo1(x: i32) -> S<{ 23 }> { ... }`, because its token-tree based search for where to inject the internal AST constructs cannot immediately see that the `{ 23 }` is within a generics list. I think we can live for this for the short-term, i.e. land the work, and continue working on it while in parallel adding a new attribute variant that takes a token-tree attribute alongside an AST annotation, which would completely resolve the issue here.) * the *intent* of `-Z contract-checks` is that it behaves like `-Z ub-checks`, in that we do not prematurely commit to including or excluding the contract evaluation in upstream crates (most notably, `core` and `std`). But the current test suite does not actually *check* that this is the case. Ideally the test suite would be extended with a multi-crate test that explores the matrix of enabling/disabling contracts on both the upstream lib and final ("leaf") bin crates.
This commit is contained in:
@@ -362,18 +362,21 @@ pub fn eq_item_kind(l: &ItemKind, r: &ItemKind) -> bool {
|
|||||||
defaultness: ld,
|
defaultness: ld,
|
||||||
sig: lf,
|
sig: lf,
|
||||||
generics: lg,
|
generics: lg,
|
||||||
|
contract: lc,
|
||||||
body: lb,
|
body: lb,
|
||||||
}),
|
}),
|
||||||
Fn(box ast::Fn {
|
Fn(box ast::Fn {
|
||||||
defaultness: rd,
|
defaultness: rd,
|
||||||
sig: rf,
|
sig: rf,
|
||||||
generics: rg,
|
generics: rg,
|
||||||
|
contract: rc,
|
||||||
body: rb,
|
body: rb,
|
||||||
}),
|
}),
|
||||||
) => {
|
) => {
|
||||||
eq_defaultness(*ld, *rd)
|
eq_defaultness(*ld, *rd)
|
||||||
&& eq_fn_sig(lf, rf)
|
&& eq_fn_sig(lf, rf)
|
||||||
&& eq_generics(lg, rg)
|
&& eq_generics(lg, rg)
|
||||||
|
&& eq_opt_fn_contract(lc, rc)
|
||||||
&& both(lb.as_ref(), rb.as_ref(), |l, r| eq_block(l, r))
|
&& both(lb.as_ref(), rb.as_ref(), |l, r| eq_block(l, r))
|
||||||
},
|
},
|
||||||
(Mod(lu, lmk), Mod(ru, rmk)) => {
|
(Mod(lu, lmk), Mod(ru, rmk)) => {
|
||||||
@@ -497,18 +500,21 @@ pub fn eq_foreign_item_kind(l: &ForeignItemKind, r: &ForeignItemKind) -> bool {
|
|||||||
defaultness: ld,
|
defaultness: ld,
|
||||||
sig: lf,
|
sig: lf,
|
||||||
generics: lg,
|
generics: lg,
|
||||||
|
contract: lc,
|
||||||
body: lb,
|
body: lb,
|
||||||
}),
|
}),
|
||||||
Fn(box ast::Fn {
|
Fn(box ast::Fn {
|
||||||
defaultness: rd,
|
defaultness: rd,
|
||||||
sig: rf,
|
sig: rf,
|
||||||
generics: rg,
|
generics: rg,
|
||||||
|
contract: rc,
|
||||||
body: rb,
|
body: rb,
|
||||||
}),
|
}),
|
||||||
) => {
|
) => {
|
||||||
eq_defaultness(*ld, *rd)
|
eq_defaultness(*ld, *rd)
|
||||||
&& eq_fn_sig(lf, rf)
|
&& eq_fn_sig(lf, rf)
|
||||||
&& eq_generics(lg, rg)
|
&& eq_generics(lg, rg)
|
||||||
|
&& eq_opt_fn_contract(lc, rc)
|
||||||
&& both(lb.as_ref(), rb.as_ref(), |l, r| eq_block(l, r))
|
&& both(lb.as_ref(), rb.as_ref(), |l, r| eq_block(l, r))
|
||||||
},
|
},
|
||||||
(
|
(
|
||||||
@@ -559,18 +565,21 @@ pub fn eq_assoc_item_kind(l: &AssocItemKind, r: &AssocItemKind) -> bool {
|
|||||||
defaultness: ld,
|
defaultness: ld,
|
||||||
sig: lf,
|
sig: lf,
|
||||||
generics: lg,
|
generics: lg,
|
||||||
|
contract: lc,
|
||||||
body: lb,
|
body: lb,
|
||||||
}),
|
}),
|
||||||
Fn(box ast::Fn {
|
Fn(box ast::Fn {
|
||||||
defaultness: rd,
|
defaultness: rd,
|
||||||
sig: rf,
|
sig: rf,
|
||||||
generics: rg,
|
generics: rg,
|
||||||
|
contract: rc,
|
||||||
body: rb,
|
body: rb,
|
||||||
}),
|
}),
|
||||||
) => {
|
) => {
|
||||||
eq_defaultness(*ld, *rd)
|
eq_defaultness(*ld, *rd)
|
||||||
&& eq_fn_sig(lf, rf)
|
&& eq_fn_sig(lf, rf)
|
||||||
&& eq_generics(lg, rg)
|
&& eq_generics(lg, rg)
|
||||||
|
&& eq_opt_fn_contract(lc, rc)
|
||||||
&& both(lb.as_ref(), rb.as_ref(), |l, r| eq_block(l, r))
|
&& both(lb.as_ref(), rb.as_ref(), |l, r| eq_block(l, r))
|
||||||
},
|
},
|
||||||
(
|
(
|
||||||
@@ -653,6 +662,17 @@ pub fn eq_fn_header(l: &FnHeader, r: &FnHeader) -> bool {
|
|||||||
&& eq_ext(&l.ext, &r.ext)
|
&& eq_ext(&l.ext, &r.ext)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pub fn eq_opt_fn_contract(l: &Option<P<FnContract>>, r: &Option<P<FnContract>>) -> bool {
|
||||||
|
match (l, r) {
|
||||||
|
(Some(l), Some(r)) => {
|
||||||
|
eq_expr_opt(l.requires.as_ref(), r.requires.as_ref())
|
||||||
|
&& eq_expr_opt(l.ensures.as_ref(), r.ensures.as_ref())
|
||||||
|
}
|
||||||
|
(None, None) => true,
|
||||||
|
(Some(_), None) | (None, Some(_)) => false,
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
pub fn eq_generics(l: &Generics, r: &Generics) -> bool {
|
pub fn eq_generics(l: &Generics, r: &Generics) -> bool {
|
||||||
over(&l.params, &r.params, eq_generic_param)
|
over(&l.params, &r.params, eq_generic_param)
|
||||||
&& over(&l.where_clause.predicates, &r.where_clause.predicates, |l, r| {
|
&& over(&l.where_clause.predicates, &r.where_clause.predicates, |l, r| {
|
||||||
|
|||||||
@@ -179,7 +179,7 @@ fn check_rvalue<'tcx>(
|
|||||||
))
|
))
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
Rvalue::NullaryOp(NullOp::SizeOf | NullOp::AlignOf | NullOp::OffsetOf(_) | NullOp::UbChecks, _)
|
Rvalue::NullaryOp(NullOp::SizeOf | NullOp::AlignOf | NullOp::OffsetOf(_) | NullOp::UbChecks | NullOp::ContractChecks, _)
|
||||||
| Rvalue::ShallowInitBox(_, _) => Ok(()),
|
| Rvalue::ShallowInitBox(_, _) => Ok(()),
|
||||||
Rvalue::UnaryOp(_, operand) => {
|
Rvalue::UnaryOp(_, operand) => {
|
||||||
let ty = operand.ty(body, tcx);
|
let ty = operand.ty(body, tcx);
|
||||||
|
|||||||
Reference in New Issue
Block a user