/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 | 72.4k | ConditionTruthVal(bool constraint) : Val(constraint) {} |
45 | | |
46 | | /// Construct a ConstraintVal indicating the constraint is underconstrained. |
47 | 47.6k | ConditionTruthVal() = default; |
48 | | |
49 | | /// \return Stored value, assuming that the value is known. |
50 | | /// Crashes otherwise. |
51 | 18.6k | bool getValue() const { |
52 | 18.6k | return *Val; |
53 | 18.6k | } |
54 | | |
55 | | /// Return true if the constraint is perfectly constrained to 'true'. |
56 | 93.3k | bool isConstrainedTrue() const { |
57 | 93.3k | return Val.hasValue() && Val.getValue()46.7k ; |
58 | 93.3k | } |
59 | | |
60 | | /// Return true if the constraint is perfectly constrained to 'false'. |
61 | 1.81k | bool isConstrainedFalse() const { |
62 | 1.81k | return Val.hasValue() && !Val.getValue()915 ; |
63 | 1.81k | } |
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 | 33.0k | bool isUnderconstrained() const { |
73 | 33.0k | return !Val.hasValue(); |
74 | 33.0k | } |
75 | | }; |
76 | | |
77 | | class ConstraintManager { |
78 | | public: |
79 | 15.3k | ConstraintManager() = default; |
80 | | virtual ~ConstraintManager(); |
81 | | |
82 | | virtual bool haveEqualConstraints(ProgramStateRef S1, |
83 | | ProgramStateRef S2) const = 0; |
84 | | |
85 | | ProgramStateRef assume(ProgramStateRef state, DefinedSVal Cond, |
86 | | bool Assumption); |
87 | | |
88 | | using ProgramStatePair = std::pair<ProgramStateRef, ProgramStateRef>; |
89 | | |
90 | | /// Returns a pair of states (StTrue, StFalse) where the given condition is |
91 | | /// assumed to be true or false, respectively. |
92 | | /// (Note that these two states might be equal if the parent state turns out |
93 | | /// to be infeasible. This may happen if the underlying constraint solver is |
94 | | /// not perfectly precise and this may happen very rarely.) |
95 | | ProgramStatePair assumeDual(ProgramStateRef State, DefinedSVal Cond); |
96 | | |
97 | | virtual ProgramStateRef assumeInclusiveRange(ProgramStateRef State, |
98 | | NonLoc Value, |
99 | | const llvm::APSInt &From, |
100 | | const llvm::APSInt &To, |
101 | | bool InBound) = 0; |
102 | | |
103 | | virtual ProgramStatePair assumeInclusiveRangeDual(ProgramStateRef State, |
104 | | NonLoc Value, |
105 | | const llvm::APSInt &From, |
106 | 636 | const llvm::APSInt &To) { |
107 | 636 | ProgramStateRef StInRange = |
108 | 636 | assumeInclusiveRange(State, Value, From, To, true); |
109 | | |
110 | | // If StTrue is infeasible, asserting the falseness of Cond is unnecessary |
111 | | // because the existing constraints already establish this. |
112 | 636 | if (!StInRange) |
113 | 165 | return ProgramStatePair((ProgramStateRef)nullptr, State); |
114 | | |
115 | 471 | ProgramStateRef StOutOfRange = |
116 | 471 | assumeInclusiveRange(State, Value, From, To, false); |
117 | 471 | if (!StOutOfRange) { |
118 | | // We are careful to return the original state, /not/ StTrue, |
119 | | // because we want to avoid having callers generate a new node |
120 | | // in the ExplodedGraph. |
121 | 120 | return ProgramStatePair(State, (ProgramStateRef)nullptr); |
122 | 120 | } |
123 | | |
124 | 351 | return ProgramStatePair(StInRange, StOutOfRange); |
125 | 471 | } |
126 | | |
127 | | /// If a symbol is perfectly constrained to a constant, attempt |
128 | | /// to return the concrete value. |
129 | | /// |
130 | | /// Note that a ConstraintManager is not obligated to return a concretized |
131 | | /// value for a symbol, even if it is perfectly constrained. |
132 | | virtual const llvm::APSInt* getSymVal(ProgramStateRef state, |
133 | 0 | SymbolRef sym) const { |
134 | 0 | return nullptr; |
135 | 0 | } |
136 | | |
137 | | /// Scan all symbols referenced by the constraints. If the symbol is not |
138 | | /// alive, remove it. |
139 | | virtual ProgramStateRef removeDeadBindings(ProgramStateRef state, |
140 | | SymbolReaper& SymReaper) = 0; |
141 | | |
142 | | virtual void printJson(raw_ostream &Out, ProgramStateRef State, |
143 | | const char *NL, unsigned int Space, |
144 | | bool IsDot) const = 0; |
145 | | |
146 | | /// Convenience method to query the state to see if a symbol is null or |
147 | | /// not null, or if neither assumption can be made. |
148 | 66.6k | ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) { |
149 | 66.6k | SaveAndRestore<bool> DisableNotify(NotifyAssumeClients, false); |
150 | | |
151 | 66.6k | return checkNull(State, Sym); |
152 | 66.6k | } |
153 | | |
154 | | protected: |
155 | | /// A flag to indicate that clients should be notified of assumptions. |
156 | | /// By default this is the case, but sometimes this needs to be restricted |
157 | | /// to avoid infinite recursions within the ConstraintManager. |
158 | | /// |
159 | | /// Note that this flag allows the ConstraintManager to be re-entrant, |
160 | | /// but not thread-safe. |
161 | | bool NotifyAssumeClients = true; |
162 | | |
163 | | virtual ProgramStateRef assumeInternal(ProgramStateRef state, |
164 | | DefinedSVal Cond, bool Assumption) = 0; |
165 | | |
166 | | /// canReasonAbout - Not all ConstraintManagers can accurately reason about |
167 | | /// all SVal values. This method returns true if the ConstraintManager can |
168 | | /// reasonably handle a given SVal value. This is typically queried by |
169 | | /// ExprEngine to determine if the value should be replaced with a |
170 | | /// conjured symbolic value in order to recover some precision. |
171 | | virtual bool canReasonAbout(SVal X) const = 0; |
172 | | |
173 | | /// Returns whether or not a symbol is known to be null ("true"), known to be |
174 | | /// non-null ("false"), or may be either ("underconstrained"). |
175 | | virtual ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym); |
176 | | }; |
177 | | |
178 | | std::unique_ptr<ConstraintManager> |
179 | | CreateRangeConstraintManager(ProgramStateManager &statemgr, |
180 | | ExprEngine *exprengine); |
181 | | |
182 | | std::unique_ptr<ConstraintManager> |
183 | | CreateZ3ConstraintManager(ProgramStateManager &statemgr, |
184 | | ExprEngine *exprengine); |
185 | | |
186 | | } // namespace ento |
187 | | } // namespace clang |
188 | | |
189 | | #endif // LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H |