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