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 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
