[analyzer] Templatefy SMTConstraintManager so more generic code can be moved from solver specific implementations. NFC.

Summary:
By making SMTConstraintManager a template and passing the SMT constraint type and expr, we can further move code from the Z3ConstraintManager class to the generic SMT constraint Manager.

Now, each SMT specific constraint manager only needs to implement the method `bool canReasonAbout(SVal X) const`.

Reviewers: NoQ, george.karpenkov

Reviewed By: george.karpenkov

Subscribers: mgorny, xazax.hun, szepet, a.sidorin, Szelethus

Differential Revision: https://reviews.llvm.org/D50770

llvm-svn: 340533

3 files changed, 1 insertions, 240 deletions

diff --git a/clang/lib/StaticAnalyzer/Core/CMakeLists.txt b/clang/lib/StaticAnalyzer/Core/CMakeLists.txt
index 86f2abf8b28..db06e4efd54 100644
--- a/clang/lib/StaticAnalyzer/Core/CMakeLists.txt
+++ b/clang/lib/StaticAnalyzer/Core/CMakeLists.txt
@@ -49,7 +49,6 @@ add_clang_library(clangStaticAnalyzerCore
   SVals.cpp
   SimpleConstraintManager.cpp
   SimpleSValBuilder.cpp
-  SMTConstraintManager.cpp
   Store.cpp
   SubEngine.cpp
   SymbolManager.cpp
diff --git a/clang/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
deleted file mode 100644
index d379562bf32..00000000000
--- a/clang/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
+++ /dev/null
@@ -1,181 +0,0 @@
-//== SMTConstraintManager.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/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;
-
-ProgramStateRef SMTConstraintManager::assumeSym(ProgramStateRef State,
-                                                SymbolRef Sym,
-                                                bool Assumption) {
-  ASTContext &Ctx = getBasicVals().getContext();
-
-  QualType RetTy;
-  bool hasComparison;
-
-  SMTExprRef Exp = Solver->getExpr(Ctx, Sym, &RetTy, &hasComparison);
-
-  // Create zero comparison for implicit boolean cast, with reversed assumption
-  if (!hasComparison && !RetTy->isBooleanType())
-    return assumeExpr(State, Sym,
-                      Solver->getZeroExpr(Ctx, Exp, RetTy, !Assumption));
-
-  return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp));
-}
-
-ProgramStateRef SMTConstraintManager::assumeSymInclusiveRange(
-    ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
-    const llvm::APSInt &To, bool InRange) {
-  ASTContext &Ctx = getBasicVals().getContext();
-  return assumeExpr(State, Sym,
-                    Solver->getRangeExpr(Ctx, Sym, From, To, InRange));
-}
-
-ProgramStateRef
-SMTConstraintManager::assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
-                                           bool Assumption) {
-  // Skip anything that is unsupported
-  return State;
-}
-
-ConditionTruthVal SMTConstraintManager::checkNull(ProgramStateRef State,
-                                                  SymbolRef Sym) {
-  ASTContext &Ctx = getBasicVals().getContext();
-
-  QualType RetTy;
-  // The expression may be casted, so we cannot call getZ3DataExpr() directly
-  SMTExprRef VarExp = Solver->getExpr(Ctx, Sym, &RetTy);
-  SMTExprRef Exp = Solver->getZeroExpr(Ctx, VarExp, RetTy, /*Assumption=*/true);
-
-  // Negate the constraint
-  SMTExprRef NotExp =
-      Solver->getZeroExpr(Ctx, VarExp, RetTy, /*Assumption=*/false);
-
-  Solver->reset();
-  addStateConstraints(State);
-
-  Solver->push();
-  Solver->addConstraint(Exp);
-  ConditionTruthVal isSat = Solver->check();
-
-  Solver->pop();
-  Solver->addConstraint(NotExp);
-  ConditionTruthVal isNotSat = Solver->check();
-
-  // Zero is the only possible solution
-  if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse())
-    return true;
-
-  // Zero is not a solution
-  if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue())
-    return false;
-
-  // Zero may be a solution
-  return ConditionTruthVal();
-}
-
-const llvm::APSInt *SMTConstraintManager::getSymVal(ProgramStateRef State,
-                                                    SymbolRef Sym) const {
-  BasicValueFactory &BVF = getBasicVals();
-  ASTContext &Ctx = BVF.getContext();
-
-  if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
-    QualType Ty = Sym->getType();
-    assert(!Ty->isRealFloatingType());
-    llvm::APSInt Value(Ctx.getTypeSize(Ty),
-                       !Ty->isSignedIntegerOrEnumerationType());
-
-    SMTExprRef Exp =
-        Solver->fromData(SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty));
-
-    Solver->reset();
-    addStateConstraints(State);
-
-    // Constraints are unsatisfiable
-    ConditionTruthVal isSat = Solver->check();
-    if (!isSat.isConstrainedTrue())
-      return nullptr;
-
-    // Model does not assign interpretation
-    if (!Solver->getInterpretation(Exp, Value))
-      return nullptr;
-
-    // A value has been obtained, check if it is the only value
-    SMTExprRef NotExp = Solver->fromBinOp(
-        Exp, BO_NE,
-        Ty->isBooleanType() ? Solver->fromBoolean(Value.getBoolValue())
-                            : Solver->fromAPSInt(Value),
-        false);
-
-    Solver->addConstraint(NotExp);
-
-    ConditionTruthVal isNotSat = Solver->check();
-    if (isNotSat.isConstrainedTrue())
-      return nullptr;
-
-    // This is the only solution, store it
-    return &BVF.getValue(Value);
-  }
-
-  if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
-    SymbolRef CastSym = SC->getOperand();
-    QualType CastTy = SC->getType();
-    // Skip the void type
-    if (CastTy->isVoidType())
-      return nullptr;
-
-    const llvm::APSInt *Value;
-    if (!(Value = getSymVal(State, CastSym)))
-      return nullptr;
-    return &BVF.Convert(SC->getType(), *Value);
-  }
-
-  if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
-    const llvm::APSInt *LHS, *RHS;
-    if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
-      LHS = getSymVal(State, SIE->getLHS());
-      RHS = &SIE->getRHS();
-    } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
-      LHS = &ISE->getLHS();
-      RHS = getSymVal(State, ISE->getRHS());
-    } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
-      // Early termination to avoid expensive call
-      LHS = getSymVal(State, SSM->getLHS());
-      RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;
-    } else {
-      llvm_unreachable("Unsupported binary expression to get symbol value!");
-    }
-
-    if (!LHS || !RHS)
-      return nullptr;
-
-    llvm::APSInt ConvertedLHS, ConvertedRHS;
-    QualType LTy, RTy;
-    std::tie(ConvertedLHS, LTy) = Solver->fixAPSInt(Ctx, *LHS);
-    std::tie(ConvertedRHS, RTy) = Solver->fixAPSInt(Ctx, *RHS);
-    Solver->doIntTypeConversion<llvm::APSInt, &SMTSolver::castAPSInt>(
-        Ctx, ConvertedLHS, LTy, ConvertedRHS, RTy);
-    return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
-  }
-
-  llvm_unreachable("Unsupported expression to get symbol value!");
-}
-
-ConditionTruthVal
-SMTConstraintManager::checkModel(ProgramStateRef State,
-                                 const SMTExprRef &Exp) const {
-  Solver->reset();
-  Solver->addConstraint(Exp);
-  addStateConstraints(State);
-  return Solver->check();
-}
diff --git a/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
index fc936cb0539..a71749bf169 100644
--- a/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -904,31 +904,13 @@ public:
   }
 }; // end class Z3Solver
 
-class Z3ConstraintManager : public SMTConstraintManager {
+class Z3ConstraintManager : public SMTConstraintManager<ConstraintZ3, Z3Expr> {
   SMTSolverRef Solver = CreateZ3Solver();
 
 public:
   Z3ConstraintManager(SubEngine *SE, SValBuilder &SB)
       : SMTConstraintManager(SE, SB, Solver) {}
 
-  void addStateConstraints(ProgramStateRef State) const override {
-    // TODO: Don't add all the constraints, only the relevant ones
-    ConstraintZ3Ty CZ = State->get<ConstraintZ3>();
-    ConstraintZ3Ty::iterator I = CZ.begin(), IE = CZ.end();
-
-    // Construct the logical AND of all the constraints
-    if (I != IE) {
-      std::vector<SMTExprRef> ASTs;
-
-      SMTExprRef Constraint = Solver->newExprRef(I++->second);
-      while (I != IE) {
-        Constraint = Solver->mkAnd(Constraint, Solver->newExprRef(I++->second));
-      }
-
-      Solver->addConstraint(Constraint);
-    }
-  }
-
   bool canReasonAbout(SVal X) const override {
     const TargetInfo &TI = getBasicVals().getContext().getTargetInfo();
 
@@ -971,45 +953,6 @@ public:
 
     llvm_unreachable("Unsupported expression to reason about!");
   }
-
-  ProgramStateRef removeDeadBindings(ProgramStateRef State,
-                                     SymbolReaper &SymReaper) override {
-    ConstraintZ3Ty CZ = State->get<ConstraintZ3>();
-    ConstraintZ3Ty::Factory &CZFactory = State->get_context<ConstraintZ3>();
-
-    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);
-  }
-
-  ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym,
-                             const SMTExprRef &Exp) override {
-    // Check the model, avoid simplifying AST to save time
-    if (checkModel(State, Exp).isConstrainedTrue())
-      return State->add<ConstraintZ3>(std::make_pair(Sym, toZ3Expr(*Exp)));
-
-    return nullptr;
-  }
-
-  //==------------------------------------------------------------------------==/
-  // Pretty-printing.
-  //==------------------------------------------------------------------------==/
-
-  void print(ProgramStateRef St, raw_ostream &OS, const char *nl,
-             const char *sep) override {
-
-    ConstraintZ3Ty CZ = St->get<ConstraintZ3>();
-
-    OS << nl << sep << "Constraints:";
-    for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) {
-      OS << nl << ' ' << I->first << " : ";
-      I->second.print(OS);
-    }
-    OS << nl;
-  }
 }; // end class Z3ConstraintManager
 
 } // end anonymous namespace