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

[George Karpenkov via Phabricator via cfe-commits]

george.karpenkov requested changes to this revision.
george.karpenkov added a comment.
This revision now requires changes to proceed.

Thanks, this is going in the right direction!



================
Comment at: include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:182
 
+  virtual void reset() {}
+  virtual bool isModelFeasible() { return true; }
----------------
We don't need reset anymore.


================
Comment at: include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:183
+  virtual void reset() {}
+  virtual bool isModelFeasible() { return true; }
+  virtual void addRangeConstraints(ConstraintRangeTy) {}
----------------
Making those virtual does not make much sense to me.
Returning `true` by default is not correct.
When we are using the visitor, we should already know we have a `Z3ConstraintsManager`, why can't we just use methods of that class?


================
Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2377
+    // Try to create the refutation manager, using Z3
+    std::unique_ptr<ConstraintManager> RefutationMgr =
+        Opts.shouldCrosscheckWithZ3()
----------------
1. RefutationMgr should be created in the visitor constructor.
2. At this point we should not check options; if the visitor is created, we are assuming that the option is on.
3. Consequently, the subsequent assert should be dropped.


================
Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2391
+    if (!RefutationMgr->isModelFeasible())
+      BR.markInvalid("Infeasible constraints", N->getLocationContext());
+  }
----------------
That would be checking all constraints in all nodes one by one. I thought the idea was to encode all constraints from the entire path and then check all of it.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:889
+
+  LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
 }; // end class Z3Solver
----------------
👍


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:925
 
+  void reset() override { Solver.reset(); }
+
----------------
We don't need `reset` anymore.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:928
+  bool isModelFeasible() override {
+    return Solver.check() != Z3_L_FALSE;
+  }
----------------
The semantics of this method is incorrect. It should return a tri-value somehow (e.g. `Optional<bool>`, and then higher-level logic in visitor should decide what to do with it.)


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1272
+      // FIXME: fix available in D35450
+      if (RangeTy.isNull())
+        continue;
----------------
Since https://reviews.llvm.org/D47603 has landed we should drop this branch.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1282
+
+      Z3Expr LHS = getZ3BinExpr(Exp, SymTy, BO_GE, FromExp, RangeTy, nullptr);
+      Z3Expr RHS = getZ3BinExpr(Exp, SymTy, BO_LE, ToExp, RangeTy, nullptr);
----------------
/*RetTy=*/nullptr


https://reviews.llvm.org/D45517