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

@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!

If that is the reason, at the very least a comment is needed to explain that.

There are comments in the builtin macro implementation. Would you like me to add comments to this file as well?

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

Check ensures on early return due to Try / Yeet Expand these two expressions to include a call to contract checking

…ostcondition predicate.

The extended syntax for function signature that includes contract clauses should never be user exposed versus the interface we want to ship externally eventually.

Instead of parsing the different components of a function signature, eagerly look for either the `where` keyword or the function body. - Also address feedback to use `From` instead of `TryFrom` in cranelift contract and ubcheck codegen.

1. Document the new intrinsics. 2. Make the intrinsics actually check the contract if enabled, and remove `contract::check_requires` function. 3. Use panic with no unwind in case contract is using to check for safety, we probably don't want to unwind. Following the same reasoning as UB checks.

This is now a valid expected value.

This has now been approved as a language feature and no longer needs a `rustc_` prefix. Also change the `contracts` feature to be marked as incomplete and `contracts_internals` as internal.

celinval · 2025-02-03T23:22:55Z

@bors rollup r=@oli-obk

bors · 2025-02-03T23:22:58Z

📌 Commit ddbf54b has been approved by oli-obk

It is now in the queue for this repository.

#[contracts::requires(...)] + #[contracts::ensures(...)] cc rust-lang#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.

Rollup of 9 pull requests Successful merges: - rust-lang#128045 (#[contracts::requires(...)] + #[contracts::ensures(...)]) - rust-lang#136263 (rustdoc: clean up a bunch of ts-expected-error declarations in main) - rust-lang#136375 (cg_llvm: Replace some DIBuilder wrappers with LLVM-C API bindings (part 1)) - rust-lang#136392 (bootstrap: add wrapper macros for `feature = "tracing"`-gated `tracing` macros) - rust-lang#136405 (rustdoc-book: Clean up section on `--output-format`) - rust-lang#136497 (Report generic mismatches when calling bodyless trait functions) - rust-lang#136502 (Mark `std::fmt::from_fn` as `#[must_use]`) - rust-lang#136509 (Add tests for nested macro_rules edition behavior) - rust-lang#136526 (mir_build: Rename `thir::cx::Cx` to `ThirBuildCx` and remove `UserAnnotatedTyHelpers`) r? `@ghost` `@rustbot` modify labels: rollup

Rollup of 8 pull requests Successful merges: - rust-lang#128045 (#[contracts::requires(...)] + #[contracts::ensures(...)]) - rust-lang#136263 (rustdoc: clean up a bunch of ts-expected-error declarations in main) - rust-lang#136375 (cg_llvm: Replace some DIBuilder wrappers with LLVM-C API bindings (part 1)) - rust-lang#136392 (bootstrap: add wrapper macros for `feature = "tracing"`-gated `tracing` macros) - rust-lang#136396 (rustdoc-json-types: Document that crate name isn't package name.) - rust-lang#136405 (rustdoc-book: Clean up section on `--output-format`) - rust-lang#136502 (Mark `std::fmt::from_fn` as `#[must_use]`) - rust-lang#136509 (Add tests for nested macro_rules edition behavior) r? `@ghost` `@rustbot` modify labels: rollup

Rollup merge of rust-lang#128045 - pnkfelix:rustc-contracts, r=oli-obk #[contracts::requires(...)] + #[contracts::ensures(...)] cc rust-lang#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.

Uses the contracts syntax introduced in rust-lang#128045.

Refactor FnKind variant to hold &Fn Pulling the change suggested in rust-lang#128045 to reduce the impact of changing `Fn` item. r? `@oli-obk`

#[contracts::requires(...)] + #[contracts::ensures(...)] cc rust-lang#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.

Uses the contracts syntax introduced in rust-lang#128045.

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

celinval force-pushed the rustc-contracts branch from 42722b8 to d280c18 Compare February 3, 2025 21:46

pnkfelix and others added 7 commits February 3, 2025 13:54

Desugars contract into the internal AST extensions

ae7eff0

Check ensures on early return due to Try / Yeet Expand these two expressions to include a call to contract checking

demonstrate how to capture state at precondition time and feed into p…

b279ff9

…ostcondition predicate.

Separate contract feature gates for the internal machinery

6a6c6b8

The extended syntax for function signature that includes contract clauses should never be user exposed versus the interface we want to ship externally eventually.

Refactor contract builtin macro + error handling

804cce4

Instead of parsing the different components of a function signature, eagerly look for either the `where` keyword or the function body. - Also address feedback to use `From` instead of `TryFrom` in cranelift contract and ubcheck codegen.

Update test output to include check_contracts cfg

2c4923e

This is now a valid expected value.

Rename rustc_contract to contract

ddbf54b

This has now been approved as a language feature and no longer needs a `rustc_` prefix. Also change the `contracts` feature to be marked as incomplete and `contracts_internals` as internal.

celinval force-pushed the rustc-contracts branch from d280c18 to ddbf54b Compare February 3, 2025 22:27

bors added S-waiting-on-bors Status: Waiting on bors to run and complete tests. Bors will change the label on completion. and removed S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. labels Feb 3, 2025

jhpratt mentioned this pull request Feb 4, 2025

Rollup of 9 pull requests #136531

Closed

fmease mentioned this pull request Feb 5, 2025

Rollup of 8 pull requests #136564

Merged

bors merged commit d81701b into rust-lang:master Feb 5, 2025
6 checks passed

rustbot added this to the 1.86.0 milestone Feb 5, 2025

tautschnig mentioned this pull request Feb 5, 2025

Add contracts for all functions in Alignment #136578

Draft

tautschnig added a commit to tautschnig/verify-rust-std that referenced this pull request Feb 5, 2025

Add contracts for all functions in Alignment

7288286

Uses the contracts syntax introduced in rust-lang#128045.

tautschnig added a commit to tautschnig/verify-rust-std that referenced this pull request Feb 6, 2025

Add contracts for all functions in Alignment

c180bd0

Uses the contracts syntax introduced in rust-lang#128045.

rust-timer mentioned this pull request Feb 7, 2025

Rollup of 7 pull requests #136658

Merged

tautschnig added a commit to tautschnig/verify-rust-std that referenced this pull request Feb 11, 2025

Add contracts for all functions in Alignment

4322394

Uses the contracts syntax introduced in rust-lang#128045.

tautschnig added a commit to tautschnig/verify-rust-std that referenced this pull request Feb 12, 2025

Add contracts for all functions in Alignment

dfd17f1

Uses the contracts syntax introduced in rust-lang#128045.

fmease mentioned this pull request Feb 16, 2025

Rust Contracts syntax #137134

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

#[contracts::requires(...)] + #[contracts::ensures(...)] #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

celinval Jan 10, 2025

RalfJung Jan 16, 2025

celinval Jan 27, 2025 •

edited

Loading

fee1-dead commented 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

celinval commented Feb 3, 2025

bors commented Feb 3, 2025

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

#[contracts::requires(...)] + #[contracts::ensures(...)] #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

petrochenkov Jul 22, 2024

Choose a reason for hiding this comment

jieyouxu Jul 28, 2024

Choose a reason for hiding this comment

jieyouxu Jul 28, 2024

Choose a reason for hiding this comment

pnkfelix Aug 1, 2024

Choose a reason for hiding this comment

celinval Jan 10, 2025

Choose a reason for hiding this comment

RalfJung Jan 16, 2025

Choose a reason for hiding this comment

celinval Jan 27, 2025 • edited Loading

Choose a reason for hiding this comment

fee1-dead commented 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

celinval commented Feb 3, 2025

bors commented Feb 3, 2025

pnkfelix commented Jul 21, 2024 •

edited

Loading

celinval Jan 27, 2025 •

edited

Loading