SMTConstraintManager.h source code [clang_source_code/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h]

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

clang::ento::SMTConstraintManager::Solver

clang::ento::SMTConstraintManager::assumeSym

clang::ento::SMTConstraintManager::assumeSymInclusiveRange

clang::ento::SMTConstraintManager::assumeSymUnsupported

clang::ento::SMTConstraintManager::checkNull

clang::ento::SMTConstraintManager::getSymVal

clang::ento::SMTConstraintManager::removeDeadBindings

clang::ento::SMTConstraintManager::print

clang::ento::SMTConstraintManager::haveEqualConstraints

clang::ento::SMTConstraintManager::canReasonAbout

clang::ento::SMTConstraintManager::dump

clang::ento::SMTConstraintManager::assumeExpr

clang::ento::SMTConstraintManager::addStateConstraints

clang::ento::SMTConstraintManager::checkModel

clang::ento::SMTConstraintManager::Cached

Clang Project