/Users/buildslave/jenkins/workspace/coverage/llvm-project/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
Line | Count | Source (jump to first uncovered line) |
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 ExprEngine; |
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 | 58.0k | ConditionTruthVal(bool constraint) : Val(constraint) {} |
45 | | |
46 | | /// Construct a ConstraintVal indicating the constraint is underconstrained. |
47 | 41.9k | ConditionTruthVal() = default; |
48 | | |
49 | | /// \return Stored value, assuming that the value is known. |
50 | | /// Crashes otherwise. |
51 | 15.1k | bool getValue() const { |
52 | 15.1k | return *Val; |
53 | 15.1k | } |
54 | | |
55 | | /// Return true if the constraint is perfectly constrained to 'true'. |
56 | 77.1k | bool isConstrainedTrue() const { |
57 | 77.1k | return Val.hasValue() && Val.getValue()36.2k ; |
58 | 77.1k | } |
59 | | |
60 | | /// Return true if the constraint is perfectly constrained to 'false'. |
61 | 1.80k | bool isConstrainedFalse() const { |
62 | 1.80k | return Val.hasValue() && !Val.getValue()911 ; |
63 | 1.80k | } |
64 | | |
65 | | /// Return true if the constrained is perfectly constrained. |
66 | 24 | bool isConstrained() const { |
67 | 24 | return Val.hasValue(); |
68 | 24 | } |
69 | | |
70 | | /// Return true if the constrained is underconstrained and we do not know |
71 | | /// if the constraint is true of value. |
72 | 28.7k | bool isUnderconstrained() const { |
73 | 28.7k | return !Val.hasValue(); |
74 | 28.7k | } |
75 | | }; |
76 | | |
77 | | class ConstraintManager { |
78 | | public: |
79 | 13.7k | 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 | 362k | ProgramStatePair assumeDual(ProgramStateRef State, DefinedSVal Cond) { |
94 | 362k | 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 | 362k | if (!StTrue) { |
99 | | #ifdef EXPENSIVE_CHECKS |
100 | | assert(assume(State, Cond, false) && "System is over constrained."); |
101 | | #endif |
102 | 17.0k | return ProgramStatePair((ProgramStateRef)nullptr, State); |
103 | 17.0k | } |
104 | | |
105 | 345k | ProgramStateRef StFalse = assume(State, Cond, false); |
106 | 345k | if (!StFalse) { |
107 | | // We are careful to return the original state, /not/ StTrue, |
108 | | // because we want to avoid having callers generate a new node |
109 | | // in the ExplodedGraph. |
110 | 305k | return ProgramStatePair(State, (ProgramStateRef)nullptr); |
111 | 305k | } |
112 | | |
113 | 39.8k | return ProgramStatePair(StTrue, StFalse); |
114 | 39.8k | } |
115 | | |
116 | | virtual ProgramStateRef assumeInclusiveRange(ProgramStateRef State, |
117 | | NonLoc Value, |
118 | | const llvm::APSInt &From, |
119 | | const llvm::APSInt &To, |
120 | | bool InBound) = 0; |
121 | | |
122 | | virtual ProgramStatePair assumeInclusiveRangeDual(ProgramStateRef State, |
123 | | NonLoc Value, |
124 | | const llvm::APSInt &From, |
125 | 617 | const llvm::APSInt &To) { |
126 | 617 | ProgramStateRef StInRange = |
127 | 617 | assumeInclusiveRange(State, Value, From, To, true); |
128 | | |
129 | | // If StTrue is infeasible, asserting the falseness of Cond is unnecessary |
130 | | // because the existing constraints already establish this. |
131 | 617 | if (!StInRange) |
132 | 165 | return ProgramStatePair((ProgramStateRef)nullptr, State); |
133 | | |
134 | 452 | ProgramStateRef StOutOfRange = |
135 | 452 | assumeInclusiveRange(State, Value, From, To, false); |
136 | 452 | if (!StOutOfRange) { |
137 | | // We are careful to return the original state, /not/ StTrue, |
138 | | // because we want to avoid having callers generate a new node |
139 | | // in the ExplodedGraph. |
140 | 120 | return ProgramStatePair(State, (ProgramStateRef)nullptr); |
141 | 120 | } |
142 | | |
143 | 332 | return ProgramStatePair(StInRange, StOutOfRange); |
144 | 332 | } |
145 | | |
146 | | /// If a symbol is perfectly constrained to a constant, attempt |
147 | | /// to return the concrete value. |
148 | | /// |
149 | | /// Note that a ConstraintManager is not obligated to return a concretized |
150 | | /// value for a symbol, even if it is perfectly constrained. |
151 | | virtual const llvm::APSInt* getSymVal(ProgramStateRef state, |
152 | 0 | SymbolRef sym) const { |
153 | 0 | return nullptr; |
154 | 0 | } |
155 | | |
156 | | /// Scan all symbols referenced by the constraints. If the symbol is not |
157 | | /// alive, remove it. |
158 | | virtual ProgramStateRef removeDeadBindings(ProgramStateRef state, |
159 | | SymbolReaper& SymReaper) = 0; |
160 | | |
161 | | virtual void printJson(raw_ostream &Out, ProgramStateRef State, |
162 | | const char *NL, unsigned int Space, |
163 | | bool IsDot) const = 0; |
164 | | |
165 | | /// Convenience method to query the state to see if a symbol is null or |
166 | | /// not null, or if neither assumption can be made. |
167 | 57.3k | ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) { |
168 | 57.3k | SaveAndRestore<bool> DisableNotify(NotifyAssumeClients, false); |
169 | | |
170 | 57.3k | return checkNull(State, Sym); |
171 | 57.3k | } |
172 | | |
173 | | protected: |
174 | | /// A flag to indicate that clients should be notified of assumptions. |
175 | | /// By default this is the case, but sometimes this needs to be restricted |
176 | | /// to avoid infinite recursions within the ConstraintManager. |
177 | | /// |
178 | | /// Note that this flag allows the ConstraintManager to be re-entrant, |
179 | | /// but not thread-safe. |
180 | | bool NotifyAssumeClients = true; |
181 | | |
182 | | /// canReasonAbout - Not all ConstraintManagers can accurately reason about |
183 | | /// all SVal values. This method returns true if the ConstraintManager can |
184 | | /// reasonably handle a given SVal value. This is typically queried by |
185 | | /// ExprEngine to determine if the value should be replaced with a |
186 | | /// conjured symbolic value in order to recover some precision. |
187 | | virtual bool canReasonAbout(SVal X) const = 0; |
188 | | |
189 | | /// Returns whether or not a symbol is known to be null ("true"), known to be |
190 | | /// non-null ("false"), or may be either ("underconstrained"). |
191 | | virtual ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym); |
192 | | }; |
193 | | |
194 | | std::unique_ptr<ConstraintManager> |
195 | | CreateRangeConstraintManager(ProgramStateManager &statemgr, |
196 | | ExprEngine *exprengine); |
197 | | |
198 | | std::unique_ptr<ConstraintManager> |
199 | | CreateZ3ConstraintManager(ProgramStateManager &statemgr, |
200 | | ExprEngine *exprengine); |
201 | | |
202 | | } // namespace ento |
203 | | } // namespace clang |
204 | | |
205 | | #endif // LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H |