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

[mikhail.ramalho]

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.

[george.karpenkov]

The trouble with templates is that you have to move code to the header, which then requires recompilation of all transitive includes on every single change...
But then I don't suppose we would be touching that header often.

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

 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
 
 #include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h"
 
 namespace clang {
 namespace ento {
 
+template <typename ConstraintSMT, typename SMTExprTy>
 class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
   SMTSolverRef &Solver;
 
 public:
   SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB,
                        SMTSolverRef &S)
       : SimpleConstraintManager(SE, SB), Solver(S) {}
   virtual ~SMTConstraintManager() = default;
 
   //===------------------------------------------------------------------===//
   // Implementation for interface from SimpleConstraintManager.
   //===------------------------------------------------------------------===//
 
-  ProgramStateRef assumeSym(ProgramStateRef state, SymbolRef Sym,
-                            bool Assumption) override;
+  ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym,
+                            bool Assumption) override {
+    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 assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
                                           const llvm::APSInt &From,
                                           const llvm::APSInt &To,
-                                          bool InRange) override;
+                                          bool InRange) override {
+    ASTContext &Ctx = getBasicVals().getContext();
+    return assumeExpr(State, Sym,
+                      Solver->getRangeExpr(Ctx, Sym, From, To, InRange));
+  }
 
   ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
-                                       bool Assumption) override;
+                                       bool Assumption) override {
+    // Skip anything that is unsupported
+    return State;
+  }
 
   //===------------------------------------------------------------------===//
   // Implementation for interface from ConstraintManager.
   //===------------------------------------------------------------------===//
 
-  ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
+  ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override {
+    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 *getSymVal(ProgramStateRef State,
-                                SymbolRef Sym) const override;
+                                SymbolRef Sym) const override {
+    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!");
+  }
+
+  ProgramStateRef removeDeadBindings(ProgramStateRef State,
+                                     SymbolReaper &SymReaper) override {
+    auto CZ = State->get<ConstraintSMT>();
+    auto &CZFactory = State->get_context<ConstraintSMT>();
+
+    for (auto I = CZ.begin(), E = CZ.end(); I != E; ++I) {
+      if (SymReaper.maybeDead(I->first))
+        CZ = CZFactory.remove(CZ, *I);
+    }
+
+    return State->set<ConstraintSMT>(CZ);
+  }
+
+  void print(ProgramStateRef St, raw_ostream &OS, const char *nl,
+             const char *sep) override {
+
+    auto CZ = St->get<ConstraintSMT>();
+
+    OS << nl << sep << "Constraints:";
+    for (auto I = CZ.begin(), E = CZ.end(); I != E; ++I) {
+      OS << nl << ' ' << I->first << " : ";
+      I->second.print(OS);
+    }
+    OS << nl;
+  }
 
   /// Dumps SMT formula
   LLVM_DUMP_METHOD void dump() const { Solver->dump(); }
 
 protected:
   // Check whether a new model is satisfiable, and update the program state.
   virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym,
-                                     const SMTExprRef &Exp) = 0;
+                                     const SMTExprRef &Exp) {
+    // Check the model, avoid simplifying AST to save time
+    if (checkModel(State, Exp).isConstrainedTrue())
+      return State->add<ConstraintSMT>(
+          std::make_pair(Sym, static_cast<const SMTExprTy &>(*Exp)));
+
+    return nullptr;
+  }
 
   /// Given a program state, construct the logical conjunction and add it to
   /// the solver
-  virtual void addStateConstraints(ProgramStateRef State) const = 0;
+  virtual void addStateConstraints(ProgramStateRef State) const {
+    // TODO: Don't add all the constraints, only the relevant ones
+    auto CZ = State->get<ConstraintSMT>();
+    auto 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);
+    }
+  }
 
   // Generate and check a Z3 model, using the given constraint.
   ConditionTruthVal checkModel(ProgramStateRef State,
-                               const SMTExprRef &Exp) const;
+                               const SMTExprRef &Exp) const {
+    Solver->reset();
+    Solver->addConstraint(Exp);
+    addStateConstraints(State);
+    return Solver->check();
+  }
+
 }; // end class SMTConstraintManager
 
 } // namespace ento
 } // namespace clang
 
 #endif

cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt

add_clang_library(clangStaticAnalyzerCore
   RangeConstraintManager.cpp
   RangedConstraintManager.cpp
   RegionStore.cpp
   RetainSummaryManager.cpp
   SValBuilder.cpp
   SVals.cpp
   SimpleConstraintManager.cpp
   SimpleSValBuilder.cpp
-  SMTConstraintManager.cpp
   Store.cpp
   SubEngine.cpp
   SymbolManager.cpp
   WorkList.cpp
   Z3ConstraintManager.cpp
 
   LINK_LIBS
   clangAST

cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp

-//== 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();
-}

cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

public:
   /// Reset the solver and remove all constraints.
   void reset() const override { Z3_solver_reset(Context.Context, Solver); }
 
   void print(raw_ostream &OS) const override {
     OS << Z3_solver_to_string(Context.Context, Solver);
   }
 }; // 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();
 
     Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
     if (!SymVal)
       return true;
 
     const SymExpr *Sym = SymVal->getSymbol();
if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
 
       if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(BSE))
         return canReasonAbout(SVB.makeSymbolVal(SSE->getLHS())) &&
                canReasonAbout(SVB.makeSymbolVal(SSE->getRHS()));
     }
 
     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
 
 #endif
 
 std::unique_ptr<SMTSolver> clang::ento::CreateZ3Solver() {
 #if CLANG_ANALYZER_WITH_Z3