/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.8k | 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.5k | bool isConstrainedTrue() const { return Val && Val.value()46.7k ; } |
57 | | |
58 | | /// Return true if the constraint is perfectly constrained to 'false'. |
59 | 1.81k | bool isConstrainedFalse() const { return Val && !Val.value()915 ; } |
60 | | |
61 | | /// Return true if the constrained is perfectly constrained. |
62 | 24 | 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 | 33.1k | bool isUnderconstrained() const { return !Val.has_value(); } |
67 | | }; |
68 | | |
69 | | class ConstraintManager { |
70 | | public: |
71 | 15.6k | 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 | 0 | SymbolRef sym) const { |
110 | 0 | return nullptr; |
111 | 0 | } |
112 | | |
113 | | /// Scan all symbols referenced by the constraints. If the symbol is not |
114 | | /// alive, remove it. |
115 | | virtual ProgramStateRef removeDeadBindings(ProgramStateRef state, |
116 | | SymbolReaper& SymReaper) = 0; |
117 | | |
118 | | virtual void printJson(raw_ostream &Out, ProgramStateRef State, |
119 | | const char *NL, unsigned int Space, |
120 | | bool IsDot) const = 0; |
121 | | |
122 | | virtual void printValue(raw_ostream &Out, ProgramStateRef State, |
123 | 0 | SymbolRef Sym) {} |
124 | | |
125 | | /// Convenience method to query the state to see if a symbol is null or |
126 | | /// not null, or if neither assumption can be made. |
127 | 66.6k | ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) { |
128 | 66.6k | return checkNull(State, Sym); |
129 | 66.6k | } |
130 | | |
131 | | protected: |
132 | | /// A helper class to simulate the call stack of nested assume calls. |
133 | | class AssumeStackTy { |
134 | | public: |
135 | 629k | void push(const ProgramState *S) { Aux.push_back(S); } |
136 | 629k | void pop() { Aux.pop_back(); } |
137 | 629k | bool contains(const ProgramState *S) const { |
138 | 629k | return llvm::is_contained(Aux, S); |
139 | 629k | } |
140 | | |
141 | | private: |
142 | | llvm::SmallVector<const ProgramState *, 4> Aux; |
143 | | }; |
144 | | AssumeStackTy AssumeStack; |
145 | | |
146 | | virtual ProgramStateRef assumeInternal(ProgramStateRef state, |
147 | | DefinedSVal Cond, bool Assumption) = 0; |
148 | | |
149 | | virtual ProgramStateRef assumeInclusiveRangeInternal(ProgramStateRef State, |
150 | | NonLoc Value, |
151 | | const llvm::APSInt &From, |
152 | | const llvm::APSInt &To, |
153 | | bool InBound) = 0; |
154 | | |
155 | | /// canReasonAbout - Not all ConstraintManagers can accurately reason about |
156 | | /// all SVal values. This method returns true if the ConstraintManager can |
157 | | /// reasonably handle a given SVal value. This is typically queried by |
158 | | /// ExprEngine to determine if the value should be replaced with a |
159 | | /// conjured symbolic value in order to recover some precision. |
160 | | virtual bool canReasonAbout(SVal X) const = 0; |
161 | | |
162 | | /// Returns whether or not a symbol is known to be null ("true"), known to be |
163 | | /// non-null ("false"), or may be either ("underconstrained"). |
164 | | virtual ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym); |
165 | | |
166 | | template <typename AssumeFunction> |
167 | | ProgramStatePair assumeDualImpl(ProgramStateRef &State, |
168 | | AssumeFunction &Assume); |
169 | | }; |
170 | | |
171 | | std::unique_ptr<ConstraintManager> |
172 | | CreateRangeConstraintManager(ProgramStateManager &statemgr, |
173 | | ExprEngine *exprengine); |
174 | | |
175 | | std::unique_ptr<ConstraintManager> |
176 | | CreateZ3ConstraintManager(ProgramStateManager &statemgr, |
177 | | ExprEngine *exprengine); |
178 | | |
179 | | } // namespace ento |
180 | | } // namespace clang |
181 | | |
182 | | #endif // LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H |