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

[George Karpenkov via Phabricator via cfe-commits]

george.karpenkov added inline comments.


================
Comment at: lib/StaticAnalyzer/Core/BugReporter.cpp:3153
+    if (getAnalyzerOptions().shouldCrosscheckWithZ3())
+      R->addVisitor(llvm::make_unique<FalsePositiveRefutationBRVisitor>());
+
----------------
Unless I'm mistaken, visitors are run in the order they are being declared.
It seems to me we would want to register our visitor first, as it does not make sense to run diagnostics-visitors if we have already deemed the path to be unfeasible.

Probably `LikelyFalsePositiveSuppressionBRVisitor` should be even before that.


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


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:923
+
+  void addRangeConstraints(ConstraintRangeTy PrevCR, ConstraintRangeTy SuccCR,
+                           bool OnlyPurged) override;
----------------
@mikhail.ramalho I know the first version was not yours, but could you write a doxygen comment explaining the semantics of all parameters? (I know we are guilty for not writing those often).

I am also quite confused by the semantics of `OnlyPurged` variable.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1249
+bool Z3ConstraintManager::isModelFeasible() {
+  return Solver.check() != Z3_L_FALSE;
+}
----------------
solver can also return "unknown", what happens then?


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1259
+    return;
+  ConstraintRangeTy CR = OnlyPurged ? PrevCR : SuccCR;
+
----------------
TBH I'm really confused here. Why does the method take two constraint ranges? What's `OnlyPurged`? From reading the code it seems it's set by seeing whether the program point only purges dead symbols, but at least a comment should be added as to why this affects behavior.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1264
+
+    if (OnlyPurged && SuccCR.contains(Sym))
+      continue;
----------------
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.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1267
+
+    Z3Expr Constraints = Z3Expr::fromBoolean(false);
+
----------------
almost certainly a bug, we shouldn't default to unfeasible when the list of constraints is empty.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1278
+      // a valid APSIntType.
+      if (RangeTy.isNull())
+        continue;
----------------
I'm really curious where does it happen and why.


https://reviews.llvm.org/D45517