Sound MoreCompleteExhale on demand

[marcoeilers]

This PR does two things:

First, it adds a mode where Silicon's MoreCompleteExhale mode is used on retry only. That is, Silicon works in its normal greedy mode, and whenever it cannot prove an assertion and retries the proof, MoreCompleteExhale is temporarily turned on (for this purpose, a moreCompleteExhale flag is introduced in the State). Then, the assertion is proved in MCE mode, and the branch continues verifying in greedy mode.
The idea is that MCE is often needed to prove a few assertions in large examples, but is not needed for the vast majority. Since MCE also comes with a performance penalty, we try to do as much as possible in the faster greedy mode, and only switch to MCE when needed.
To do this, the PR adds a new command line flag exhaleMode, which can be set to greedy (default), MCE, or MCE-on-demand. The existing enableMoreCompleteExhale flag is kept for compatibility reasons but deprecated.

Second, it fixes the unsoundness mentioned in issue #594 and #523. I.e., when checking function preconditions in MCE mode, Silicon used to ignore permission amounts and just prove that some permission for every mentioned field and predicate was available. For consistency (until we switch everything to ignoring permission amounts in function preconditions), we now consider permission amounts in these situations as well. The implementation simply uses the existing MCE functionality and, when wildcards are used, also uses the existing summarise function, which is already used elsewhere and does not have the incompleteness problems of the existing implementation.

[jcp19]

On the "on-demand" mode, does silicon still retry once without mce after a failure, but after performing heap consolidation? In other words, is this the sequence of steps that silicon performs on a failure?

1. perform heap-consolidation and retry
2. If failed again, enable mce and retry

[marcoeilers]

On the "on-demand" mode, does silicon still retry once without mce after a failure, but after performing heap consolidation? In other words, is this the sequence of steps that silicon performs on a failure?

1. perform heap-consolidation and retry
2. If failed again, enable mce and retry

On retry, it immediately performs a state consolidation and switches on MCE in one step. I agree it might be worth trying to do only a state consolidation first, but with the current system of nested retries, I don't want to generally add a second retry. If we ever change the retry system in general to avoid the nesting (I still don't know if that's possible or worth it), then this might be a thing we could change.

[jcp19]

LGTM

[marcoeilers]

I added a small change that fixes issue #205, which was previously fixed for standard (greedy) Silicon, also in MCE mode.
As a result, in the test suite, only one test actually fails with MCE and another one times out (see the update in issue #557).

[jcp19]

I added a small change that fixes issue #205, which was previously fixed for standard (greedy) Silicon, also in MCE mode.

As a result, in the test suite, only one test actually fails with MCE and another one times out (see the update in issue #557).

@marcoeilers do you expect this change to have major performance implications when running in mce mode?

[marcoeilers]

I added a small change that fixes issue #205, which was previously fixed for standard (greedy) Silicon, also in MCE mode.
As a result, in the test suite, only one test actually fails with MCE and another one times out (see the update in issue #557).

@marcoeilers do you expect this change to have major performance implications when running in mce mode?

No. In greedy mode, the exact same fix made basically no difference at all.

[mschwerhoff]

LGTM