14#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
15#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
23typedef llvm::ImmutableSet<
24 std::pair<clang::ento::SymbolRef, const llvm::SMTExpr *>>
32 mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver();
45 bool Assumption)
override {
51 llvm::SMTExprRef Exp =
61 return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp));
65 const llvm::APSInt &From,
66 const llvm::APSInt &To,
67 bool InRange)
override {
74 bool Assumption)
override {
89 llvm::SMTExprRef Exp =
93 llvm::SMTExprRef NotExp =
116 if (
const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
132 std::optional<bool> isSat = Solver->check();
133 if (!isSat || !*isSat)
137 if (!Solver->getInterpretation(Exp,
Value))
144 : Solver->mkBitvector(
Value,
Value.getBitWidth()),
147 Solver->addConstraint(NotExp);
149 std::optional<bool> isNotSat = Solver->check();
150 if (!isNotSat || *isNotSat)
154 return &BVF.getValue(
Value);
157 if (
const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
164 const llvm::APSInt *
Value;
170 if (
const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
171 const llvm::APSInt *LHS, *RHS;
172 if (
const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
174 RHS = &SIE->getRHS();
175 }
else if (
const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
176 LHS = &ISE->getLHS();
178 }
else if (
const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
181 RHS = LHS ?
getSymVal(State, SSM->getRHS()) :
nullptr;
183 llvm_unreachable(
"Unsupported binary expression to get symbol value!");
189 llvm::APSInt ConvertedLHS, ConvertedRHS;
193 SMTConv::doIntTypeConversion<llvm::APSInt, &SMTConv::castAPSInt>(
194 Solver, Ctx, ConvertedLHS, LTy, ConvertedRHS, RTy);
195 return BVF.
evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
198 llvm_unreachable(
"Unsupported expression to get symbol value!");
203 auto CZ = State->get<ConstraintSMT>();
204 auto &CZFactory = State->get_context<ConstraintSMT>();
206 for (
const auto &Entry : CZ) {
207 if (SymReaper.
isDead(Entry.first))
208 CZ = CZFactory.remove(CZ, Entry);
211 return State->set<ConstraintSMT>(CZ);
215 unsigned int Space = 0,
bool IsDot =
false)
const override {
218 Indent(Out, Space, IsDot) <<
"\"constraints\": ";
219 if (Constraints.isEmpty()) {
220 Out <<
"null," << NL;
226 for (ConstraintSMTType::iterator I = Constraints.begin();
227 I != Constraints.end(); ++I) {
228 Indent(Out, Space, IsDot)
229 <<
"{ \"symbol\": \"" << I->first <<
"\", \"range\": \"";
230 I->second->print(Out);
233 if (std::next(I) != Constraints.end())
239 Indent(Out, Space, IsDot) <<
"],";
244 return S1->get<ConstraintSMT>() == S2->get<ConstraintSMT>();
254 const SymExpr *Sym = SymVal->getSymbol();
268 return Solver->isFPSupported();
270 if (isa<SymbolData>(Sym))
275 if (
const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
278 if (
const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
279 if (
const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE))
282 if (
const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE))
285 if (
const SymSymExpr *SSE = dyn_cast<SymSymExpr>(BSE))
290 llvm_unreachable(
"Unsupported expression to reason about!");
294 LLVM_DUMP_METHOD
void dump()
const { Solver->dump(); }
299 const llvm::SMTExprRef &Exp) {
301 if (
checkModel(State, Sym, Exp).isConstrainedTrue())
302 return State->add<ConstraintSMT>(std::make_pair(Sym, Exp));
311 auto CZ = State->get<ConstraintSMT>();
312 auto I = CZ.begin(), IE = CZ.end();
316 std::vector<llvm::SMTExprRef> ASTs;
318 llvm::SMTExprRef Constraint = I++->second;
320 Constraint = Solver->mkAnd(Constraint, I++->second);
323 Solver->addConstraint(Constraint);
329 const llvm::SMTExprRef &Exp)
const {
331 State->add<ConstraintSMT>(std::make_pair(Sym, Exp));
333 llvm::FoldingSetNodeID
ID;
334 NewState->get<ConstraintSMT>().Profile(
ID);
336 unsigned hash =
ID.ComputeHash();
337 auto I =
Cached.find(hash);
344 std::optional<bool> res = Solver->check();
355 mutable llvm::DenseMap<unsigned, ConditionTruthVal>
Cached;
#define REGISTER_TRAIT_WITH_PROGRAMSTATE(Name, Type)
Declares a program state trait for type Type called Name, and introduce a type named NameTy.
llvm::ImmutableSet< std::pair< clang::ento::SymbolRef, const llvm::SMTExpr * > > ConstraintSMTType
Holds long-lived AST nodes (such as types and decls) that can be referred to throughout the semantic ...
uint64_t getTypeSize(QualType T) const
Return the size of the specified (complete) type T, in bits.
const TargetInfo & getTargetInfo() const
A (possibly-)qualified type.
Exposes information about the current target.
const llvm::fltSemantics & getLongDoubleFormat() const
bool isBooleanType() const
bool isSignedIntegerOrEnumerationType() const
Determines whether this is an integer type that is signed or an enumeration types whose underlying ty...
bool isComplexType() const
isComplexType() does not include complex integers (a GCC extension).
bool isSpecificBuiltinType(unsigned K) const
Test for a particular builtin type.
bool isComplexIntegerType() const
bool isRealFloatingType() const
Floating point categories.
const llvm::APSInt & Convert(const llvm::APSInt &To, const llvm::APSInt &From)
Convert - Create a new persistent APSInt with the same value as 'From' but with the bitwidth and sign...
const llvm::APSInt * evalAPSInt(BinaryOperator::Opcode Op, const llvm::APSInt &V1, const llvm::APSInt &V2)
ASTContext & getContext() const
Template implementation for all binary symbolic expressions.
Represents a symbolic expression involving a binary operator.
bool isConstrainedFalse() const
Return true if the constraint is perfectly constrained to 'false'.
bool isConstrainedTrue() const
Return true if the constraint is perfectly constrained to 'true'.
SMTConstraintManager(clang::ento::ExprEngine *EE, clang::ento::SValBuilder &SB)
virtual void addStateConstraints(ProgramStateRef State) const
Given a program state, construct the logical conjunction and add it to the solver.
bool canReasonAbout(SVal X) const override
canReasonAbout - Not all ConstraintManagers can accurately reason about all SVal values.
ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) override
Given a symbolic expression within the range [From, To], assume that it is true/false and generate th...
LLVM_DUMP_METHOD void dump() const
Dumps SMT formula.
ConditionTruthVal checkModel(ProgramStateRef State, SymbolRef Sym, const llvm::SMTExprRef &Exp) const
const llvm::APSInt * getSymVal(ProgramStateRef State, SymbolRef Sym) const override
If a symbol is perfectly constrained to a constant, attempt to return the concrete value.
ProgramStateRef removeDeadBindings(ProgramStateRef State, SymbolReaper &SymReaper) override
Scan all symbols referenced by the constraints.
ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override
Returns whether or not a symbol is known to be null ("true"), known to be non-null ("false"),...
ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym, bool Assumption) override
Given a symbolic expression that can be reasoned about, assume that it is true/false and generate the...
llvm::DenseMap< unsigned, ConditionTruthVal > Cached
virtual ~SMTConstraintManager()=default
virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym, const llvm::SMTExprRef &Exp)
void printJson(raw_ostream &Out, ProgramStateRef State, const char *NL="\n", unsigned int Space=0, bool IsDot=false) const override
ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym, bool Assumption) override
Given a symbolic expression that cannot be reasoned about, assume that it is zero/nonzero and add it ...
bool haveEqualConstraints(ProgramStateRef S1, ProgramStateRef S2) const override
static llvm::SMTExprRef getZeroExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const llvm::SMTExprRef &Exp, QualType Ty, bool Assumption)
static llvm::SMTExprRef getRangeExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange)
static llvm::SMTExprRef getExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, QualType *RetTy=nullptr, bool *hasComparison=nullptr)
static llvm::SMTExprRef fromData(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const SymbolData *Sym)
Construct an SMTSolverRef from a SymbolData.
static llvm::SMTExprRef fromBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS, const BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS, bool isSigned)
Construct an SMTSolverRef from a binary operator.
static std::pair< llvm::APSInt, QualType > fixAPSInt(ASTContext &Ctx, const llvm::APSInt &Int)
DefinedSVal makeSymbolVal(SymbolRef Sym)
Make an SVal that represents the given symbol.
SVal - This represents a symbolic expression, which can be either an L-value or an R-value.
SValBuilder & getSValBuilder() const
BasicValueFactory & getBasicVals() const
virtual QualType getType() const =0
Represents a cast expression.
A symbol representing data which can be stored in a memory location (region).
A class responsible for cleaning up unused symbols.
bool isDead(SymbolRef sym)
Returns whether or not a symbol has been confirmed dead.
Represents symbolic expression that isn't a location.
Defines the clang::TargetInfo interface.