#include <CoreEngine.h>

Public Types
typedef std::vector< std::pair < BlockEdge, const ExplodedNode * > >	BlocksExhausted
typedef std::vector< std::pair < const CFGBlock , const ExplodedNode > >	BlocksAborted
Public Member Functions
	CoreEngine (SubEngine &subengine, FunctionSummariesTy *FS)
	Construct a CoreEngine object to analyze the provided CFG.
ExplodedGraph &	getGraph ()
	getGraph - Returns the exploded graph.
bool	ExecuteWorkList (const LocationContext *L, unsigned Steps, ProgramStateRef InitState)
	ExecuteWorkList - Run the worklist algorithm for a maximum number of steps.
bool	ExecuteWorkListWithInitialState (const LocationContext *L, unsigned Steps, ProgramStateRef InitState, ExplodedNodeSet &Dst)
	Returns true if there is still simulation state on the worklist.
void	dispatchWorkItem (ExplodedNode *Pred, ProgramPoint Loc, const WorkListUnit &WU)
bool	wasBlockAborted () const
bool	wasBlocksExhausted () const
bool	hasWorkRemaining () const
void	addAbortedBlock (const ExplodedNode node, const CFGBlock block)
WorkList *	getWorkList () const
BlocksExhausted::const_iterator	blocks_exhausted_begin () const
BlocksExhausted::const_iterator	blocks_exhausted_end () const
BlocksAborted::const_iterator	blocks_aborted_begin () const
BlocksAborted::const_iterator	blocks_aborted_end () const
void	enqueue (ExplodedNodeSet &Set)
	Enqueue the given set of nodes onto the work list.
void	enqueue (ExplodedNodeSet &Set, const CFGBlock *Block, unsigned Idx)
	Enqueue nodes that were created as a result of processing a statement onto the work list.
void	enqueueEndOfFunction (ExplodedNodeSet &Set)
	enqueue the nodes corresponding to the end of function onto the end of path / work list.
void	enqueueStmtNode (ExplodedNode N, const CFGBlock Block, unsigned Idx)
	Enqueue a single node created as a result of statement processing.
Friends
struct	NodeBuilderContext
class	NodeBuilder
class	ExprEngine
class	CommonNodeBuilder
class	IndirectGotoNodeBuilder
class	SwitchNodeBuilder
class	EndOfFunctionNodeBuilder

Detailed Description

CoreEngine - Implements the core logic of the graph-reachability analysis. It traverses the CFG and generates the ExplodedGraph. Program "states" are treated as opaque void pointers. The template class CoreEngine (which subclasses CoreEngine) provides the matching component to the engine that knows the actual types for states. Note that this engine only dispatches to transfer functions at the statement and block-level. The analyses themselves must implement any transfer function logic and the sub-expression level (if any).

Definition at line 43 of file CoreEngine.h.

Member Typedef Documentation

typedef std::vector<std::pair<const CFGBlock*, const ExplodedNode*> > clang::ento::CoreEngine::BlocksAborted

Definition at line 56 of file CoreEngine.h.

typedef std::vector<std::pair<BlockEdge, const ExplodedNode*> > clang::ento::CoreEngine::BlocksExhausted

Definition at line 53 of file CoreEngine.h.

Constructor & Destructor Documentation

clang::ento::CoreEngine::CoreEngine	(	SubEngine &	subengine,
		FunctionSummariesTy *	FS
	)		`[inline]`

Construct a CoreEngine object to analyze the provided CFG.

Definition at line 113 of file CoreEngine.h.

Member Function Documentation

void clang::ento::CoreEngine::addAbortedBlock	(	const ExplodedNode *	node,
		const CFGBlock *	block
	)		`[inline]`

Inform the CoreEngine that a basic block was aborted because it could not be completely analyzed.

Definition at line 144 of file CoreEngine.h.

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

BlocksAborted::const_iterator clang::ento::CoreEngine::blocks_aborted_begin ( ) const [inline]

Definition at line 156 of file CoreEngine.h.

BlocksAborted::const_iterator clang::ento::CoreEngine::blocks_aborted_end ( ) const [inline]

Definition at line 159 of file CoreEngine.h.

BlocksExhausted::const_iterator clang::ento::CoreEngine::blocks_exhausted_begin ( ) const [inline]

Definition at line 150 of file CoreEngine.h.

BlocksExhausted::const_iterator clang::ento::CoreEngine::blocks_exhausted_end ( ) const [inline]

Definition at line 153 of file CoreEngine.h.

void CoreEngine::dispatchWorkItem	(	ExplodedNode *	Pred,
		ProgramPoint	Loc,
		const WorkListUnit &	WU
	)

Dispatch the work list item based on the given location information. Use Pred parameter as the predecessor state.

Definition at line 229 of file CoreEngine.cpp.

void CoreEngine::enqueue ( ExplodedNodeSet & Set )

Enqueue the given set of nodes onto the work list.

Definition at line 591 of file CoreEngine.cpp.

References clang::ento::ExplodedNodeSet::begin(), and clang::ento::ExplodedNodeSet::end().

Referenced by clang::ento::ExprEngine::ProcessImplicitDtor(), clang::ento::ExprEngine::ProcessInitializer(), clang::ento::ExprEngine::ProcessNewAllocator(), and clang::ento::ExprEngine::ProcessStmt().

void CoreEngine::enqueue	(	ExplodedNodeSet &	Set,
		const CFGBlock *	Block,
		unsigned	Idx
	)

Enqueue nodes that were created as a result of processing a statement onto the work list.

Definition at line 598 of file CoreEngine.cpp.

References clang::ento::ExplodedNodeSet::begin(), and clang::ento::ExplodedNodeSet::end().

void CoreEngine::enqueueEndOfFunction ( ExplodedNodeSet & Set )

enqueue the nodes corresponding to the end of function onto the end of path / work list.

Definition at line 606 of file CoreEngine.cpp.

References clang::ento::ExplodedNodeSet::begin(), clang::ento::ExplodedNodeSet::end(), clang::ento::ExplodedNode::getLocationContext(), and clang::LocationContext::getParent().

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

void CoreEngine::enqueueStmtNode	(	ExplodedNode *	N,
		const CFGBlock *	Block,
		unsigned	Idx
	)

Enqueue a single node created as a result of statement processing.

Definition at line 527 of file CoreEngine.cpp.

References clang::ento::ExplodedNode::addPredecessor(), clang::CFGElement::castAs(), clang::ProgramPoint::getAs(), getKind(), clang::ento::ExplodedNode::getLocation(), clang::ento::ExplodedNode::getLocationContext(), clang::ento::ExplodedNode::getState(), clang::CFGStmt::getStmt(), clang::ento::ExplodedNode::isSink(), clang::CFGElement::NewAllocator, and clang::ProgramPoint::withTag().

bool CoreEngine::ExecuteWorkList	(	const LocationContext *	L,
		unsigned	Steps,
		ProgramStateRef	InitState
	)

ExecuteWorkList - Run the worklist algorithm for a maximum number of steps.

ExecuteWorkList - Run the worklist algorithm for a maximum number of steps. Returns true if there is still simulation state on the worklist.

Definition at line 165 of file CoreEngine.cpp.

References clang::CFGBlock::empty(), clang::ento::WorkListUnit::getBlockCounter(), clang::CFGBlock::getBlockID(), clang::LocationContext::getCFG(), clang::LocationContext::getDecl(), clang::CFG::getEntry(), clang::ento::ExplodedNode::getLocation(), clang::ento::WorkListUnit::getNode(), clang::CFG::getNumBlockIDs(), Node, clang::CFGBlock::succ_begin(), and clang::CFGBlock::succ_size().

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

bool CoreEngine::ExecuteWorkListWithInitialState	(	const LocationContext *	L,
		unsigned	Steps,
		ProgramStateRef	InitState,
		ExplodedNodeSet &	Dst
	)

Returns true if there is still simulation state on the worklist.

Definition at line 272 of file CoreEngine.cpp.

References clang::ento::ExplodedNodeSet::Add().

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

ExplodedGraph& clang::ento::CoreEngine::getGraph ( ) [inline]

getGraph - Returns the exploded graph.

Definition at line 118 of file CoreEngine.h.

WorkList* clang::ento::CoreEngine::getWorkList ( ) const [inline]

Definition at line 148 of file CoreEngine.h.

Referenced by clang::ento::ExprEngine::hasEmptyWorkList(), clang::ento::ExprEngine::processCallEnter(), and clang::ento::ExprEngine::processCallExit().

bool clang::ento::CoreEngine::hasWorkRemaining ( ) const [inline]

Definition at line 138 of file CoreEngine.h.

References wasBlockAborted(), and wasBlocksExhausted().

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

bool clang::ento::CoreEngine::wasBlockAborted ( ) const [inline]

Definition at line 136 of file CoreEngine.h.

Referenced by hasWorkRemaining().

bool clang::ento::CoreEngine::wasBlocksExhausted ( ) const [inline]

Definition at line 137 of file CoreEngine.h.

Referenced by hasWorkRemaining(), and clang::ento::ExprEngine::wasBlocksExhausted().

Friends And Related Function Documentation

friend class CommonNodeBuilder [friend]

Definition at line 47 of file CoreEngine.h.

friend class EndOfFunctionNodeBuilder [friend]

Definition at line 50 of file CoreEngine.h.

friend class ExprEngine [friend]

Definition at line 46 of file CoreEngine.h.

friend class IndirectGotoNodeBuilder [friend]

Definition at line 48 of file CoreEngine.h.

friend class NodeBuilder [friend]

Definition at line 45 of file CoreEngine.h.

friend struct NodeBuilderContext [friend]

Definition at line 44 of file CoreEngine.h.

friend class SwitchNodeBuilder [friend]

Definition at line 49 of file CoreEngine.h.

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

Public Types

Public Member Functions

Friends

Detailed Description

Member Typedef Documentation

Constructor & Destructor Documentation

Member Function Documentation

Friends And Related Function Documentation