Automatically add loop guards without preconditions as invariants

[JonasAlaif]

Currently, when encoding loops:

while { g = G; g } { B1; invariant!(I); B2 }

Prusti will translate this into the Viper:

// Encoding 1
g = G
if (g) {
  B1
  exhale I
  // ... havoc local variables modified in G, B1, or B2
  inhale I
  B2
  g = G
  if (g) {
    B1
    exhale I
    assume false
  }
  // We know !g at this point
}

We can try to assume the loop guard by adding the following:

// Encoding 2
g = G
if (g) {
  B1
  exhale I
  // ... havoc local variables modified in G, B1, or B2

  g = G
  assume g
  B1

  inhale I
  ...
}

This works great, except for when G or B1 include exhale/assert statements (including function calls with preconditions). In such a case, these statements would very likely fail (everything has been havoced, and we have-not/cannot yet assume the invariant) resulting in an unavoidable verification failure. The solution I take is to use encoding 2 if we find no such preconditions, and otherwise fall back to encoding 1 with a warning to the user.
Fixes #448, fixes #995

[JonasAlaif]

The check for fun_preconds is quite surely wrong - I'll need help figuring out where to find the preconditions of relevant functions (I assume that non-pure method calls will already have been inlined as requires/ensures)

[Aurel300]

I think this approach is too hacky. We generate stuff (the invariant) then figure out if what we generated fits into a particular shape (a "pure" invariant). It might also be a bit unpredictable as far as the user is concerned.

[JonasAlaif]

@Aurel300 maybe you saw the version from the first commit, but the second one 1b9ed1a fixes the issue with unnecessarily generating stuff. The way it now works is that we generate (line by line):

g = G
if (g) {
  B1
  exhale I
  // ... havoc local variables modified in G, B1, or B2

  // Check if the above generated G and B1 have preconditions
  // Only generate if yes:
  g = G
  assume g
  B1
 
  // Continue as normal
  inhale I
  ...

There is no looking back at what we generated anymore.
Regarding the second point, I think that making use of the ExprFolder has made things more durable, to the point that it's very predictable to a user which encoding is used. Most of the time if we decide to not use the new Encoding 2, then one couldn't simply just copy and paste the loop guard as a body_invariant!. Moreover, Prusti will emit a warning in such a case, telling you to manually try copy-pasting it, if that's what you need.
I do agree though that this isn't ideal. A better solution would be to always use Encoding 2 and then go through and assume/inhale the required "preconditions" at the correct places.

[Aurel300]

There is no looking back at what we generated anymore.

What I'm referring to is that you walk the generated VIR at all, and figure out which functions were called based on matching FuncApp and which methods based on Exhales. I think more ideally we would have a way to remember that information as we were encoding the loop guard in the first place.

[fpoli]

What I'm referring to is that you walk the generated VIR at all, and figure out which functions were called based on matching FuncApp and which methods based on Exhales.

I agree with this; it's the same issue that we have with the fold-unfold pass. A consequence is that the "it requires the viper preconditions: ..." messages in this PR are going to be as unreadable as the current fold-unfold errors are. The difference is that fold-unfold errors are always bugs of some kind, so the user is not supposed to see them in the long term, while these loop invariant warnings only exist to help the user, so they should be fully understandable.

I think more ideally we would have a way to remember that information as we were encoding the loop guard in the first place.

Either that, or block_preconditions could be redefined on MIR blocks, collecting readable reasons why the block cannot be added to a loop invariant. The existing block_preconditions on VIR could still be used in a debug_assert!(..) to keep the two definitions in sync.

[JonasAlaif]

It seems that with Change asserts to assumes after unrolling this actually succeeds in unrolling every time except for when it runs into pure functions. The impure ones are handily inlined with the functional spec encoded with asserts rather than exhales. Therefore I think we could, in most cases, just report the set of pure functions which prevented the unrolling - this would be readable, without much extra work. Otherwise have just some message that the user should manually add the loop guard as a body_invariant, without further explanation (ideally with some way to disable the warning)

[JonasAlaif]

bors r+

[bors]

Build succeeded:

• all-tests (macos-latest)
• all-tests (ubuntu-latest)
• all-tests (windows-latest)
• clippy-check
• fmt-check
• purification-tests
• test-crates