Reachability slicer: split cfg walks into two phases #3218
Conversation
smowton
requested review from
chrisr-diffblue,
martin-cs and
peterschrammel
as code owners
smowton
force-pushed
the
smowton/fix/reachability-slicer-take-3
branch
from
3ef6172 to
4d1cc88
Compare
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 4d1cc88).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/88799021
| /// \param criterion the criterion we are trying to hit | ||
| void reachability_slicert::fixedpoint_from_assertions( | ||
| const is_threadedt &is_threaded, | ||
| slicing_criteriont &criterion) |
There was a problem hiding this comment.
what are the side effects on this?
There was a problem hiding this comment.
None. Pushed an extra commit to constify these, at the risk of @tautschnig's ire re: scope creep ;)
| ^SIGNAL=0$ | ||
| main\(\) | ||
| -- | ||
| ^warning: ignoring |
There was a problem hiding this comment.
Can you check that b is not in the slice?
There was a problem hiding this comment.
No, it is in the slice, since it calls c.
There was a problem hiding this comment.
Ah, I see, the forward walk is not used in the way I assumed.
There was a problem hiding this comment.
Is there a test that actually slices away something?
There was a problem hiding this comment.
The original cbmc/reachability-slice has two tests looking for slicing. These new ones were particularly looking for over-slicing since that's the bug @polgreen / @tautschnig encountered.
The first phase walks outwards towards __CPROVER__start, visiting all callers but recording callsites seen en route, then the second phase walks into callees not seen in the first phase, restricting the search to known reachable functions. This fixes the previous algorithm, which attempted the same logic but could visit too few functions when a particular functions was encountered as a callee before later being seen as a caller -- the latter results in more code being visited because the calling context is unknown, and so must be done first.
smowton
force-pushed
the
smowton/fix/reachability-slicer-take-3
branch
from
1a7b501 to
0b64e10
Compare
This enables us to use a const-ref in the reachability and full slicers.
smowton
force-pushed
the
smowton/fix/reachability-slicer-take-3
branch
from
0b64e10 to
0d8e3c1
Compare
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 0d8e3c1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/88837602
|
As a side remark before getting to the key parts: "Constify slicing_criteriont::operator()" would make for a nice separate PR - it could likely be merged more or less immediately, but also it may need to be reverted in future in case someone comes up with a criterion that evolves as you query it (maybe that's weird, but that was my thinking when I originally wrote this code and I thus left it non-const). |
There was a problem hiding this comment.
I think this is ok, but I can hardly believe we'd be the first to solve this problem. @kroening mentioned BEBOP (I think that would be Fig. 3 of https://drona.csa.iisc.ac.in/~deepakd/tpa-2016/bebop.pdf), and there might be others. If at all possible, we should be re-using algorithms and terminology and refer to those for documentation.
|
I find it quite hard to parse those academic code listings with highly abbreviated and subscript-littered function and variable names, but I don't think this particularly relates to their reachability algorithm, because the algorithm described in Figure 3 starts at the head of |
|
I'll have a search for something comparable though, and let you know what I find. Merging these meanwhile, then will follow up with a doc PR if I find anything. |
The first phase walks outwards towards __CPROVER__start, visiting all callers but recording
callsites seen en route, then the second phase walks into callees not seen in the first phase,
restricting the search to known reachable functions. This fixes the previous algorithm, which
attempted the same logic but could visit too few functions when a particular functions was
encountered as a callee before later being seen as a caller -- the latter results in more code
being visited because the calling context is unknown, and so must be done first.
This is an alternative to #2748, see comments there for more detail.