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

[Gábor Horváth via Phabricator via cfe-commits]

xazax.hun added inline comments.


================
Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2382
+    // Reset the solver
+    RefutationMgr.reset();
+  }
----------------
george.karpenkov wrote:
> george.karpenkov wrote:
> > (apologies in advance for nitpicking not on your code).
> > 
> > Currently, this is written in a stateful way: we have a solver, at each iteration we add constraints, and at the end we reset it. To me it would make considerably more sense to write the code in a functional style: as we go, generate a vector of formulas, then once we reach the path end, create the solver object, check satisfiability, and then destroy the entire solver.
> Elaborating more: we are already forced to have visitor object state, let's use that. `RefutationMgr` is essentially a wrapper around a Z3 solver object, let's just create one when visitor is constructed (directly or in unique_ptr) and then rely on the destructor to destroy it.
> Then no `reset` is necessary.
Note that while constructing the constraint solver here might make perfect sense now, it also inhibits incremental solving.  If we do not plan to experiment with incremental solvers anytime soon I am fine with this direction as well.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1264
+
+    if (OnlyPurged && SuccCR.contains(Sym))
+      continue;
----------------
george.karpenkov wrote:
> I would guess that this is an optimization done in order not to re-add the constraints we already have.
> I think we should really not bother doing that, as Z3 will do a much better job here then we can.
Note that we are using lots of domain knowledge here like we have the most info about a symbol just before it dies. Also This optimization is a single lookup on the symbol level. I am not sure if Z3 could deal with this on the symbol level. It might need to do this on the constraint level.
My point is, I am perfectly fine removing this optimization but I would like to see some performance numbers first either on a project that exercises refutation quite a bit or on some synthetic test cases.



https://reviews.llvm.org/D45517