clang  15.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  bool Assumption);
87 
88  using ProgramStatePair = std::pair<ProgramStateRef, ProgramStateRef>;
89 
90  /// Returns a pair of states (StTrue, StFalse) where the given condition is
91  /// assumed to be true or false, respectively.
92  /// (Note that these two states might be equal if the parent state turns out
93  /// to be infeasible. This may happen if the underlying constraint solver is
94  /// not perfectly precise and this may happen very rarely.)
96 
98  NonLoc Value,
99  const llvm::APSInt &From,
100  const llvm::APSInt &To,
101  bool InBound) = 0;
102 
104  NonLoc Value,
105  const llvm::APSInt &From,
106  const llvm::APSInt &To) {
107  ProgramStateRef StInRange =
108  assumeInclusiveRange(State, Value, From, To, true);
109 
110  // If StTrue is infeasible, asserting the falseness of Cond is unnecessary
111  // because the existing constraints already establish this.
112  if (!StInRange)
113  return ProgramStatePair((ProgramStateRef)nullptr, State);
114 
115  ProgramStateRef StOutOfRange =
116  assumeInclusiveRange(State, Value, From, To, false);
117  if (!StOutOfRange) {
118  // We are careful to return the original state, /not/ StTrue,
119  // because we want to avoid having callers generate a new node
120  // in the ExplodedGraph.
121  return ProgramStatePair(State, (ProgramStateRef)nullptr);
122  }
123 
124  return ProgramStatePair(StInRange, StOutOfRange);
125  }
126 
127  /// If a symbol is perfectly constrained to a constant, attempt
128  /// to return the concrete value.
129  ///
130  /// Note that a ConstraintManager is not obligated to return a concretized
131  /// value for a symbol, even if it is perfectly constrained.
133  SymbolRef sym) const {
134  return nullptr;
135  }
136 
137  /// Scan all symbols referenced by the constraints. If the symbol is not
138  /// alive, remove it.
140  SymbolReaper& SymReaper) = 0;
141 
142  virtual void printJson(raw_ostream &Out, ProgramStateRef State,
143  const char *NL, unsigned int Space,
144  bool IsDot) const = 0;
145 
146  /// Convenience method to query the state to see if a symbol is null or
147  /// not null, or if neither assumption can be made.
149  SaveAndRestore<bool> DisableNotify(NotifyAssumeClients, false);
150 
151  return checkNull(State, Sym);
152  }
153 
154 protected:
155  /// A flag to indicate that clients should be notified of assumptions.
156  /// By default this is the case, but sometimes this needs to be restricted
157  /// to avoid infinite recursions within the ConstraintManager.
158  ///
159  /// Note that this flag allows the ConstraintManager to be re-entrant,
160  /// but not thread-safe.
161  bool NotifyAssumeClients = true;
162 
164  DefinedSVal Cond, bool Assumption) = 0;
165 
166  /// canReasonAbout - Not all ConstraintManagers can accurately reason about
167  /// all SVal values. This method returns true if the ConstraintManager can
168  /// reasonably handle a given SVal value. This is typically queried by
169  /// ExprEngine to determine if the value should be replaced with a
170  /// conjured symbolic value in order to recover some precision.
171  virtual bool canReasonAbout(SVal X) const = 0;
172 
173  /// Returns whether or not a symbol is known to be null ("true"), known to be
174  /// non-null ("false"), or may be either ("underconstrained").
176 };
177 
178 std::unique_ptr<ConstraintManager>
180  ExprEngine *exprengine);
181 
182 std::unique_ptr<ConstraintManager>
184  ExprEngine *exprengine);
185 
186 } // namespace ento
187 } // namespace clang
188 
189 #endif // LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H
llvm
YAML serialization mapping.
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:304
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:88
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:2168
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:103
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:161
clang::ento::DefinedSVal
Definition: SVals.h:268
clang::ento::SymExpr
Symbolic value.
Definition: SymExpr.h:29
clang::ento::ConstraintManager::~ConstraintManager
virtual ~ConstraintManager()
clang::ento::ConstraintManager::assume
ProgramStateRef assume(ProgramStateRef state, DefinedSVal Cond, bool Assumption)
Definition: ConstraintManager.cpp:74
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:132
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::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.cpp:46
clang::ento::CreateZ3ConstraintManager
std::unique_ptr< ConstraintManager > CreateZ3ConstraintManager(ProgramStateManager &statemgr, ExprEngine *exprengine)
Definition: SMTConstraintManager.cpp:15
clang::ento::ProgramStateManager
Definition: ProgramState.h:498
clang::ento::ConstraintManager::assumeInternal
virtual ProgramStateRef assumeInternal(ProgramStateRef state, DefinedSVal Cond, bool Assumption)=0
Value
Value
Definition: UninitializedValues.cpp:102
LLVM.h
State
LineState State
Definition: UnwrappedLineFormatter.cpp:1089
llvm::SaveAndRestore< bool >
clang::ento::ExprEngine
Definition: ExprEngine.h:123
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:74
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:148
llvm::IntrusiveRefCntPtr< const ProgramState >