[PATCH] D78457: [analyzer][Z3-refutation] Fix refutation BugReporterVisitor bug and refactor

[Balázs Benics via Phabricator via cfe-commits]

steakhal created this revision.
steakhal added reviewers: mikhail.ramalho, NoQ, Szelethus, baloghadamsoftware, xazax.hun.
Herald added subscribers: cfe-commits, ASDenysPetrov, martong, Charusso, dkrupp, donat.nagy, a.sidorin, rnkovacs, szepet, whisperity.
Herald added a project: clang.

`FalsePositiveRefutationBRVisitor` had a bug(*) where the constraints were not properly collected thus crosschecked with Z3.
This patch fixes that bug by eliminating the `FalsePositiveRefutationBRVisitor` completely.

As turned out we don't even need a `BugReporterVisitor` for doing the crosscheck.
We should simply use the constraints of the `ErrorNode` since that has all the necessary information.

Bug(*):
The visitor collected all the constraints on a `BugPath`.
Since it is a visitor, it visited the node before the `ErrorNode`, and so on until the `RootNode`.
At the end visited the ErrorNode explicitly, but that visit had no effect.
Since the constraints were collected into a map, mapping each symbol to its `RangeSet`.
If the map already had a mapping with the symbol, then it was skipped.

Consider the following case:
We already had a constraint on a symbol, but az the end in the ErrorNode we have a stricter constraint on that.
This visitor would not utilize that stricter constraint in the crosschecking.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D78457

Files:
  clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
  clang/lib/StaticAnalyzer/Core/BugReporter.cpp
  clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

-------------- next part --------------
A non-text attachment was scrubbed...
Name: D78457.258610.patch
Type: text/x-patch
Size: 7084 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20200419/c442c651/attachment-0001.bin>