Cleanup regression tests for quantified contracts #6145
Conversation
SaswatPadhi
force-pushed
the
quantifiers-tests-fix
branch
from
a503b87 to
15e3336
Compare
SaswatPadhi
force-pushed
the
quantifiers-tests-fix
branch
from
15e3336 to
303bcb5
Compare
|
@feliperodri Please review the first commit. The second one is just for renaming. |
| for(int i = 0; i <= MAX_LEN; i++) | ||
| { | ||
| if(i < len) | ||
| found_zero |= (arr[i] == 0); | ||
| } |
There was a problem hiding this comment.
We are not proving these programs are correct, because we're not unrolling these loops. Thus, we have two options here:
- Add invariants to these loops;
- Update our regression-test script to also call CBMC with the correct bounds and
--unwinding-assertions;
I'd prefer option (1). In any case, we can create a GitHub issue for this now and tackle it on a separate PR (for all test cases).
There was a problem hiding this comment.
But all loops in CBMC are always unrolled. This one is too, you can see in the CBMC output.
With symbolic bounds the unrolling just never stops, so we give --unwind to limit unrolling and then --unwinding-assertions to make sure our limited unrolling is sound.
Another way to stop the unrolling is to provide an invariant, and then we just reason about a single arbitrary iteration.
Here, since the loop bounds are constants (0 and 128), the unrolling stops automatically, and is always sound since there is nothing more to unroll (i.e. we didn't limit anything).
| range for i. However, in the current implementation of quantifier handling, | ||
| the (0 <= i && i < 10) statement is not interpreted as an explicit range, but | ||
| instead, as part of a logic formula, which causes verification to succeed. | ||
| This is fully supported (without requiring full unrolling) with the SAT backend. |
There was a problem hiding this comment.
What do you mean by without requiring full unrolling?
There was a problem hiding this comment.
May be there is a better way to phrase this. I was being lazy.
I meant to say that exists x . (L <= x <= U) && P(x) is not unrolled to P(L) \/ P(L+1) \/ ... \/ P(U-1) \/ P(U) in a negative context.
In a negative context symbolic or even no explicit bounds at all would work for exists, e.g. assume(exists x . P(x)) works fine because CBMC just introduces a temporary variable x and then assume(P(x)).
SaswatPadhi
force-pushed
the
quantifiers-tests-fix
branch
from
303bcb5 to
ea71d66
Compare
Cleaned up some the quantified contracts, changed some KNOWNBUG cases to CORE, added regex patterns in descriptions to make sure we catch expected failures (and don't ignore unexpected ones) etc.
Please review individual commits. The second commit is just a renaming:
*-01->*-enforceand*-02->*-replace. Some tests didn't adhere to this convention (and were double testing the same context, enforcement / replacement), so I changed the context appropriately and now I think we are reasonably exhaustive on corner cases.Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/My commit message includes data points confirming performance improvements (if claimed).My PR is restricted to a single feature or bugfix.White-space or formatting changes outside the feature-related changed lines are in commits of their own.