Fix reachability slicer when used with recursive or unreachable functions

[tautschnig]

No description provided.

[tautschnig]

@smowton Would you mind taking a look, and possibly check it for regressions on your end?

[smowton]

Does true, unknown, false really mean much here? I'd suggest using an enum (also documented) to indicate what we're doing

[tautschnig]

@smowton Updated in line with the suggestions you had made yesterday - thank you!

[smowton]

LGTM, some nitpicks

[smowton]

reaches_assertion doesn't seem like a great name anymore? Maybe just state?

[smowton]

How about

    /// The status of each node during backwards depth-first traversal:
    /// A functions starts out NOT_SEEN, is raised to BODY_SEEN if we have
    /// seen a call to this function but know where it was called from (at this point
    /// we mark the function and anything reachable from it), then may finally be
    /// raised to BODY_AND_CALLERS_SEEN if we don't know what function
    /// calls this function, and therefore mark all of its callers as well.

[smowton]

Oh one more thing, how convinced are you this problem is restricted to backwards operation? In forwards mode I might similarly call a() and then later return into it, leading to the same problem?

[kroening]

Is there a way to reduce these to well-known, standard graph problems? And then use standard algorithms for the graph problem?

[kroening]

Or maybe problems on pushdown machines?

[kroening]

Say use something like the bebop algorithm?

[polgreen]

Since this is a soundness bug, which gives the user no indication that they have hit a bug, could this fix please be merged? And an issue created to investigate using the bebop algorithm, and to check that the forward reachability slicer doesn't have the same bug?

(I tried to create a similar example for the forward reachability slicer and couldn't recreate it, but that doens't necessarily mean it's fixed. I don't understand what the use case is for the forward reachability slicer though so I might be missing something).

[martin-cs]

@polgreen : I don't know this part of the code super well but am happy to approve it. However, right now we can't merge it as there are CI failures. One of them is clang-format, which can easily be fixed by someone, the other is a cmake failure which I /think/ might be transitory.

[smowton]

I can take a look

[martin-cs]

@smowton : appreciated.

[allredj]

Passed Diffblue compatibility checks (cbmc commit: 25ea7b3).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87740471

[smowton]

CI fixed. I'm pretty sure the forwards slicer is vulnerable to the same mistake, but have also failed to come up with an example so far. It's tricky because when a function has different callers they're visited in arbitrary order.

Solution-wise, thinking about it more, it would surely suffice to make sure all-callers nodes are visited before known-caller ones, since in the former case we do strictly more work. Therefore we could just maintain the working set sorted (partitioned, really) by the caller-is-known flag. Equivalently, split the visit routines into one that visits outwards (the all-callers variant) and one that visits inwards (the known-caller variant), which would look like this (and does fix the test case attached to this PR): smowton@ca85bb1

My preference order:

1. Split or sort the working set -- simple, short fix, but keeps the rather tangly logic in the visit routines
2. Split fixedpoint_from/to_assertions into walk_outwards_ and walk_inwards_ variants, as in the commit linked above
3. Stick with this approach.

In any case we should surely include the forward walker -- even if we're wrong and it just happens to be (currently) impossible to break it, the new version would be more robust (if we go for options 1 or 3) and also clearer (if we go for option 2).

[smowton]

Also I don't have the right to change this code anyhow -- @peterschrammel @chrisr-diffblue @kroening you're once again the relevant owners, what do you think?

[chrisr-diffblue]

The changes look reasonable, so I'm approving but with the caveat that I don't really know this code that well, so I'd rather someone better versed in it than myself clicks the final merge button :-)

[smowton]

@tautschnig any opinion on whether to go with the approach in smowton@ca85bb1 or just merge this? Effectively that approach is specialising the walk-backwards function to the caller_is_known and !caller_is_known cases.

[tautschnig]

@smowton @polgreen My apologies for being very slow with this, and thanks a lot for stepping up to do all the further work. I'm taking a look at the both the changes here and in #3218 now.

[smowton]

Merged #3218 instead