Warnnings on assumptions that lead to vacuous proofs

[feliperodri]

CBMC version: develop

Operating system: macOS Mojave 10.14.6

What behaviour did you expect: Is there a way to detect false assumptions and throw a warning whenever they appear in the formula? This could help users detect possible vacuous satisfaction.

What happened instead: No warrings. Verification succeeds.

Exact command line resulting in the issue: cbmc main.c
Test case:

// main.c
#include <assert.h>
#include <stdbool.h>

int main() {
  bool cond;
  __CPROVER_assume(cond);
  assert(cond);
}

[feliperodri]

cc. @markrtuttle @SaswatPadhi

[tautschnig]

We currently print such warnings when simplification/constant propagation results in assume(false) (we print aborting path on assume(false) at <location>). Some assumptions, however, will only be found to be unsatisfiable when invoking the solver back-end. It shouldn't be too hard to also test these for satisfiability. Is that what you're asking for?

[tautschnig]

As a side-note: I don't really understand how the provide code example relates to the question.

[SaswatPadhi]

Hi Michael,

Some assumptions, however, will only be found to be unsatisfiable when invoking the solver back-end. It shouldn't be too hard to also test these for satisfiability. Is that what you're asking for?

Yes, precisely.

I don't think the posted code example highlights the real problem -- we just check \forall cond . cond => cond, and it should pass without any warnings.

A __CPROVER_assume essentially prunes the state space for the remainder of the program. We want to show a warning when this state space becomes "empty" after an assumption, because then all assertions would vacuously pass. As you said, aasume(false) prints aborting ... but if the check is more sophisticated we don't see any output:

#include <assert.h>

int main() {
  int x;
  __CPROVER_assume(x > 0);
  __CPROVER_assume(x < 0); // we should get a warning for this
  assert(0 == 1);
}

As you said, this would have to be checked with the solver back-end. Also, it would be nice if the messages we show (aborting ... and whatever we decide for the case above) are warnings.

[SaswatPadhi]

BTW, the fix for this issue could also subsume #5955, so we may not need a separate warning for usage of __CPROVER_r_ok / __CPROVER_w_ok.

[martin-cs]

I don't know if it would help but goto-instrument has an option for converting asserts to assumes. I wonder if something similar would help. Converting assume(X) to assert(X) or maybe assert(!X) would allow all of the existing tools to be used to check whether the assumes were triggered / vacuous. There might be options for --cover as well, for example --cover-failed-assertions. Plus I am sure there used to be an option to insert a assert(0) at the end of main to check for whether things were passing because they are vacuous.

[SaswatPadhi]

Converting assume(X) to assert(X) or maybe assert(!X) would allow all of the existing tools to be used to check whether the assumes were triggered / vacuous.

Yes, this is a nice idea. We could insert an assert(!X) right before assume(X) -- if the assertion turns out to be valid, then the assumption would render the subsequent assertions vacuously true.

Plus I am sure there used to be an option to insert a assert(0) at the end of main to check for whether things were passing because they are vacuous.

We sometimes do that manually in our proofs, but this doesn't help us find the root cause. If we could show a warning for the exact assumption after which everything was vacuously true, that would be super helpful in debugging bad proofs.

[martin-cs]

So it seems there are three possible bits of functionality here:

1. Finding reachable but vacuous / redundant assumptions.

2. Finding unreachable assumptions.

3. Finding assumptions that have no passing traces.

4. Is probably best as an option to goto-check, as you say, inserting assert(!X) before each assumption. 2. is an easy clone of --cover assertion and could be done in the coverage code. 3. Feels could be implemented either way by adding an coverage assertion after each assumption (--cover post-assumption maybe?) or adding assert(!X) after the assumption instead of before.

I see value in all of these but I think they should be instrumentation / cover modes rather than separate analyses or warnings.

[TGWDB]

Adding to the discussion, but also want to direct to a concrete plan for what a suitable solution would be.

So it seems there are three possible bits of functionality here:

1. Finding reachable but vacuous / redundant assumptions.

I agree this seems reasonable and nice, although I'm not sure it addresses the motivation/cause that was mentioned by @SaswatPadhi :

If we could show a warning for the exact assumption after which everything was vacuously true, that would be super helpful in debugging bad proofs.

My interpretation of the above is the desire to see the point at which an unreachable block/path is created (perhaps regardless of the existence of assumptions in this path?). Clarity on this interpretation appreciated.

2. Finding unreachable assumptions.

Kind of like the above, except also subtly different. Could be nice to have, but may not address the root motivation.

3. Finding assumptions that have no passing traces.

I think, this is closest to the motivation. I would perhaps rephrase this as something like: "raise a warning/error when an assumption causes traces to no longer continue/become unreachable". I think my rephrase is different in that this is to find the assumption that causes the traces to no longer pass, where as the quoted approach would (also) warn on assumptions that are unreachable due to earlier assumptions causing them to be unreachable. (Note that either of these may be the best approach, but I want to discuss the options.)

4. Is probably best as an option to goto-check, as you say, inserting assert(!X) before each assumption. 2. is an easy clone of --cover assertion and could be done in the coverage code. 3. Feels could be implemented either way by adding an coverage assertion after each assumption (--cover post-assumption maybe?) or adding assert(!X) after the assumption instead of before.

I see value in all of these but I think they should be instrumentation / cover modes rather than separate analyses or warnings.

I agree they all have value, I'd like to know which one(s) are the best to solve the issue so a fix can be developed.

[SaswatPadhi]

Thanks for looking into this issue, @TGWDB.

I agree with your assessment that (3) above is what @feliperodri and I are looking for. Our main concern is being able to root cause "VERIFICATION SUCCESSFUL" cases that were vacuous (i.e., had no passing traces).

[TGWDB]

I'm posting again to ensure that I have the right idea, I'm going to start planning a proper solution. At the moment the goal is to do the following.

cbmc will raise a warning when an assumption causes the current path/trace to cease to be reachable any further. The warning will be raised on the assumption that creates this unreachable point, not on any later points (that may still report verification successful as currently done).

If this (very short and rough) specific is acceptable we can work out how to implement. (Also feel free to comment if you foresee difficulties in achieving this.)

[SaswatPadhi]

The plan sounds good to me. I had posted this snippet above, which could be used a small regression test for this case:

#include <assert.h>

int main() {
  int x;
  __CPROVER_assume(x > 0);
  __CPROVER_assume(x < 0); // we should get a warning for this
  assert(0 == 1);
}

Regarding the implementation, Martin suggests:

3. Feels could be implemented either way by adding an coverage assertion after each assumption (--cover post-assumption maybe?) or adding assert(!X) after the assumption instead of before.

I might be missing some context regarding these coverage flags, but wouldn't assert(!X) always fail after assume(X), even when the assumption doesn't actually eliminate all paths?
I was suggesting adding assert(!X) just before assume(X).

[martin-cs]

On Mon, 2021-06-07 at 06:32 -0700, Saswat Padhi wrote: Regarding the implementation, Martin suggests: > 3. Feels could be implemented either way by adding an coverage > assertion after each assumption (`--cover post-assumption` maybe?) > or adding `assert(!X)` after the assumption instead of before. I might be missing some context regarding these coverage flags, but wouldn't `assert(!X)` always fail after `assume(X)`, even when the assumption doesn't actually eliminate all paths?

It will only fail if it is reachable. If the assumption eliminates all paths then the assertion will pass and, in keeping with the rest of the coverage infrastructure, it will be marked as unreachable.

I was suggesting adding `assert(!X)` just before `assume(X)`.

To my mind this is more like checking to see whether the assumption is vacuous. For example: x = 1; assert(x == 1); assume(x == 1); The assumption is vacuous but does have paths through it. If the assert is safe then the assumption is vacuous. These feel like two sides of the same coin. An assumption is vacuous if `path_condition => assumption` and it has no paths through it if `path_condition => !assumption`.

[SaswatPadhi]

Thanks for the explanation, @martin-cs.

I think I understand how assert(!X) after assume(X) could work too. If it passes (only possible when unreachable) then the previous assumption eliminated all paths and led to vacuity.

With my suggestion of placing assert(!X) before assume(X), if the assertion passes, then !X always holds at the code point, and thus assume(X) would be assume(false).

[martin-cs]

As I (meant to) suggest earlier, I would go with the forms that can most easily be integrated into goto_check or the coverage instrumentation #6057 (comment)

[jimgrundy]

Sorry to come very late to this party. But, I have opinions/experiences to share....

I'm used to a model checker that offer the following primitive concepts:

• assume(p) : add p to the path condition
• assert(p) : attempt to satisfy (path & ~p). If satisfied report error. If unsat, report success. (checks a universal property)
• cover(p) : attempt to satisfy (path & p). If unsatisfiable report error. If sat, report success. (checks an existential property)

@kroening mentioned the other day that CBMC (used to) support a cover primitive like this, but it didn't seem to get used much, or maybe people didn't find it intuitive. My experience was that this construct was extremely valuable for debugging.

Imagine a world in which you have this construct. Then you can achieve the goal we are shooting for here by transforming:

assume(p);

into

cover(p); assume(p);

My former tool (Jasper) would also perform the following transformation automatically (controllable with a switch):

assert(p -> q);

into

cover(p);
assert(p -> q);

A common problem I would face would be debugging why some code or a condition was unreachable. Writing covers for conditions earlier in the control flow was invaluable to me as a technique for debugging these. That's how everyone did it.

So, my suggestion is this:

1. (re)enable support for the cover construct
2. add an optional code transformation that instruments assumptions (and perhaps (implications in) assertions) with covers.

[TGWDB]

This is now supported by the --cover assume option in develop and will be in the next release.

[jimgrundy]

Looks like we'll be able to close this after the next release.

[jimgrundy]

Thanks for building this for us.