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

[pnkfelix]

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 (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]

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]

Some changes occurred to MIR optimizations

cc @rust-lang/wg-mir-opt

[oli-obk]

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]

This macro should be able to use register_attr! above.

[jieyouxu]

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?

[jieyouxu]

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.

[pnkfelix]

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 ?)

[celinval]

@petrochenkov let me know if you want me to make any changes here. Per @pnkfelix comment, using register_attr! would restrict the input of the contract attributes which is not desirable here. Thanks!

[fee1-dead]

r? compiler

[chenyukang]

r? compiler

[Nadrieril]

I don't know that part of the compiler

r? @petrochenkov would you like to review this?

[petrochenkov]

would you like to review this?

No.
r? compiler

[petrochenkov]

r? compiler

[jieyouxu]

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]

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]

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.

[oli-obk]

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

[pnkfelix]

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]

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

[pnkfelix]

(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...)

[bors]

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

[celinval]

Note to self: @jdonszelmann pointed out that we could use the parser in rustc_parse to simplify this code. I'll give it a shot next week.

[celinval]

I rebased this PR. I had to change the parser a bit due to #134470. That said, I changed parse_contract to use eat_keyword_noexpect, which allowed me to revert the changes made to rustc_parser::parser::diagnostics.