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/Support/SaveAndRestore.h" |
21 | #include <memory> |
22 | #include <optional> |
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 ExprEngine; |
36 | class SymbolReaper; |
37 | |
38 | class ConditionTruthVal { |
39 | std::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 { return Val && *Val; } |
57 | |
58 | /// Return true if the constraint is perfectly constrained to 'false'. |
59 | bool isConstrainedFalse() const { return Val && !*Val; } |
60 | |
61 | /// Return true if the constrained is perfectly constrained. |
62 | bool isConstrained() const { return Val.has_value(); } |
63 | |
64 | /// Return true if the constrained is underconstrained and we do not know |
65 | /// if the constraint is true of value. |
66 | bool isUnderconstrained() const { return !Val.has_value(); } |
67 | }; |
68 | |
69 | class ConstraintManager { |
70 | public: |
71 | ConstraintManager() = default; |
72 | virtual ~ConstraintManager(); |
73 | |
74 | virtual bool haveEqualConstraints(ProgramStateRef S1, |
75 | ProgramStateRef S2) const = 0; |
76 | |
77 | ProgramStateRef assume(ProgramStateRef state, DefinedSVal Cond, |
78 | bool Assumption); |
79 | |
80 | using ProgramStatePair = std::pair<ProgramStateRef, ProgramStateRef>; |
81 | |
82 | /// Returns a pair of states (StTrue, StFalse) where the given condition is |
83 | /// assumed to be true or false, respectively. |
84 | /// (Note that these two states might be equal if the parent state turns out |
85 | /// to be infeasible. This may happen if the underlying constraint solver is |
86 | /// not perfectly precise and this may happen very rarely.) |
87 | ProgramStatePair assumeDual(ProgramStateRef State, DefinedSVal Cond); |
88 | |
89 | ProgramStateRef assumeInclusiveRange(ProgramStateRef State, NonLoc Value, |
90 | const llvm::APSInt &From, |
91 | const llvm::APSInt &To, bool InBound); |
92 | |
93 | /// Returns a pair of states (StInRange, StOutOfRange) where the given value |
94 | /// is assumed to be in the range or out of the range, respectively. |
95 | /// (Note that these two states might be equal if the parent state turns out |
96 | /// to be infeasible. This may happen if the underlying constraint solver is |
97 | /// not perfectly precise and this may happen very rarely.) |
98 | ProgramStatePair assumeInclusiveRangeDual(ProgramStateRef State, NonLoc Value, |
99 | const llvm::APSInt &From, |
100 | const llvm::APSInt &To); |
101 | |
102 | /// If a symbol is perfectly constrained to a constant, attempt |
103 | /// to return the concrete value. |
104 | /// |
105 | /// Note that a ConstraintManager is not obligated to return a concretized |
106 | /// value for a symbol, even if it is perfectly constrained. |
107 | /// It might return null. |
108 | virtual const llvm::APSInt* getSymVal(ProgramStateRef state, |
109 | SymbolRef sym) const { |
110 | return nullptr; |
111 | } |
112 | |
113 | /// Attempt to return the minimal possible value for a given symbol. Note |
114 | /// that a ConstraintManager is not obligated to return a lower bound, it may |
115 | /// also return nullptr. |
116 | virtual const llvm::APSInt *getSymMinVal(ProgramStateRef state, |
117 | SymbolRef sym) const { |
118 | return nullptr; |
119 | } |
120 | |
121 | /// Attempt to return the minimal possible value for a given symbol. Note |
122 | /// that a ConstraintManager is not obligated to return a lower bound, it may |
123 | /// also return nullptr. |
124 | virtual const llvm::APSInt *getSymMaxVal(ProgramStateRef state, |
125 | SymbolRef sym) const { |
126 | return nullptr; |
127 | } |
128 | |
129 | /// Scan all symbols referenced by the constraints. If the symbol is not |
130 | /// alive, remove it. |
131 | virtual ProgramStateRef removeDeadBindings(ProgramStateRef state, |
132 | SymbolReaper& SymReaper) = 0; |
133 | |
134 | virtual void printJson(raw_ostream &Out, ProgramStateRef State, |
135 | const char *NL, unsigned int Space, |
136 | bool IsDot) const = 0; |
137 | |
138 | virtual void printValue(raw_ostream &Out, ProgramStateRef State, |
139 | SymbolRef Sym) {} |
140 | |
141 | /// Convenience method to query the state to see if a symbol is null or |
142 | /// not null, or if neither assumption can be made. |
143 | ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) { |
144 | return checkNull(State, Sym); |
145 | } |
146 | |
147 | protected: |
148 | /// A helper class to simulate the call stack of nested assume calls. |
149 | class AssumeStackTy { |
150 | public: |
151 | void push(const ProgramState *S) { Aux.push_back(Elt: S); } |
152 | void pop() { Aux.pop_back(); } |
153 | bool contains(const ProgramState *S) const { |
154 | return llvm::is_contained(Range: Aux, Element: S); |
155 | } |
156 | |
157 | private: |
158 | llvm::SmallVector<const ProgramState *, 4> Aux; |
159 | }; |
160 | AssumeStackTy AssumeStack; |
161 | |
162 | virtual ProgramStateRef assumeInternal(ProgramStateRef state, |
163 | DefinedSVal Cond, bool Assumption) = 0; |
164 | |
165 | virtual ProgramStateRef assumeInclusiveRangeInternal(ProgramStateRef State, |
166 | NonLoc Value, |
167 | const llvm::APSInt &From, |
168 | const llvm::APSInt &To, |
169 | bool InBound) = 0; |
170 | |
171 | /// canReasonAbout - Not all ConstraintManagers can accurately reason about |
172 | /// all SVal values. This method returns true if the ConstraintManager can |
173 | /// reasonably handle a given SVal value. This is typically queried by |
174 | /// ExprEngine to determine if the value should be replaced with a |
175 | /// conjured symbolic value in order to recover some precision. |
176 | virtual bool canReasonAbout(SVal X) const = 0; |
177 | |
178 | /// Returns whether or not a symbol is known to be null ("true"), known to be |
179 | /// non-null ("false"), or may be either ("underconstrained"). |
180 | virtual ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym); |
181 | |
182 | template <typename AssumeFunction> |
183 | ProgramStatePair assumeDualImpl(ProgramStateRef &State, |
184 | AssumeFunction &Assume); |
185 | }; |
186 | |
187 | std::unique_ptr<ConstraintManager> |
188 | CreateRangeConstraintManager(ProgramStateManager &statemgr, |
189 | ExprEngine *exprengine); |
190 | |
191 | std::unique_ptr<ConstraintManager> |
192 | CreateZ3ConstraintManager(ProgramStateManager &statemgr, |
193 | ExprEngine *exprengine); |
194 | |
195 | } // namespace ento |
196 | } // namespace clang |
197 | |
198 | #endif // LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H |
199 | |