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