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
17#include "clang/Basic/JsonSupport.h"
18#include "clang/Basic/TargetInfo.h"
19#include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
20#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
21#include <optional>
22
23typedef llvm::ImmutableSet<
24 std::pair<clang::ento::SymbolRef, const llvm::SMTExpr *>>
25 ConstraintSMTType;
26REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintSMT, ConstraintSMTType)
27
28namespace clang {
29namespace ento {
30
31class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
32 mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver();
33
34public:
35 SMTConstraintManager(clang::ento::ExprEngine *EE,
36 clang::ento::SValBuilder &SB)
37 : SimpleConstraintManager(EE, SB) {}
38 virtual ~SMTConstraintManager() = default;
39
40 //===------------------------------------------------------------------===//
41 // Implementation for interface from SimpleConstraintManager.
42 //===------------------------------------------------------------------===//
43
44 ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym,
45 bool Assumption) override {
46 ASTContext &Ctx = getBasicVals().getContext();
47
48 QualType RetTy;
49 bool hasComparison;
50
51 llvm::SMTExprRef Exp =
52 SMTConv::getExpr(Solver, Ctx, Sym, RetTy: &RetTy, hasComparison: &hasComparison);
53
54 // Create zero comparison for implicit boolean cast, with reversed
55 // assumption
56 if (!hasComparison && !RetTy->isBooleanType())
57 return assumeExpr(
58 State, Sym,
59 Exp: SMTConv::getZeroExpr(Solver, Ctx, Exp, Ty: RetTy, Assumption: !Assumption));
60
61 return assumeExpr(State, Sym, Exp: Assumption ? Exp : Solver->mkNot(Exp));
62 }
63
64 ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
65 const llvm::APSInt &From,
66 const llvm::APSInt &To,
67 bool InRange) override {
68 ASTContext &Ctx = getBasicVals().getContext();
69 return assumeExpr(
70 State, Sym, Exp: SMTConv::getRangeExpr(Solver, Ctx, Sym, From, To, InRange));
71 }
72
73 ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
74 bool Assumption) override {
75 // Skip anything that is unsupported
76 return State;
77 }
78
79 //===------------------------------------------------------------------===//
80 // Implementation for interface from ConstraintManager.
81 //===------------------------------------------------------------------===//
82
83 ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override {
84 ASTContext &Ctx = getBasicVals().getContext();
85
86 QualType RetTy;
87 // The expression may be casted, so we cannot call getZ3DataExpr() directly
88 llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, RetTy: &RetTy);
89 llvm::SMTExprRef Exp =
90 SMTConv::getZeroExpr(Solver, Ctx, Exp: VarExp, Ty: RetTy, /*Assumption=*/Assumption: true);
91
92 // Negate the constraint
93 llvm::SMTExprRef NotExp =
94 SMTConv::getZeroExpr(Solver, Ctx, Exp: VarExp, Ty: RetTy, /*Assumption=*/Assumption: false);
95
96 ConditionTruthVal isSat = checkModel(State, Sym, Exp);
97 ConditionTruthVal isNotSat = checkModel(State, Sym, Exp: NotExp);
98
99 // Zero is the only possible solution
100 if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse())
101 return true;
102
103 // Zero is not a solution
104 if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue())
105 return false;
106
107 // Zero may be a solution
108 return ConditionTruthVal();
109 }
110
111 const llvm::APSInt *getSymVal(ProgramStateRef State,
112 SymbolRef Sym) const override {
113 BasicValueFactory &BVF = getBasicVals();
114 ASTContext &Ctx = BVF.getContext();
115
116 if (const SymbolData *SD = dyn_cast<SymbolData>(Val: Sym)) {
117 QualType Ty = Sym->getType();
118 assert(!Ty->isRealFloatingType());
119 llvm::APSInt Value(Ctx.getTypeSize(T: Ty),
120 !Ty->isSignedIntegerOrEnumerationType());
121
122 // TODO: this should call checkModel so we can use the cache, however,
123 // this method tries to get the interpretation (the actual value) from
124 // the solver, which is currently not cached.
125
126 llvm::SMTExprRef Exp = SMTConv::fromData(Solver, Ctx, Sym: SD);
127
128 Solver->reset();
129 addStateConstraints(State);
130
131 // Constraints are unsatisfiable
132 std::optional<bool> isSat = Solver->check();
133 if (!isSat || !*isSat)
134 return nullptr;
135
136 // Model does not assign interpretation
137 if (!Solver->getInterpretation(Exp, Int&: Value))
138 return nullptr;
139
140 // A value has been obtained, check if it is the only value
141 llvm::SMTExprRef NotExp = SMTConv::fromBinOp(
142 Solver, LHS: Exp, Op: BO_NE,
143 RHS: Ty->isBooleanType() ? Solver->mkBoolean(b: Value.getBoolValue())
144 : Solver->mkBitvector(Int: Value, BitWidth: Value.getBitWidth()),
145 /*isSigned=*/isSigned: false);
146
147 Solver->addConstraint(Exp: NotExp);
148
149 std::optional<bool> isNotSat = Solver->check();
150 if (!isNotSat || *isNotSat)
151 return nullptr;
152
153 // This is the only solution, store it
154 return &BVF.getValue(X: Value);
155 }
156
157 if (const SymbolCast *SC = dyn_cast<SymbolCast>(Val: Sym)) {
158 SymbolRef CastSym = SC->getOperand();
159 QualType CastTy = SC->getType();
160 // Skip the void type
161 if (CastTy->isVoidType())
162 return nullptr;
163
164 const llvm::APSInt *Value;
165 if (!(Value = getSymVal(State, Sym: CastSym)))
166 return nullptr;
167 return &BVF.Convert(T: SC->getType(), From: *Value);
168 }
169
170 if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Val: Sym)) {
171 const llvm::APSInt *LHS, *RHS;
172 if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(Val: BSE)) {
173 LHS = getSymVal(State, Sym: SIE->getLHS());
174 RHS = &SIE->getRHS();
175 } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(Val: BSE)) {
176 LHS = &ISE->getLHS();
177 RHS = getSymVal(State, Sym: ISE->getRHS());
178 } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(Val: BSE)) {
179 // Early termination to avoid expensive call
180 LHS = getSymVal(State, Sym: SSM->getLHS());
181 RHS = LHS ? getSymVal(State, Sym: SSM->getRHS()) : nullptr;
182 } else {
183 llvm_unreachable("Unsupported binary expression to get symbol value!");
184 }
185
186 if (!LHS || !RHS)
187 return nullptr;
188
189 llvm::APSInt ConvertedLHS, ConvertedRHS;
190 QualType LTy, RTy;
191 std::tie(args&: ConvertedLHS, args&: LTy) = SMTConv::fixAPSInt(Ctx, *LHS);
192 std::tie(args&: ConvertedRHS, args&: RTy) = SMTConv::fixAPSInt(Ctx, Int: *RHS);
193 SMTConv::doIntTypeConversion<llvm::APSInt, &SMTConv::castAPSInt>(
194 Solver, Ctx, LHS&: ConvertedLHS, LTy, RHS&: ConvertedRHS, RTy);
195 return BVF.evalAPSInt(Op: BSE->getOpcode(), V1: ConvertedLHS, V2: ConvertedRHS);
196 }
197
198 llvm_unreachable("Unsupported expression to get symbol value!");
199 }
200
201 ProgramStateRef removeDeadBindings(ProgramStateRef State,
202 SymbolReaper &SymReaper) override {
203 auto CZ = State->get<ConstraintSMT>();
204 auto &CZFactory = State->get_context<ConstraintSMT>();
205
206 for (const auto &Entry : CZ) {
207 if (SymReaper.isDead(sym: Entry.first))
208 CZ = CZFactory.remove(Old: CZ, V: Entry);
209 }
210
211 return State->set<ConstraintSMT>(CZ);
212 }
213
214 void printJson(raw_ostream &Out, ProgramStateRef State, const char *NL = "\n",
215 unsigned int Space = 0, bool IsDot = false) const override {
216 ConstraintSMTType Constraints = State->get<ConstraintSMT>();
217
218 Indent(Out, Space, IsDot) << "\"constraints\": ";
219 if (Constraints.isEmpty()) {
220 Out << "null," << NL;
221 return;
222 }
223
224 ++Space;
225 Out << '[' << 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(OS&: Out);
231 Out << "\" }";
232
233 if (std::next(x: I) != Constraints.end())
234 Out << ',';
235 Out << NL;
236 }
237
238 --Space;
239 Indent(Out, Space, IsDot) << "],";
240 }
241
242 bool haveEqualConstraints(ProgramStateRef S1,
243 ProgramStateRef S2) const override {
244 return S1->get<ConstraintSMT>() == S2->get<ConstraintSMT>();
245 }
246
247 bool canReasonAbout(SVal X) const override {
248 const TargetInfo &TI = getBasicVals().getContext().getTargetInfo();
249
250 std::optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
251 if (!SymVal)
252 return true;
253
254 const SymExpr *Sym = SymVal->getSymbol();
255 QualType Ty = Sym->getType();
256
257 // Complex types are not modeled
258 if (Ty->isComplexType() || Ty->isComplexIntegerType())
259 return false;
260
261 // Non-IEEE 754 floating-point types are not modeled
262 if ((Ty->isSpecificBuiltinType(K: BuiltinType::LongDouble) &&
263 (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() ||
264 &TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble())))
265 return false;
266
267 if (Ty->isRealFloatingType())
268 return Solver->isFPSupported();
269
270 if (isa<SymbolData>(Val: Sym))
271 return true;
272
273 SValBuilder &SVB = getSValBuilder();
274
275 if (const SymbolCast *SC = dyn_cast<SymbolCast>(Val: Sym))
276 return canReasonAbout(X: SVB.makeSymbolVal(Sym: SC->getOperand()));
277
278 if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Val: Sym)) {
279 if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(Val: BSE))
280 return canReasonAbout(X: SVB.makeSymbolVal(Sym: SIE->getLHS()));
281
282 if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(Val: BSE))
283 return canReasonAbout(X: SVB.makeSymbolVal(Sym: ISE->getRHS()));
284
285 if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(Val: BSE))
286 return canReasonAbout(X: SVB.makeSymbolVal(Sym: SSE->getLHS())) &&
287 canReasonAbout(X: SVB.makeSymbolVal(Sym: SSE->getRHS()));
288 }
289
290 llvm_unreachable("Unsupported expression to reason about!");
291 }
292
293 /// Dumps SMT formula
294 LLVM_DUMP_METHOD void dump() const { Solver->dump(); }
295
296protected:
297 // Check whether a new model is satisfiable, and update the program state.
298 virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym,
299 const llvm::SMTExprRef &Exp) {
300 // Check the model, avoid simplifying AST to save time
301 if (checkModel(State, Sym, Exp).isConstrainedTrue())
302 return State->add<ConstraintSMT>(K: std::make_pair(x&: Sym, y: Exp));
303
304 return nullptr;
305 }
306
307 /// Given a program state, construct the logical conjunction and add it to
308 /// the solver
309 virtual void addStateConstraints(ProgramStateRef State) const {
310 // TODO: Don't add all the constraints, only the relevant ones
311 auto CZ = State->get<ConstraintSMT>();
312 auto I = CZ.begin(), IE = CZ.end();
313
314 // Construct the logical AND of all the constraints
315 if (I != IE) {
316 std::vector<llvm::SMTExprRef> ASTs;
317
318 llvm::SMTExprRef Constraint = I++->second;
319 while (I != IE) {
320 Constraint = Solver->mkAnd(LHS: Constraint, RHS: I++->second);
321 }
322
323 Solver->addConstraint(Exp: Constraint);
324 }
325 }
326
327 // Generate and check a Z3 model, using the given constraint.
328 ConditionTruthVal checkModel(ProgramStateRef State, SymbolRef Sym,
329 const llvm::SMTExprRef &Exp) const {
330 ProgramStateRef NewState =
331 State->add<ConstraintSMT>(K: std::make_pair(x&: Sym, y: Exp));
332
333 llvm::FoldingSetNodeID ID;
334 NewState->get<ConstraintSMT>().Profile(ID);
335
336 unsigned hash = ID.ComputeHash();
337 auto I = Cached.find(Val: hash);
338 if (I != Cached.end())
339 return I->second;
340
341 Solver->reset();
342 addStateConstraints(State: NewState);
343
344 std::optional<bool> res = Solver->check();
345 if (!res)
346 Cached[hash] = ConditionTruthVal();
347 else
348 Cached[hash] = ConditionTruthVal(*res);
349
350 return Cached[hash];
351 }
352
353 // Cache the result of an SMT query (true, false, unknown). The key is the
354 // hash of the constraints in a state
355 mutable llvm::DenseMap<unsigned, ConditionTruthVal> Cached;
356}; // end class SMTConstraintManager
357
358} // namespace ento
359} // namespace clang
360
361#endif
362

source code of clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h