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