#[contracts::requires(...)] + #[contracts::ensures(...)] #128045

pnkfelix · 2024-07-21T22:00:24Z

Updated contract support: attribute syntax for preconditions and postconditions, implemented via a series of desugarings that culminates in:

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,
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
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 (Contracts: Experimental attributes and language intrinsics 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.

rustbot · 2024-07-21T22:00:31Z

r? @fee1-dead

rustbot has assigned @fee1-dead.
They will have a look at your PR within the next two weeks and either review your PR or reassign to another reviewer.

Use r? to explicitly pick a reviewer

rustbot · 2024-07-21T22:00:33Z

Some changes occurred to MIR optimizations

cc @rust-lang/wg-mir-opt

oli-obk · 2024-07-22T09:08:18Z

Please add a ui test with an attribute proc-macro aux build that conflicts with contracts::requires (so I guess a crate contracts with a requires proc-macro attribute?)

petrochenkov · 2024-07-22T10:18:25Z

compiler/rustc_builtin_macros/src/lib.rs

+    register(
+        sym::contracts_requires,
+        SyntaxExtensionKind::Attr(Box::new(contracts::ExpandRequires)),
+    );


This macro should be able to use register_attr! above.

I'm not sure if we actually can, if we want to support arbitrary syntax within the contracts::require(...) -- doesn't register_attr! mandate that the requires expression conform to ast::MetaItem, which imposes restrictions on what the syntax can be, i.e. x > 0 wouldn't work?

I took a closer look at this, and this is very unfortunate. I don't believe the current builtin macro setup allows for "path segments"-like namespacing (like rustc_contracts::require). I've tried to change the builtin macro support to allow multiple "segments" via SmallVec<[Symbol; 2]>, but as one would expect, that change kept propagating outwards to attributes.

sorry for my delay in responding here.

@jieyouxu is exactly right.

specifically, register_attr! expands to a SyntaxExtensionKind::LegacyAttr, which is where the conformance to ast::MetaItem is enforced IIRC.

The plan here to support code snippets like x > 0 in a contract form means that we cannot conform to ast::MetaItem.

(In theory I could try to extend the register_attr! macro to support expansion to non LegacyAttr. Is that what you are asking for, @petrochenkov ?)

library/core/src/prelude/common.rs

fee1-dead · 2024-07-23T05:09:57Z

r? compiler

compiler/rustc_builtin_macros/src/contracts.rs

tests/ui/contracts.rs

chenyukang · 2024-07-24T01:46:27Z

r? compiler

Nadrieril · 2024-07-24T06:09:36Z

I don't know that part of the compiler

r? @petrochenkov would you like to review this?

petrochenkov · 2024-07-24T12:03:43Z

would you like to review this?

No.
r? compiler

petrochenkov · 2024-07-24T12:04:07Z

r? compiler

jieyouxu · 2024-07-24T12:41:54Z

I'll ask T-compiler for another suitable reviewer to take a look at the HIR/MIR parts of the PR, or take over the review. In the mean time, I'll also roll a T-libs reviewer for the libs part.

r? jieyouxu
r? libs

pnkfelix · 2024-12-05T12:00:20Z

Hmm. I don’t think I want contract_checks to be part of the explicit suggestions emitted by that lint; that would imply a level of stability that I do not want to commit to,

I’ll try to investigate that bit further.

pnkfelix · 2024-12-05T22:11:02Z

Hmm. I don’t think I want contract_checks to be part of the explicit suggestions emitted by that lint; that would imply a level of stability that I do not want to commit to,

Actually, ....

even though I'm still not sure about whether it is ideal to include contract_checks in the output, I now realize that there is precedent for including unstable things there. Namely ub_checks serves as obvious precedent for this.

So I'll just take the shortcut and add contract_checks to the expected output, which I infer must not have any stability guarantees.

pnkfelix · 2024-12-05T22:28:03Z

However, the analogous output for the parser, where it is actively suggesting rustc_requires and rustc_ensures as valid next tokens, is definitely not what I want and would be bad to make insta-stable.

Hmm. I'll think about bit about what to do about that. Hopefully can suppress suggestion of those tokens in a relatively easy manner.

(To be clear, I'm talking about diagnostic output like this:

LL | trait Foo { fn a() } //~ ERROR expected one of `->`, `;`, `where`, or `{`, found `}`
   |                -   ^ expected one of `->`, `;`, `rustc_contract_ensures`, `rustc_contract_requires`, `where`, or `{`
   |                |
   |                while parsing this `fn`

pnkfelix · 2024-12-09T20:08:45Z

From the description:

it definitely breaks when you try to add a contract to a function like this: fn foo1(x: i32) -> S<{ 23 }> { ... },

I had a realization over the weekend: while I myself find the placement of the internal rustc_contract_requires(EXPR) (and likewise rustc_contract_ensures(EXPR)) to be "natural" after the parameter+return-type list and before the function body itself, it is by no means a requirement that it fall there, and in fact, if we put it after the function name but before the optional generics list and requires ( for the parameter list, then that would sidestep all the parser issues here (I think), and thus make it possible to add a contract to any function header, including the pathological case described above.

I don't intend to implement that revision myself in the short term (I'd rather see this PR land as-is than block on that, since this fix can land later), but I wanted to mention it as a potential strategy in case anyone was getting worried about that comment above.

library/core/src/intrinsics/mod.rs

compiler/rustc_ast_lowering/src/item.rs

oli-obk · 2024-12-10T11:13:50Z

compiler/rustc_ast_lowering/src/expr.rs

-                    let e = e.as_ref().map(|x| self.lower_expr(x));
+                    let mut e = e.as_ref().map(|x| self.lower_expr(x));
+                    if let Some(Some((span, fresh_ident))) = self
+                        .contract
+                        .as_ref()
+                        .map(|c| c.ensures.as_ref().map(|e| (e.expr.span, e.fresh_ident)))
+                    {
+                        let checker_fn = self.expr_ident(span, fresh_ident.0, fresh_ident.2);
+                        let args = if let Some(e) = e {
+                            std::slice::from_ref(e)
+                        } else {
+                            std::slice::from_ref(self.expr_unit(span))
+                        };
+                        e = Some(self.expr_call(span, checker_fn, args));
+                    }


returns kind of duplicate logic with the trailing expression, something can be improved here

yes I agree. It should also be unified with how the Try operator is implemented. I.e. all three cases (return, ?, and the tail expression) should all call some common method so that code like this can be controlled in one place.

oli-obk · 2024-12-10T11:14:24Z

compiler/rustc_ast_lowering/src/item.rs

+                    this.stmt_expr(_contract.span, u)
+                };
+
+                let (postcond_checker, _opt_ident, result) = if let Some(ens) = _contract.ensures {


probably necessary for later in the PR, but, why is there a tuple field here that we just ignore

(I don't think I ever actually used it in the later commits. It was more that I had the info available from when I created the identifier and I wasn't sure if I might need it, so I threaded it through to at least this point...)

…ract checks are run, and 2. allow 3rd party tools to intercept and reintepret the results of running contracts.

… to invoke. see test for an example of the kind of injected code that is anticipated here.

…ower it into the previously added contract lang items. includes post-developed commit: do not suggest internal-only keywords as corrections to parse failures. includes post-developed commit: removed tabs that creeped in into rustfmt tool source code. includes post-developed commit, placating rustfmt self dogfooding. includes post-developed commit: add backquotes to prevent markdown checking from trying to treat an attr as a markdown hyperlink/ includes post-developed commit: fix lowering to keep contracts from being erroneously inherited by nested bodies (like closures).

…xtensions added earlier.

…ostcondition predicate.

…e user exposed versus the interface we want to ship externally eventually.

…alue.

bors · 2024-12-14T02:12:52Z

☔ The latest upstream changes (presumably #134269) made this pull request unmergeable. Please resolve the merge conflicts.

rustbot assigned fee1-dead Jul 21, 2024

rustbot added S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. T-compiler Relevant to the compiler team, which will review and decide on the PR/issue. T-libs Relevant to the library team, which will review and decide on the PR/issue. labels Jul 21, 2024

petrochenkov reviewed Jul 22, 2024

View reviewed changes

rustbot assigned chenyukang and unassigned fee1-dead Jul 23, 2024

celinval mentioned this pull request Jul 23, 2024

Update contract syntax to include contract forms as proposed in the MCP model-checking/verify-rust-std#44

Open

celinval reviewed Jul 23, 2024

View reviewed changes

compiler/rustc_builtin_macros/src/contracts.rs Show resolved Hide resolved

tests/ui/contracts.rs Outdated Show resolved Hide resolved

rustbot assigned Nadrieril and unassigned chenyukang Jul 24, 2024

rustbot assigned petrochenkov and unassigned Nadrieril Jul 24, 2024

rustbot assigned chenyukang and unassigned petrochenkov Jul 24, 2024

rustbot assigned jieyouxu and unassigned chenyukang Jul 24, 2024

rustbot assigned Amanieu and unassigned jieyouxu Jul 24, 2024

jieyouxu self-assigned this Jul 24, 2024

oli-obk self-assigned this Jul 24, 2024

pnkfelix force-pushed the rustc-contracts branch from ddf5369 to 2399210 Compare December 5, 2024 00:59