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 | d81701b61074356afc062ac9972000abc03498d3 (patch) | |
| tree | e79bb77bd02764ca95bfd7093f61f60bf5a773f1 /compiler/rustc_const_eval/src | |
| parent | e5f11af042ad099102efd572743138df60764a4e (diff) | |
| parent | ddbf54b67d9befcf1fb90613d2a6f7f6aa03141e (diff) | |
| download | rust-d81701b61074356afc062ac9972000abc03498d3.tar.gz rust-d81701b61074356afc062ac9972000abc03498d3.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_const_eval/src')
| -rw-r--r-- | compiler/rustc_const_eval/src/check_consts/check.rs | 6 | ||||
| -rw-r--r-- | compiler/rustc_const_eval/src/interpret/machine.rs | 10 | ||||
| -rw-r--r-- | compiler/rustc_const_eval/src/interpret/operator.rs | 1 |
3 files changed, 16 insertions, 1 deletions
diff --git a/compiler/rustc_const_eval/src/check_consts/check.rs b/compiler/rustc_const_eval/src/check_consts/check.rs index e8052a3c83a..d0ce027ec2b 100644 --- a/compiler/rustc_const_eval/src/check_consts/check.rs +++ b/compiler/rustc_const_eval/src/check_consts/check.rs @@ -675,7 +675,11 @@ impl<'tcx> Visitor<'tcx> for Checker<'_, 'tcx> { Rvalue::Cast(_, _, _) => {} Rvalue::NullaryOp( - NullOp::SizeOf | NullOp::AlignOf | NullOp::OffsetOf(_) | NullOp::UbChecks, + NullOp::SizeOf + | NullOp::AlignOf + | NullOp::OffsetOf(_) + | NullOp::UbChecks + | NullOp::ContractChecks, _, ) => {} Rvalue::ShallowInitBox(_, _) => {} diff --git a/compiler/rustc_const_eval/src/interpret/machine.rs b/compiler/rustc_const_eval/src/interpret/machine.rs index 8f6b15b8df0..1a799f5dea5 100644 --- a/compiler/rustc_const_eval/src/interpret/machine.rs +++ b/compiler/rustc_const_eval/src/interpret/machine.rs @@ -293,6 +293,9 @@ pub trait Machine<'tcx>: Sized { /// Determines the result of a `NullaryOp::UbChecks` invocation. fn ub_checks(_ecx: &InterpCx<'tcx, Self>) -> InterpResult<'tcx, bool>; + /// Determines the result of a `NullaryOp::ContractChecks` invocation. + fn contract_checks(_ecx: &InterpCx<'tcx, Self>) -> InterpResult<'tcx, bool>; + /// Called when the interpreter encounters a `StatementKind::ConstEvalCounter` instruction. /// You can use this to detect long or endlessly running programs. #[inline] @@ -680,6 +683,13 @@ pub macro compile_time_machine(<$tcx: lifetime>) { } #[inline(always)] + fn contract_checks(_ecx: &InterpCx<$tcx, Self>) -> InterpResult<$tcx, bool> { + // We can't look at `tcx.sess` here as that can differ across crates, which can lead to + // unsound differences in evaluating the same constant at different instantiation sites. + interp_ok(true) + } + + #[inline(always)] fn adjust_global_allocation<'b>( _ecx: &InterpCx<$tcx, Self>, _id: AllocId, diff --git a/compiler/rustc_const_eval/src/interpret/operator.rs b/compiler/rustc_const_eval/src/interpret/operator.rs index 5fa632fc57a..899670aeb62 100644 --- a/compiler/rustc_const_eval/src/interpret/operator.rs +++ b/compiler/rustc_const_eval/src/interpret/operator.rs @@ -537,6 +537,7 @@ impl<'tcx, M: Machine<'tcx>> InterpCx<'tcx, M> { ImmTy::from_uint(val, usize_layout()) } UbChecks => ImmTy::from_bool(M::ub_checks(self)?, *self.tcx), + ContractChecks => ImmTy::from_bool(M::contract_checks(self)?, *self.tcx), }) } } |
