clang-r433403b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h - platform/prebuilts/clang/host/windows-x86 - Git at Google

 //== SMTConstraintManager.h -------------------------------------*- C++ -*--==//
 //
 // 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
 //
 //===----------------------------------------------------------------------===//
 //
 //  This file defines a SMT generic API, which will be the base class for
 //  every SMT solver specific class.
 //
 //===----------------------------------------------------------------------===//

 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H

 #include "clang/Basic/JsonSupport.h"
 #include "clang/Basic/TargetInfo.h"
 #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 {

 class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
   mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver();

 public:
   SMTConstraintManager(clang::ento::ExprEngine *EE,
                        clang::ento::SValBuilder &SB)
       : SimpleConstraintManager(EE, SB) {}
   virtual ~SMTConstraintManager() = default;

   //===------------------------------------------------------------------===//
   // Implementation for interface from SimpleConstraintManager.
   //===------------------------------------------------------------------===//

   ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym,
                             bool Assumption) override {
     ASTContext &Ctx = getBasicVals().getContext();

     QualType RetTy;
     bool hasComparison;

     llvm::SMTExprRef Exp =
         SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison);

     // Create zero comparison for implicit boolean cast, with reversed
     // assumption
     if (!hasComparison && !RetTy->isBooleanType())
       return assumeExpr(
           State, Sym,
           SMTConv::getZeroExpr(Solver, 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 {
     ASTContext &Ctx = getBasicVals().getContext();
     return assumeExpr(
         State, Sym, SMTConv::getRangeExpr(Solver, Ctx, Sym, From, To, InRange));
   }

   ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
                                        bool Assumption) override {
     // Skip anything that is unsupported
     return State;
   }

   //===------------------------------------------------------------------===//
   // Implementation for interface from ConstraintManager.
   //===------------------------------------------------------------------===//

   ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override {
     ASTContext &Ctx = getBasicVals().getContext();

     QualType RetTy;
     // The expression may be casted, so we cannot call getZ3DataExpr() directly
     llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy);
     llvm::SMTExprRef Exp =
         SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true);

     // Negate the constraint
     llvm::SMTExprRef NotExp =
         SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false);

     ConditionTruthVal isSat = checkModel(State, Sym, Exp);
     ConditionTruthVal isNotSat = checkModel(State, Sym, NotExp);

     // 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 {
     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.

       llvm::SMTExprRef Exp = SMTConv::fromData(Solver, Ctx, SD);

       Solver->reset();
       addStateConstraints(State);

       // Constraints are unsatisfiable
       Optional<bool> isSat = Solver->check();
       if (!isSat.hasValue() || !isSat.getValue())
         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
       llvm::SMTExprRef NotExp = SMTConv::fromBinOp(
           Solver, Exp, BO_NE,
           Ty->isBooleanType() ? Solver->mkBoolean(Value.getBoolValue())
                               : Solver->mkBitvector(Value, Value.getBitWidth()),
           /*isSigned=*/false);

       Solver->addConstraint(NotExp);

       Optional<bool> isNotSat = Solver->check();
       if (!isNotSat.hasValue() || isNotSat.getValue())
         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) = SMTConv::fixAPSInt(Ctx, *LHS);
       std::tie(ConvertedRHS, RTy) = SMTConv::fixAPSInt(Ctx, *RHS);
       SMTConv::doIntTypeConversion<llvm::APSInt, &SMTConv::castAPSInt>(
           Solver, 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.isDead(I->first))
         CZ = CZFactory.remove(CZ, *I);
     }

     return State->set<ConstraintSMT>(CZ);
   }

   void printJson(raw_ostream &Out, ProgramStateRef State, const char *NL = "\n",
                  unsigned int Space = 0, bool IsDot = false) const override {
     ConstraintSMTType Constraints = State->get<ConstraintSMT>();

     Indent(Out, Space, IsDot) << "\"constraints\": ";
     if (Constraints.isEmpty()) {
       Out << "null," << NL;
       return;
     }

     ++Space;
     Out << '[' << NL;
     for (ConstraintSMTType::iterator I = Constraints.begin();
          I != Constraints.end(); ++I) {
       Indent(Out, Space, IsDot)
           << "{ \"symbol\": \"" << I->first << "\", \"range\": \"";
       I->second->print(Out);
       Out << "\" }";

       if (std::next(I) != Constraints.end())
         Out << ',';
       Out << NL;
     }

     --Space;
     Indent(Out, Space, IsDot) << "],";
   }

   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();

     Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
     if (!SymVal)
       return true;

     const SymExpr *Sym = SymVal->getSymbol();
     QualType Ty = Sym->getType();

     // Complex types are not modeled
     if (Ty->isComplexType() || Ty->isComplexIntegerType())
       return false;

     // Non-IEEE 754 floating-point types are not modeled
     if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) &&
          (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() ||
           &TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble())))
       return false;

     if (Ty->isRealFloatingType())
       return Solver->isFPSupported();

     if (isa<SymbolData>(Sym))
       return true;

     SValBuilder &SVB = getSValBuilder();

     if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
       return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));

     if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
       if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE))
         return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS()));

       if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE))
         return canReasonAbout(SVB.makeSymbolVal(ISE->getRHS()));

       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!");
   }

   /// 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 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, Exp));

     return nullptr;
   }

   /// Given a program state, construct the logical conjunction and add it to
   /// the solver
   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<llvm::SMTExprRef> ASTs;

       llvm::SMTExprRef Constraint = I++->second;
       while (I != IE) {
         Constraint = Solver->mkAnd(Constraint, I++->second);
       }

       Solver->addConstraint(Constraint);
     }
   }

   // Generate and check a Z3 model, using the given constraint.
   ConditionTruthVal checkModel(ProgramStateRef State, SymbolRef Sym,
                                const llvm::SMTExprRef &Exp) const {
     ProgramStateRef NewState =
         State->add<ConstraintSMT>(std::make_pair(Sym, 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();
     addStateConstraints(NewState);

     Optional<bool> res = Solver->check();
     if (!res.hasValue())
       Cached[hash] = ConditionTruthVal();
     else
       Cached[hash] = 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
	//== SMTConstraintManager.h -------------------------------------- C++ ---==//
	//
	// 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
	//
	//===----------------------------------------------------------------------===//
	//
	// This file defines a SMT generic API, which will be the base class for
	// every SMT solver specific class.
	//
	//===----------------------------------------------------------------------===//

	#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
	#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H

	#include "clang/Basic/JsonSupport.h"
	#include "clang/Basic/TargetInfo.h"
	#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 {

	class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
	mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver();

	public:
	SMTConstraintManager(clang::ento::ExprEngine *EE,
	clang::ento::SValBuilder &SB)
	: SimpleConstraintManager(EE, SB) {}
	virtual ~SMTConstraintManager() = default;

	//===------------------------------------------------------------------===//
	// Implementation for interface from SimpleConstraintManager.
	//===------------------------------------------------------------------===//

	ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym,
	bool Assumption) override {
	ASTContext &Ctx = getBasicVals().getContext();

	QualType RetTy;
	bool hasComparison;

	llvm::SMTExprRef Exp =
	SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison);

	// Create zero comparison for implicit boolean cast, with reversed
	// assumption
	if (!hasComparison && !RetTy->isBooleanType())
	return assumeExpr(
	State, Sym,
	SMTConv::getZeroExpr(Solver, 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 {
	ASTContext &Ctx = getBasicVals().getContext();
	return assumeExpr(
	State, Sym, SMTConv::getRangeExpr(Solver, Ctx, Sym, From, To, InRange));
	}

	ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
	bool Assumption) override {
	// Skip anything that is unsupported
	return State;
	}

	//===------------------------------------------------------------------===//
	// Implementation for interface from ConstraintManager.
	//===------------------------------------------------------------------===//

	ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override {
	ASTContext &Ctx = getBasicVals().getContext();

	QualType RetTy;
	// The expression may be casted, so we cannot call getZ3DataExpr() directly
	llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy);
	llvm::SMTExprRef Exp =
	SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /Assumption=/true);

	// Negate the constraint
	llvm::SMTExprRef NotExp =
	SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /Assumption=/false);

	ConditionTruthVal isSat = checkModel(State, Sym, Exp);
	ConditionTruthVal isNotSat = checkModel(State, Sym, NotExp);

	// 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 {
	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.

	llvm::SMTExprRef Exp = SMTConv::fromData(Solver, Ctx, SD);

	Solver->reset();
	addStateConstraints(State);

	// Constraints are unsatisfiable
	Optional<bool> isSat = Solver->check();
	if (!isSat.hasValue() \|\| !isSat.getValue())
	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
	llvm::SMTExprRef NotExp = SMTConv::fromBinOp(
	Solver, Exp, BO_NE,
	Ty->isBooleanType() ? Solver->mkBoolean(Value.getBoolValue())
	: Solver->mkBitvector(Value, Value.getBitWidth()),
	/isSigned=/false);

	Solver->addConstraint(NotExp);

	Optional<bool> isNotSat = Solver->check();
	if (!isNotSat.hasValue() \|\| isNotSat.getValue())
	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) = SMTConv::fixAPSInt(Ctx, *LHS);
	std::tie(ConvertedRHS, RTy) = SMTConv::fixAPSInt(Ctx, *RHS);
	SMTConv::doIntTypeConversion<llvm::APSInt, &SMTConv::castAPSInt>(
	Solver, 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.isDead(I->first))
	CZ = CZFactory.remove(CZ, *I);
	}

	return State->set<ConstraintSMT>(CZ);
	}

	void printJson(raw_ostream &Out, ProgramStateRef State, const char *NL = "\n",
	unsigned int Space = 0, bool IsDot = false) const override {
	ConstraintSMTType Constraints = State->get<ConstraintSMT>();

	Indent(Out, Space, IsDot) << "\"constraints\": ";
	if (Constraints.isEmpty()) {
	Out << "null," << NL;
	return;
	}

	++Space;
	Out << '[' << NL;
	for (ConstraintSMTType::iterator I = Constraints.begin();
	I != Constraints.end(); ++I) {
	Indent(Out, Space, IsDot)
	<< "{ \"symbol\": \"" << I->first << "\", \"range\": \"";
	I->second->print(Out);
	Out << "\" }";

	if (std::next(I) != Constraints.end())
	Out << ',';
	Out << NL;
	}

	--Space;
	Indent(Out, Space, IsDot) << "],";
	}

	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();

	Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
	if (!SymVal)
	return true;

	const SymExpr *Sym = SymVal->getSymbol();
	QualType Ty = Sym->getType();

	// Complex types are not modeled
	if (Ty->isComplexType() \|\| Ty->isComplexIntegerType())
	return false;

	// Non-IEEE 754 floating-point types are not modeled
	if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) &&
	(&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() \|\|
	&TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble())))
	return false;

	if (Ty->isRealFloatingType())
	return Solver->isFPSupported();

	if (isa<SymbolData>(Sym))
	return true;

	SValBuilder &SVB = getSValBuilder();

	if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
	return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));

	if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
	if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE))
	return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS()));

	if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE))
	return canReasonAbout(SVB.makeSymbolVal(ISE->getRHS()));

	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!");
	}

	/// 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 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, Exp));

	return nullptr;
	}

	/// Given a program state, construct the logical conjunction and add it to
	/// the solver
	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<llvm::SMTExprRef> ASTs;

	llvm::SMTExprRef Constraint = I++->second;
	while (I != IE) {
	Constraint = Solver->mkAnd(Constraint, I++->second);
	}

	Solver->addConstraint(Constraint);
	}
	}

	// Generate and check a Z3 model, using the given constraint.
	ConditionTruthVal checkModel(ProgramStateRef State, SymbolRef Sym,
	const llvm::SMTExprRef &Exp) const {
	ProgramStateRef NewState =
	State->add<ConstraintSMT>(std::make_pair(Sym, 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();
	addStateConstraints(NewState);

	Optional<bool> res = Solver->check();
	if (!res.hasValue())
	Cached[hash] = ConditionTruthVal();
	else
	Cached[hash] = 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