diff options
| author | León Orell Valerian Liehr <me@fmease.dev> | 2025-02-05 05:03:01 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2025-02-05 05:03:01 +0100 |
| commit | 4c11087e517f10ee35bbe1829e3e580fc5ca1e01 (patch) | |
| tree | 6b8c04760773bc0291b7a39e004a555b5c9b0d87 /compiler/rustc_interface/src | |
| parent | c1e4249e0d686c60239ec545e49246948a3c78b5 (diff) | |
| parent | 0a8331f681e6b82183947cf82b25566bfab3750e (diff) | |
| download | rust-4c11087e517f10ee35bbe1829e3e580fc5ca1e01.tar.gz rust-4c11087e517f10ee35bbe1829e3e580fc5ca1e01.zip | |
Rollup merge of #128045 - pnkfelix:rustc-contracts, r=oli-obk
#[contracts::requires(...)] + #[contracts::ensures(...)]
cc https://github.com/rust-lang/rust/issues/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 (https://github.com/rust-lang/compiler-team/issues/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.
Diffstat (limited to 'compiler/rustc_interface/src')
0 files changed, 0 insertions, 0 deletions
