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

[Reka Kovacs via Phabricator via cfe-commits]

rnkovacs created this revision.
rnkovacs added reviewers: george.karpenkov, NoQ, dcoughlin.
Herald added subscribers: a.sidorin, szepet, baloghadamsoftware, whisperity, fhahn.

This is a prototype of a bug reporter visitor that invalidates bug reports by re-checking constraints of certain states on the bug path using the Z3 constraint manager backend. The functionality is available under the `postprocess-reports` analyzer config flag.

Results of analysis runs on a few open-source projects with this option turned on can be explored here <http://cc.elte.hu/refutation.html>.

This work is preliminary and any comments are appreciated. A few remarks:

- In order to work with constraints generated by the range-based constraint manager outside its own file, much of the `Range`, `RangeTrait` and `RangeSet` classes have been moved to the corresponding header file.

- 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.

- 1-bit APSInts obtained from ranged constraints crashed when `isSignedIntegerOrEnumerationType()` was called on them inside `Z3ConstraintManager`'s methods. This issue is currently sidestepped, but they might be converted to a valid built-in type at some point.


Repository:
  rC Clang

https://reviews.llvm.org/D45517

Files:
  include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
  include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
  include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
  include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h
  lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
  lib/StaticAnalyzer/Core/BugReporter.cpp
  lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
  lib/StaticAnalyzer/Core/ProgramState.cpp
  lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  lib/StaticAnalyzer/Core/RangedConstraintManager.h
  lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

-------------- next part --------------
A non-text attachment was scrubbed...
Name: D45517.141994.patch
Type: text/x-patch
Size: 30707 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20180411/326cc044/attachment-0001.bin>