Only safety-check paths when new VCCs get added #3237
Conversation
karkhaz
requested review from
kroening,
peterschrammel,
pkesseli,
smowton and
tautschnig
as code owners
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 75d1f94).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/89423550
karkhaz
force-pushed
the
kk-thrifty-model-checking
branch
from
75d1f94 to
b5cbaa0
Compare
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: b5cbaa0).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/89583138
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.
The path strategy unit tests now emit an index showing which result in the expected list of results was the one that failed.
This is in preparation for a future commit, where the static method do_language_agnostic_bmc will need to make a final report after all paths have been exhausted. These methods were previously marked as virtual, so the zero-parameter non-static variants of these methods have been kept as a convenience; they do nothing other than call into the static variant.
CBMC will no longer bother running safety checks on path segments that did not generate any new VCCs when running in path-exploration mode. A "path segment" is a list of instructions between two program branch points. CBMC would previously pause symbolic execution and run safety checks at every branch point, which is wasteful when no additional VCCs have been generated since the last pause. As of this commit, CBMC will check to see if new VCCs have been added, and only do the safety check if so. To support this, the new member goto_symext::path_segment_vccs records the number of VCCs that were newly generated along this path segment. It differs from the VCC counters in goto_symex_statet, which hold the number of VCCs generated along the current path since the start of the program. goto_symext objects are minted for each path segment, so they don't hold any information about the VCCs previously along the path. This commit also removes the "Starting new path" output, since this no longer makes much sense. On the other hand, there is an additional final status output; CBMC will report failure after the entire program has been explored if even a single path contained a failing assertion, and report success otherwise. The unit tests have been updated to reflect the fact that CBMC no longer emits "SUCCESS" at each branch point and at the end of paths, and also that CBMC makes one final report of the program safety as a whole. This commit fixes diffblue#2684.
karkhaz
force-pushed
the
kk-thrifty-model-checking
branch
from
b5cbaa0 to
5099467
Compare
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: 5099467).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/89602775
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.
|
Oh okay. Thank you for the merge! |
CBMC will no longer bother running safety checks on path segments that
did not generate any new VCCs when running in path-exploration mode.
A "path segment" is a list of instructions between two program branch
points. CBMC would previously pause symbolic execution and run safety
checks at every branch point, which is wasteful when no additional VCCs
have been generated since the last pause. As of this commit, CBMC will
check to see if new VCCs have been added, and only do the safety check
if so.
To support this, the new member goto_symext::path_segment_vccs records
the number of VCCs that were newly generated along this path segment. It
differs from the VCC counters in goto_symex_statet, which hold the
number of VCCs generated along the current path since the start of the
program. goto_symext objects are minted for each path segment, so they
don't hold any information about the VCCs previously along the path.
This commit also removes the "Starting new path" output, since this no
longer makes much sense. On the other hand, there is an additional final
status output; CBMC will report failure after the entire program has
been explored if even a single path contained a failing assertion, and
report success otherwise.
The unit tests have been updated to reflect the fact that CBMC no longer
emits "SUCCESS" at each branch point and at the end of paths, and also
that CBMC makes one final report of the program safety as a whole.
This commit fixes #2684.