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

[George Karpenkov via Phabricator via cfe-commits]

george.karpenkov added inline comments.


================
Comment at: include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h:496
   std::unique_ptr<ConstraintManager>   ConstraintMgr;
+  std::unique_ptr<ConstraintManager>   RefutationMgr;
 
----------------
See the comment below, I think we should not have this manager here. Just create one in the visitor constructor.


================
Comment at: include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h:563
+
+  ConstraintManager& getRefutationManager() {
+    return *RefutationMgr;
----------------
This should be deleted as well (see the comment above)


================
Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2382
+    // Reset the solver
+    RefutationMgr.reset();
+  }
----------------
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.


================
Comment at: lib/StaticAnalyzer/Core/ProgramState.cpp:83
   ConstraintMgr = (*CreateCMgr)(*this, SubEng);
+  AnalyzerOptions &Opts = SubEng->getAnalysisManager().getAnalyzerOptions();
+  RefutationMgr = Opts.shouldCrosscheckWithZ3()
----------------
This could be removed as well (see the comment above)


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:919
 
+  void reset() override;
+
----------------
`reset` should be removed, see comments above.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1246
 
+void Z3ConstraintManager::reset() { Solver.reset(); }
+
----------------
I would remove this, see comments above.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1292
+      Constraints =
+          Z3Expr::fromBinOp(Constraints, BO_LOr, SymRange, IsSignedTy);
+    }
----------------
I'm very confused as to why are we doing disjunctions here.


https://reviews.llvm.org/D45517