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.
This commit is contained in:
commit
d81701b610
123 changed files with 1869 additions and 39 deletions
|
@ -132,6 +132,9 @@ pub fn intrinsic_operation_unsafety(tcx: TyCtxt<'_>, intrinsic_id: LocalDefId) -
|
|||
| sym::aggregate_raw_ptr
|
||||
| sym::ptr_metadata
|
||||
| sym::ub_checks
|
||||
| sym::contract_checks
|
||||
| sym::contract_check_requires
|
||||
| sym::contract_check_ensures
|
||||
| sym::fadd_algebraic
|
||||
| sym::fsub_algebraic
|
||||
| sym::fmul_algebraic
|
||||
|
@ -219,6 +222,16 @@ pub fn check_intrinsic_type(
|
|||
}
|
||||
};
|
||||
(n_tps, 0, 0, inputs, output, hir::Safety::Unsafe)
|
||||
} else if intrinsic_name == sym::contract_check_ensures {
|
||||
// contract_check_ensures::<'a, Ret, C>(&'a Ret, C)
|
||||
// where C: impl Fn(&'a Ret) -> bool,
|
||||
//
|
||||
// so: two type params, one lifetime param, 0 const params, two inputs, no return
|
||||
|
||||
let p = generics.param_at(0, tcx);
|
||||
let r = ty::Region::new_early_param(tcx, p.to_early_bound_region_data());
|
||||
let ref_ret = Ty::new_imm_ref(tcx, r, param(1));
|
||||
(2, 1, 0, vec![ref_ret, param(2)], tcx.types.unit, hir::Safety::Safe)
|
||||
} else {
|
||||
let safety = intrinsic_operation_unsafety(tcx, intrinsic_id);
|
||||
let (n_tps, n_cts, inputs, output) = match intrinsic_name {
|
||||
|
@ -610,6 +623,11 @@ pub fn check_intrinsic_type(
|
|||
|
||||
sym::box_new => (1, 0, vec![param(0)], Ty::new_box(tcx, param(0))),
|
||||
|
||||
// contract_checks() -> bool
|
||||
sym::contract_checks => (0, 0, Vec::new(), tcx.types.bool),
|
||||
// contract_check_requires::<C>(C) -> bool, where C: impl Fn() -> bool
|
||||
sym::contract_check_requires => (1, 0, vec![param(0)], tcx.types.unit),
|
||||
|
||||
sym::simd_eq
|
||||
| sym::simd_ne
|
||||
| sym::simd_lt
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue