[DRAFT] #[contracts::requires(...)] #128045

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

Initial go at contract support: attribute syntax for preconditions, and an intrinsic for checking it.

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.
The macro is currently expanding to a core::intrinsics::contract_check path. I suspect that the expansion will actually want to be conditional based on whether it is expanding within std or outside of std.
The macro itself is very naive; it assumes the first occurrence of { ... } in the token-stream will be the function body (and injects the intrinsic call there). I suspect there are some constructs like const { ... } that might mess that up if they occur in certain contexts (I'm thinking first and foremost of where-clauses here)..
The emitted abort message when a contract fails is just "contract failure". Obviously the message should include more details, e.g. what function failed, which contract-expression failed and (maybe) what value caused the failure.

…nd an intrinsic for checking it. 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`. * The macro is currently expanding to a `core::intrinsics::contract_check` path. I suspect that the expansion will actually want to be conditional based on whether it is expanding within std or outside of std. * The macro itself is very naive; it assumes the first occurrence of `{ ... }` in the token-stream will be the function body (and injects the intrinsic call there). I suspect there are some contracts like `const { ... }` that might mess that up. * The emitted abort message when a contract fails is just "contract failure". Obviously the message should include more details, e.g. what function failed, which contract-expression failed and (maybe) what value caused the failure.

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

petrochenkov · 2024-07-22T10:21:00Z

library/core/src/prelude/common.rs

+*/
+#[cfg(not(bootstrap))]
+#[unstable(feature = "rustc_contracts", issue = "none")]
+pub use crate::contracts;


Adding experimental stuff to the prelude is probably premature.

yeah that's probably true.

(context: an earlier version of this branch had named this module rustc_contracts instead of contracts, in order to enable #[rustc_contract::requires(...). but for some reason our handling of rustc_-prefixed attributes made that not work at all, and so I fell back on this approach. But you are right that it doesn't need to be in the prelude.)

Adding macros to the prelude will likely break things since name resolution for macros AFAIK does not de-prioritize unstable macros until name resolution for normal items. Can this be changed to require an explicit import?

yes I'll remove the change to the prelude.

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

r? compiler

celinval · 2024-07-23T20:44:37Z

compiler/rustc_builtin_macros/src/contracts.rs

+
+pub struct ExpandRequires;
+
+impl AttrProcMacro for ExpandRequires {


Would it make sense for this to be a no-op if contract option is set to none?

celinval · 2024-07-23T21:00:41Z

tests/ui/contracts.rs

+#![allow(internal_features)]
+#![feature(rustc_attrs, rustc_contracts, core_intrinsics)]
+
+#[contracts::requires(x > 0)]


I do like contracts::, but it just occurred to me that it could conflict with the crate contracts.

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

oli-obk

HIR and MIR changes lgtm

oli-obk · 2024-07-25T09:00:38Z

compiler/rustc_mir_transform/src/lower_intrinsics.rs

@@ -333,6 +333,12 @@ impl<'tcx> MirPass<'tcx> for LowerIntrinsics {
 });
 terminator.kind = TerminatorKind::Goto { target };
 }
+ sym::contract_check => {
+ if tcx.sess.opts.unstable_opts.contract_checking.no_checks() {


the no_checks method tripped me up a bit. Slight preference for not having it at all and using an exhaustive match here instead

jieyouxu · 2024-07-28T03:10:32Z

I took a closer look at the #[contracts] namespacing issue, and could not come up with a good solution that doesn't involve a bunch of changes throughout resolve/ast and likely more. I've noticed two points:

For built-in macros, we currently seem to simply assume the attribute only has one primary symbol like #[contracts], and do not have support for #[rustc_contracts::require] (not without a bunch of changes to use SmallVec<[Symbol; 2]> instead of just Symbol). The closest workaround that I can think of is just to use something like rustc_contracts_* prefixes (certainly not ideal in the long run, but sufficient for experimentation) that do not collide with a crate named contracts. Tools are handled differently (like #[diagnostic] tool namespace) that does not allow us to trivially use a similar implementation.
I did some more fiddling, and could not come up with a less fragile solution for the contract_check rewrite itself (that is, the problem with braces { } before the annotated function's body, such as const { } in where-clauses). While I believe this rewrite logic would only error out if there's a #[contract::requires] annotation, it's still not ideal.

Unfortunately, I don't have good solutions for your problems. So I'm also going to reroll in the hopes that other reviewers could help you out here with better ideas... @oli-obk Oli, would you like to take over the review, or should we try to find someone else who might have a better idea of how to work around these issues?

oli-obk · 2024-07-30T09:16:29Z

compiler/rustc_builtin_macros/src/contracts.rs

+ // NOTE: this will break if you have a `{ ... }` syntactically prior to the fn body,
+ // e.g. if a `const { ... }` can occur in a where clause. We need to do something
+ // smarter for injecting this code into the right place.


using register_attr will resolve this, as you get access to an https://doc.rust-lang.org/nightly/nightly-rustc/rustc_expand/base/enum.Annotatable.html directly, so you can easily find the body and create wrappers for it and such. It's how we handle tests and benchmarks

I think I've tried this myself too, but doesn't register_attr expect either a function or something that has a expand signature of

fn expand( &self, ecx: &mut ExtCtxt<'_>, span: Span, meta_item: &ast::MetaItem, item: Annotatable, )

Specifically, ast::MetaItem the annotation here limits what syntax is permitted within a hypothetical #[contracts::requires(<requires_expr>)]? It would fix the { ... } breaking issue, but then wouldn't it introduce a new <requires_expr> can no longer be a complex expression issue?

hmm... true... but if we want to permit expressions there we should teach NestedItem about it anyway (gated appropriately that it won't be permitted without feature gates even behind #[cfg(FALSE)])

Hmm.

So... rather than trying to build this atop Attr (which is oriented around TokenTree to TokenTree transformations) they way that I have done here, ...

... it sounds like you are encouraging that I try to extend the functionality of the expanders we feed into LegacyAttr (namely functions that implement the MultiItemModifier trait, such as the signature @jieyouxu wrote above), which will then involve expanding the definition of ast::MetaItem (or one of the types it uses, such as NestedMetaItem) to now be able to take as inputs ... token trees? (or ... asts? is that distinction meaningful here?)

Do I have that right?

Yea, we already support #[foo = bar] where bar is an arbitrary expression, we just error on it in ast lowering. Seems fine to teach that to parse #[foo(someexpr)], too. But I'd want a @petrochenkov vibe check on that before touching it

jieyouxu · 2024-08-03T19:55:02Z

Since oli is on leave, I'll try to find you another suitable reviewer.
In the meantime, r? jieyouxu

jieyouxu · 2024-08-03T20:01:07Z

This PR is going to need a more suitable reviewer who's more familiar with attribute handling, and possibly another reviewer who's familiar with the HIR/MIR changes, so nominating for T-compiler discussion to find more suitable reviewer(s).

The current challenge seems to be that existing attribute handling only supports a "single path segment", i.e. #[contracts(<inner_expr>)] but not #[contracts::requires(<inner_expr>)]. We also can't trivially reuse existing register_attr! or visitor because they impose strict limits on the <inner_expr> and require it to be very primitive (like literals or identifiers or simple lists) but does not support arbitrary expressions like x > 0. To support the arbitrary inner expression (in that it may not necessarily be a valid rust expression), it may require relaxing that restriction, but it may raise further parsing/grammar questions.

@rustbot labels +I-compiler-nominated

(Also see previous reviewer request)

pnkfelix · 2024-08-05T15:06:54Z

I agree that the compiler team should discuss the best way to change the compiler to support the attributes described here,
on both the axes describe by @jieyouxu

So I'm going to leave that nomination label on it.

In addition, i really should have changed the tags and metadata to reflect that this is no longer "ready for review" -- the review feedback has made it clear that this should not land as-is. So I will also fix that now.

@rustbot label: +S-waiting-on-author -S-waiting-on-review

apiraino · 2024-08-22T15:11:31Z

Discussed in t-compiler meeting on Zulip.

This deserve a dedicated design meeting. @pnkfelix when you have a chance, could you file it up with a bit of context? thanks

@rustbot label -I-compiler-nominated

pnkfelix added 2 commits July 21, 2024 17:23

placate tidy.

1fb4ea4

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

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

oli-obk approved these changes Jul 25, 2024

View reviewed changes

oli-obk assigned oli-obk and unassigned oli-obk Jul 25, 2024

oli-obk reviewed Jul 25, 2024

View reviewed changes

jieyouxu removed their assignment Jul 28, 2024

oli-obk self-assigned this Jul 28, 2024

oli-obk reviewed Jul 30, 2024

View reviewed changes

oli-obk removed their assignment Jul 31, 2024

rustbot assigned jieyouxu and unassigned Amanieu Aug 3, 2024

rustbot added the I-compiler-nominated Nominated for discussion during a compiler team meeting. label Aug 3, 2024

jieyouxu added the F-rustc_contracts `#![feature(rustc_contracts)]` label Aug 5, 2024

rustbot added S-waiting-on-author Status: This is awaiting some action (such as code changes or more information) from the author. and removed S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. labels Aug 5, 2024

pnkfelix changed the title ~~#[contracts::requires(...)]~~ [DRAfT] #[contracts::requires(...)] Aug 5, 2024

pnkfelix changed the title ~~[DRAfT] #[contracts::requires(...)]~~ [DRAFT] #[contracts::requires(...)] Aug 5, 2024

pnkfelix marked this pull request as draft August 5, 2024 15:07

rustbot removed the I-compiler-nominated Nominated for discussion during a compiler team meeting. label Aug 22, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[DRAFT] #[contracts::requires(...)] #128045

[DRAFT] #[contracts::requires(...)] #128045

pnkfelix commented Jul 21, 2024 •

edited

Loading

rustbot commented Jul 21, 2024

rustbot commented Jul 21, 2024

oli-obk commented Jul 22, 2024

petrochenkov Jul 22, 2024

jieyouxu Jul 28, 2024

jieyouxu Jul 28, 2024

pnkfelix Aug 1, 2024

petrochenkov Jul 22, 2024

pnkfelix Jul 23, 2024

Amanieu Jul 25, 2024

pnkfelix Aug 1, 2024

fee1-dead commented Jul 23, 2024

celinval Jul 23, 2024

celinval Jul 23, 2024

chenyukang commented Jul 24, 2024

Nadrieril commented Jul 24, 2024

petrochenkov commented Jul 24, 2024

petrochenkov commented Jul 24, 2024

jieyouxu commented Jul 24, 2024

oli-obk left a comment •

edited

Loading

oli-obk Jul 25, 2024

jieyouxu commented Jul 28, 2024 •

edited

Loading

oli-obk Jul 30, 2024

jieyouxu Jul 30, 2024

oli-obk Jul 30, 2024

pnkfelix Aug 1, 2024 •

edited

Loading

oli-obk Aug 1, 2024

jieyouxu commented Aug 3, 2024

jieyouxu commented Aug 3, 2024 •

edited

Loading

pnkfelix commented Aug 5, 2024

apiraino commented Aug 22, 2024


		pub struct ExpandRequires;

		impl AttrProcMacro for ExpandRequires {

[DRAFT] #[contracts::requires(...)] #128045

Are you sure you want to change the base?

[DRAFT] #[contracts::requires(...)] #128045

Conversation

pnkfelix commented Jul 21, 2024 • edited Loading

rustbot commented Jul 21, 2024

rustbot commented Jul 21, 2024

oli-obk commented Jul 22, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

fee1-dead commented Jul 23, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

chenyukang commented Jul 24, 2024

Nadrieril commented Jul 24, 2024

petrochenkov commented Jul 24, 2024

petrochenkov commented Jul 24, 2024

jieyouxu commented Jul 24, 2024

oli-obk left a comment • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jieyouxu commented Jul 28, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

pnkfelix Aug 1, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jieyouxu commented Aug 3, 2024

jieyouxu commented Aug 3, 2024 • edited Loading

pnkfelix commented Aug 5, 2024

apiraino commented Aug 22, 2024

pnkfelix commented Jul 21, 2024 •

edited

Loading

oli-obk left a comment •

edited

Loading

jieyouxu commented Jul 28, 2024 •

edited

Loading

pnkfelix Aug 1, 2024 •

edited

Loading

jieyouxu commented Aug 3, 2024 •

edited

Loading