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

2018-05-26 Thread Dávid Bolvanský via Phabricator via cfe-commits
xbolva00 added inline comments. Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1261 + + for (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) { +SymbolRef Sym = I.getKey(); for (auto I : CR)?

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

2018-05-26 Thread Dominic Chen via Phabricator via cfe-commits
ddcc added a comment. FYI the fix for the 1-bit APSInt issue is in https://reviews.llvm.org/D35450#change-ifYnQ3IlVso https://reviews.llvm.org/D45517 ___ cfe-commits mailing list cfe-commits@lists.llvm.org

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

2018-05-10 Thread Mikhail Ramalho via Phabricator via cfe-commits
mikhail.ramalho added a comment. Commandeering the PR because of GSoC. https://reviews.llvm.org/D45517 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

2018-05-08 Thread Reka Kovacs via Phabricator via cfe-commits
rnkovacs added inline comments. Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2342 +BugReport ) { + if (isInvalidated) +return nullptr; george.karpenkov wrote: > Is this field actually necessary? Do

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

2018-05-08 Thread Reka Kovacs via Phabricator via cfe-commits
rnkovacs updated this revision to Diff 145762. rnkovacs marked 4 inline comments as done. rnkovacs edited the summary of this revision. rnkovacs added a comment. Expression chaining is fixed. The visitor now collects constraints that are about to disappear along the bug path and checks them once

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

2018-04-23 Thread Artem Dergachev via Phabricator via cfe-commits
NoQ added a comment. In https://reviews.llvm.org/D45517#1074422, @rnkovacs wrote: > In https://reviews.llvm.org/D45517#1074057, @NoQ wrote: > > > 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 > >

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

2018-04-21 Thread George Karpenkov via Phabricator via cfe-commits
george.karpenkov added inline comments. Comment at: include/clang/StaticAnalyzer/Core/AnalyzerOptions.h:284 + /// \sa shouldPostProcessBugReports + Optional PostProcessBugReports; + The option name should be more self-explanatory, post-processing in general

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

2018-04-21 Thread Reka Kovacs via Phabricator via cfe-commits
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

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

2018-04-21 Thread Reka Kovacs via Phabricator via cfe-commits
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

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

2018-04-21 Thread Reka Kovacs via Phabricator via cfe-commits
rnkovacs updated this revision to Diff 143440. 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

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

2018-04-20 Thread Artem Dergachev via Phabricator via cfe-commits
NoQ added a comment. > 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

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

2018-04-20 Thread Reka Kovacs via Phabricator via cfe-commits
rnkovacs updated this revision to Diff 143287. rnkovacs edited the summary of this revision. rnkovacs added a comment. Fixed logical operator in the `Z3ConstraintManager::checkRangedStateConstraints()` function. https://reviews.llvm.org/D45517 Files:

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

2018-04-11 Thread 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