Guard HIR lowered contracts with contract_checks

[dawidl022]

Refactor contract HIR lowering to ensure no contract code is executed when contract-checks are disabled.

The call to contract_checks is moved to inside the lowered fn body, and contract closures are built conditionally, ensuring no side-effects present in contracts occur when those are disabled. This partially addresses #139548, i.e. the bad behavior no longer happens with contract checks disabled (-Zcontract-checks=no).

The change is made in preparation for adding contract variable declarations - variables declared before the requires assertion, and accessible from both requires and ensures, but not in the function body (PR #144444). As those declarations may also have side-effects, it's good to guard them with contract_checks - the new lowering approach allows for this to be done easily.

Contracts tracking issue: #128044

Known limiatations:

• It is still possible to early return from the function from within a contract, e.g.

  #[ensures({if x > 0 { return 0 }; |_| true})]
  fn foo(x: u32) -> i32 {
      42
  }

  When foo is called with an argument greater than 0, instead of 42, 0 will be returned.

  As this is not a regression, it is not addressed in this PR. However, it may be worth revisiting later down the line, as users may expect a form of early return from contract specifications, and so returning from the entire function could cause confusion.

• Contracts are still not optimised out when disabled. Currently, even when contracts are disabled, the code generated causes existing optimisations to fail, meaning even disabled contracts could impact runtime performance. This issue is blocking Add contracts for all functions in Alignment #136578, and has not been addressed in this PR, i.e. the mir-opt and codegen tests that fail in Add contracts for all functions in Alignment #136578 still fail with these new HIR lowering changes.

[rustbot]

r? @oli-obk

rustbot has assigned @oli-obk.
They will have a look at your PR within the next two weeks and either review your PR or reassign to another reviewer.

Use r? to explicitly pick a reviewer

[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

[celinval]

What if we remove the contract_checks intrinsic for now? Instead, we only lower the contracts if the user passes -Zcontract-checks=yes. I think this will be much simpler and it won't add extra optimization overhead it will likely fix the issue from #136578.

The main downside is that there will be no way to enable the std contract check without rebuilding it. But I think this is something that we can worry about later. Most analysis tools, including MIRI, already rebuilds the std library, so they should be able to enable contracts.

[dawidl022]

What if we remove the contract_checks intrinsic for now? Instead, we only lower the contracts if the user passes -Zcontract-checks=yes. I think this will be much simpler and it won't add extra optimization overhead it will likely fix the issue from #136578.

I think this would indeed fix the issue. I wanted to try it out, but wasn't sure how to access compiler flags (e.g. -Zcontract-checks=yes) from the lowering code (or the parser for that matter). Any advice on how to achieve this?

[celinval]

You should be able to access them through self.tcx.sess.opts.unstable_opts.

[RalfJung]

Making the same thing both a lang item and an intrinsic doesn't make a lot of sense. Why do you propose to do this?

[dawidl022]

Making the same thing both a lang item and an intrinsic doesn't make a lot of sense.

Could you please elaborate why this doesn't make sense, or point me to sources where I can read up on this? I don't really understand the relationship between the two.

Why do you propose to do this?

I added the lang item annotation so that I can generate HIR code referring to contract_checks, and did not think there was anything wrong with that, given that both contract_check_requires and contract_check_ensures are already marked both as lang items and intrinsics.

[RalfJung]

Hm, I didn't realize we already have things hat are both.

The reason I said that it doesn't make sense is that intrinsics are one way to make a function magic, and lang items are another. Having a function be magic in 2 different ways is... a bit too much magic?^^

Lang items are strictly more powerful than intrinsics, so I would have expected this to be just a lang item then, and not also an intrinsic. But if this works fine then I guess we can keep it for now. It can always be changed later.

[dawidl022]

What if we remove the contract_checks intrinsic for now? Instead, we only lower the contracts if the user passes -Zcontract-checks=yes. I think this will be much simpler and it won't add extra optimization overhead it will likely fix the issue from #136578.

I'm happy to implement it that way, and if there is consensus, close this this PR in favour of that solution. I imagine that even with -Zcontract-checks=no, we'd still want to typecheck the contracts (at least in the debug build) to ensure they are well-formed. I'm wondering what would be the best way to achieve this, given typechecking occurs after HIR lowering.

Maybe the "typechecking when disabled issue" is not a priority right now, given that we're still figuring out what exactly the contract language should be (i.e. what extra rules contracts have to obey w.r.t. regular rust code). If that's the case, I'm happy to proceed with whatever makes most sense for now.

Right now, when naively guarding the call to lower_contract with self.tcx.sess.opts.unstable_opts I'm getting a regression fixed by #136837, so I need to figure out what exactly is going on there with associated items.

[celinval]

The suggestion is for this code to be either:

let __postcond = if false {
  // ...
}

or

let __postcond = if true {
  // ...
}

depending on the value of the -Z contract-checks

[dawidl022]

Thanks for the suggestion! I tried implementing this change in a branch, and the codegen test still fails (tests/codegen/cross-crate-inlining/leaf-inlining.rs) with the alignment contracts from #136578.

I have not looked into why the test is failing, but based on the name, I suspect the optimiser is not able to inline functions it was previously able to, because now they have the if false ... contract code, and maybe the inlining optimisation runs before the if false elimination run, (or there is no if false optimisation in the optimisation settings the test runs under, even though it is set to opt-level 3)?

I'm happy to investigate more deeply why this test fails, so that we understand how to fix this optimisation problem.

My branch: https://github.com/dawidl022/rust/tree/contracts/guarded-lowering-compiler-flag-alignment-tests

[celinval]

If you want to debug this further you should first check if the branch has been eliminated in the final optimized mir. If it has, you should check if rustc runs the inline pass after dead code elimination or just before.

I believe that llvm inline pass will still run, so this may not be a problem and we may need to adjust the tests. But it's worth checking with the library team.

[dawidl022]

@celinval @tautschnig a small update on the progress on my investigation. I noticed that removing #[rustc_intrinsic] from contract_check_requires and contract_check_ensures allows the optimiser to do its job. As @RalfJung pointed out in another comment here, having both lang_item and rustc_intrinsic on the same function seems suspicious. What is the reason why those functions were annotated with both?

Unfortunately, just removing those annotations is yet not enough to fix the issue, as contract_checks itself remains an intrinsic (therefore not inlinable?), and doesn't seem to work properly when the rustc_intrinsic annotation is removed, and the body replaced with cfg!(contract_checks) (as suggested by the FIXME comment).

When using the approach @celinval suggested here with let __postcond = if false {, I'm struggling to get the constants to propagate and get eliminated from contract_check_ensures.

I.e. wrapping the body of contract_check_ensures with if false { successfully gets optimised and the codegen inlining tests pass, but doing the same with an argument passed to contract_check_ensures that is set to false doesn't seem to work. I will continue to investigate to see if we can resolve this somehow. I'd also appreciate any further suggestions of things to try :)

[celinval]

The reason for this to be an intrinsic is for tools / custom backends to be able to override the behavior

[celinval]

Why would you still need the lang item?

[dawidl022]

I'm not sure. Do you know the reason they were marked as lang items to begin with?

[RalfJung]

I.e. wrapping the body of contract_check_ensures with if false { successfully gets optimised and the codegen inlining tests pass, but doing the same with an argument passed to contract_check_ensures that is set to false doesn't seem to work. I will continue to investigate to see if we can resolve this somehow. I'd also appreciate any further suggestions of things to try :)

It is very hard to follow what you are doing when all one can look at is a big PR. Would be much easier to have a high-level discussion first, sketching out the lowering "on paper" until it has a shape that has good chances of being optimizeable.

It seems you want to do something that involves inlining, and intrinsics don't get inlined. So you'll either need not-an-intrinsic or a custom opt pass. But I really don't know since I don't have the time to reverse engineer what you are trying to do.

[dawidl022]

Goal: fully optimise out contracts when disabled, whilst preserving type checking

As suggested by @RalfJung, I am starting a high-level discussion on what the HIR lowering should look like "sketching out the lowering "on paper" until it has a shape that has good chances of being optimizeable.", detailing the designed I've tried out and what didn't work in each. Hopefully, we can together come up with a lowering strategy that meets the above goal.

Note: the above goal was not the original purpose of this PR, but given the discussions here, it seems it is desirable. The original purpose of the PR was to ensure no part of the contract was executed when disabled, and to prepare for #144444.

New lowering approach proposed in this PR

We split the lowering of contracts into 4 distinct cases, providing the lowered pseudocode for each:

1. Both a requires and an ensures clause is present:

   let __postcond = if contracts_checks() {
       contract_check_requires(PRECOND);
       Some(|ret_val| POSTCOND)
   } else {
       None
   };
   contract_check_ensures(__postcond, { body })

2. Only a requires clause is present:

   if contracts_check() {
       contract_requires(PRECOND);
   }
   body

3. Only an ensures clause is present:

   let __postcond = if contracts_check() {
       Some(|ret_val| POSTCOND)
   } else {
       None
   };
   contract_check_ensures(__postcond, { body })

4. Neither requires nor ensures is present:

   body

Limitations of the lowering approach

Since contracts_checks is an intrinsic, it cannot be inlined, and therefore when contract checks are disabled, they cannot be optimised out via an if false elimination optimisation pass. This in turn affects the ability of functions to be inlined, as seen in the codegen test failure in #136578.

Potential solutions

Evaluate contract_checks compiler flag during lowering

To ensure contracts are still type checked, they should be present in the lowered HIR, but optimised out during later passes of the compiler.

One approach is to inline the value of the contract_checks flag directly into the lowered HIR (as suggested by @celinval):

let __postcond = if false {
    contract_check_requires(PRECOND);
    Some(|ret_val| POSTCOND)
} else {
    None
};
contract_check_ensures(__postcond, { body })

Another approach is to use cfg!(contract_checks):

let __postcond = if cfg!(contract_checks) {
    contract_check_requires(PRECOND);
    Some(|ret_val| POSTCOND)
} else {
    None
};
contract_check_ensures(__postcond, { body })

The difference between the above two approaches is not clear to me, so I'd appreciate any comments on the matter.

While this approach ensures the call to contract_check_requires is indeed optimised out, the call to contract_check_ensures remains, which is not optimised out (due to it being an intrinsic).

Remove #[rustc_intrinsic] annotations in contract_check_ensures

In addition to the above, we also remove the rustc_intrinsic annotation from contract_check_ensures so that it can be inlined and optimised out when __postcond is None.

However, this optimisation does not seem to occur, i.e.

contract_check_ensures(__postcond, { body })

does not get optimised to just body when __postcond is None.

Remove #[rustc_intrinsic] annotations on all contract intrinsics

This would make contract_checks, contract_check_requires and contract_check_ensures all potentially inlinable.

The body of contract_checks would be:

pub const fn contract_checks() -> bool {
    cfg!(contract_checks)
}

However, for whatever reason, this approach was broken - contract checks never got enabled, even when compiled with the contract_checks flag.

Conditionally compile call to contract_check_ensures

let __postcond = if false {
    contract_check_requires(PRECOND);
    Some(|ret_val| POSTCOND)
} else {
    None
};
{ body }

Since contracts are already type checked in the let __postcond = if false { part of the lowered body, we could simply conditionally compile the call to contract_check_ensures based on the value of the contract_checks compiler flag. However, this seems to break type inference on the ensures clause, likely because the __postcond closure never gets used when contracts are disabled:

error[E0283]: type annotations needed for `&_`
  --> /Users/dawidl022/Development/rust/tests/ui/feature-gates/feature-gate-contracts.rs:7:29
   |
LL | #[core::contracts::ensures(|ret| *ret > 0)]
   |                             ^^^       - type must be known at this point
   |
   = note: cannot satisfy `_: PartialOrd<i32>`
help: consider giving this closure parameter an explicit type, where the placeholders `_` are specified
   |
LL | #[core::contracts::ensures(|ret: &_| *ret > 0)]

Wrap call to contract_check_ensures in another if statement

let __postcond = if cfg!(contract_checks) {
    contract_check_requires(PRECOND);
    Some(|ret_val| POSTCOND)
} else {
    None
};

if cfg!(contract_checks) {
    contract_check_ensures(__postcond, { body })
} else {
    { body }
}

For some reason, the compiler did not like the fact that body was lowered twice, or at least that's the impression I got based on the error message. Maybe I did something wrong in the lowering implementation?

error: internal compiler error: `usize` overridden by `usize` for HirId(DefId(0:26407 ~ core[b102]::ptr::alignment::{impl#0}::mask).67) in DefId(0:26407 ~ core[b102]::ptr::alignment::{impl#0}::mask)
   --> library/core/src/ptr/alignment.rs:189:38
    |
189 |       pub const fn mask(self) -> usize {
    |  ______________________________________^
190 | |         // SAFETY: The alignment is always nonzero, and therefore decrementing won't overflow.
191 | |         !(unsafe { self.as_usize().unchecked_sub(1) })
192 | |     }
    | |_____^
    |
note: delayed at compiler/rustc_hir_typeck/src/fn_ctxt/_impl.rs:154:28

Lower body once, but wrap call to contract_check_ensures

let __postcond = if cfg!(contract_checks) {
    contract_check_requires(PRECOND);
    Some(|ret_val| POSTCOND)
} else {
    None
};

let ret = { body };

if cfg!(contract_checks) {
    contract_check_ensures(__postcond, ret)
} else {
    ret
}

I did not test this lowering approach yet.

Conclusion

There are probably many lowering strategies that I have not mentioned here, so I'd appreciate any suggestions!

[RalfJung]

Remove #[rustc_intrinsic] annotations in contract_check_ensures

contract_check_ensures is probably too big for the inliner, that's why this does not suffice.

Remove #[rustc_intrinsic] annotations on all contract intrinsics

However, for whatever reason, this approach was broken - contract checks never got enabled, even when compiled with the contract_checks flag.

Is something setting cfg!(contract_checks)? You can't just write cfg!(ponies_and_rainbows) and expect that to work without actually adding support for that cfg in the compiler.^^

However, I also don't understand what you think that would achieve. You already generate hard-coded false/true constants. Why do you even want to also have a contract_checks() -> bool function and who's in charge of keeping that in sync?

Conditionally compile call to contract_check_ensures

Regarding the inference issue - the type of ret should be the return type of the function so the desugaring should be able to add a type annotation for that?

Lower body once, but wrap call to contract_check_ensures

This one seems most promising to me. Everything the MIR opts need is right there in the body without knowing anything about what the intrinsics do, and passing ret to contract_check_ensures might be enough for type inference to figure out the type of the postcondition predicate.