Incremental solving producing cprover status as it goes #5316
Conversation
thk123
changed the title
thk123
force-pushed
the
print-status-during-incremental-solving
branch
from
c743717 to
1af207d
Compare
thk123
force-pushed
the
print-status-during-incremental-solving
branch
from
1af207d to
9efa16d
Compare
thk123
requested review from
chrisr-diffblue,
kroening,
peterschrammel,
smowton and
tautschnig
as code owners
thk123
force-pushed
the
print-status-during-incremental-solving
branch
from
9efa16d to
b75ab07
Compare
| [](const std::pair<irep_idt, property_infot> &property) { | ||
| return property.second.status == property_statust::FAIL; | ||
| }); | ||
| std::string status = any_failures ? "FAILURE" : "INCONCLUSIVE"; |
There was a problem hiding this comment.
How does this behave in the success case?
Please check the output also on a VERIFICATION SUCCESSFUL test.
There was a problem hiding this comment.
@peterschrammel In the commit message this says that it's not possible to conclude that verification is successful before the unwinding is finished, so it doesn't matter?
| [](const std::pair<irep_idt, property_infot> &property) { | ||
| return property.second.status == property_statust::FAIL; | ||
| }); | ||
| std::string status = any_failures ? "FAILURE" : "INCONCLUSIVE"; |
There was a problem hiding this comment.
@peterschrammel In the commit message this says that it's not possible to conclude that verification is successful before the unwinding is finished, so it doesn't matter?
| -- | ||
| ^warning: ignoring | ||
| -- | ||
| Ensure that with multiple properites, the incremental stauts |
There was a problem hiding this comment.
Can this be changed?
properites->propertiesstauts->status
| switches to failure as soon as one property has been falsified | ||
| but keeps unwinding till it has resolved them all | ||
|
|
||
| Use `--no-propagation` to ensure that even the output is the same regardless of whether the asserts are checked via the solver or the constant propogator |
There was a problem hiding this comment.
propogator -> propagator
| -- | ||
| ^warning: ignoring | ||
| -- | ||
| Ensure that with multiple properites, the incremental stauts |
The incremental status should report failure from the first unwinding for which one property is falsified.
It is not possible to conclude successful verification before the unwinding has finished, so this prints inconclusive until the analysis is complete. However, if one property has been falsified, then even though the analysis can continue to check other properties, the verification will certainly fail.
We want to print the status after we've done any solving for that unwind, but before we've done an extra step of symexing. We should not print in the event the full equation has been generated, as then we have a full solution so ins't incremental. Ditto we don't need to print the status if we've found a failure, as this function will be called again to do the next symex invocation if there are further propreties to check
We now print after all solving, and the last thing before the next increment, therefore the printing checks are easier to check immediately precedes the next unwinding, rather than checking appears after the increment we are talking about.
In this case, the status is inconclusive until completion, at which point success will be reported by CBMC overall.
thk123
force-pushed
the
print-status-during-incremental-solving
branch
2 times, most recently
from
1cf3722 to
4972f54
Compare
|
@peterschrammel @NlightNFotis comments addressed -> it required a little tweaking to exactly where the printing went to get it working correctly but I'm happy with it now. The behaviour is: In each step, before doing the next round of unwinding, but after solving the equation, we will print inconclusive if there no failed properties yet, otherwise we'll print failed. Once we've either got an answer to all properties, or finished unwinding, no incremental status will be reported, since the final status will be reported next. |
Needs some tidy up but this prints output that is consistent with the
old version