clang 20.0.0git
SMTConstraintManager.h
Go to the documentation of this file.
1//== SMTConstraintManager.h -------------------------------------*- C++ -*--==//
2//
3// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4// See https://llvm.org/LICENSE.txt for license information.
5// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6//
7//===----------------------------------------------------------------------===//
8//
9// This file defines a SMT generic API, which will be the base class for
10// every SMT solver specific class.
11//
12//===----------------------------------------------------------------------===//
13
14#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
15#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
16
21#include <optional>
22
23typedef llvm::ImmutableSet<
24 std::pair<clang::ento::SymbolRef, const llvm::SMTExpr *>>
27
28namespace clang {
29namespace ento {
30
32 mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver();
33
34public:
37 : SimpleConstraintManager(EE, SB) {
38 Solver->setBoolParam("model", true); // Enable model finding
39 Solver->setUnsignedParam("timeout", 15000 /*milliseconds*/);
40 }
41 virtual ~SMTConstraintManager() = default;
42
43 //===------------------------------------------------------------------===//
44 // Implementation for interface from SimpleConstraintManager.
45 //===------------------------------------------------------------------===//
46
48 bool Assumption) override {
50
51 QualType RetTy;
52 bool hasComparison;
53
54 llvm::SMTExprRef Exp =
55 SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison);
56
57 // Create zero comparison for implicit boolean cast, with reversed
58 // assumption
59 if (!hasComparison && !RetTy->isBooleanType())
60 return assumeExpr(
61 State, Sym,
62 SMTConv::getZeroExpr(Solver, Ctx, Exp, RetTy, !Assumption));
63
64 return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp));
65 }
66
68 const llvm::APSInt &From,
69 const llvm::APSInt &To,
70 bool InRange) override {
72 return assumeExpr(
73 State, Sym, SMTConv::getRangeExpr(Solver, Ctx, Sym, From, To, InRange));
74 }
75
77 bool Assumption) override {
78 // Skip anything that is unsupported
79 return State;
80 }
81
82 //===------------------------------------------------------------------===//
83 // Implementation for interface from ConstraintManager.
84 //===------------------------------------------------------------------===//
85
88
89 QualType RetTy;
90 // The expression may be casted, so we cannot call getZ3DataExpr() directly
91 llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy);
92 llvm::SMTExprRef Exp =
93 SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true);
94
95 // Negate the constraint
96 llvm::SMTExprRef NotExp =
97 SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false);
98
99 ConditionTruthVal isSat = checkModel(State, Sym, Exp);
100 ConditionTruthVal isNotSat = checkModel(State, Sym, NotExp);
101
102 // Zero is the only possible solution
103 if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse())
104 return true;
105
106 // Zero is not a solution
107 if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue())
108 return false;
109
110 // Zero may be a solution
111 return ConditionTruthVal();
112 }
113
114 const llvm::APSInt *getSymVal(ProgramStateRef State,
115 SymbolRef Sym) const override {
117 ASTContext &Ctx = BVF.getContext();
118
119 if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
120 QualType Ty = Sym->getType();
121 assert(!Ty->isRealFloatingType());
122 llvm::APSInt Value(Ctx.getTypeSize(Ty),
124
125 // TODO: this should call checkModel so we can use the cache, however,
126 // this method tries to get the interpretation (the actual value) from
127 // the solver, which is currently not cached.
128
129 llvm::SMTExprRef Exp = SMTConv::fromData(Solver, Ctx, SD);
130
131 Solver->reset();
132 addStateConstraints(State);
133
134 // Constraints are unsatisfiable
135 std::optional<bool> isSat = Solver->check();
136 if (!isSat || !*isSat)
137 return nullptr;
138
139 // Model does not assign interpretation
140 if (!Solver->getInterpretation(Exp, Value))
141 return nullptr;
142
143 // A value has been obtained, check if it is the only value
144 llvm::SMTExprRef NotExp = SMTConv::fromBinOp(
145 Solver, Exp, BO_NE,
146 Ty->isBooleanType() ? Solver->mkBoolean(Value.getBoolValue())
147 : Solver->mkBitvector(Value, Value.getBitWidth()),
148 /*isSigned=*/false);
149
150 Solver->addConstraint(NotExp);
151
152 std::optional<bool> isNotSat = Solver->check();
153 if (!isNotSat || *isNotSat)
154 return nullptr;
155
156 // This is the only solution, store it
157 return &BVF.getValue(Value);
158 }
159
160 if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
161 SymbolRef CastSym = SC->getOperand();
162 QualType CastTy = SC->getType();
163 // Skip the void type
164 if (CastTy->isVoidType())
165 return nullptr;
166
167 const llvm::APSInt *Value;
168 if (!(Value = getSymVal(State, CastSym)))
169 return nullptr;
170 return &BVF.Convert(SC->getType(), *Value);
171 }
172
173 if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
174 const llvm::APSInt *LHS, *RHS;
175 if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
176 LHS = getSymVal(State, SIE->getLHS());
177 RHS = &SIE->getRHS();
178 } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
179 LHS = &ISE->getLHS();
180 RHS = getSymVal(State, ISE->getRHS());
181 } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
182 // Early termination to avoid expensive call
183 LHS = getSymVal(State, SSM->getLHS());
184 RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;
185 } else {
186 llvm_unreachable("Unsupported binary expression to get symbol value!");
187 }
188
189 if (!LHS || !RHS)
190 return nullptr;
191
192 llvm::APSInt ConvertedLHS, ConvertedRHS;
193 QualType LTy, RTy;
194 std::tie(ConvertedLHS, LTy) = SMTConv::fixAPSInt(Ctx, *LHS);
195 std::tie(ConvertedRHS, RTy) = SMTConv::fixAPSInt(Ctx, *RHS);
196 SMTConv::doIntTypeConversion<llvm::APSInt, &SMTConv::castAPSInt>(
197 Solver, Ctx, ConvertedLHS, LTy, ConvertedRHS, RTy);
198 return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
199 }
200
201 llvm_unreachable("Unsupported expression to get symbol value!");
202 }
203
205 SymbolReaper &SymReaper) override {
206 auto CZ = State->get<ConstraintSMT>();
207 auto &CZFactory = State->get_context<ConstraintSMT>();
208
209 for (const auto &Entry : CZ) {
210 if (SymReaper.isDead(Entry.first))
211 CZ = CZFactory.remove(CZ, Entry);
212 }
213
214 return State->set<ConstraintSMT>(CZ);
215 }
216
217 void printJson(raw_ostream &Out, ProgramStateRef State, const char *NL = "\n",
218 unsigned int Space = 0, bool IsDot = false) const override {
219 ConstraintSMTType Constraints = State->get<ConstraintSMT>();
220
221 Indent(Out, Space, IsDot) << "\"constraints\": ";
222 if (Constraints.isEmpty()) {
223 Out << "null," << NL;
224 return;
225 }
226
227 ++Space;
228 Out << '[' << NL;
229 for (ConstraintSMTType::iterator I = Constraints.begin();
230 I != Constraints.end(); ++I) {
231 Indent(Out, Space, IsDot)
232 << "{ \"symbol\": \"" << I->first << "\", \"range\": \"";
233 I->second->print(Out);
234 Out << "\" }";
235
236 if (std::next(I) != Constraints.end())
237 Out << ',';
238 Out << NL;
239 }
240
241 --Space;
242 Indent(Out, Space, IsDot) << "],";
243 }
244
246 ProgramStateRef S2) const override {
247 return S1->get<ConstraintSMT>() == S2->get<ConstraintSMT>();
248 }
249
250 bool canReasonAbout(SVal X) const override {
252
253 std::optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
254 if (!SymVal)
255 return true;
256
257 const SymExpr *Sym = SymVal->getSymbol();
258 QualType Ty = Sym->getType();
259
260 // Complex types are not modeled
261 if (Ty->isComplexType() || Ty->isComplexIntegerType())
262 return false;
263
264 // Non-IEEE 754 floating-point types are not modeled
265 if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) &&
266 (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() ||
267 &TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble())))
268 return false;
269
270 if (Ty->isRealFloatingType())
271 return Solver->isFPSupported();
272
273 if (isa<SymbolData>(Sym))
274 return true;
275
277
278 if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
279 return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
280
281 if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
282 if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE))
283 return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS()));
284
285 if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE))
286 return canReasonAbout(SVB.makeSymbolVal(ISE->getRHS()));
287
288 if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(BSE))
289 return canReasonAbout(SVB.makeSymbolVal(SSE->getLHS())) &&
290 canReasonAbout(SVB.makeSymbolVal(SSE->getRHS()));
291 }
292
293 llvm_unreachable("Unsupported expression to reason about!");
294 }
295
296 /// Dumps SMT formula
297 LLVM_DUMP_METHOD void dump() const { Solver->dump(); }
298
299protected:
300 // Check whether a new model is satisfiable, and update the program state.
302 const llvm::SMTExprRef &Exp) {
303 // Check the model, avoid simplifying AST to save time
304 if (checkModel(State, Sym, Exp).isConstrainedTrue())
305 return State->add<ConstraintSMT>(std::make_pair(Sym, Exp));
306
307 return nullptr;
308 }
309
310 /// Given a program state, construct the logical conjunction and add it to
311 /// the solver
312 virtual void addStateConstraints(ProgramStateRef State) const {
313 // TODO: Don't add all the constraints, only the relevant ones
314 auto CZ = State->get<ConstraintSMT>();
315 auto I = CZ.begin(), IE = CZ.end();
316
317 // Construct the logical AND of all the constraints
318 if (I != IE) {
319 std::vector<llvm::SMTExprRef> ASTs;
320
321 llvm::SMTExprRef Constraint = I++->second;
322 while (I != IE) {
323 Constraint = Solver->mkAnd(Constraint, I++->second);
324 }
325
326 Solver->addConstraint(Constraint);
327 }
328 }
329
330 // Generate and check a Z3 model, using the given constraint.
332 const llvm::SMTExprRef &Exp) const {
333 ProgramStateRef NewState =
334 State->add<ConstraintSMT>(std::make_pair(Sym, Exp));
335
336 llvm::FoldingSetNodeID ID;
337 NewState->get<ConstraintSMT>().Profile(ID);
338
339 unsigned hash = ID.ComputeHash();
340 auto I = Cached.find(hash);
341 if (I != Cached.end())
342 return I->second;
343
344 Solver->reset();
345 addStateConstraints(NewState);
346
347 std::optional<bool> res = Solver->check();
348 if (!res)
349 Cached[hash] = ConditionTruthVal();
350 else
351 Cached[hash] = ConditionTruthVal(*res);
352
353 return Cached[hash];
354 }
355
356 // Cache the result of an SMT query (true, false, unknown). The key is the
357 // hash of the constraints in a state
358 mutable llvm::DenseMap<unsigned, ConditionTruthVal> Cached;
359}; // end class SMTConstraintManager
360
361} // namespace ento
362} // namespace clang
363
364#endif
static char ID
Definition: Arena.cpp:183
#define X(type, name)
Definition: Value.h:143
#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 ...
Definition: ASTContext.h:187
uint64_t getTypeSize(QualType T) const
Return the size of the specified (complete) type T, in bits.
Definition: ASTContext.h:2394
const TargetInfo & getTargetInfo() const
Definition: ASTContext.h:779
A (possibly-)qualified type.
Definition: Type.h:941
Exposes information about the current target.
Definition: TargetInfo.h:218
const llvm::fltSemantics & getLongDoubleFormat() const
Definition: TargetInfo.h:785
bool isVoidType() const
Definition: Type.h:8324
bool isBooleanType() const
Definition: Type.h:8452
bool isSignedIntegerOrEnumerationType() const
Determines whether this is an integer type that is signed or an enumeration types whose underlying ty...
Definition: Type.cpp:2167
bool isComplexType() const
isComplexType() does not include complex integers (a GCC extension).
Definition: Type.cpp:677
bool isSpecificBuiltinType(unsigned K) const
Test for a particular builtin type.
Definition: Type.h:8293
bool isComplexIntegerType() const
Definition: Type.cpp:683
bool isRealFloatingType() const
Floating point categories.
Definition: Type.cpp:2266
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)
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)
Definition: SMTConv.h:501
static llvm::SMTExprRef getRangeExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange)
Definition: SMTConv.h:532
static llvm::SMTExprRef getExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, QualType *RetTy=nullptr, bool *hasComparison=nullptr)
Definition: SMTConv.h:489
static llvm::SMTExprRef fromData(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const SymbolData *Sym)
Construct an SMTSolverRef from a SymbolData.
Definition: SMTConv.h:323
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.
Definition: SMTConv.h:90
static std::pair< llvm::APSInt, QualType > fixAPSInt(ASTContext &Ctx, const llvm::APSInt &Int)
Definition: SMTConv.h:578
DefinedSVal makeSymbolVal(SymbolRef Sym)
Make an SVal that represents the given symbol.
Definition: SValBuilder.h:400
SVal - This represents a symbolic expression, which can be either an L-value or an R-value.
Definition: SVals.h:55
BasicValueFactory & getBasicVals() const
Symbolic value.
Definition: SymExpr.h:30
virtual QualType getType() const =0
Represents a cast expression.
A symbol representing data which can be stored in a memory location (region).
Definition: SymExpr.h:119
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.
Definition: SVals.h:276
Defines the clang::TargetInfo interface.
The JSON file list parser is used to communicate input to InstallAPI.