Enable contracts for const functions

[celinval]

Use const_eval_select!() macro to enable contract checking only at runtime. The existing contract logic relies on closures, which are not supported in constant functions.

This commit also removes one level of indirection for ensures clauses since we no longer build a closure around the ensures predicate.

Resolves #136925

Call-out: This is still a draft PR since CI is broken due to a new warning message for unreachable code when the bottom of the function is indeed unreachable. It's not clear to me why the warning wasn't triggered before.

r? @compiler-errors

[compiler-errors]

In what case is the unreachable error being generated? Can you turn it into a minimal example? I'm not totally sure what's going on with the code generation.

[celinval]

I am still trying to understand why the new logic triggers the new warning, when the old one didn't.

In what case is the unreachable error being generated? Can you turn it into a minimal example? I'm not totally sure what's going on with the code generation.

So, if you look at the following example from one of the tests:

#![feature(contracts)]

pub struct Baz { baz: i32 }

#[core::contracts::requires(x.baz > 0)]
#[core::contracts::ensures(|ret| *ret > 100)]
pub fn nest(x: Baz) -> i32
{
    loop {
        return x.baz + 50;
    }
}

with the existing changes, you will get a warning:

warning: unreachable expression
  --> bar.rs:6:1
   |
6  | #[core::contracts::ensures(|ret| *ret > 100)]
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ unreachable expression
...
10 |         return x.baz + 50;
   |         ----------------- any code following this expression is unreachable
   |

which in a way it makes sense, since we do add a call to check the post-condition after the loop statement. What I don't get is why it wasn't being triggered before, and whether I can mark the new code as allow(unreachable_code).

If I compile with Z unpretty=hir, this is what I get with this PR:

fn nest(x: Baz) -> i32 {
    #[lang = "contract_check_requires"](|| x.baz > 0);
    let __ensures_checker = #[lang = "contract_build_check_ensures"](|ret| *ret > 100);
    #[lang = "contract_check_ensures"]({
            loop { return #[lang = "contract_check_ensures"](x.baz + 50, __ensures_checker); }
    }, __ensures_checker)
}

before the changes, we had:

fn nest(x: Baz) -> i32 {
    #[lang = "contract_check_requires"](|| x.baz > 0);
    let __ensures_checker = #[lang = "contract_build_check_ensures"](|ret| *ret > 100);
    __ensures_checker({ loop { return __ensures_checker(x.baz + 50); } })
}

[celinval]

@compiler-errors any thoughts?

[compiler-errors]

No, I didn't look at it yet

[RalfJung]

This is now outdated, isn't it?

[celinval]

Let me see if we can get rid of it completely

[RalfJung]

Why are you using two different feature gates here?

[celinval]

Good question, for some reason the const stability check isn't working with contracts_internal.

[RalfJung]

What does "isn't working" mean?

We used to have a bug where using a language feature for const stability didn't work (the feature would not get enabled properly), but I thought we had fixed that...

[celinval]

Because I'm getting this error:

error: `contract_check_ensures` is not yet stable as a const intrinsic
  --> contract-const-fn.rs:39:1
   |
39 | #[ensures(move |ret: &u32| *ret > x)]
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |
help: add `#![feature(contracts_internals)]` to the crate attributes to enable
   |
20 + #![feature(contracts_internals)]
   |

[RalfJung]

Ah okay, there's a bunch of macro trickery here that I didn't properly understand.
Your original approach is fine, but should come with a comment:

// Calls to this function get inserted by an AST expansion pass, which uses the equivalent of
// `#[allow_internal_unstable]` to allow using `contracts_internals` functions. Const-checking
// doesn't honor `#[allow_internal_unstable]`, so for the const feature gate we use the user-facing
// `contracts` feature rather than the perma-unstable `contracts_internals`.
#[rustc_const_unstable(feature = "contracts", issue = "128044")]

[fpoli]

I am still trying to understand why the new logic triggers the new warning, when the old one didn't.

In the example, __ensures_checker is an unreachable expression because it's after the argument whose evaluation always returns. Normally, the compiler would highlight __ensures_checker. For example (playground):

warning: unreachable expression
  --> src/lib.rs:22:8
   |
21 |             loop { return contract_check_ensures(x.baz + 50, __ensures_checker); }
   |                    ------------------------------------------------------------ any code following this expression is unreachable
22 |     }, __ensures_checker)
   |        ^^^^^^^^^^^^^^^^^ unreachable expression
   |
   = note: `#[warn(unreachable_code)]` on by default

My understanding is that __ensures_checker is generated by a procedural macro, which attaches the span information of the ensures attribute to __ensures_checker. So, when the compiler tries to highlight __ensures_checker it actually highlights #[core::contracts::ensures(|ret| *ret > 100)]. If this explanation is correct, adding #[allow(unreachable_code)] just before the __ensures_checker in the generated code should suppress the warning:

fn nest(x: Baz) -> i32 {
    #[lang = "contract_check_requires"](|| x.baz > 0);
    let __ensures_checker = #[lang = "contract_build_check_ensures"](|ret| *ret > 100);
    #[lang = "contract_check_ensures"]({
            loop { return #[lang = "contract_check_ensures"](x.baz + 50, __ensures_checker); }
    }, #[allow(unreachable_code)] __ensures_checker)
}

[celinval]

I am still trying to understand why the new logic triggers the new warning, when the old one didn't.

In the example, __ensures_checker is an unreachable expression because it's after the argument whose evaluation always returns. Normally, the compiler would highlight __ensures_checker. For example (playground):

warning: unreachable expression
  --> src/lib.rs:22:8
   |
21 |             loop { return contract_check_ensures(x.baz + 50, __ensures_checker); }
   |                    ------------------------------------------------------------ any code following this expression is unreachable
22 |     }, __ensures_checker)
   |        ^^^^^^^^^^^^^^^^^ unreachable expression
   |
   = note: `#[warn(unreachable_code)]` on by default

My understanding is that __ensures_checker is generated by a procedural macro, which attaches the span information of the ensures attribute to __ensures_checker. So, when the compiler tries to highlight __ensures_checker it actually highlights #[core::contracts::ensures(|ret| *ret > 100)]. If this explanation is correct, adding #[allow(unreachable_code)] just before the __ensures_checker in the generated code should suppress the warning:

fn nest(x: Baz) -> i32 {
    #[lang = "contract_check_requires"](|| x.baz > 0);
    let __ensures_checker = #[lang = "contract_build_check_ensures"](|ret| *ret > 100);
    #[lang = "contract_check_ensures"]({
            loop { return #[lang = "contract_check_ensures"](x.baz + 50, __ensures_checker); }
    }, #[allow(unreachable_code)] __ensures_checker)
}

The call is added as part of lowering the AST today. We can reconsider it though.

[bors]

☔ The latest upstream changes (presumably #138996) made this pull request unmergeable. Please resolve the merge conflicts.

[celinval]

@RalfJung I had to add this line in order to use the same feature gate for unstable and rustc_const_unstable

[RalfJung]

No, we definitely do not want to check the span here, that could be used to bypass recursive const stability.

[rustbot]

Some changes occurred to the intrinsics. Make sure the CTFE / Miri interpreter
gets adapted for the changes, if necessary.

cc @rust-lang/miri, @RalfJung, @oli-obk, @lcnr

Some changes occurred to the CTFE machinery

cc @RalfJung, @oli-obk, @lcnr

Some changes occurred to constck

cc @fee1-dead