Quantifier test: The second assertion does not hold [blocks: #2574, #3725, #3924]

[tautschnig]

The assertion requires, among other things, that (i>=0 && i<2) be true for all
values of i, and thus i>=0 (or i<2) for all values of i.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[tautschnig]

I am now wondering what the expectations for a statement like

__CPROVER_assume(!__CPROVER_exists { int i; (i>=0 && i<2) ==> (!__CPROVER_exists{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) });

are. I believe this is actually equivalent to __CPROVER_assume(0); because i>=0 isn't true for all values of i. But that's neither how the back-end currently translates this nor does that match the intention in the regression test.

Edit: I think the assumption one would want is

__CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<2) ==> (__CPROVER_forall{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) });

[tautschnig]

This PR now only has fixes to regression tests as well as additional tests. The actual code fixes will follow in separate PRs.

[tautschnig]

All follow-up PRs actually fixing bugs have now been created.

[allredj]

🚫
This PR failed Diffblue compatibility checks (cbmc commit: fae55f8).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98544461
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

• the cbmc commit has disappeared in the mean time (e.g. in a force-push)
• the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: 52794ca).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98714017

[martin-cs]

I recall @theyoucheng being the original author of these tests, maybe he can provide some input on the original intent. I think they were written as part of the work on AutoSAC.

[tautschnig]

@theyoucheng Input would certainly be appreciated! Merging this for now to unblock other PRs, but comments and fixes will surely be addressed in follow-up work.

[theyoucheng]

I am now wondering what the expectations for a statement like

__CPROVER_assume(!__CPROVER_exists { int i; (i>=0 && i<2) ==> (!__CPROVER_exists{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) });

are. I believe this is actually equivalent to __CPROVER_assume(0); because i>=0 isn't true for all values of i. But that's neither how the back-end currently translates this nor does that match the intention in the regression test.

Edit: I think the assumption one would want is

__CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<2) ==> (__CPROVER_forall{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) });

This test is designed to stress if the quantification back-end handles correctly the input code of the format !__CPROVER_exists. It seems that not (∃a: b) is internally translated into ∀ a: not b. There is the restriction that a is in the form that some integer is both lower and upper bounded. Consequently,

__CPROVER_assume(!__CPROVER_exists { int i; (i>=0 && i<2) ==> (!__CPROVER_exists{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) });

encodes the following

__CPROVER_assume (∀ 0<=i<2 ∃0<=j<2: 1<=c[i][j]<=10);

[tautschnig]

@theyoucheng This suggests that ==> isn't actually implication? My reading of

_CPROVER_assume (∀ 0<=i<2 ∃0<=j<2: 1<=c[i][j]<=10);

Is "for all i in [0, 2) ...", which I'd write as ∀ i. 0<=i<2 => ∃ j. 0<=j<2 && 1<=c[i][j]<=10, but that isn't equivalent to the above __CPROVER_exists if ==> were to be read as implication.

[theyoucheng]

No, ==> is not implication. I think it is just the way that quantifier syntax in CBMC requires. E.g.,

__CPROVER_forall { int i; (i>=0 && i<10) ==> zero_array[i]==0 }

means ∀ 0<=int i<10: zero_array[i]==0.

[tautschnig]

No, ==> is not implication.

Hmm, ok, but that's how it's encoded at expression level and that is also what the simplifier assumes and transforms.

That said, the example you've just given is perfectly sound with ==> interpreted as implication. Questions only arise with existential quantification, where bounded quantification translates into conjunction, not implication.