clang  8.0.0svn
Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
clang::ento::SMTConstraintManager< ConstraintSMT, SMTExprTy > Class Template Reference

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

Inheritance diagram for clang::ento::SMTConstraintManager< ConstraintSMT, SMTExprTy >:
Inheritance graph
[legend]
Collaboration diagram for clang::ento::SMTConstraintManager< ConstraintSMT, SMTExprTy >:
Collaboration graph
[legend]

Public Member Functions

 SMTConstraintManager (clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB, SMTSolverRef &S)
 
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. More...
 
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. More...
 
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. More...
 
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"). More...
 
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. More...
 
ProgramStateRef removeDeadBindings (ProgramStateRef State, SymbolReaper &SymReaper) override
 Scan all symbols referenced by the constraints. More...
 
void print (ProgramStateRef St, raw_ostream &OS, const char *nl, const char *sep) override
 
bool canReasonAbout (SVal X) const override
 canReasonAbout - Not all ConstraintManagers can accurately reason about all SVal values. More...
 
LLVM_DUMP_METHOD void dump () const
 Dumps SMT formula. More...
 
- Public Member Functions inherited from clang::ento::SimpleConstraintManager
 SimpleConstraintManager (SubEngine *subengine, SValBuilder &SB)
 
 ~SimpleConstraintManager () override
 
ProgramStateRef assume (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. More...
 
ProgramStateRef assumeInclusiveRange (ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) override
 
- Public Member Functions inherited from clang::ento::ConstraintManager
 ConstraintManager ()=default
 
virtual ~ConstraintManager ()
 
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. More...
 
virtual ProgramStatePair assumeInclusiveRangeDual (ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, const llvm::APSInt &To)
 
virtual void EndPath (ProgramStateRef state)
 
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. More...
 

Protected Member Functions

virtual ProgramStateRef assumeExpr (ProgramStateRef State, SymbolRef Sym, const SMTExprRef &Exp)
 
virtual void addStateConstraints (ProgramStateRef State) const
 Given a program state, construct the logical conjunction and add it to the solver. More...
 
ConditionTruthVal checkModel (ProgramStateRef State, SymbolRef Sym, const SMTExprRef &Exp) const
 
- Protected Member Functions inherited from clang::ento::SimpleConstraintManager
SValBuildergetSValBuilder () const
 
BasicValueFactorygetBasicVals () const
 
SymbolManagergetSymbolManager () const
 

Protected Attributes

llvm::DenseMap< unsigned, ConditionTruthValCached
 
- Protected Attributes inherited from clang::ento::ConstraintManager
bool NotifyAssumeClients = true
 A flag to indicate that clients should be notified of assumptions. More...
 

Additional Inherited Members

- Public Types inherited from clang::ento::ConstraintManager
using ProgramStatePair = std::pair< ProgramStateRef, ProgramStateRef >
 

Detailed Description

template<typename ConstraintSMT, typename SMTExprTy>
class clang::ento::SMTConstraintManager< ConstraintSMT, SMTExprTy >

Definition at line 25 of file SMTConstraintManager.h.

Constructor & Destructor Documentation

◆ SMTConstraintManager()

template<typename ConstraintSMT , typename SMTExprTy >
clang::ento::SMTConstraintManager< ConstraintSMT, SMTExprTy >::SMTConstraintManager ( clang::ento::SubEngine SE,
clang::ento::SValBuilder SB,
SMTSolverRef S 
)
inline

Definition at line 29 of file SMTConstraintManager.h.

◆ ~SMTConstraintManager()

template<typename ConstraintSMT , typename SMTExprTy >
virtual clang::ento::SMTConstraintManager< ConstraintSMT, SMTExprTy >::~SMTConstraintManager ( )
virtualdefault

Member Function Documentation

◆ addStateConstraints()

template<typename ConstraintSMT , typename SMTExprTy >
virtual void clang::ento::SMTConstraintManager< ConstraintSMT, SMTExprTy >::addStateConstraints ( ProgramStateRef  State) const
inlineprotectedvirtual

Given a program state, construct the logical conjunction and add it to the solver.

Definition at line 284 of file SMTConstraintManager.h.

Referenced by clang::ento::SMTConstraintManager< ConstraintSMT, SMTExprTy >::checkModel(), and clang::ento::SMTConstraintManager< ConstraintSMT, SMTExprTy >::getSymVal().

◆ assumeExpr()

template<typename ConstraintSMT , typename SMTExprTy >
virtual ProgramStateRef clang::ento::SMTConstraintManager< ConstraintSMT, SMTExprTy >::assumeExpr ( ProgramStateRef  State,
SymbolRef  Sym,
const SMTExprRef Exp 
)
inlineprotectedvirtual

◆ assumeSym()

template<typename ConstraintSMT , typename SMTExprTy >
ProgramStateRef clang::ento::SMTConstraintManager< ConstraintSMT, SMTExprTy >::assumeSym ( ProgramStateRef  State,
SymbolRef  Sym,
bool  Assumption 
)
inlineoverridevirtual

◆ assumeSymInclusiveRange()

template<typename ConstraintSMT , typename SMTExprTy >
ProgramStateRef clang::ento::SMTConstraintManager< ConstraintSMT, SMTExprTy >::assumeSymInclusiveRange ( ProgramStateRef  State,
SymbolRef  Sym,
const llvm::APSInt &  From,
const llvm::APSInt &  To,
bool  InRange 
)
inlineoverridevirtual

Given a symbolic expression within the range [From, To], assume that it is true/false and generate the new program state.

This function is used to handle case ranges produced by a language extension for switch case statements.

Implements clang::ento::SimpleConstraintManager.

Definition at line 57 of file SMTConstraintManager.h.

References clang::ento::SMTConstraintManager< ConstraintSMT, SMTExprTy >::assumeExpr(), clang::ento::SimpleConstraintManager::getBasicVals(), clang::ento::BasicValueFactory::getContext(), and clang::ento::SMTConv::getRangeExpr().

◆ assumeSymUnsupported()

template<typename ConstraintSMT , typename SMTExprTy >
ProgramStateRef clang::ento::SMTConstraintManager< ConstraintSMT, SMTExprTy >::assumeSymUnsupported ( ProgramStateRef  State,
SymbolRef  Sym,
bool  Assumption 
)
inlineoverridevirtual

Given a symbolic expression that cannot be reasoned about, assume that it is zero/nonzero and add it directly to the solver state.

Implements clang::ento::SimpleConstraintManager.

Definition at line 66 of file SMTConstraintManager.h.

References State.

◆ canReasonAbout()

template<typename ConstraintSMT , typename SMTExprTy >
bool clang::ento::SMTConstraintManager< ConstraintSMT, SMTExprTy >::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 221 of file SMTConstraintManager.h.

References clang::ento::SVal::getAs(), 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(), and clang::ento::SValBuilder::makeSymbolVal().

◆ checkModel()

template<typename ConstraintSMT , typename SMTExprTy >
ConditionTruthVal clang::ento::SMTConstraintManager< ConstraintSMT, SMTExprTy >::checkModel ( ProgramStateRef  State,
SymbolRef  Sym,
const SMTExprRef Exp 
) const
inlineprotected

◆ checkNull()

template<typename ConstraintSMT , typename SMTExprTy >
ConditionTruthVal clang::ento::SMTConstraintManager< ConstraintSMT, SMTExprTy >::checkNull ( ProgramStateRef  State,
SymbolRef  Sym 
)
inlineoverridevirtual

◆ dump()

template<typename ConstraintSMT , typename SMTExprTy >
LLVM_DUMP_METHOD void clang::ento::SMTConstraintManager< ConstraintSMT, SMTExprTy >::dump ( ) const
inline

Dumps SMT formula.

Definition at line 268 of file SMTConstraintManager.h.

◆ getSymVal()

template<typename ConstraintSMT , typename SMTExprTy >
const llvm::APSInt* clang::ento::SMTConstraintManager< ConstraintSMT, SMTExprTy >::getSymVal ( ProgramStateRef  state,
SymbolRef  sym 
) const
inlineoverridevirtual

◆ print()

template<typename ConstraintSMT , typename SMTExprTy >
void clang::ento::SMTConstraintManager< ConstraintSMT, SMTExprTy >::print ( ProgramStateRef  St,
raw_ostream &  OS,
const char *  nl,
const char *  sep 
)
inlineoverridevirtual

Implements clang::ento::ConstraintManager.

Definition at line 208 of file SMTConstraintManager.h.

◆ removeDeadBindings()

template<typename ConstraintSMT , typename SMTExprTy >
ProgramStateRef clang::ento::SMTConstraintManager< ConstraintSMT, SMTExprTy >::removeDeadBindings ( ProgramStateRef  state,
SymbolReaper SymReaper 
)
inlineoverridevirtual

Scan all symbols referenced by the constraints.

If the symbol is not alive, remove it.

Implements clang::ento::ConstraintManager.

Definition at line 195 of file SMTConstraintManager.h.

References clang::ento::SymbolReaper::isDead().

Member Data Documentation

◆ Cached

template<typename ConstraintSMT , typename SMTExprTy >
llvm::DenseMap<unsigned, ConditionTruthVal> clang::ento::SMTConstraintManager< ConstraintSMT, SMTExprTy >::Cached
mutableprotected

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