[PATCH] D45517: [analyzer] WIP: False positive refutation with Z3

Sat Apr 21 05:05:56 PDT 2018

rnkovacs added a comment.

In https://reviews.llvm.org/D45517#1074057, @NoQ wrote:

> > The visitor currently checks states appearing as block edges in the exploded graph. The first idea was to filter states based on the shape of the exploded graph, by checking the number of successors of the parent node, but surprisingly, both `succ_size()` and `pred_size()` seemed to return 1 for each node in the graph (except for the root), even if there clearly were branchings in the code (and on the `.dot` picture). To my understanding, the exploded graph is fully constructed at the stage where visitors are run, so I must be missing something.
>
> Aha, yep, that's probably because visitors are operating on the "trimmed" exploded graph. You can paint it via the `-trim-egraph` flag or by calling `ViewGraph(1)` in the debugger.

Oh, thanks! That explains a lot.

> So, yeah, that's a good optimization that we're not invoking the solver on every node. But i don't think we should focus on improving this optimization further; instead, i think the next obvious step here is to implement it in such a way that we only needed to call the solver //once// for every report. We could simply collect all constraints from all states along the path and put them into the solver all together. This will work because symbols are not mutable and they don't reincarnate.

Won't collecting all constraints and solving a ~100ish equations at once take a long time? Maybe the timeout limit for Z3 will need to be slightly increased for refutation then.

> Apart from that, the patch seems to be going in the right direction. It should be possible to split up the `RangeSet` refactoring into a different review, for easier reviewing and better commit history.

Done in https://reviews.llvm.org/D45920.

I'll update this patch shortly.

https://reviews.llvm.org/D45517