clang  14.0.0git
ConstraintManager.h
Go to the documentation of this file.
1 //===- ConstraintManager.h - Constraints on symbolic values. ----*- C++ -*-===//
2 //
3 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4 // See https://llvm.org/LICENSE.txt for license information.
5 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6 //
7 //===----------------------------------------------------------------------===//
8 //
9 // This file defined the interface to manage constraints on symbolic values.
10 //
11 //===----------------------------------------------------------------------===//
12 
13 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H
14 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H
15 
16 #include "clang/Basic/LLVM.h"
20 #include "llvm/ADT/Optional.h"
21 #include "llvm/Support/SaveAndRestore.h"
22 #include <memory>
23 #include <utility>
24 
25 namespace llvm {
26 
27 class APSInt;
28 
29 } // namespace llvm
30 
31 namespace clang {
32 namespace ento {
33 
34 class ProgramStateManager;
35 class ExprEngine;
36 class SymbolReaper;
37 
39  Optional<bool> Val;
40 
41 public:
42  /// Construct a ConditionTruthVal indicating the constraint is constrained
43  /// to either true or false, depending on the boolean value provided.
44  ConditionTruthVal(bool constraint) : Val(constraint) {}
45 
46  /// Construct a ConstraintVal indicating the constraint is underconstrained.
47  ConditionTruthVal() = default;
48 
49  /// \return Stored value, assuming that the value is known.
50  /// Crashes otherwise.
51  bool getValue() const {
52  return *Val;
53  }
54 
55  /// Return true if the constraint is perfectly constrained to 'true'.
56  bool isConstrainedTrue() const {
57  return Val.hasValue() && Val.getValue();
58  }
59 
60  /// Return true if the constraint is perfectly constrained to 'false'.
61  bool isConstrainedFalse() const {
62  return Val.hasValue() && !Val.getValue();
63  }
64 
65  /// Return true if the constrained is perfectly constrained.
66  bool isConstrained() const {
67  return Val.hasValue();
68  }
69 
70  /// Return true if the constrained is underconstrained and we do not know
71  /// if the constraint is true of value.
72  bool isUnderconstrained() const {
73  return !Val.hasValue();
74  }
75 };
76 
78 public:
79  ConstraintManager() = default;
80  virtual ~ConstraintManager();
81 
82  virtual bool haveEqualConstraints(ProgramStateRef S1,
83  ProgramStateRef S2) const = 0;
84 
86  DefinedSVal Cond,
87  bool Assumption) = 0;
88 
89  using ProgramStatePair = std::pair<ProgramStateRef, ProgramStateRef>;
90 
91  /// Returns a pair of states (StTrue, StFalse) where the given condition is
92  /// assumed to be true or false, respectively.
94  ProgramStateRef StTrue = assume(State, Cond, true);
95 
96  // If StTrue is infeasible, asserting the falseness of Cond is unnecessary
97  // because the existing constraints already establish this.
98  if (!StTrue) {
99 #ifdef EXPENSIVE_CHECKS
100  assert(assume(State, Cond, false) && "System is over constrained.");
101 #endif
102  return ProgramStatePair((ProgramStateRef)nullptr, State);
103  }
104 
105  ProgramStateRef StFalse = assume(State, Cond, false);
106  if (!StFalse) {
107  // We are careful to return the original state, /not/ StTrue,
108  // because we want to avoid having callers generate a new node
109  // in the ExplodedGraph.
110  return ProgramStatePair(State, (ProgramStateRef)nullptr);
111  }
112 
113  return ProgramStatePair(StTrue, StFalse);
114  }
115 
117  NonLoc Value,
118  const llvm::APSInt &From,
119  const llvm::APSInt &To,
120  bool InBound) = 0;
121 
123  NonLoc Value,
124  const llvm::APSInt &From,
125  const llvm::APSInt &To) {
126  ProgramStateRef StInRange =
127  assumeInclusiveRange(State, Value, From, To, true);
128 
129  // If StTrue is infeasible, asserting the falseness of Cond is unnecessary
130  // because the existing constraints already establish this.
131  if (!StInRange)
132  return ProgramStatePair((ProgramStateRef)nullptr, State);
133 
134  ProgramStateRef StOutOfRange =
135  assumeInclusiveRange(State, Value, From, To, false);
136  if (!StOutOfRange) {
137  // We are careful to return the original state, /not/ StTrue,
138  // because we want to avoid having callers generate a new node
139  // in the ExplodedGraph.
140  return ProgramStatePair(State, (ProgramStateRef)nullptr);
141  }
142 
143  return ProgramStatePair(StInRange, StOutOfRange);
144  }
145 
146  /// If a symbol is perfectly constrained to a constant, attempt
147  /// to return the concrete value.
148  ///
149  /// Note that a ConstraintManager is not obligated to return a concretized
150  /// value for a symbol, even if it is perfectly constrained.
152  SymbolRef sym) const {
153  return nullptr;
154  }
155 
156  /// Scan all symbols referenced by the constraints. If the symbol is not
157  /// alive, remove it.
159  SymbolReaper& SymReaper) = 0;
160 
161  virtual void printJson(raw_ostream &Out, ProgramStateRef State,
162  const char *NL, unsigned int Space,
163  bool IsDot) const = 0;
164 
165  /// Convenience method to query the state to see if a symbol is null or
166  /// not null, or if neither assumption can be made.
168  SaveAndRestore<bool> DisableNotify(NotifyAssumeClients, false);
169 
170  return checkNull(State, Sym);
171  }
172 
173 protected:
174  /// A flag to indicate that clients should be notified of assumptions.
175  /// By default this is the case, but sometimes this needs to be restricted
176  /// to avoid infinite recursions within the ConstraintManager.
177  ///
178  /// Note that this flag allows the ConstraintManager to be re-entrant,
179  /// but not thread-safe.
180  bool NotifyAssumeClients = true;
181 
182  /// canReasonAbout - Not all ConstraintManagers can accurately reason about
183  /// all SVal values. This method returns true if the ConstraintManager can
184  /// reasonably handle a given SVal value. This is typically queried by
185  /// ExprEngine to determine if the value should be replaced with a
186  /// conjured symbolic value in order to recover some precision.
187  virtual bool canReasonAbout(SVal X) const = 0;
188 
189  /// Returns whether or not a symbol is known to be null ("true"), known to be
190  /// non-null ("false"), or may be either ("underconstrained").
192 };
193 
194 std::unique_ptr<ConstraintManager>
196  ExprEngine *exprengine);
197 
198 std::unique_ptr<ConstraintManager>
200  ExprEngine *exprengine);
201 
202 } // namespace ento
203 } // namespace clang
204 
205 #endif // LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H
llvm
Definition: Dominators.h:30
SVals.h
clang::ento::ConstraintManager::canReasonAbout
virtual bool canReasonAbout(SVal X) const =0
canReasonAbout - Not all ConstraintManagers can accurately reason about all SVal values.
clang::ento::NonLoc
Definition: SVals.h:305
clang::ento::ConstraintManager
Definition: ConstraintManager.h:77
clang::ento::ConstraintManager::printJson
virtual void printJson(raw_ostream &Out, ProgramStateRef State, const char *NL, unsigned int Space, bool IsDot) const =0
clang::ento::ConstraintManager::ProgramStatePair
std::pair< ProgramStateRef, ProgramStateRef > ProgramStatePair
Definition: ConstraintManager.h:89
clang::ento::ConstraintManager::assume
virtual ProgramStateRef assume(ProgramStateRef state, DefinedSVal Cond, bool Assumption)=0
clang::ento::ConditionTruthVal::isConstrainedFalse
bool isConstrainedFalse() const
Return true if the constraint is perfectly constrained to 'false'.
Definition: ConstraintManager.h:61
clang::ento::CreateRangeConstraintManager
std::unique_ptr< ConstraintManager > CreateRangeConstraintManager(ProgramStateManager &statemgr, ExprEngine *exprengine)
Definition: RangeConstraintManager.cpp:1802
ProgramState_Fwd.h
llvm::Optional< bool >
clang::tooling::X
static ToolExecutorPluginRegistry::Add< AllTUsToolExecutorPlugin > X("all-TUs", "Runs FrontendActions on all TUs in the compilation database. " "Tool results are stored in memory.")
clang::ento::ConstraintManager::ConstraintManager
ConstraintManager()=default
clang::ento::ConstraintManager::assumeInclusiveRangeDual
virtual ProgramStatePair assumeInclusiveRangeDual(ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, const llvm::APSInt &To)
Definition: ConstraintManager.h:122
clang::ento::ConstraintManager::haveEqualConstraints
virtual bool haveEqualConstraints(ProgramStateRef S1, ProgramStateRef S2) const =0
clang::ento::ConditionTruthVal
Definition: ConstraintManager.h:38
APSInt
llvm::APSInt APSInt
Definition: ByteCodeEmitter.cpp:19
clang::ento::ConditionTruthVal::ConditionTruthVal
ConditionTruthVal()=default
Construct a ConstraintVal indicating the constraint is underconstrained.
SymExpr.h
clang::ento::ConstraintManager::NotifyAssumeClients
bool NotifyAssumeClients
A flag to indicate that clients should be notified of assumptions.
Definition: ConstraintManager.h:180
clang::ento::DefinedSVal
Definition: SVals.h:269
clang::ento::SymExpr
Symbolic value.
Definition: SymExpr.h:29
clang::ento::ConstraintManager::~ConstraintManager
virtual ~ConstraintManager()
clang::ento::SymbolReaper
A class responsible for cleaning up unused symbols.
Definition: SymbolManager.h:505
clang::ento::ConstraintManager::getSymVal
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.
Definition: ConstraintManager.h:151
state
and static some checkers Checker The latter are built on top of the former via the Checker and CheckerVisitor and attempts to isolate them from much of the gore of the internal analysis the analyzer is basically a source code simulator that traces out possible paths of execution The state of the and the combination of state and program point is a node in an exploded which has the entry program point and initial state
Definition: README.txt:30
clang::ento::ConstraintManager::removeDeadBindings
virtual ProgramStateRef removeDeadBindings(ProgramStateRef state, SymbolReaper &SymReaper)=0
Scan all symbols referenced by the constraints.
clang::ento::ConditionTruthVal::isConstrainedTrue
bool isConstrainedTrue() const
Return true if the constraint is perfectly constrained to 'true'.
Definition: ConstraintManager.h:56
clang::ento::CreateZ3ConstraintManager
std::unique_ptr< ConstraintManager > CreateZ3ConstraintManager(ProgramStateManager &statemgr, ExprEngine *exprengine)
Definition: SMTConstraintManager.cpp:15
clang::ento::ProgramStateManager
Definition: ProgramState.h:463
Value
Value
Definition: UninitializedValues.cpp:102
LLVM.h
State
LineState State
Definition: UnwrappedLineFormatter.cpp:987
llvm::SaveAndRestore< bool >
clang::ento::ExprEngine
Definition: ExprEngine.h:127
clang::ento::ConstraintManager::assumeDual
ProgramStatePair assumeDual(ProgramStateRef State, DefinedSVal Cond)
Returns a pair of states (StTrue, StFalse) where the given condition is assumed to be true or false,...
Definition: ConstraintManager.h:93
clang
Definition: CalledOnceCheck.h:17
clang::ento::ConstraintManager::checkNull
virtual ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym)
Returns whether or not a symbol is known to be null ("true"), known to be non-null ("false"),...
Definition: ConstraintManager.cpp:32
clang::ento::ConstraintManager::assumeInclusiveRange
virtual ProgramStateRef assumeInclusiveRange(ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, const llvm::APSInt &To, bool InBound)=0
clang::ento::ConditionTruthVal::ConditionTruthVal
ConditionTruthVal(bool constraint)
Construct a ConditionTruthVal indicating the constraint is constrained to either true or false,...
Definition: ConstraintManager.h:44
clang::ento::SVal
SVal - This represents a symbolic expression, which can be either an L-value or an R-value.
Definition: SVals.h:75
clang::ento::ConditionTruthVal::isUnderconstrained
bool isUnderconstrained() const
Return true if the constrained is underconstrained and we do not know if the constraint is true of va...
Definition: ConstraintManager.h:72
clang::ento::ConditionTruthVal::isConstrained
bool isConstrained() const
Return true if the constrained is perfectly constrained.
Definition: ConstraintManager.h:66
clang::ento::ConditionTruthVal::getValue
bool getValue() const
Definition: ConstraintManager.h:51
clang::ento::ConstraintManager::isNull
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...
Definition: ConstraintManager.h:167
llvm::IntrusiveRefCntPtr< const ProgramState >