Commit 1420e03
authored
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.4 files changed
+98
-0
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| 5 | + | |
| 6 | + | |
| 7 | + | |
| 8 | + | |
| 9 | + | |
| 10 | + | |
| 11 | + | |
| 12 | + | |
| 13 | + | |
| 14 | + | |
| 15 | + | |
| 16 | + | |
| 17 | + | |
| 18 | + | |
| 19 | + | |
| 20 | + | |
| 21 | + | |
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
4064 | 4064 | | |
4065 | 4065 | | |
4066 | 4066 | | |
| 4067 | + | |
| 4068 | + | |
| 4069 | + | |
| 4070 | + | |
| 4071 | + | |
| 4072 | + | |
| 4073 | + | |
| 4074 | + | |
| 4075 | + | |
| 4076 | + | |
| 4077 | + | |
| 4078 | + | |
| 4079 | + | |
| 4080 | + | |
| 4081 | + | |
| 4082 | + | |
| 4083 | + | |
| 4084 | + | |
| 4085 | + | |
| 4086 | + | |
| 4087 | + | |
| 4088 | + | |
| 4089 | + | |
| 4090 | + | |
| 4091 | + | |
| 4092 | + | |
| 4093 | + | |
| 4094 | + | |
| 4095 | + | |
| 4096 | + | |
| 4097 | + | |
| 4098 | + | |
| 4099 | + | |
| 4100 | + | |
| 4101 | + | |
| 4102 | + | |
| 4103 | + | |
| 4104 | + | |
| 4105 | + | |
| 4106 | + | |
| 4107 | + | |
| 4108 | + | |
| 4109 | + | |
| 4110 | + | |
| 4111 | + | |
| 4112 | + | |
4067 | 4113 | | |
4068 | 4114 | | |
4069 | 4115 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
113 | 113 | | |
114 | 114 | | |
115 | 115 | | |
| 116 | + | |
116 | 117 | | |
117 | 118 | | |
118 | 119 | | |
| |||
247 | 248 | | |
248 | 249 | | |
249 | 250 | | |
| 251 | + | |
| 252 | + | |
| 253 | + | |
| 254 | + | |
250 | 255 | | |
251 | 256 | | |
252 | 257 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1777 | 1777 | | |
1778 | 1778 | | |
1779 | 1779 | | |
| 1780 | + | |
| 1781 | + | |
| 1782 | + | |
| 1783 | + | |
| 1784 | + | |
| 1785 | + | |
| 1786 | + | |
| 1787 | + | |
| 1788 | + | |
| 1789 | + | |
| 1790 | + | |
| 1791 | + | |
| 1792 | + | |
| 1793 | + | |
| 1794 | + | |
| 1795 | + | |
| 1796 | + | |
| 1797 | + | |
| 1798 | + | |
| 1799 | + | |
| 1800 | + | |
| 1801 | + | |
| 1802 | + | |
| 1803 | + | |
| 1804 | + | |
| 1805 | + | |
1780 | 1806 | | |
1781 | 1807 | | |
1782 | 1808 | | |
| |||
0 commit comments