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