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