10b57cec5SDimitry Andric //== SMTConstraintManager.h -------------------------------------*- C++ -*--==//
20b57cec5SDimitry Andric //
30b57cec5SDimitry Andric // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
40b57cec5SDimitry Andric // See https://llvm.org/LICENSE.txt for license information.
50b57cec5SDimitry Andric // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
60b57cec5SDimitry Andric //
70b57cec5SDimitry Andric //===----------------------------------------------------------------------===//
80b57cec5SDimitry Andric //
90b57cec5SDimitry Andric // This file defines a SMT generic API, which will be the base class for
100b57cec5SDimitry Andric // every SMT solver specific class.
110b57cec5SDimitry Andric //
120b57cec5SDimitry Andric //===----------------------------------------------------------------------===//
130b57cec5SDimitry Andric
140b57cec5SDimitry Andric #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
150b57cec5SDimitry Andric #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
160b57cec5SDimitry Andric
170b57cec5SDimitry Andric #include "clang/Basic/JsonSupport.h"
185ffd83dbSDimitry Andric #include "clang/Basic/TargetInfo.h"
190b57cec5SDimitry Andric #include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
200b57cec5SDimitry Andric #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
21bdd1243dSDimitry Andric #include <optional>
220b57cec5SDimitry Andric
230b57cec5SDimitry Andric typedef llvm::ImmutableSet<
240b57cec5SDimitry Andric std::pair<clang::ento::SymbolRef, const llvm::SMTExpr *>>
250b57cec5SDimitry Andric ConstraintSMTType;
REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintSMT,ConstraintSMTType)260b57cec5SDimitry Andric REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintSMT, ConstraintSMTType)
270b57cec5SDimitry Andric
280b57cec5SDimitry Andric namespace clang {
290b57cec5SDimitry Andric namespace ento {
300b57cec5SDimitry Andric
310b57cec5SDimitry Andric class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
320b57cec5SDimitry Andric mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver();
330b57cec5SDimitry Andric
340b57cec5SDimitry Andric public:
355ffd83dbSDimitry Andric SMTConstraintManager(clang::ento::ExprEngine *EE,
365ffd83dbSDimitry Andric clang::ento::SValBuilder &SB)
375ffd83dbSDimitry Andric : SimpleConstraintManager(EE, SB) {}
380b57cec5SDimitry Andric virtual ~SMTConstraintManager() = default;
390b57cec5SDimitry Andric
400b57cec5SDimitry Andric //===------------------------------------------------------------------===//
410b57cec5SDimitry Andric // Implementation for interface from SimpleConstraintManager.
420b57cec5SDimitry Andric //===------------------------------------------------------------------===//
430b57cec5SDimitry Andric
440b57cec5SDimitry Andric ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym,
450b57cec5SDimitry Andric bool Assumption) override {
460b57cec5SDimitry Andric ASTContext &Ctx = getBasicVals().getContext();
470b57cec5SDimitry Andric
480b57cec5SDimitry Andric QualType RetTy;
490b57cec5SDimitry Andric bool hasComparison;
500b57cec5SDimitry Andric
510b57cec5SDimitry Andric llvm::SMTExprRef Exp =
520b57cec5SDimitry Andric SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison);
530b57cec5SDimitry Andric
540b57cec5SDimitry Andric // Create zero comparison for implicit boolean cast, with reversed
550b57cec5SDimitry Andric // assumption
560b57cec5SDimitry Andric if (!hasComparison && !RetTy->isBooleanType())
570b57cec5SDimitry Andric return assumeExpr(
580b57cec5SDimitry Andric State, Sym,
590b57cec5SDimitry Andric SMTConv::getZeroExpr(Solver, Ctx, Exp, RetTy, !Assumption));
600b57cec5SDimitry Andric
610b57cec5SDimitry Andric return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp));
620b57cec5SDimitry Andric }
630b57cec5SDimitry Andric
640b57cec5SDimitry Andric ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
650b57cec5SDimitry Andric const llvm::APSInt &From,
660b57cec5SDimitry Andric const llvm::APSInt &To,
670b57cec5SDimitry Andric bool InRange) override {
680b57cec5SDimitry Andric ASTContext &Ctx = getBasicVals().getContext();
690b57cec5SDimitry Andric return assumeExpr(
700b57cec5SDimitry Andric State, Sym, SMTConv::getRangeExpr(Solver, Ctx, Sym, From, To, InRange));
710b57cec5SDimitry Andric }
720b57cec5SDimitry Andric
730b57cec5SDimitry Andric ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
740b57cec5SDimitry Andric bool Assumption) override {
750b57cec5SDimitry Andric // Skip anything that is unsupported
760b57cec5SDimitry Andric return State;
770b57cec5SDimitry Andric }
780b57cec5SDimitry Andric
790b57cec5SDimitry Andric //===------------------------------------------------------------------===//
800b57cec5SDimitry Andric // Implementation for interface from ConstraintManager.
810b57cec5SDimitry Andric //===------------------------------------------------------------------===//
820b57cec5SDimitry Andric
830b57cec5SDimitry Andric ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override {
840b57cec5SDimitry Andric ASTContext &Ctx = getBasicVals().getContext();
850b57cec5SDimitry Andric
860b57cec5SDimitry Andric QualType RetTy;
870b57cec5SDimitry Andric // The expression may be casted, so we cannot call getZ3DataExpr() directly
880b57cec5SDimitry Andric llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy);
890b57cec5SDimitry Andric llvm::SMTExprRef Exp =
900b57cec5SDimitry Andric SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true);
910b57cec5SDimitry Andric
920b57cec5SDimitry Andric // Negate the constraint
930b57cec5SDimitry Andric llvm::SMTExprRef NotExp =
940b57cec5SDimitry Andric SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false);
950b57cec5SDimitry Andric
960b57cec5SDimitry Andric ConditionTruthVal isSat = checkModel(State, Sym, Exp);
970b57cec5SDimitry Andric ConditionTruthVal isNotSat = checkModel(State, Sym, NotExp);
980b57cec5SDimitry Andric
990b57cec5SDimitry Andric // Zero is the only possible solution
1000b57cec5SDimitry Andric if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse())
1010b57cec5SDimitry Andric return true;
1020b57cec5SDimitry Andric
1030b57cec5SDimitry Andric // Zero is not a solution
1040b57cec5SDimitry Andric if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue())
1050b57cec5SDimitry Andric return false;
1060b57cec5SDimitry Andric
1070b57cec5SDimitry Andric // Zero may be a solution
1080b57cec5SDimitry Andric return ConditionTruthVal();
1090b57cec5SDimitry Andric }
1100b57cec5SDimitry Andric
1110b57cec5SDimitry Andric const llvm::APSInt *getSymVal(ProgramStateRef State,
1120b57cec5SDimitry Andric SymbolRef Sym) const override {
1130b57cec5SDimitry Andric BasicValueFactory &BVF = getBasicVals();
1140b57cec5SDimitry Andric ASTContext &Ctx = BVF.getContext();
1150b57cec5SDimitry Andric
1160b57cec5SDimitry Andric if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
1170b57cec5SDimitry Andric QualType Ty = Sym->getType();
1180b57cec5SDimitry Andric assert(!Ty->isRealFloatingType());
1190b57cec5SDimitry Andric llvm::APSInt Value(Ctx.getTypeSize(Ty),
1200b57cec5SDimitry Andric !Ty->isSignedIntegerOrEnumerationType());
1210b57cec5SDimitry Andric
1220b57cec5SDimitry Andric // TODO: this should call checkModel so we can use the cache, however,
1230b57cec5SDimitry Andric // this method tries to get the interpretation (the actual value) from
1240b57cec5SDimitry Andric // the solver, which is currently not cached.
1250b57cec5SDimitry Andric
126e8d8bef9SDimitry Andric llvm::SMTExprRef Exp = SMTConv::fromData(Solver, Ctx, SD);
1270b57cec5SDimitry Andric
1280b57cec5SDimitry Andric Solver->reset();
1290b57cec5SDimitry Andric addStateConstraints(State);
1300b57cec5SDimitry Andric
1310b57cec5SDimitry Andric // Constraints are unsatisfiable
132bdd1243dSDimitry Andric std::optional<bool> isSat = Solver->check();
13381ad6265SDimitry Andric if (!isSat || !*isSat)
1340b57cec5SDimitry Andric return nullptr;
1350b57cec5SDimitry Andric
1360b57cec5SDimitry Andric // Model does not assign interpretation
1370b57cec5SDimitry Andric if (!Solver->getInterpretation(Exp, Value))
1380b57cec5SDimitry Andric return nullptr;
1390b57cec5SDimitry Andric
1400b57cec5SDimitry Andric // A value has been obtained, check if it is the only value
1410b57cec5SDimitry Andric llvm::SMTExprRef NotExp = SMTConv::fromBinOp(
1420b57cec5SDimitry Andric Solver, Exp, BO_NE,
1430b57cec5SDimitry Andric Ty->isBooleanType() ? Solver->mkBoolean(Value.getBoolValue())
1440b57cec5SDimitry Andric : Solver->mkBitvector(Value, Value.getBitWidth()),
1450b57cec5SDimitry Andric /*isSigned=*/false);
1460b57cec5SDimitry Andric
1470b57cec5SDimitry Andric Solver->addConstraint(NotExp);
1480b57cec5SDimitry Andric
149bdd1243dSDimitry Andric std::optional<bool> isNotSat = Solver->check();
15081ad6265SDimitry Andric if (!isNotSat || *isNotSat)
1510b57cec5SDimitry Andric return nullptr;
1520b57cec5SDimitry Andric
1530b57cec5SDimitry Andric // This is the only solution, store it
1540b57cec5SDimitry Andric return &BVF.getValue(Value);
1550b57cec5SDimitry Andric }
1560b57cec5SDimitry Andric
1570b57cec5SDimitry Andric if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
1580b57cec5SDimitry Andric SymbolRef CastSym = SC->getOperand();
1590b57cec5SDimitry Andric QualType CastTy = SC->getType();
1600b57cec5SDimitry Andric // Skip the void type
1610b57cec5SDimitry Andric if (CastTy->isVoidType())
1620b57cec5SDimitry Andric return nullptr;
1630b57cec5SDimitry Andric
1640b57cec5SDimitry Andric const llvm::APSInt *Value;
1650b57cec5SDimitry Andric if (!(Value = getSymVal(State, CastSym)))
1660b57cec5SDimitry Andric return nullptr;
1670b57cec5SDimitry Andric return &BVF.Convert(SC->getType(), *Value);
1680b57cec5SDimitry Andric }
1690b57cec5SDimitry Andric
1700b57cec5SDimitry Andric if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
1710b57cec5SDimitry Andric const llvm::APSInt *LHS, *RHS;
1720b57cec5SDimitry Andric if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
1730b57cec5SDimitry Andric LHS = getSymVal(State, SIE->getLHS());
1740b57cec5SDimitry Andric RHS = &SIE->getRHS();
1750b57cec5SDimitry Andric } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
1760b57cec5SDimitry Andric LHS = &ISE->getLHS();
1770b57cec5SDimitry Andric RHS = getSymVal(State, ISE->getRHS());
1780b57cec5SDimitry Andric } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
1790b57cec5SDimitry Andric // Early termination to avoid expensive call
1800b57cec5SDimitry Andric LHS = getSymVal(State, SSM->getLHS());
1810b57cec5SDimitry Andric RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;
1820b57cec5SDimitry Andric } else {
1830b57cec5SDimitry Andric llvm_unreachable("Unsupported binary expression to get symbol value!");
1840b57cec5SDimitry Andric }
1850b57cec5SDimitry Andric
1860b57cec5SDimitry Andric if (!LHS || !RHS)
1870b57cec5SDimitry Andric return nullptr;
1880b57cec5SDimitry Andric
1890b57cec5SDimitry Andric llvm::APSInt ConvertedLHS, ConvertedRHS;
1900b57cec5SDimitry Andric QualType LTy, RTy;
1910b57cec5SDimitry Andric std::tie(ConvertedLHS, LTy) = SMTConv::fixAPSInt(Ctx, *LHS);
1920b57cec5SDimitry Andric std::tie(ConvertedRHS, RTy) = SMTConv::fixAPSInt(Ctx, *RHS);
1930b57cec5SDimitry Andric SMTConv::doIntTypeConversion<llvm::APSInt, &SMTConv::castAPSInt>(
1940b57cec5SDimitry Andric Solver, Ctx, ConvertedLHS, LTy, ConvertedRHS, RTy);
1950b57cec5SDimitry Andric return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
1960b57cec5SDimitry Andric }
1970b57cec5SDimitry Andric
1980b57cec5SDimitry Andric llvm_unreachable("Unsupported expression to get symbol value!");
1990b57cec5SDimitry Andric }
2000b57cec5SDimitry Andric
2010b57cec5SDimitry Andric ProgramStateRef removeDeadBindings(ProgramStateRef State,
2020b57cec5SDimitry Andric SymbolReaper &SymReaper) override {
2030b57cec5SDimitry Andric auto CZ = State->get<ConstraintSMT>();
2040b57cec5SDimitry Andric auto &CZFactory = State->get_context<ConstraintSMT>();
2050b57cec5SDimitry Andric
20606c3fb27SDimitry Andric for (const auto &Entry : CZ) {
20706c3fb27SDimitry Andric if (SymReaper.isDead(Entry.first))
20806c3fb27SDimitry Andric CZ = CZFactory.remove(CZ, Entry);
2090b57cec5SDimitry Andric }
2100b57cec5SDimitry Andric
2110b57cec5SDimitry Andric return State->set<ConstraintSMT>(CZ);
2120b57cec5SDimitry Andric }
2130b57cec5SDimitry Andric
2140b57cec5SDimitry Andric void printJson(raw_ostream &Out, ProgramStateRef State, const char *NL = "\n",
2150b57cec5SDimitry Andric unsigned int Space = 0, bool IsDot = false) const override {
2160b57cec5SDimitry Andric ConstraintSMTType Constraints = State->get<ConstraintSMT>();
2170b57cec5SDimitry Andric
2180b57cec5SDimitry Andric Indent(Out, Space, IsDot) << "\"constraints\": ";
2190b57cec5SDimitry Andric if (Constraints.isEmpty()) {
2200b57cec5SDimitry Andric Out << "null," << NL;
2210b57cec5SDimitry Andric return;
2220b57cec5SDimitry Andric }
2230b57cec5SDimitry Andric
2240b57cec5SDimitry Andric ++Space;
2250b57cec5SDimitry Andric Out << '[' << NL;
2260b57cec5SDimitry Andric for (ConstraintSMTType::iterator I = Constraints.begin();
2270b57cec5SDimitry Andric I != Constraints.end(); ++I) {
2280b57cec5SDimitry Andric Indent(Out, Space, IsDot)
2290b57cec5SDimitry Andric << "{ \"symbol\": \"" << I->first << "\", \"range\": \"";
2300b57cec5SDimitry Andric I->second->print(Out);
2310b57cec5SDimitry Andric Out << "\" }";
2320b57cec5SDimitry Andric
2330b57cec5SDimitry Andric if (std::next(I) != Constraints.end())
2340b57cec5SDimitry Andric Out << ',';
2350b57cec5SDimitry Andric Out << NL;
2360b57cec5SDimitry Andric }
2370b57cec5SDimitry Andric
2380b57cec5SDimitry Andric --Space;
2390b57cec5SDimitry Andric Indent(Out, Space, IsDot) << "],";
2400b57cec5SDimitry Andric }
2410b57cec5SDimitry Andric
2420b57cec5SDimitry Andric bool haveEqualConstraints(ProgramStateRef S1,
2430b57cec5SDimitry Andric ProgramStateRef S2) const override {
2440b57cec5SDimitry Andric return S1->get<ConstraintSMT>() == S2->get<ConstraintSMT>();
2450b57cec5SDimitry Andric }
2460b57cec5SDimitry Andric
2470b57cec5SDimitry Andric bool canReasonAbout(SVal X) const override {
2480b57cec5SDimitry Andric const TargetInfo &TI = getBasicVals().getContext().getTargetInfo();
2490b57cec5SDimitry Andric
250bdd1243dSDimitry Andric std::optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
2510b57cec5SDimitry Andric if (!SymVal)
2520b57cec5SDimitry Andric return true;
2530b57cec5SDimitry Andric
2540b57cec5SDimitry Andric const SymExpr *Sym = SymVal->getSymbol();
2550b57cec5SDimitry Andric QualType Ty = Sym->getType();
2560b57cec5SDimitry Andric
2570b57cec5SDimitry Andric // Complex types are not modeled
2580b57cec5SDimitry Andric if (Ty->isComplexType() || Ty->isComplexIntegerType())
2590b57cec5SDimitry Andric return false;
2600b57cec5SDimitry Andric
2610b57cec5SDimitry Andric // Non-IEEE 754 floating-point types are not modeled
2620b57cec5SDimitry Andric if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) &&
2630b57cec5SDimitry Andric (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() ||
2640b57cec5SDimitry Andric &TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble())))
2650b57cec5SDimitry Andric return false;
2660b57cec5SDimitry Andric
2670b57cec5SDimitry Andric if (Ty->isRealFloatingType())
2680b57cec5SDimitry Andric return Solver->isFPSupported();
2690b57cec5SDimitry Andric
2700b57cec5SDimitry Andric if (isa<SymbolData>(Sym))
2710b57cec5SDimitry Andric return true;
2720b57cec5SDimitry Andric
2730b57cec5SDimitry Andric SValBuilder &SVB = getSValBuilder();
2740b57cec5SDimitry Andric
2750b57cec5SDimitry Andric if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
2760b57cec5SDimitry Andric return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
2770b57cec5SDimitry Andric
2780b57cec5SDimitry Andric if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
2790b57cec5SDimitry Andric if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE))
2800b57cec5SDimitry Andric return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS()));
2810b57cec5SDimitry Andric
2820b57cec5SDimitry Andric if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE))
2830b57cec5SDimitry Andric return canReasonAbout(SVB.makeSymbolVal(ISE->getRHS()));
2840b57cec5SDimitry Andric
2850b57cec5SDimitry Andric if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(BSE))
2860b57cec5SDimitry Andric return canReasonAbout(SVB.makeSymbolVal(SSE->getLHS())) &&
2870b57cec5SDimitry Andric canReasonAbout(SVB.makeSymbolVal(SSE->getRHS()));
2880b57cec5SDimitry Andric }
2890b57cec5SDimitry Andric
2900b57cec5SDimitry Andric llvm_unreachable("Unsupported expression to reason about!");
2910b57cec5SDimitry Andric }
2920b57cec5SDimitry Andric
2930b57cec5SDimitry Andric /// Dumps SMT formula
2940b57cec5SDimitry Andric LLVM_DUMP_METHOD void dump() const { Solver->dump(); }
2950b57cec5SDimitry Andric
2960b57cec5SDimitry Andric protected:
2970b57cec5SDimitry Andric // Check whether a new model is satisfiable, and update the program state.
2980b57cec5SDimitry Andric virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym,
2990b57cec5SDimitry Andric const llvm::SMTExprRef &Exp) {
3000b57cec5SDimitry Andric // Check the model, avoid simplifying AST to save time
3010b57cec5SDimitry Andric if (checkModel(State, Sym, Exp).isConstrainedTrue())
3020b57cec5SDimitry Andric return State->add<ConstraintSMT>(std::make_pair(Sym, Exp));
3030b57cec5SDimitry Andric
3040b57cec5SDimitry Andric return nullptr;
3050b57cec5SDimitry Andric }
3060b57cec5SDimitry Andric
3070b57cec5SDimitry Andric /// Given a program state, construct the logical conjunction and add it to
3080b57cec5SDimitry Andric /// the solver
3090b57cec5SDimitry Andric virtual void addStateConstraints(ProgramStateRef State) const {
3100b57cec5SDimitry Andric // TODO: Don't add all the constraints, only the relevant ones
3110b57cec5SDimitry Andric auto CZ = State->get<ConstraintSMT>();
3120b57cec5SDimitry Andric auto I = CZ.begin(), IE = CZ.end();
3130b57cec5SDimitry Andric
3140b57cec5SDimitry Andric // Construct the logical AND of all the constraints
3150b57cec5SDimitry Andric if (I != IE) {
3160b57cec5SDimitry Andric std::vector<llvm::SMTExprRef> ASTs;
3170b57cec5SDimitry Andric
3180b57cec5SDimitry Andric llvm::SMTExprRef Constraint = I++->second;
3190b57cec5SDimitry Andric while (I != IE) {
3200b57cec5SDimitry Andric Constraint = Solver->mkAnd(Constraint, I++->second);
3210b57cec5SDimitry Andric }
3220b57cec5SDimitry Andric
3230b57cec5SDimitry Andric Solver->addConstraint(Constraint);
3240b57cec5SDimitry Andric }
3250b57cec5SDimitry Andric }
3260b57cec5SDimitry Andric
3270b57cec5SDimitry Andric // Generate and check a Z3 model, using the given constraint.
3280b57cec5SDimitry Andric ConditionTruthVal checkModel(ProgramStateRef State, SymbolRef Sym,
3290b57cec5SDimitry Andric const llvm::SMTExprRef &Exp) const {
3300b57cec5SDimitry Andric ProgramStateRef NewState =
3310b57cec5SDimitry Andric State->add<ConstraintSMT>(std::make_pair(Sym, Exp));
3320b57cec5SDimitry Andric
3330b57cec5SDimitry Andric llvm::FoldingSetNodeID ID;
3340b57cec5SDimitry Andric NewState->get<ConstraintSMT>().Profile(ID);
3350b57cec5SDimitry Andric
3360b57cec5SDimitry Andric unsigned hash = ID.ComputeHash();
3370b57cec5SDimitry Andric auto I = Cached.find(hash);
3380b57cec5SDimitry Andric if (I != Cached.end())
3390b57cec5SDimitry Andric return I->second;
3400b57cec5SDimitry Andric
3410b57cec5SDimitry Andric Solver->reset();
3420b57cec5SDimitry Andric addStateConstraints(NewState);
3430b57cec5SDimitry Andric
344bdd1243dSDimitry Andric std::optional<bool> res = Solver->check();
34581ad6265SDimitry Andric if (!res)
3460b57cec5SDimitry Andric Cached[hash] = ConditionTruthVal();
3470b57cec5SDimitry Andric else
348bdd1243dSDimitry Andric Cached[hash] = ConditionTruthVal(*res);
3490b57cec5SDimitry Andric
3500b57cec5SDimitry Andric return Cached[hash];
3510b57cec5SDimitry Andric }
3520b57cec5SDimitry Andric
3530b57cec5SDimitry Andric // Cache the result of an SMT query (true, false, unknown). The key is the
3540b57cec5SDimitry Andric // hash of the constraints in a state
3550b57cec5SDimitry Andric mutable llvm::DenseMap<unsigned, ConditionTruthVal> Cached;
3560b57cec5SDimitry Andric }; // end class SMTConstraintManager
3570b57cec5SDimitry Andric
3580b57cec5SDimitry Andric } // namespace ento
3590b57cec5SDimitry Andric } // namespace clang
3600b57cec5SDimitry Andric
3610b57cec5SDimitry Andric #endif
362