clang  16.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 { return Val && Val.value(); }
57 
58  /// Return true if the constraint is perfectly constrained to 'false'.
59  bool isConstrainedFalse() const { return Val && !Val.value(); }
60 
61  /// Return true if the constrained is perfectly constrained.
62  bool isConstrained() const { return Val.has_value(); }
63 
64  /// Return true if the constrained is underconstrained and we do not know
65  /// if the constraint is true of value.
66  bool isUnderconstrained() const { return !Val.has_value(); }
67 };
68 
70 public:
71  ConstraintManager() = default;
72  virtual ~ConstraintManager();
73 
74  virtual bool haveEqualConstraints(ProgramStateRef S1,
75  ProgramStateRef S2) const = 0;
76 
78  bool Assumption);
79 
80  using ProgramStatePair = std::pair<ProgramStateRef, ProgramStateRef>;
81 
82  /// Returns a pair of states (StTrue, StFalse) where the given condition is
83  /// assumed to be true or false, respectively.
84  /// (Note that these two states might be equal if the parent state turns out
85  /// to be infeasible. This may happen if the underlying constraint solver is
86  /// not perfectly precise and this may happen very rarely.)
88 
90  const llvm::APSInt &From,
91  const llvm::APSInt &To, bool InBound);
92 
93  /// Returns a pair of states (StInRange, StOutOfRange) where the given value
94  /// is assumed to be in the range or out of the range, respectively.
95  /// (Note that these two states might be equal if the parent state turns out
96  /// to be infeasible. This may happen if the underlying constraint solver is
97  /// not perfectly precise and this may happen very rarely.)
99  const llvm::APSInt &From,
100  const llvm::APSInt &To);
101 
102  /// If a symbol is perfectly constrained to a constant, attempt
103  /// to return the concrete value.
104  ///
105  /// Note that a ConstraintManager is not obligated to return a concretized
106  /// value for a symbol, even if it is perfectly constrained.
107  /// It might return null.
109  SymbolRef sym) const {
110  return nullptr;
111  }
112 
113  /// Scan all symbols referenced by the constraints. If the symbol is not
114  /// alive, remove it.
116  SymbolReaper& SymReaper) = 0;
117 
118  virtual void printJson(raw_ostream &Out, ProgramStateRef State,
119  const char *NL, unsigned int Space,
120  bool IsDot) const = 0;
121 
122  virtual void printValue(raw_ostream &Out, ProgramStateRef State,
123  SymbolRef Sym) {}
124 
125  /// Convenience method to query the state to see if a symbol is null or
126  /// not null, or if neither assumption can be made.
128  return checkNull(State, Sym);
129  }
130 
131 protected:
132  /// A helper class to simulate the call stack of nested assume calls.
134  public:
135  void push(const ProgramState *S) { Aux.push_back(S); }
136  void pop() { Aux.pop_back(); }
137  bool contains(const ProgramState *S) const {
138  return llvm::is_contained(Aux, S);
139  }
140 
141  private:
143  };
145 
147  DefinedSVal Cond, bool Assumption) = 0;
148 
150  NonLoc Value,
151  const llvm::APSInt &From,
152  const llvm::APSInt &To,
153  bool InBound) = 0;
154 
155  /// canReasonAbout - Not all ConstraintManagers can accurately reason about
156  /// all SVal values. This method returns true if the ConstraintManager can
157  /// reasonably handle a given SVal value. This is typically queried by
158  /// ExprEngine to determine if the value should be replaced with a
159  /// conjured symbolic value in order to recover some precision.
160  virtual bool canReasonAbout(SVal X) const = 0;
161 
162  /// Returns whether or not a symbol is known to be null ("true"), known to be
163  /// non-null ("false"), or may be either ("underconstrained").
165 
166  template <typename AssumeFunction>
168  AssumeFunction &Assume);
169 };
170 
171 std::unique_ptr<ConstraintManager>
173  ExprEngine *exprengine);
174 
175 std::unique_ptr<ConstraintManager>
177  ExprEngine *exprengine);
178 
179 } // namespace ento
180 } // namespace clang
181 
182 #endif // LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H
clang::ento::ConstraintManager::assumeInclusiveRangeDual
ProgramStatePair assumeInclusiveRangeDual(ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, const llvm::APSInt &To)
Returns a pair of states (StInRange, StOutOfRange) where the given value is assumed to be in the rang...
Definition: ConstraintManager.cpp:101
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:266
clang::ento::ConstraintManager
Definition: ConstraintManager.h:69
clang::ento::ConstraintManager::printJson
virtual void printJson(raw_ostream &Out, ProgramStateRef State, const char *NL, unsigned int Space, bool IsDot) const =0
llvm::SmallVector
Definition: LLVM.h:38
clang::ento::ConstraintManager::ProgramStatePair
std::pair< ProgramStateRef, ProgramStateRef > ProgramStatePair
Definition: ConstraintManager.h:80
clang::ento::ConditionTruthVal::isConstrainedFalse
bool isConstrainedFalse() const
Return true if the constraint is perfectly constrained to 'false'.
Definition: ConstraintManager.h:59
clang::ento::CreateRangeConstraintManager
std::unique_ptr< ConstraintManager > CreateRangeConstraintManager(ProgramStateManager &statemgr, ExprEngine *exprengine)
Definition: RangeConstraintManager.cpp:2192
clang::ento::ConstraintManager::AssumeStackTy::contains
bool contains(const ProgramState *S) const
Definition: ConstraintManager.h:137
ProgramState_Fwd.h
clang::ento::ConstraintManager::AssumeStackTy::push
void push(const ProgramState *S)
Definition: ConstraintManager.h:135
llvm::Optional< bool >
clang::ento::ConstraintManager::AssumeStackTy::pop
void pop()
Definition: ConstraintManager.h:136
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::ProgramState
Definition: ProgramState.h:70
clang::ento::ConstraintManager::haveEqualConstraints
virtual bool haveEqualConstraints(ProgramStateRef S1, ProgramStateRef S2) const =0
clang::ento::ConstraintManager::AssumeStack
AssumeStackTy AssumeStack
Definition: ConstraintManager.h:144
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::DefinedSVal
Definition: SVals.h:243
clang::ento::SymExpr
Symbolic value.
Definition: SymExpr.h:29
clang::ento::ConstraintManager::AssumeStackTy
A helper class to simulate the call stack of nested assume calls.
Definition: ConstraintManager.h:133
clang::ento::ConstraintManager::~ConstraintManager
virtual ~ConstraintManager()
clang::ento::ConstraintManager::assume
ProgramStateRef assume(ProgramStateRef state, DefinedSVal Cond, bool Assumption)
Definition: ConstraintManager.cpp:110
clang::ento::SymbolReaper
A class responsible for cleaning up unused symbols.
Definition: SymbolManager.h:572
clang::ento::ConstraintManager::assumeDualImpl
ProgramStatePair assumeDualImpl(ProgramStateRef &State, AssumeFunction &Assume)
clang::ento::ConstraintManager::assumeInclusiveRangeInternal
virtual ProgramStateRef assumeInclusiveRangeInternal(ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, const llvm::APSInt &To, bool InBound)=0
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:108
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:93
clang::ento::CreateZ3ConstraintManager
std::unique_ptr< ConstraintManager > CreateZ3ConstraintManager(ProgramStateManager &statemgr, ExprEngine *exprengine)
Definition: SMTConstraintManager.cpp:15
clang::ento::ProgramStateManager
Definition: ProgramState.h:502
clang::ento::ConstraintManager::assumeInternal
virtual ProgramStateRef assumeInternal(ProgramStateRef state, DefinedSVal Cond, bool Assumption)=0
Value
Value
Definition: UninitializedValues.cpp:103
LLVM.h
State
LineState State
Definition: UnwrappedLineFormatter.cpp:1147
clang::ento::ExprEngine
Definition: ExprEngine.h:123
clang
Definition: CalledOnceCheck.h:17
clang::ento::ConstraintManager::assumeInclusiveRange
ProgramStateRef assumeInclusiveRange(ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, const llvm::APSInt &To, bool InBound)
Definition: ConstraintManager.cpp:117
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:33
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::ConstraintManager::printValue
virtual void printValue(raw_ostream &Out, ProgramStateRef State, SymbolRef Sym)
Definition: ConstraintManager.h:122
clang::ento::SVal
SVal - This represents a symbolic expression, which can be either an L-value or an R-value.
Definition: SVals.h:73
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:66
clang::ento::ConditionTruthVal::isConstrained
bool isConstrained() const
Return true if the constrained is perfectly constrained.
Definition: ConstraintManager.h:62
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:127
llvm::IntrusiveRefCntPtr< const ProgramState >