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