[analyzer] added cache for SMT queries in the SMTConstraintManager

[mikhail.ramalho]

Summary

This patch implements a new cache for the result of SMT queries; with this patch the regression tests are 25% faster.

It's implemented as a llvm::DenseMap where the key is the hash of the set of the constraints in a state.

There is still one method that does not use the cache, getSymVal, because it needs to get a symbol interpretation from the SMT, which is not cached yet.

[mikhail.ramalho]

Add comment to the cache member

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

ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override {
     SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy);
     SMTExprRef Exp =
         SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true);
 
     // Negate the constraint
     SMTExprRef NotExp =
         SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false);
 
-    Solver->reset();
-    addStateConstraints(State);
-
-    Solver->push();
-    Solver->addConstraint(Exp);
-
-    Optional<bool> isSat = Solver->check();
-    if (!isSat.hasValue())
-      return ConditionTruthVal();
-
-    Solver->pop();
-    Solver->addConstraint(NotExp);
-
-    Optional<bool> isNotSat = Solver->check();
-    if (!isNotSat.hasValue())
-      return ConditionTruthVal();
+    ConditionTruthVal isSat = checkModel(State, Sym, Exp);
+    ConditionTruthVal isNotSat = checkModel(State, Sym, NotExp);
 
     // Zero is the only possible solution
-    if (isSat.getValue() && !isNotSat.getValue())
+    if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse())
       return true;
 
     // Zero is not a solution
-    if (!isSat.getValue() && isNotSat.getValue())
+    if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue())
       return false;
 
     // Zero may be a solution
     return ConditionTruthVal();
   }
 
   const llvm::APSInt *getSymVal(ProgramStateRef State,
                                 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());
 
+      // TODO: this should call checkModel so we can use the cache, however,
+      // this method tries to get the interpretation (the actual value) from
+      // the solver, which is currently not cached.
+
       SMTExprRef Exp =
           SMTConv::fromData(Solver, SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty));
 
       Solver->reset();
       addStateConstraints(State);
 
       // Constraints are unsatisfiable
       Optional<bool> isSat = Solver->check();
public:
   /// 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) {
     // Check the model, avoid simplifying AST to save time
-    if (checkModel(State, Exp).isConstrainedTrue())
+    if (checkModel(State, Sym, 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
if (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,
+  ConditionTruthVal checkModel(ProgramStateRef State, SymbolRef Sym,
                                const SMTExprRef &Exp) const {
+    ProgramStateRef NewState = State->add<ConstraintSMT>(
+        std::make_pair(Sym, static_cast<const SMTExprTy &>(*Exp)));
+
+    llvm::FoldingSetNodeID ID;
+    NewState->get<ConstraintSMT>().Profile(ID);
+
+    unsigned hash = ID.ComputeHash();
+    auto I = Cached.find(hash);
+    if (I != Cached.end())
+      return I->second;
+
     Solver->reset();
-    Solver->addConstraint(Exp);
-    addStateConstraints(State);
+    addStateConstraints(NewState);
 
     Optional<bool> res = Solver->check();
     if (!res.hasValue())
-      return ConditionTruthVal();
+      Cached[hash] = ConditionTruthVal();
+    else
+      Cached[hash] = ConditionTruthVal(res.getValue());
 
-    return ConditionTruthVal(res.getValue());
+    return Cached[hash];
   }
+
+  // Cache the result of an SMT query (true, false, unknown). The key is the
+  // hash of the constraints in a state
+  mutable llvm::DenseMap<unsigned, ConditionTruthVal> Cached;
 }; // end class SMTConstraintManager
 
 } // namespace ento
 } // namespace clang
 
 #endif