clang 19.0.0git
Classes | Public Types | Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
clang::ento::ConstraintManager Class Referenceabstract

#include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h"

Inheritance diagram for clang::ento::ConstraintManager:
Inheritance graph
[legend]

Classes

class  AssumeStackTy
 A helper class to simulate the call stack of nested assume calls. More...
 

Public Types

using ProgramStatePair = std::pair< ProgramStateRef, ProgramStateRef >
 

Public Member Functions

 ConstraintManager ()=default
 
virtual ~ConstraintManager ()
 
virtual bool haveEqualConstraints (ProgramStateRef S1, ProgramStateRef S2) const =0
 
ProgramStateRef assume (ProgramStateRef state, DefinedSVal Cond, bool Assumption)
 
ProgramStatePair assumeDual (ProgramStateRef State, DefinedSVal Cond)
 Returns a pair of states (StTrue, StFalse) where the given condition is assumed to be true or false, respectively.
 
ProgramStateRef assumeInclusiveRange (ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, const llvm::APSInt &To, bool InBound)
 
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 range or out of the range, respectively.
 
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.
 
virtual const llvm::APSInt * getSymMinVal (ProgramStateRef state, SymbolRef sym) const
 Attempt to return the minimal possible value for a given symbol.
 
virtual const llvm::APSInt * getSymMaxVal (ProgramStateRef state, SymbolRef sym) const
 Attempt to return the minimal possible value for a given symbol.
 
virtual ProgramStateRef removeDeadBindings (ProgramStateRef state, SymbolReaper &SymReaper)=0
 Scan all symbols referenced by the constraints.
 
virtual void printJson (raw_ostream &Out, ProgramStateRef State, const char *NL, unsigned int Space, bool IsDot) const =0
 
virtual void printValue (raw_ostream &Out, ProgramStateRef State, SymbolRef Sym)
 
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 assumption can be made.
 

Protected Member Functions

virtual ProgramStateRef assumeInternal (ProgramStateRef state, DefinedSVal Cond, bool Assumption)=0
 
virtual ProgramStateRef assumeInclusiveRangeInternal (ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, const llvm::APSInt &To, bool InBound)=0
 
virtual bool canReasonAbout (SVal X) const =0
 canReasonAbout - Not all ConstraintManagers can accurately reason about all SVal values.
 
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"), or may be either ("underconstrained").
 
template<typename AssumeFunction >
ProgramStatePair assumeDualImpl (ProgramStateRef &State, AssumeFunction &Assume)
 

Protected Attributes

AssumeStackTy AssumeStack
 

Detailed Description

Definition at line 69 of file ConstraintManager.h.

Member Typedef Documentation

◆ ProgramStatePair

Definition at line 80 of file ConstraintManager.h.

Constructor & Destructor Documentation

◆ ConstraintManager()

clang::ento::ConstraintManager::ConstraintManager ( )
default

◆ ~ConstraintManager()

ConstraintManager::~ConstraintManager ( )
virtualdefault

Member Function Documentation

◆ assume()

ProgramStateRef ConstraintManager::assume ( ProgramStateRef  state,
DefinedSVal  Cond,
bool  Assumption 
)

Definition at line 110 of file ConstraintManager.cpp.

References assumeDual().

◆ assumeDual()

ConstraintManager::ProgramStatePair ConstraintManager::assumeDual ( ProgramStateRef  State,
DefinedSVal  Cond 
)

Returns a pair of states (StTrue, StFalse) where the given condition is assumed to be true or false, respectively.

(Note that these two states might be equal if the parent state turns out to be infeasible. This may happen if the underlying constraint solver is not perfectly precise and this may happen very rarely.)

Definition at line 93 of file ConstraintManager.cpp.

References assumeDualImpl(), and assumeInternal().

Referenced by assume(), clang::ento::ProgramState::assumeInBoundDual(), and checkNull().

◆ assumeDualImpl()

template<typename AssumeFunction >
ConstraintManager::ProgramStatePair ConstraintManager::assumeDualImpl ( ProgramStateRef State,
AssumeFunction &  Assume 
)
protected

◆ assumeInclusiveRange()

ProgramStateRef ConstraintManager::assumeInclusiveRange ( ProgramStateRef  State,
NonLoc  Value,
const llvm::APSInt &  From,
const llvm::APSInt &  To,
bool  InBound 
)

Definition at line 117 of file ConstraintManager.cpp.

References assumeInclusiveRangeDual().

◆ assumeInclusiveRangeDual()

ConstraintManager::ProgramStatePair ConstraintManager::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 range or out of the range, respectively.

(Note that these two states might be equal if the parent state turns out to be infeasible. This may happen if the underlying constraint solver is not perfectly precise and this may happen very rarely.)

Definition at line 101 of file ConstraintManager.cpp.

References assumeDualImpl(), and assumeInclusiveRangeInternal().

Referenced by assumeInclusiveRange().

◆ assumeInclusiveRangeInternal()

virtual ProgramStateRef clang::ento::ConstraintManager::assumeInclusiveRangeInternal ( ProgramStateRef  State,
NonLoc  Value,
const llvm::APSInt &  From,
const llvm::APSInt &  To,
bool  InBound 
)
protectedpure virtual

◆ assumeInternal()

virtual ProgramStateRef clang::ento::ConstraintManager::assumeInternal ( ProgramStateRef  state,
DefinedSVal  Cond,
bool  Assumption 
)
protectedpure virtual

Implemented in clang::ento::SimpleConstraintManager.

Referenced by assumeDual().

◆ canReasonAbout()

virtual bool clang::ento::ConstraintManager::canReasonAbout ( SVal  X) const
protectedpure virtual

canReasonAbout - Not all ConstraintManagers can accurately reason about all SVal values.

This method returns true if the ConstraintManager can reasonably handle a given SVal value. This is typically queried by ExprEngine to determine if the value should be replaced with a conjured symbolic value in order to recover some precision.

Implemented in clang::ento::SMTConstraintManager.

Referenced by clang::ento::SimpleConstraintManager::assumeInclusiveRangeInternal().

◆ checkNull()

ConditionTruthVal ConstraintManager::checkNull ( ProgramStateRef  State,
SymbolRef  Sym 
)
protectedvirtual

Returns whether or not a symbol is known to be null ("true"), known to be non-null ("false"), or may be either ("underconstrained").

Reimplemented in clang::ento::SMTConstraintManager.

Definition at line 33 of file ConstraintManager.cpp.

References assumeDual(), getLocFromSymbol(), clang::ento::SymExpr::getType(), clang::ento::Loc::isLocType(), P, and V.

Referenced by isNull().

◆ getSymMaxVal()

virtual const llvm::APSInt * clang::ento::ConstraintManager::getSymMaxVal ( ProgramStateRef  state,
SymbolRef  sym 
) const
inlinevirtual

Attempt to return the minimal possible value for a given symbol.

Note that a ConstraintManager is not obligated to return a lower bound, it may also return nullptr.

Definition at line 124 of file ConstraintManager.h.

◆ getSymMinVal()

virtual const llvm::APSInt * clang::ento::ConstraintManager::getSymMinVal ( ProgramStateRef  state,
SymbolRef  sym 
) const
inlinevirtual

Attempt to return the minimal possible value for a given symbol.

Note that a ConstraintManager is not obligated to return a lower bound, it may also return nullptr.

Definition at line 116 of file ConstraintManager.h.

◆ getSymVal()

virtual const llvm::APSInt * clang::ento::ConstraintManager::getSymVal ( ProgramStateRef  state,
SymbolRef  sym 
) const
inlinevirtual

If a symbol is perfectly constrained to a constant, attempt to return the concrete value.

Note that a ConstraintManager is not obligated to return a concretized value for a symbol, even if it is perfectly constrained. It might return null.

Reimplemented in clang::ento::SMTConstraintManager.

Definition at line 108 of file ConstraintManager.h.

◆ haveEqualConstraints()

virtual bool clang::ento::ConstraintManager::haveEqualConstraints ( ProgramStateRef  S1,
ProgramStateRef  S2 
) const
pure virtual

◆ isNull()

ConditionTruthVal clang::ento::ConstraintManager::isNull ( ProgramStateRef  State,
SymbolRef  Sym 
)
inline

Convenience method to query the state to see if a symbol is null or not null, or if neither assumption can be made.

Definition at line 143 of file ConstraintManager.h.

References checkNull().

Referenced by clang::ento::retaincountchecker::RetainCountChecker::checkPostStmt(), didPreviousFreeFail(), and isLeaked().

◆ printJson()

virtual void clang::ento::ConstraintManager::printJson ( raw_ostream &  Out,
ProgramStateRef  State,
const char *  NL,
unsigned int  Space,
bool  IsDot 
) const
pure virtual

◆ printValue()

virtual void clang::ento::ConstraintManager::printValue ( raw_ostream &  Out,
ProgramStateRef  State,
SymbolRef  Sym 
)
inlinevirtual

Definition at line 138 of file ConstraintManager.h.

◆ removeDeadBindings()

virtual ProgramStateRef clang::ento::ConstraintManager::removeDeadBindings ( ProgramStateRef  state,
SymbolReaper SymReaper 
)
pure virtual

Scan all symbols referenced by the constraints.

If the symbol is not alive, remove it.

Implemented in clang::ento::SMTConstraintManager.

Referenced by clang::ento::ExprEngine::removeDead().

Member Data Documentation

◆ AssumeStack

AssumeStackTy clang::ento::ConstraintManager::AssumeStack
protected

Definition at line 160 of file ConstraintManager.h.

Referenced by assumeDualImpl().


The documentation for this class was generated from the following files: