Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit d81701b

Browse files
authoredFeb 5, 2025
Rollup merge of #128045 - pnkfelix:rustc-contracts, r=oli-obk
#[contracts::requires(...)] + #[contracts::ensures(...)] cc #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 (rust-lang/compiler-team#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.
2 parents e5f11af + ddbf54b commit d81701b

File tree

123 files changed

+1869
-39
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

123 files changed

+1869
-39
lines changed
 

‎compiler/rustc_ast/src/ast.rs

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3348,11 +3348,18 @@ pub struct Impl {
33483348
pub items: ThinVec<P<AssocItem>>,
33493349
}
33503350

3351+
#[derive(Clone, Encodable, Decodable, Debug, Default)]
3352+
pub struct FnContract {
3353+
pub requires: Option<P<Expr>>,
3354+
pub ensures: Option<P<Expr>>,
3355+
}
3356+
33513357
#[derive(Clone, Encodable, Decodable, Debug)]
33523358
pub struct Fn {
33533359
pub defaultness: Defaultness,
33543360
pub generics: Generics,
33553361
pub sig: FnSig,
3362+
pub contract: Option<P<FnContract>>,
33563363
pub body: Option<P<Block>>,
33573364
}
33583365

@@ -3650,7 +3657,7 @@ mod size_asserts {
36503657
static_assert_size!(Block, 32);
36513658
static_assert_size!(Expr, 72);
36523659
static_assert_size!(ExprKind, 40);
3653-
static_assert_size!(Fn, 160);
3660+
static_assert_size!(Fn, 168);
36543661
static_assert_size!(ForeignItem, 88);
36553662
static_assert_size!(ForeignItemKind, 16);
36563663
static_assert_size!(GenericArg, 24);

‎compiler/rustc_ast/src/mut_visit.rs

Lines changed: 18 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -143,6 +143,10 @@ pub trait MutVisitor: Sized {
143143
walk_flat_map_assoc_item(self, i, ctxt)
144144
}
145145

146+
fn visit_contract(&mut self, c: &mut P<FnContract>) {
147+
walk_contract(self, c);
148+
}
149+
146150
fn visit_fn_decl(&mut self, d: &mut P<FnDecl>) {
147151
walk_fn_decl(self, d);
148152
}
@@ -958,13 +962,16 @@ fn walk_fn<T: MutVisitor>(vis: &mut T, kind: FnKind<'_>) {
958962
_ctxt,
959963
_ident,
960964
_vis,
961-
Fn { defaultness, generics, body, sig: FnSig { header, decl, span } },
965+
Fn { defaultness, generics, contract, body, sig: FnSig { header, decl, span } },
962966
) => {
963967
// Identifier and visibility are visited as a part of the item.
964968
visit_defaultness(vis, defaultness);
965969
vis.visit_fn_header(header);
966970
vis.visit_generics(generics);
967971
vis.visit_fn_decl(decl);
972+
if let Some(contract) = contract {
973+
vis.visit_contract(contract);
974+
}
968975
if let Some(body) = body {
969976
vis.visit_block(body);
970977
}
@@ -979,6 +986,16 @@ fn walk_fn<T: MutVisitor>(vis: &mut T, kind: FnKind<'_>) {
979986
}
980987
}
981988

989+
fn walk_contract<T: MutVisitor>(vis: &mut T, contract: &mut P<FnContract>) {
990+
let FnContract { requires, ensures } = contract.deref_mut();
991+
if let Some(pred) = requires {
992+
vis.visit_expr(pred);
993+
}
994+
if let Some(pred) = ensures {
995+
vis.visit_expr(pred);
996+
}
997+
}
998+
982999
fn walk_fn_decl<T: MutVisitor>(vis: &mut T, decl: &mut P<FnDecl>) {
9831000
let FnDecl { inputs, output } = decl.deref_mut();
9841001
inputs.flat_map_in_place(|param| vis.flat_map_param(param));

0 commit comments

Comments
 (0)
Please sign in to comment.