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

Inheritance diagram for clang::ento::SMTConstraintManager:

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<typename AssumeFunction >
ProgramStatePair	assumeDualImpl (ProgramStateRef &State, AssumeFunction &Assume)

Protected Attributes
llvm::DenseMap< unsigned, ConditionTruthVal >	Cached

Protected Attributes inherited from clang::ento::ConstraintManager
AssumeStackTy	AssumeStack

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

Detailed Description

Definition at line 31 of file SMTConstraintManager.h.

Constructor & Destructor Documentation

◆ SMTConstraintManager()

clang::ento::SMTConstraintManager::SMTConstraintManager	(	clang::ento::ExprEngine *	EE,
		clang::ento::SValBuilder &	SB
	)

inline

Definition at line 35 of file SMTConstraintManager.h.

◆ ~SMTConstraintManager()

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

virtualdefault

Member Function Documentation

◆ addStateConstraints()

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

inlineprotectedvirtual

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

Definition at line 312 of file SMTConstraintManager.h.

Referenced by checkModel(), and getSymVal().

◆ assumeExpr()

virtual ProgramStateRef clang::ento::SMTConstraintManager::assumeExpr	(	ProgramStateRef	State,
		SymbolRef	Sym,
		const llvm::SMTExprRef &	Exp
	)

inlineprotectedvirtual

Definition at line 301 of file SMTConstraintManager.h.

References checkModel().

Referenced by assumeSym(), and assumeSymInclusiveRange().

◆ assumeSym()

ProgramStateRef clang::ento::SMTConstraintManager::assumeSym	(	ProgramStateRef	State,
		SymbolRef	Sym,
		bool	Assumption
	)

inlineoverridevirtual

Given a symbolic expression that can be reasoned about, assume that it is true/false and generate the new program state.

Implements clang::ento::SimpleConstraintManager.

Definition at line 47 of file SMTConstraintManager.h.

References assumeExpr(), clang::ento::SimpleConstraintManager::getBasicVals(), clang::ento::BasicValueFactory::getContext(), clang::ento::SMTConv::getExpr(), clang::ento::SMTConv::getZeroExpr(), and clang::Type::isBooleanType().

◆ assumeSymInclusiveRange()

ProgramStateRef clang::ento::SMTConstraintManager::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 67 of file SMTConstraintManager.h.

References assumeExpr(), clang::ento::SimpleConstraintManager::getBasicVals(), clang::ento::BasicValueFactory::getContext(), and clang::ento::SMTConv::getRangeExpr().

◆ assumeSymUnsupported()

ProgramStateRef clang::ento::SMTConstraintManager::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 76 of file SMTConstraintManager.h.

◆ 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 250 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()

ConditionTruthVal clang::ento::SMTConstraintManager::checkModel	(	ProgramStateRef	State,
		SymbolRef	Sym,
		const llvm::SMTExprRef &	Exp
	)		const

inlineprotected

Definition at line 331 of file SMTConstraintManager.h.

References addStateConstraints(), Cached, and ID.

Referenced by assumeExpr(), and checkNull().

◆ checkNull()

ConditionTruthVal clang::ento::SMTConstraintManager::checkNull	(	ProgramStateRef	State,
		SymbolRef	Sym
	)

inlineoverridevirtual

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

Reimplemented from clang::ento::ConstraintManager.

Definition at line 86 of file SMTConstraintManager.h.

References checkModel(), clang::ento::SimpleConstraintManager::getBasicVals(), clang::ento::BasicValueFactory::getContext(), clang::ento::SMTConv::getExpr(), clang::ento::SMTConv::getZeroExpr(), clang::ento::ConditionTruthVal::isConstrainedFalse(), and clang::ento::ConditionTruthVal::isConstrainedTrue().

◆ dump()

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

inline

Dumps SMT formula.

Definition at line 297 of file SMTConstraintManager.h.

◆ 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 114 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::SimpleConstraintManager::getBasicVals(), clang::ento::BasicValueFactory::getContext(), getSymVal(), clang::ento::SymExpr::getType(), clang::ASTContext::getTypeSize(), clang::Type::isBooleanType(), clang::Type::isRealFloatingType(), clang::Type::isSignedIntegerOrEnumerationType(), and clang::Type::isVoidType().

Referenced by getSymVal().

◆ haveEqualConstraints()

bool clang::ento::SMTConstraintManager::haveEqualConstraints	(	ProgramStateRef	S1,
		ProgramStateRef	S2
	)		const

inlineoverridevirtual

Implements clang::ento::ConstraintManager.

Definition at line 245 of file SMTConstraintManager.h.

◆ printJson()

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

inlineoverridevirtual

Implements clang::ento::ConstraintManager.

Definition at line 217 of file SMTConstraintManager.h.

◆ removeDeadBindings()

ProgramStateRef clang::ento::SMTConstraintManager::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 204 of file SMTConstraintManager.h.

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

Member Data Documentation

◆ Cached

llvm::DenseMap<unsigned, ConditionTruthVal> clang::ento::SMTConstraintManager::Cached

mutableprotected

Definition at line 358 of file SMTConstraintManager.h.

Referenced by checkModel().

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

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

Public Member Functions

Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ SMTConstraintManager()

◆ ~SMTConstraintManager()

Member Function Documentation

◆ addStateConstraints()

◆ assumeExpr()

◆ assumeSym()

◆ assumeSymInclusiveRange()

◆ assumeSymUnsupported()

◆ canReasonAbout()

◆ checkModel()

◆ checkNull()

◆ dump()

◆ getSymVal()

◆ haveEqualConstraints()

◆ printJson()

◆ removeDeadBindings()

Member Data Documentation

◆ Cached