clang: clang::ento::SMTConstraintManager Class Reference (original) (raw)

#include "[clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h](SMTConstraintManager%5F8h%5Fsource.html)"

Public Member Functions
SMTConstraintManager (clang::ento::ExprEngine *EE, clang::ento::SValBuilder &SB)
virtual ~SMTConstraintManager ()=default
ProgramStateRef assumeSym (ProgramStateRef State, SymbolRef Sym, bool Assumption) override
Given a symbolic expression that can be reasoned about, assume that it is true/false and generate the new program state.
ProgramStateRef assumeSymInclusiveRange (ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) override
Given a symbolic expression within the range [From, To], assume that it is true/false and generate the new program state.
ProgramStateRef assumeSymUnsupported (ProgramStateRef State, SymbolRef Sym, bool Assumption) override
Given a symbolic expression that cannot be reasoned about, assume that it is zero/nonzero and add it directly to the solver state.
ConditionTruthVal checkNull (ProgramStateRef State, SymbolRef Sym) override
Returns whether or not a symbol is known to be null ("true"), known to be non-null ("false"), or may be either ("underconstrained").
const llvm::APSInt * getSymVal (ProgramStateRef State, SymbolRef Sym) const override
If a symbol is perfectly constrained to a constant, attempt to return the concrete value.
ProgramStateRef removeDeadBindings (ProgramStateRef State, SymbolReaper &SymReaper) override
Scan all symbols referenced by the constraints.
void printJson (raw_ostream &Out, ProgramStateRef State, const char *NL="\n", unsigned int Space=0, bool IsDot=false) const override
bool haveEqualConstraints (ProgramStateRef S1, ProgramStateRef S2) const override
bool canReasonAbout (SVal X) const override
canReasonAbout - Not all ConstraintManagers can accurately reason about all SVal values.
LLVM_DUMP_METHOD void dump () const
Dumps SMT formula.
- Public Member Functions inherited from clang::ento::SimpleConstraintManager
SimpleConstraintManager (ExprEngine *exprengine, SValBuilder &SB)
~SimpleConstraintManager () override
- Public Member Functions inherited from clang::ento::ConstraintManager
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 assumeExpr (ProgramStateRef State, SymbolRef Sym, const llvm::SMTExprRef &Exp)
virtual void addStateConstraints (ProgramStateRef State) const
Given a program state, construct the logical conjunction and add it to the solver.
ConditionTruthVal checkModel (ProgramStateRef State, SymbolRef Sym, const llvm::SMTExprRef &Exp) const
- Protected Member Functions inherited from clang::ento::SimpleConstraintManager
virtual ProgramStateRef assumeSym (ProgramStateRef State, SymbolRef Sym, bool Assumption)=0
Given a symbolic expression that can be reasoned about, assume that it is true/false and generate the new program state.
virtual ProgramStateRef assumeSymInclusiveRange (ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange)=0
Given a symbolic expression within the range [From, To], assume that it is true/false and generate the new program state.
virtual ProgramStateRef assumeSymUnsupported (ProgramStateRef State, SymbolRef Sym, bool Assumption)=0
Given a symbolic expression that cannot be reasoned about, assume that it is zero/nonzero and add it directly to the solver state.
ProgramStateRef assumeInternal (ProgramStateRef State, DefinedSVal Cond, bool Assumption) override
Ensures that the DefinedSVal conditional is expressed as a NonLoc by creating boolean casts to handle Loc's.
ProgramStateRef assumeInclusiveRangeInternal (ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) override
SValBuilder & getSValBuilder () const
BasicValueFactory & getBasicVals () const
SymbolManager & getSymbolManager () const
- Protected Member Functions inherited from clang::ento::ConstraintManager
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
ProgramStatePair assumeDualImpl (ProgramStateRef &State, AssumeFunction &Assume)
Protected Attributes
llvm::DenseMap< unsigned, ConditionTruthVal > Cached
- Protected Attributes inherited from clang::ento::ConstraintManager
AssumeStackTy AssumeStack

Definition at line 32 of file SMTConstraintManager.h.

◆ ~SMTConstraintManager()

virtual clang::ento::SMTConstraintManager::~SMTConstraintManager ( ) virtualdefault

◆ addStateConstraints()

virtual void clang::ento::SMTConstraintManager::addStateConstraints ( ProgramStateRef State) const inlineprotectedvirtual

◆ assumeExpr()

◆ assumeSym()

◆ assumeSymInclusiveRange()

◆ assumeSymUnsupported()

◆ canReasonAbout()

bool clang::ento::SMTConstraintManager::canReasonAbout ( SVal X) const inlineoverridevirtual

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.

Implements clang::ento::ConstraintManager.

Definition at line 253 of file SMTConstraintManager.h.

References canReasonAbout(), clang::ento::SimpleConstraintManager::getBasicVals(), clang::ento::BasicValueFactory::getContext(), clang::TargetInfo::getLongDoubleFormat(), clang::ento::SimpleConstraintManager::getSValBuilder(), clang::ASTContext::getTargetInfo(), clang::ento::SymExpr::getType(), clang::Type::isComplexIntegerType(), clang::Type::isComplexType(), clang::Type::isRealFloatingType(), clang::Type::isSpecificBuiltinType(), clang::ento::SValBuilder::makeSymbolVal(), and X.

Referenced by canReasonAbout().

◆ checkModel()

◆ checkNull()

◆ dump()

LLVM_DUMP_METHOD void clang::ento::SMTConstraintManager::dump ( ) const inline

◆ getSymVal()

const llvm::APSInt * clang::ento::SMTConstraintManager::getSymVal ( ProgramStateRef state, SymbolRef sym ) const inlineoverridevirtual

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 from clang::ento::ConstraintManager.

Definition at line 115 of file SMTConstraintManager.h.

References addStateConstraints(), clang::ento::BasicValueFactory::Convert(), clang::ento::BasicValueFactory::evalAPSInt(), clang::ento::SMTConv::fixAPSInt(), clang::ento::SMTConv::fromBinOp(), clang::ento::SMTConv::fromData(), clang::ento::APSIntPtr::get(), clang::ento::SimpleConstraintManager::getBasicVals(), clang::ento::BasicValueFactory::getContext(), getSymVal(), clang::ento::SymExpr::getType(), clang::Type::isBooleanType(), clang::Type::isRealFloatingType(), clang::Type::isSignedIntegerOrEnumerationType(), and clang::Type::isVoidType().

Referenced by getSymVal().

◆ haveEqualConstraints()

◆ printJson()

void clang::ento::SMTConstraintManager::printJson ( raw_ostream & Out, ProgramStateRef State, const char * NL = "\n", unsigned int Space = 0, bool IsDot = false ) const inlineoverridevirtual

◆ removeDeadBindings()

◆ Cached

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