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

[George Karpenkov via Phabricator via cfe-commits]

george.karpenkov added inline comments.


================
Comment at: include/clang/StaticAnalyzer/Core/AnalyzerOptions.h:284
+  /// \sa shouldPostProcessBugReports
+  Optional<bool> PostProcessBugReports;
+
----------------
The option name should be more self-explanatory, post-processing in general can mean anything


================
Comment at: include/clang/StaticAnalyzer/Core/AnalyzerOptions.h:586
+  /// which accepts the values "true" and "false".
+  bool shouldPostProcessBugReports();
+
----------------
Same here


================
Comment at: include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h:348
+    : public BugReporterVisitorImpl<FalsePositiveRefutationBRVisitor> {
+  bool isInvalidated = false;
+
----------------
LLVM coding standart mandates capital case for field names.


================
Comment at: lib/StaticAnalyzer/Core/AnalyzerOptions.cpp:301
+  return getBooleanOption(PostProcessBugReports,
+                          "postprocess-reports",
+                          /* Default = */ false);
----------------
Same for the option name. "crosscheck-with-z3"?


================
Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2342
+                                            BugReport &BR) {
+  if (isInvalidated)
+    return nullptr;
----------------
Is this field actually necessary? Do we ever check the same bug report with the same visitor multiple times?


================
Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2351
+
+  if (!RefutationMgr.checkRangedStateConstraints(Succ->getState())) {
+    const LocationContext *LC = Succ->getLocationContext();
----------------
For the initial version I would just do all work in the visitor, but that's a matter of taste.


================
Comment at: lib/StaticAnalyzer/Core/ProgramState.cpp:86
+                  ? CreateZ3ConstraintManager(*this, SubEng)
+                  : nullptr;
 }
----------------
Would then we crash on NPE if `getRefutationManager` is called? Getters should preferably not cause crashes.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1268
+      if (From == To) {
+        Z3Expr Eq = getZ3BinExpr(Exp, SymTy, BO_EQ, FromExp, RangeTy, nullptr);
+        Solver.addConstraint(Eq);
----------------
I wouldn't even bother with this branch, but again, a matter of taste.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1273
+        Z3Expr RHS = getZ3BinExpr(Exp, SymTy, BO_LE, ToExp, RangeTy, nullptr);
+        Solver.addConstraint(Z3Expr::fromBinOp(LHS, BO_LOr, RHS, isSignedTy));
+      }
----------------
Why `OR`? Shouldn't it be AND?


https://reviews.llvm.org/D45517