clang  8.0.0svn
ConstraintManager.h
Go to the documentation of this file.
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"
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 
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) {}
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 
56  /// Return true if the constraint is perfectly constrained to 'true'.
57  bool isConstrainedTrue() const {
58  return Val.hasValue() && Val.getValue();
59  }
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 
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  }
76 };
77 
79 public:
80  ConstraintManager() = default;
81  virtual ~ConstraintManager();
82 
83  virtual ProgramStateRef assume(ProgramStateRef state,
84  DefinedSVal Cond,
85  bool Assumption) = 0;
86 
87  using ProgramStatePair = std::pair<ProgramStateRef, ProgramStateRef>;
88 
89  /// Returns a pair of states (StTrue, StFalse) where the given condition is
90  /// assumed to be true or false, respectively.
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,
119  NonLoc Value,
120  const llvm::APSInt &From,
121  const llvm::APSInt &To,
122  bool InBound) = 0;
123 
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.
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>
201  SubEngine *subengine);
202 
203 std::unique_ptr<ConstraintManager>
205 
206 } // namespace ento
207 } // namespace clang
208 
209 #endif // LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H
bool isConstrainedFalse() const
Return true if the constraint is perfectly constrained to &#39;false&#39;.
bool isUnderconstrained() const
Return true if the constrained is underconstrained and we do not know if the constraint is true of va...
DominatorTree GraphTraits specialization so the DominatorTree can be iterable by generic graph iterat...
Definition: Dominators.h:30
std::unique_ptr< ConstraintManager > CreateRangeConstraintManager(ProgramStateManager &statemgr, SubEngine *subengine)
virtual void EndPath(ProgramStateRef state)
Symbolic value.
Definition: SymExpr.h:30
virtual ProgramStatePair assumeInclusiveRangeDual(ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, const llvm::APSInt &To)
ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym)
Convenience method to query the state to see if a symbol is null or not null, or if neither assumptio...
LineState State
i32 captured_struct **param SharedsTy A type which contains references the shared variables *param Shareds Context with the list of shared variables from the p *TaskFunction *param Data Additional data for task generation like final * state
Forward-declares and imports various common LLVM datatypes that clang wants to use unqualified...
std::unique_ptr< ConstraintManager > CreateZ3ConstraintManager(ProgramStateManager &statemgr, SubEngine *subengine)
bool isConstrainedTrue() const
Return true if the constraint is perfectly constrained to &#39;true&#39;.
ProgramStatePair assumeDual(ProgramStateRef State, DefinedSVal Cond)
Returns a pair of states (StTrue, StFalse) where the given condition is assumed to be true or false...
SVal - This represents a symbolic expression, which can be either an L-value or an R-value...
Definition: SVals.h:76
A class responsible for cleaning up unused symbols.
Dataflow Directional Tag Classes.
ConditionTruthVal(bool constraint)
Construct a ConditionTruthVal indicating the constraint is constrained to either true or false...
virtual const llvm::APSInt * getSymVal(ProgramStateRef state, SymbolRef sym) const
If a symbol is perfectly constrained to a constant, attempt to return the concrete value...
bool isConstrained() const
Return true if the constrained is perfectly constrained.
X
Add a minimal nested name specifier fixit hint to allow lookup of a tag name from an outer enclosing ...
Definition: SemaDecl.cpp:13853
std::pair< ProgramStateRef, ProgramStateRef > ProgramStatePair