Created a tiny SMT interface and make Z3ConstraintManager implement it

[mikhail.ramalho]

Summary

This patch implements a simple SMTConstraintManager API, and requires the implementation of two methods for now: addRangeConstraints and isModelFeasible.

Update Z3ConstraintManager to inherit it and implement required methods.

I also moved the method to dump the SMT formula from D45517 to this patch.

This patch was created based on the reviews from D47640.

[george.karpenkov]

LGTM with a nit.

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

8

Add a sentence/few sentences description here.

[mikhail.ramalho]

Added small description in the SMTConstraintManager header.

[george.karpenkov]

yep, this can be committed.

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

+//== SMTConstraintManager.h -------------------------------------*- C++ -*--==//
+//
+//                     The LLVM Compiler Infrastructure
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+//
+//  This file defines a SMT generic API, which will be the base class for
+//  every SMT solver specific class.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
+#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
+
+#include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
+
+namespace clang {
+namespace ento {
+
+class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
+
+public:
+  SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB)
+      : SimpleConstraintManager(SE, SB) {}
+  virtual ~SMTConstraintManager() = default;
+
+  /// Converts the ranged constraints of a set of symbols to SMT
+  ///
+  /// \param CR The set of constraints.
+  virtual void addRangeConstraints(clang::ento::ConstraintRangeTy CR) = 0;
+
+  /// Checks if the added constraints are satisfiable
+  virtual clang::ento::ConditionTruthVal isModelFeasible() = 0;
+
+}; // end class SMTConstraintManager
+
+} // namespace ento
+} // namespace clang
+
+#endif

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

 //== Z3ConstraintManager.cpp --------------------------------*- C++ -*--==//
 //
 //                     The LLVM Compiler Infrastructure
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
 //===----------------------------------------------------------------------===//
 
 #include "clang/Basic/TargetInfo.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
 
 #include "clang/Config/config.h"
 
 using namespace clang;
 using namespace ento;
 
 #if CLANG_ANALYZER_WITH_Z3
 
public:
   /// Get a model from the solver. Caller should check the model is
   /// satisfiable.
   Z3Model getModel() {
     return Z3Model(Z3_solver_get_model(Z3Context::ZC, Solver));
   }
 
   /// Reset the solver and remove all constraints.
   void reset() { Z3_solver_reset(Z3Context::ZC, Solver); }
+
+  void print(raw_ostream &OS) const {
+    OS << Z3_solver_to_string(Z3Context::ZC, Solver);
+  }
+
+  LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
 }; // end class Z3Solver
 
 void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) {
   llvm::report_fatal_error("Z3 error: " +
                            llvm::Twine(Z3_get_error_msg_ex(Context, Error)));
 }
 
-class Z3ConstraintManager : public SimpleConstraintManager {
+class Z3ConstraintManager : public SMTConstraintManager {
   Z3Context Context;
   mutable Z3Solver Solver;
 
 public:
   Z3ConstraintManager(SubEngine *SE, SValBuilder &SB)
-      : SimpleConstraintManager(SE, SB),
+      : SMTConstraintManager(SE, SB),
         Solver(Z3_mk_simple_solver(Z3Context::ZC)) {
     Z3_set_error_handler(Z3Context::ZC, Z3ErrorHandler);
   }
+  //===------------------------------------------------------------------===//
+  // Implementation for Refutation.
+  //===------------------------------------------------------------------===//
+
+  void addRangeConstraints(clang::ento::ConstraintRangeTy CR) override;
+
+  ConditionTruthVal isModelFeasible() override;
 
   //===------------------------------------------------------------------===//
   // Implementation for interface from ConstraintManager.
   //===------------------------------------------------------------------===//
 
   bool canReasonAbout(SVal X) const override;
 
   ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
Z3ConstraintManager::removeDeadBindings(ProgramStateRef State,
   for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) {
     if (SymReaper.maybeDead(I->first))
       CZ = CZFactory.remove(CZ, *I);
   }
 
   return State->set<ConstraintZ3>(CZ);
 }
 
+void Z3ConstraintManager::addRangeConstraints(ConstraintRangeTy CR) {
+  for (const auto &I : CR) {
+    SymbolRef Sym = I.first;
+
+    Z3Expr Constraints = Z3Expr::fromBoolean(false);
+
+    for (const auto &Range : I.second) {
+      const llvm::APSInt &From = Range.From();
+      const llvm::APSInt &To = Range.To();
+
+      QualType FromTy;
+      llvm::APSInt NewFromInt;
+      std::tie(NewFromInt, FromTy) = fixAPSInt(From);
+      Z3Expr FromExp = Z3Expr::fromAPSInt(NewFromInt);
+      QualType SymTy;
+      Z3Expr Exp = getZ3Expr(Sym, &SymTy);
+      bool IsSignedTy = SymTy->isSignedIntegerOrEnumerationType();
+      QualType ToTy;
+      llvm::APSInt NewToInt;
+      std::tie(NewToInt, ToTy) = fixAPSInt(To);
+      Z3Expr ToExp = Z3Expr::fromAPSInt(NewToInt);
+      assert(FromTy == ToTy && "Range values have different types!");
+
+      Z3Expr LHS =
+          getZ3BinExpr(Exp, SymTy, BO_GE, FromExp, FromTy, /*RetTy=*/nullptr);
+      Z3Expr RHS =
+          getZ3BinExpr(Exp, SymTy, BO_LE, ToExp, FromTy, /*RetTy=*/nullptr);
+      Z3Expr SymRange = Z3Expr::fromBinOp(LHS, BO_LAnd, RHS, IsSignedTy);
+      Constraints =
+          Z3Expr::fromBinOp(Constraints, BO_LOr, SymRange, IsSignedTy);
+    }
+    Solver.addConstraint(Constraints);
+  }
+}
+
+clang::ento::ConditionTruthVal Z3ConstraintManager::isModelFeasible() {
+  if (Solver.check() == Z3_L_FALSE)
+    return false;
+
+  return ConditionTruthVal();
+}
+
 //===------------------------------------------------------------------===//
 // Internal implementation.
 //===------------------------------------------------------------------===//
 
 ProgramStateRef Z3ConstraintManager::assumeZ3Expr(ProgramStateRef State,
                                                   SymbolRef Sym,
                                                   const Z3Expr &Exp) {
   // Check the model, avoid simplifying AST to save time