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

1	//===- ConstraintManager.h - Constraints on symbolic values. ----- 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 defined the interface to manage constraints on symbolic values.
10	//
11	//===----------------------------------------------------------------------===//
12
13	#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H
14	#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H
15
16	#include "clang/Basic/LLVM.h"
17	#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h"
18	#include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
19	#include "clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h"
20	#include "llvm/ADT/Optional.h"
21	#include "llvm/Support/SaveAndRestore.h"
22	#include <memory>
23	#include <utility>
24
25	namespace llvm {
26
27	class APSInt;
28
29	} // namespace llvm
30
31	namespace clang {
32	namespace ento {
33
34	class ProgramStateManager;
35	class SubEngine;
36	class SymbolReaper;
37
38	class ConditionTruthVal {
39	Optional<bool> Val;
40
41	public:
42	/// Construct a ConditionTruthVal indicating the constraint is constrained
43	/// to either true or false, depending on the boolean value provided.
44	ConditionTruthVal(bool constraint) : Val(constraint) {}
45
46	/// Construct a ConstraintVal indicating the constraint is underconstrained.
47	ConditionTruthVal() = default;
48
49	/// \return Stored value, assuming that the value is known.
50	/// Crashes otherwise.
51	bool getValue() const {
52	return *Val;
53	}
54
55	/// Return true if the constraint is perfectly constrained to 'true'.
56	bool isConstrainedTrue() const {
57	return Val.hasValue() && Val.getValue();
58	}
59
60	/// Return true if the constraint is perfectly constrained to 'false'.
61	bool isConstrainedFalse() const {
62	return Val.hasValue() && !Val.getValue();
63	}
64
65	/// Return true if the constrained is perfectly constrained.
66	bool isConstrained() const {
67	return Val.hasValue();
68	}
69
70	/// Return true if the constrained is underconstrained and we do not know
71	/// if the constraint is true of value.
72	bool isUnderconstrained() const {
73	return !Val.hasValue();
74	}
75	};
76
77	class ConstraintManager {
78	public:
79	ConstraintManager() = default;
80	virtual ~ConstraintManager();
81
82	virtual bool haveEqualConstraints(ProgramStateRef S1,
83	ProgramStateRef S2) const = 0;
84
85	virtual ProgramStateRef assume(ProgramStateRef state,
86	DefinedSVal Cond,
87	bool Assumption) = 0;
88
89	using ProgramStatePair = std::pair<ProgramStateRef, ProgramStateRef>;
90
91	/// Returns a pair of states (StTrue, StFalse) where the given condition is
92	/// assumed to be true or false, respectively.
93	ProgramStatePair assumeDual(ProgramStateRef State, DefinedSVal Cond) {
94	ProgramStateRef StTrue = assume(State, Cond, true);
95
96	// If StTrue is infeasible, asserting the falseness of Cond is unnecessary
97	// because the existing constraints already establish this.
98	if (!StTrue) {
99	#ifndef __OPTIMIZE__
100	// This check is expensive and should be disabled even in Release+Asserts
101	// builds.
102	// FIXME: __OPTIMIZE__ is a GNU extension that Clang implements but MSVC
103	// does not. Is there a good equivalent there?
104	(0) . __assert_fail ("assume(State, Cond, false) && \"System is over constrained.\"", "/home/seafit/code_projects/clang_source/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h", 104, __PRETTY_FUNCTION__))" file_link="../../../../../../include/assert.h.html#88" macro="true">assert(assume(State, Cond, false) && "System is over constrained.");
105	#endif
106	return ProgramStatePair((ProgramStateRef)nullptr, State);
107	}
108
109	ProgramStateRef StFalse = assume(State, Cond, false);
110	if (!StFalse) {
111	// We are careful to return the original state, /not/ StTrue,
112	// because we want to avoid having callers generate a new node
113	// in the ExplodedGraph.
114	return ProgramStatePair(State, (ProgramStateRef)nullptr);
115	}
116
117	return ProgramStatePair(StTrue, StFalse);
118	}
119
120	virtual ProgramStateRef assumeInclusiveRange(ProgramStateRef State,
121	NonLoc Value,
122	const llvm::APSInt &From,
123	const llvm::APSInt &To,
124	bool InBound) = 0;
125
126	virtual ProgramStatePair assumeInclusiveRangeDual(ProgramStateRef State,
127	NonLoc Value,
128	const llvm::APSInt &From,
129	const llvm::APSInt &To) {
130	ProgramStateRef StInRange =
131	assumeInclusiveRange(State, Value, From, To, true);
132
133	// If StTrue is infeasible, asserting the falseness of Cond is unnecessary
134	// because the existing constraints already establish this.
135	if (!StInRange)
136	return ProgramStatePair((ProgramStateRef)nullptr, State);
137
138	ProgramStateRef StOutOfRange =
139	assumeInclusiveRange(State, Value, From, To, false);
140	if (!StOutOfRange) {
141	// We are careful to return the original state, /not/ StTrue,
142	// because we want to avoid having callers generate a new node
143	// in the ExplodedGraph.
144	return ProgramStatePair(State, (ProgramStateRef)nullptr);
145	}
146
147	return ProgramStatePair(StInRange, StOutOfRange);
148	}
149
150	/// If a symbol is perfectly constrained to a constant, attempt
151	/// to return the concrete value.
152	///
153	/// Note that a ConstraintManager is not obligated to return a concretized
154	/// value for a symbol, even if it is perfectly constrained.
155	virtual const llvm::APSInt* getSymVal(ProgramStateRef state,
156	SymbolRef sym) const {
157	return nullptr;
158	}
159
160	/// Scan all symbols referenced by the constraints. If the symbol is not
161	/// alive, remove it.
162	virtual ProgramStateRef removeDeadBindings(ProgramStateRef state,
163	SymbolReaper& SymReaper) = 0;
164
165	virtual void print(ProgramStateRef state,
166	raw_ostream &Out,
167	const char* nl,
168	const char *sep) = 0;
169
170	virtual void EndPath(ProgramStateRef state) {}
171
172	/// Convenience method to query the state to see if a symbol is null or
173	/// not null, or if neither assumption can be made.
174	ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) {
175	SaveAndRestore<bool> DisableNotify(NotifyAssumeClients, false);
176
177	return checkNull(State, Sym);
178	}
179
180	protected:
181	/// A flag to indicate that clients should be notified of assumptions.
182	/// By default this is the case, but sometimes this needs to be restricted
183	/// to avoid infinite recursions within the ConstraintManager.
184	///
185	/// Note that this flag allows the ConstraintManager to be re-entrant,
186	/// but not thread-safe.
187	bool NotifyAssumeClients = true;
188
189	/// canReasonAbout - Not all ConstraintManagers can accurately reason about
190	/// all SVal values. This method returns true if the ConstraintManager can
191	/// reasonably handle a given SVal value. This is typically queried by
192	/// ExprEngine to determine if the value should be replaced with a
193	/// conjured symbolic value in order to recover some precision.
194	virtual bool canReasonAbout(SVal X) const = 0;
195
196	/// Returns whether or not a symbol is known to be null ("true"), known to be
197	/// non-null ("false"), or may be either ("underconstrained").
198	virtual ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym);
199	};
200
201	std::unique_ptr<ConstraintManager>
202	CreateRangeConstraintManager(ProgramStateManager &statemgr,
203	SubEngine *subengine);
204
205	std::unique_ptr<ConstraintManager>
206	CreateZ3ConstraintManager(ProgramStateManager &statemgr, SubEngine *subengine);
207
208	} // namespace ento
209	} // namespace clang
210
211	#endif // LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H
212