1 files changed, 32 insertions, 25 deletions

diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
index 8eaa9365be..fe097b92b3 100644
--- a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -1,9 +1,8 @@
 //== SMTConstraintManager.h -------------------------------------*- C++ -*--==//
 //
-//                     The LLVM Compiler Infrastructure
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
 //
 //===----------------------------------------------------------------------===//
 //
@@ -18,17 +17,20 @@
 #include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
 
+typedef llvm::ImmutableSet<
+    std::pair<clang::ento::SymbolRef, const llvm::SMTExpr *>>
+    ConstraintSMTType;
+REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintSMT, ConstraintSMTType)
+
 namespace clang {
 namespace ento {
 
-template <typename ConstraintSMT, typename SMTExprTy>
 class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
-  SMTSolverRef &Solver;
+  mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver();
 
 public:
-  SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB,
-                       SMTSolverRef &S)
-      : SimpleConstraintManager(SE, SB), Solver(S) {}
+  SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB)
+      : SimpleConstraintManager(SE, SB) {}
   virtual ~SMTConstraintManager() = default;
 
   //===------------------------------------------------------------------===//
@@ -42,7 +44,8 @@ public:
     QualType RetTy;
     bool hasComparison;
 
-    SMTExprRef Exp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison);
+    llvm::SMTExprRef Exp =
+        SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison);
 
     // Create zero comparison for implicit boolean cast, with reversed
     // assumption
@@ -78,12 +81,12 @@ public:
 
     QualType RetTy;
     // The expression may be casted, so we cannot call getZ3DataExpr() directly
-    SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy);
-    SMTExprRef Exp =
+    llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy);
+    llvm::SMTExprRef Exp =
         SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true);
 
     // Negate the constraint
-    SMTExprRef NotExp =
+    llvm::SMTExprRef NotExp =
         SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false);
 
     ConditionTruthVal isSat = checkModel(State, Sym, Exp);
@@ -116,7 +119,7 @@ public:
       // this method tries to get the interpretation (the actual value) from
       // the solver, which is currently not cached.
 
-      SMTExprRef Exp =
+      llvm::SMTExprRef Exp =
           SMTConv::fromData(Solver, SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty));
 
       Solver->reset();
@@ -132,7 +135,7 @@ public:
         return nullptr;
 
       // A value has been obtained, check if it is the only value
-      SMTExprRef NotExp = SMTConv::fromBinOp(
+      llvm::SMTExprRef NotExp = SMTConv::fromBinOp(
           Solver, Exp, BO_NE,
           Ty->isBooleanType() ? Solver->mkBoolean(Value.getBoolValue())
                               : Solver->mkBitvector(Value, Value.getBitWidth()),
@@ -213,11 +216,16 @@ public:
     OS << nl << sep << "Constraints:";
     for (auto I = CZ.begin(), E = CZ.end(); I != E; ++I) {
       OS << nl << ' ' << I->first << " : ";
-      I->second.print(OS);
+      I->second->print(OS);
     }
     OS << nl;
   }
 
+  bool haveEqualConstraints(ProgramStateRef S1,
+                            ProgramStateRef S2) const override {
+    return S1->get<ConstraintSMT>() == S2->get<ConstraintSMT>();
+  }
+
   bool canReasonAbout(SVal X) const override {
     const TargetInfo &TI = getBasicVals().getContext().getTargetInfo();
 
@@ -270,11 +278,10 @@ public:
 protected:
   // Check whether a new model is satisfiable, and update the program state.
   virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym,
-                                     const SMTExprRef &Exp) {
+                                     const llvm::SMTExprRef &Exp) {
     // Check the model, avoid simplifying AST to save time
     if (checkModel(State, Sym, Exp).isConstrainedTrue())
-      return State->add<ConstraintSMT>(
-          std::make_pair(Sym, static_cast<const SMTExprTy &>(*Exp)));
+      return State->add<ConstraintSMT>(std::make_pair(Sym, Exp));
 
     return nullptr;
   }
@@ -288,11 +295,11 @@ protected:
 
     // Construct the logical AND of all the constraints
     if (I != IE) {
-      std::vector<SMTExprRef> ASTs;
+      std::vector<llvm::SMTExprRef> ASTs;
 
-      SMTExprRef Constraint = Solver->newExprRef(I++->second);
+      llvm::SMTExprRef Constraint = I++->second;
       while (I != IE) {
-        Constraint = Solver->mkAnd(Constraint, Solver->newExprRef(I++->second));
+        Constraint = Solver->mkAnd(Constraint, I++->second);
       }
 
       Solver->addConstraint(Constraint);
@@ -301,9 +308,9 @@ protected:
 
   // Generate and check a Z3 model, using the given constraint.
   ConditionTruthVal checkModel(ProgramStateRef State, SymbolRef Sym,
-                               const SMTExprRef &Exp) const {
-    ProgramStateRef NewState = State->add<ConstraintSMT>(
-        std::make_pair(Sym, static_cast<const SMTExprTy &>(*Exp)));
+                               const llvm::SMTExprRef &Exp) const {
+    ProgramStateRef NewState =
+        State->add<ConstraintSMT>(std::make_pair(Sym, Exp));
 
     llvm::FoldingSetNodeID ID;
     NewState->get<ConstraintSMT>().Profile(ID);