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