Warnings not removed for unreachable code (contexts) with incremental post-solving

[michael-schwarz]

@stilscher and I discovered the following problem: Superstable contains too many things which causes spurious warnings to remain after an incremental run in cases where code is no longer reachable after the patch.

The fundamental issue is that we do not destabilize (and don't want to) into function calls (of unchanged functions) that no longer happen (or do at least no longer happen in a given context). Hence the unknowns corresponding to such code remain superstable and the warnings are re-used.

I added an example to this branch where a call to a function is removed so an entire function becomes uncalled: https://github.com/goblint/analyzer/tree/interactive_postsolver_pruning
It behaves as expected when one disables the incremental post-solver.

The same issue happens also when only certain calling contexts go away.

Short of a full reachability or horrible hacks where one destabilizes every unknown that is no longer queried at calls, it does not seem obvious how to fix this.

One way that I am currently investigating (suggested by Helmut) is doing a lightweight full reachability where we record for each unknown the set of unknowns its last evaluation depended on. This way, one does not have to execute all the right-hand sides for reachability. For those things that are reachable & superstable, I can reuse the old warnings and accesses, for those things that are reachable and not superstable, I then need to execute the right-hand sides as I currently do.

This is reasonable if most time in the post-solver is spent executing right-hand sides instead of doing reachability.

[sim642]

record for each unknown the set of unknowns its last evaluation depended on

That's something the TD3 aborting already has implemented.

For those things that are reachable & superstable, I can reuse the old warnings and accesses, for those things that are reachable and not superstable, I then need to execute the right-hand sides as I currently do.

Not sure I understand the logic here, because it sounds to me exactly what the incremental postsolver already does, since it never iterates to unreachable unknowns to begin with.

Or do you intend to again split the postsolving back to separate reachability and warning phases? Because the current postsolver mechanism integrates them all into a single pass, where reachability itself is computed while outputting the warnings, so the warning generation doesn't yet know about the final reachability result.

[michael-schwarz]

Or do you intend to again split the postsolving back to separate reachability and warning phases?

I think in some sense we have to do this to get actual reachability for the superstable set instead of just assuming everything in superstable remains reachable?

[sim642]

Probably, but then we just go back to non-incremental reachability computation as before, which is one of the big bottlenecks we initially wanted to avoid. So your idea now is to essentially use aborting just for that from-scratch reachability computation to avoid evaluating the right-hand sides, but not use the general aborting during the analysis?

[michael-schwarz]

The idea would be a cheap from-scratch reachability (under the assumption what is expensive about postsolving is the evaluation of right-hand sides, which I am currently benchmarking).
Not sure where aborting comes into play here, how do I know without iterating through the entire constraint system which things are reachable (superstable doesn't help as we have established)? So there is no natural point at which to actually abort.

[sim642]

The general TD3 aborting exactly collects the dependencies of previous right-hand side evaluations such that next time the right-hand side needs to be evaluated, it can be aborted if all those dependencies are unchanged.
From what I understand, the cheaper from-scratch reachability more or less exploits the same ideas to avoid actually executing the right-hand sides. I suppose doing it for just a single reachability specializes the general algorithm to a much simpler one since it only needs to work on a post-fixpoint solution.

Now saying that, I'm starting to get more concerned because if due to some issue the solver finishes, but hasn't reached a fixpoint (e.g. would suddenly have an extra dependency if evaluated again), then the new reachability run would work on that non-fixpoint (but it doesn't know because it doesn't evaluate anything). Then the actual postsolving which performs fixpoint verification is based on that possibly-flawed reachability run.