[analyzer] [WIP] Added new member to cache unsat cores, between equivalent bug reports

[mikhail.ramalho]

Summary

This patch implements an unsat core caching mechanism, which holds a vector of assumptions shared between equivalent bug reports.

I removed two static functions areConstraintsUnfeasible and addNewConstraints because they were quite small and moved their code to FalsePositiveRefutationBRVisitor::finalizeVisitor and FalsePositiveRefutationBRVisitor::VisitNode, respectively; keeping them around would mean adding a new parameter to areConstraintsUnfeasible, to pass the vector of assumptions, which didn't seem worth it.

It's a work-in-progress, because all the unsat cores are currently empty (at least with Z3 4.6).

[george.karpenkov]

Let's hold on with this until we can get UNSAT cores working.
Maybe it's easier to just invoke the visitor on the entire equivalence class at once.

include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h

 //
 //===----------------------------------------------------------------------===//
 
 #ifndef LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_BUGREPORTERVISITORS_H
 #define LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_BUGREPORTERVISITORS_H
 
 #include "clang/Basic/LLVM.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
 #include "llvm/ADT/FoldingSet.h"
 #include "llvm/ADT/STLExtras.h"
 #include "llvm/ADT/StringRef.h"
 #include <memory>
 
 namespace clang {
 

 /// The bug visitor will walk all the nodes in a path and collect all the
 /// constraints. When it reaches the root node, will create a refutation
 /// manager and check if the constraints are satisfiable
 class FalsePositiveRefutationBRVisitor final : public BugReporterVisitor {
 private:
   /// Holds the constraints in a given path
   ConstraintRangeTy Constraints;
 
+  /// Holds previous unsat core's assumptions
+  std::vector<SMTExprRef> &UnsatCore;
+
 public:
-  FalsePositiveRefutationBRVisitor();
+  FalsePositiveRefutationBRVisitor(std::vector<SMTExprRef> &UC);
 
   void Profile(llvm::FoldingSetNodeID &ID) const override;
 
   std::shared_ptr<PathDiagnosticPiece> VisitNode(const ExplodedNode *N,
                                                  const ExplodedNode *PrevN,
                                                  BugReporterContext &BRC,
                                                  BugReport &BR) override;
 

include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h

public:
   /// Converts the ranged constraints of a set of symbols to SMT
   ///
   /// \param CR The set of constraints.
   void addRangeConstraints(clang::ento::ConstraintRangeTy CR);
 
   /// Checks if the added constraints are satisfiable
   clang::ento::ConditionTruthVal isModelFeasible();
 
+  /// Return the unsat core from the solver
+  std::vector<SMTExprRef> getUnsatCore() { return Solver->getUnsatCore(); }
+
+  /// Add constraints from an unsat core
+  void addConstraintFromUnsatCore(std::vector<SMTExprRef> &UC);
+
   /// Dumps SMT formula
   LLVM_DUMP_METHOD void dump() const { Solver->dump(); }
 
 protected:
   //===------------------------------------------------------------------===//
   // Internal implementation.
   //===------------------------------------------------------------------===//
 

include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h

public:
 
   /// Construct a const SMTExprRef &From a SymbolData, given a SMT_context.
   virtual SMTExprRef fromData(const SymbolID ID, const QualType &Ty,
                               uint64_t BitWidth) = 0;
 
   /// Check if the constraints are satisfiable
   virtual ConditionTruthVal check() const = 0;
 
+  /// Get the unsat core from the solver
+  virtual std::vector<SMTExprRef> getUnsatCore() = 0;
+
   /// Push the current solver state
   virtual void push() = 0;
 
   /// Pop the previous solver state
   virtual void pop(unsigned NumStates = 1) = 0;
 
   /// Reset the solver and remove all constraints.
   virtual void reset() const = 0;

lib/StaticAnalyzer/Core/BugReporter.cpp

 static
 std::pair<BugReport*, std::unique_ptr<VisitorsDiagnosticsTy>> findValidReport(
   TrimmedGraph &TrimG,
   ReportGraph &ErrorGraph,
   ArrayRef<BugReport *> &bugReports,
   AnalyzerOptions &Opts,
   GRBugReporter &Reporter) {
 
+  std::vector<SMTExprRef> UnsatCore;
   while (TrimG.popNextReportGraph(ErrorGraph)) {
     // Find the BugReport with the original location.
     assert(ErrorGraph.Index < bugReports.size());
     BugReport *R = bugReports[ErrorGraph.Index];
     assert(R && "No original report found for sliced graph.");
     assert(R->isValid() && "Report selected by trimmed graph marked invalid.");
     const ExplodedNode *ErrorNode = ErrorGraph.ErrorNode;
 
     // Register refutation visitors first, if they mark the bug invalid no
     // further analysis is required
     R->addVisitor(llvm::make_unique<LikelyFalsePositiveSuppressionBRVisitor>());
     if (Opts.shouldCrosscheckWithZ3())
-      R->addVisitor(llvm::make_unique<FalsePositiveRefutationBRVisitor>());
+      R->addVisitor(
+          llvm::make_unique<FalsePositiveRefutationBRVisitor>(UnsatCore));
 
     // Register additional node visitors.
     R->addVisitor(llvm::make_unique<NilReceiverBRVisitor>());
     R->addVisitor(llvm::make_unique<ConditionBRVisitor>());
     R->addVisitor(llvm::make_unique<CXXSelfAssignmentBRVisitor>());
 
     BugReporterContext BRC(Reporter, ErrorGraph.BackMap);
 

lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

TaintBugVisitor::VisitNode(const ExplodedNode *N, const ExplodedNode *PrevN,
   PathDiagnosticLocation L =
       PathDiagnosticLocation::createBegin(S, BRC.getSourceManager(), NCtx);
   if (!L.isValid() || !L.asLocation().isValid())
     return nullptr;
 
   return std::make_shared<PathDiagnosticEventPiece>(L, "Taint originated here");
 }
 
-static bool areConstraintsUnfeasible(BugReporterContext &BRC,
-                                     const ConstraintRangeTy &Cs) {
+FalsePositiveRefutationBRVisitor::FalsePositiveRefutationBRVisitor(
+    std::vector<SMTExprRef> &UC)
+    : Constraints(ConstraintRangeTy::Factory().getEmptyMap()), UnsatCore(UC) {}
+
+void FalsePositiveRefutationBRVisitor::finalizeVisitor(
+    BugReporterContext &BRC, const ExplodedNode *EndPathNode, BugReport &BR) {
+  // Collect new constraints
+  VisitNode(EndPathNode, nullptr, BRC, BR);
+
   // Create a refutation manager
   std::unique_ptr<ConstraintManager> RefutationMgr = CreateZ3ConstraintManager(
       BRC.getStateManager(), BRC.getStateManager().getOwningEngine());
 
   SMTConstraintManager *SMTRefutationMgr =
       static_cast<SMTConstraintManager *>(RefutationMgr.get());
 
   // Add constraints to the solver
-  SMTRefutationMgr->addRangeConstraints(Cs);
-
-  // And check for satisfiability
-  return SMTRefutationMgr->isModelFeasible().isConstrainedFalse();
-}
+  SMTRefutationMgr->addRangeConstraints(Constraints);
 
-static void addNewConstraints(ConstraintRangeTy &Cs,
-                              const ConstraintRangeTy &NewCs,
-                              ConstraintRangeTy::Factory &CF) {
-  // Add constraints if we don't have them yet
-  for (auto const &C : NewCs) {
-    const SymbolRef &Sym = C.first;
-    if (!Cs.contains(Sym)) {
-      Cs = CF.add(Cs, Sym, C.second);
-    }
-  }
-}
+  // Add constraints from the unsat core
+  SMTRefutationMgr->addConstraintFromUnsatCore(UnsatCore);
 
-FalsePositiveRefutationBRVisitor::FalsePositiveRefutationBRVisitor()
-    : Constraints(ConstraintRangeTy::Factory().getEmptyMap()) {}
+  // And check for satisfiability
+  if (SMTRefutationMgr->isModelFeasible().isConstrainedFalse()) {
+    // Mark the bug as invalid
+    BR.markInvalid("Infeasible constraints", EndPathNode->getLocationContext());
 
-void FalsePositiveRefutationBRVisitor::finalizeVisitor(
-    BugReporterContext &BRC, const ExplodedNode *EndPathNode, BugReport &BR) {
-  // Collect new constraints
-  VisitNode(EndPathNode, nullptr, BRC, BR);
+    // And save the unsat core
+    std::vector<SMTExprRef> NewUnsatCore = SMTRefutationMgr->getUnsatCore();
 
-  // Create a new refutation manager and check feasibility
-  if (areConstraintsUnfeasible(BRC, Constraints))
-    BR.markInvalid("Infeasible constraints", EndPathNode->getLocationContext());
+    UnsatCore.insert(UnsatCore.begin(), NewUnsatCore.begin(),
+                     NewUnsatCore.end());
+  }
 }
 
 std::shared_ptr<PathDiagnosticPiece>
 FalsePositiveRefutationBRVisitor::VisitNode(const ExplodedNode *N,
                                             const ExplodedNode *PrevN,
                                             BugReporterContext &BRC,
                                             BugReport &BR) {
+  const ConstraintRangeTy &Cs = N->getState()->get<ConstraintRange>();
+  ConstraintRangeTy::Factory &CF = N->getState()->get_context<ConstraintRange>();
+
   // Collect new constraints
-  addNewConstraints(Constraints, N->getState()->get<ConstraintRange>(),
-                    N->getState()->get_context<ConstraintRange>());
+  // Add constraints if we don't have them yet
+  for (auto const &C : Cs) {
+    const SymbolRef &Sym = C.first;
+    if (!Constraints.contains(Sym)) {
+      Constraints = CF.add(Constraints, Sym, C.second);
+    }
+  }
 
   return nullptr;
 }
 
 void FalsePositiveRefutationBRVisitor::Profile(
     llvm::FoldingSetNodeID &ID) const {
   static int Tag = 0;
   ID.AddPointer(&Tag);
 }

lib/StaticAnalyzer/Core/SMTConstraintManager.cpp

 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
 #include "clang/Basic/TargetInfo.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 
 using namespace clang;
 using namespace ento;
 
+void SMTConstraintManager::addConstraintFromUnsatCore(
+    std::vector<SMTExprRef> &UC) {
+  for (const auto &E : UC) {
+    Solver->addConstraint(E);
+  }
+}
+
 void SMTConstraintManager::addRangeConstraints(ConstraintRangeTy CR) {
   Solver->reset();
 
   for (const auto &I : CR) {
     SymbolRef Sym = I.first;
 
     SMTExprRef Constraints = Solver->fromBoolean(false);
     for (const auto &Range : I.second) {

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

 public:
   Z3Config() : Config(Z3_mk_config()) {
     // Enable model finding
     Z3_set_param_value(Config, "model", "true");
     // Disable proof generation
     Z3_set_param_value(Config, "proof", "false");
     // Set timeout to 15000ms = 15s
     Z3_set_param_value(Config, "timeout", "15000");
+    // Enable unsat core generation
+    Z3_set_param_value(Config, "unsat_core", "true");
   }
 
   ~Z3Config() { Z3_del_config(Config); }
 }; // end class Z3Config
 
 void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) {
   llvm::report_fatal_error("Z3 error: " +
                            llvm::Twine(Z3_get_error_msg_ex(Context, Error)));
if (res == Z3_L_TRUE)
       return true;
 
     if (res == Z3_L_FALSE)
       return false;
 
     return ConditionTruthVal();
   }
 
+  std::vector<SMTExprRef> getUnsatCore() override {
+    Z3_ast_vector Core = Z3_solver_get_unsat_core(Context.Context, Solver);
+    unsigned Size = Z3_ast_vector_size(Context.Context, Core);
+
+    std::vector<SMTExprRef> UnsatCore;
+    for (unsigned i = 0; i < Size; i++) {
+      UnsatCore.push_back(std::make_shared<Z3Expr>(
+          Context, Z3_ast_vector_get(Context.Context, Core, i)));
+    }
+
+    return UnsatCore;
+  }
+
   /// Push the current solver state
   void push() override { return Z3_solver_push(Context.Context, Solver); }
 
   /// Pop the previous solver state
   void pop(unsigned NumStates = 1) override {
     assert(Z3_solver_get_num_scopes(Context.Context, Solver) >= NumStates);
     return Z3_solver_pop(Context.Context, Solver, NumStates);
   }