clang: include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Source File (original) (raw)
1
2
3
4
5
6
7
8
9
10
11
12
13
14#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
15#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
16
22#include
23
24typedef llvm::ImmutableSet<
25 std::pair<clang::ento::SymbolRef, const llvm::SMTExpr *>>
28
30namespace ento {
31
33 mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver();
34
35public:
39 Solver->setBoolParam("model", true);
40 Solver->setUnsignedParam("timeout", 15000 );
41 }
43
44
45
46
47
49 bool Assumption) override {
51
53 bool hasComparison;
54
55 llvm::SMTExprRef Exp =
57
58
59
62 State, Sym,
64
65 return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp));
66 }
67
69 const llvm::APSInt &From,
70 const llvm::APSInt &To,
71 bool InRange) override {
75 }
76
78 bool Assumption) override {
79
80 return State;
81 }
82
83
84
85
86
89
91
92 llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy);
93 llvm::SMTExprRef Exp =
95
96
97 llvm::SMTExprRef NotExp =
99
102
103
105 return true;
106
107
109 return false;
110
111
113 }
114
119
120 if (const SymbolData *SD = dyn_cast(Sym)) {
123 llvm::APSInt Value(Ctx.getTypeSize(Ty),
125
126
127
128
129
131
132 Solver->reset();
134
135
136 std::optional isSat = Solver->check();
137 if (!isSat || !*isSat)
138 return nullptr;
139
140
141 if (!Solver->getInterpretation(Exp, Value))
142 return nullptr;
143
144
146 Solver, Exp, BO_NE,
148 : Solver->mkBitvector(Value, Value.getBitWidth()),
149 false);
150
151 Solver->addConstraint(NotExp);
152
153 std::optional isNotSat = Solver->check();
154 if (!isNotSat || *isNotSat)
155 return nullptr;
156
157
158 return BVF.getValue(Value).get();
159 }
160
161 if (const SymbolCast *SC = dyn_cast(Sym)) {
162 SymbolRef CastSym = SC->getOperand();
163 QualType CastTy = SC->getType();
164
166 return nullptr;
167
168 const llvm::APSInt *Value;
170 return nullptr;
172 }
173
174 if (const BinarySymExpr *BSE = dyn_cast(Sym)) {
175 const llvm::APSInt *LHS, *RHS;
176 if (const SymIntExpr *SIE = dyn_cast(BSE)) {
177 LHS = getSymVal(State, SIE->getLHS());
178 RHS = SIE->getRHS().get();
179 } else if (const IntSymExpr *ISE = dyn_cast(BSE)) {
180 LHS = ISE->getLHS().get();
181 RHS = getSymVal(State, ISE->getRHS());
182 } else if (const SymSymExpr *SSM = dyn_cast(BSE)) {
183
184 LHS = getSymVal(State, SSM->getLHS());
185 RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;
186 } else {
187 llvm_unreachable("Unsupported binary expression to get symbol value!");
188 }
189
190 if (!LHS || !RHS)
191 return nullptr;
192
193 llvm::APSInt ConvertedLHS, ConvertedRHS;
197 SMTConv::doIntTypeConversion<llvm::APSInt, &SMTConv::castAPSInt>(
198 Solver, Ctx, ConvertedLHS, LTy, ConvertedRHS, RTy);
199 std::optional Res =
200 BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
201 return Res ? Res.value().get() : nullptr;
202 }
203
204 llvm_unreachable("Unsupported expression to get symbol value!");
205 }
206
209 auto CZ = State->get();
210 auto &CZFactory = State->get_context();
211
212 for (const auto &Entry : CZ) {
213 if (SymReaper.isDead(Entry.first))
214 CZ = CZFactory.remove(CZ, Entry);
215 }
216
217 return State->set(CZ);
218 }
219
221 unsigned int Space = 0, bool IsDot = false) const override {
223
224 Indent(Out, Space, IsDot) << "\"constraints\": ";
225 if (Constraints.isEmpty()) {
226 Out << "null," << NL;
227 return;
228 }
229
230 ++Space;
231 Out << '[' << NL;
232 for (ConstraintSMTType::iterator I = Constraints.begin();
233 I != Constraints.end(); ++I) {
234 Indent(Out, Space, IsDot)
235 << "{ \"symbol\": \"" << I->first << "\", \"range\": \"";
236 I->second->print(Out);
237 Out << "\" }";
238
239 if (std::next(I) != Constraints.end())
240 Out << ',';
241 Out << NL;
242 }
243
244 --Space;
245 Indent(Out, Space, IsDot) << "],";
246 }
247
250 return S1->get() == S2->get();
251 }
252
255
256 std::optionalnonloc::SymbolVal SymVal = X.getAs<nonloc::SymbolVal>();
257 if (!SymVal)
258 return true;
259
260 const SymExpr *Sym = SymVal->getSymbol();
262
263
265 return false;
266
267
271 return false;
272
274 return Solver->isFPSupported();
275
276 if (isa(Sym))
277 return true;
278
280
281 if (const SymbolCast *SC = dyn_cast(Sym))
283
284
285 if (isa(Sym)) {
286 return false;
287 }
288
289 if (const BinarySymExpr *BSE = dyn_cast(Sym)) {
290 if (const SymIntExpr *SIE = dyn_cast(BSE))
292
293 if (const IntSymExpr *ISE = dyn_cast(BSE))
295
296 if (const SymSymExpr *SSE = dyn_cast(BSE))
299 }
300
301 llvm_unreachable("Unsupported expression to reason about!");
302 }
303
304
305 LLVM_DUMP_METHOD void dump() const { Solver->dump(); }
306
307protected:
308
310 const llvm::SMTExprRef &Exp) {
311
312 if (checkModel(State, Sym, Exp).isConstrainedTrue())
313 return State->add(std::make_pair(Sym, Exp));
314
315 return nullptr;
316 }
317
318
319
321
322 auto CZ = State->get();
323 auto I = CZ.begin(), IE = CZ.end();
324
325
326 if (I != IE) {
327 std::vectorllvm::SMTExprRef ASTs;
328
329 llvm::SMTExprRef Constraint = I++->second;
330 while (I != IE) {
331 Constraint = Solver->mkAnd(Constraint, I++->second);
332 }
333
334 Solver->addConstraint(Constraint);
335 }
336 }
337
338
340 const llvm::SMTExprRef &Exp) const {
342 State->add(std::make_pair(Sym, Exp));
343
344 llvm::FoldingSetNodeID ID;
345 NewState->get().Profile(ID);
346
347 unsigned hash = ID.ComputeHash();
348 auto I = Cached.find(hash);
349 if (I != Cached.end())
350 return I->second;
351
352 Solver->reset();
354
355 std::optional res = Solver->check();
356 if (!res)
358 else
360
362 }
363
364
365
366 mutable llvm::DenseMap<unsigned, ConditionTruthVal> Cached;
367};
368
369}
370}
371
372#endif
#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 ...
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.
LLVM_ATTRIBUTE_RETURNS_NONNULL const APSInt * get() const
std::optional< APSIntPtr > evalAPSInt(BinaryOperator::Opcode Op, const llvm::APSInt &V1, const llvm::APSInt &V2)
ASTContext & getContext() const
APSIntPtr 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...
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.
The JSON file list parser is used to communicate input to InstallAPI.