Commit 4c11087
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.2 files changed
+21
-1
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
362 | 362 | | |
363 | 363 | | |
364 | 364 | | |
| 365 | + | |
365 | 366 | | |
366 | 367 | | |
367 | 368 | | |
368 | 369 | | |
369 | 370 | | |
370 | 371 | | |
| 372 | + | |
371 | 373 | | |
372 | 374 | | |
373 | 375 | | |
374 | 376 | | |
375 | 377 | | |
376 | 378 | | |
| 379 | + | |
377 | 380 | | |
378 | 381 | | |
379 | 382 | | |
| |||
497 | 500 | | |
498 | 501 | | |
499 | 502 | | |
| 503 | + | |
500 | 504 | | |
501 | 505 | | |
502 | 506 | | |
503 | 507 | | |
504 | 508 | | |
505 | 509 | | |
| 510 | + | |
506 | 511 | | |
507 | 512 | | |
508 | 513 | | |
509 | 514 | | |
510 | 515 | | |
511 | 516 | | |
| 517 | + | |
512 | 518 | | |
513 | 519 | | |
514 | 520 | | |
| |||
559 | 565 | | |
560 | 566 | | |
561 | 567 | | |
| 568 | + | |
562 | 569 | | |
563 | 570 | | |
564 | 571 | | |
565 | 572 | | |
566 | 573 | | |
567 | 574 | | |
| 575 | + | |
568 | 576 | | |
569 | 577 | | |
570 | 578 | | |
571 | 579 | | |
572 | 580 | | |
573 | 581 | | |
| 582 | + | |
574 | 583 | | |
575 | 584 | | |
576 | 585 | | |
| |||
653 | 662 | | |
654 | 663 | | |
655 | 664 | | |
| 665 | + | |
| 666 | + | |
| 667 | + | |
| 668 | + | |
| 669 | + | |
| 670 | + | |
| 671 | + | |
| 672 | + | |
| 673 | + | |
| 674 | + | |
| 675 | + | |
656 | 676 | | |
657 | 677 | | |
658 | 678 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
179 | 179 | | |
180 | 180 | | |
181 | 181 | | |
182 | | - | |
| 182 | + | |
183 | 183 | | |
184 | 184 | | |
185 | 185 | | |
| |||
0 commit comments