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

[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.

[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

[RalfJung]

Just a nit

[RalfJung]

LGTM from a const-eval perspective. I can't say anything about the compiler/ changes though.

[tautschnig]

Just confirming that all the contracts proposed in #136578 pass with the latest set of changes in this PR.

[celinval]

@compiler-errors, any chance you can take a look at this PR?

[oli-obk]

@bors r=compiler-errors,oli-obk,RalfJung

[bors]

📌 Commit 13f1c84 has been approved by compiler-errors,oli-obk,RalfJung

It is now in the queue for this repository.