CoreEngine - Implements the core logic of the graph-reachability analysis. More...

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

Public Types
using	BlocksExhausted
using	BlocksAborted

Public Member Functions
	CoreEngine (ExprEngine &exprengine, FunctionSummariesTy *FS, AnalyzerOptions &Opts)
	Construct a CoreEngine object to analyze the provided CFG.
	CoreEngine (const CoreEngine &)=delete
CoreEngine &	operator= (const CoreEngine &)=delete
ExplodedGraph &	getGraph ()
	getGraph - Returns the exploded graph.
bool	ExecuteWorkList (const StackFrame *SF, unsigned Steps, ProgramStateRef InitState)
	ExecuteWorkList - Run the worklist algorithm for a maximum number of steps.
void	dispatchWorkItem (ExplodedNode *Pred, ProgramPoint Loc, const WorkListUnit &WU)
	Dispatch the work list item based on the given location information.
bool	wasBlockAborted () const
bool	wasBlocksExhausted () const
bool	hasExploredAllPaths () const
void	addAbortedBlock (const ExplodedNode node, const CFGBlock block)
	Inform the CoreEngine that a basic block was aborted because it could not be completely analyzed.
WorkList *	getWorkList () const
WorkList *	getCTUWorkList () const
auto	exhausted_blocks () const
auto	aborted_blocks () const
ExplodedNode *	makeNode (const ProgramPoint &Loc, ProgramStateRef State, ExplodedNode *Pred, bool MarkAsSink=false) const
ExplodedNode *	makePostStmtNode (const Stmt S, ProgramStateRef State, ExplodedNode Pred, bool MarkAsSink=false) const
ExplodedNode *	makeNodeWithBinding (ExplodedNode Pred, const Expr E, SVal V, ProgramStateRef State, ProgramPoint::Kind K=ProgramPoint::PostStmtKind) const
ExplodedNode *	makeNodeWithBinding (ExplodedNode Pred, const Expr E, SVal V, ProgramPoint::Kind K=ProgramPoint::PostStmtKind) const
void	enqueue (ExplodedNodeSet &Set)
	Enqueue the given set of nodes onto the work list.
void	enqueueStmtNodes (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, const ReturnStmt *RS)
	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.
DataTag::Factory &	getDataTags ()

Friends
class	ExprEngine

Detailed Description

CoreEngine - Implements the core logic of the graph-reachability analysis.

It traverses the CFG and generates the ExplodedGraph.

Definition at line 50 of file CoreEngine.h.

Member Typedef Documentation

◆ BlocksAborted

using clang::ento::CoreEngine::BlocksAborted

Initial value:

std::vector<std::pair<const CFGBlock *, const ExplodedNode *>>

Definition at line 57 of file CoreEngine.h.

◆ BlocksExhausted

using clang::ento::CoreEngine::BlocksExhausted

Initial value:

std::vector<std::pair<BlockEntrance, const ExplodedNode *>>

Definition at line 54 of file CoreEngine.h.

Constructor & Destructor Documentation

◆ CoreEngine() [1/2]

CoreEngine::CoreEngine	(	ExprEngine &	exprengine,
		FunctionSummariesTy *	FS,
		AnalyzerOptions &	Opts )

Construct a CoreEngine object to analyze the provided CFG.

Definition at line 74 of file CoreEngine.cpp.

References ExprEngine, generateWorkList(), and clang::nullptr.

Referenced by CoreEngine(), and operator=().

◆ CoreEngine() [2/2]

clang::ento::CoreEngine::CoreEngine ( const CoreEngine & )

delete

References CoreEngine().

Member Function Documentation

◆ aborted_blocks()

auto clang::ento::CoreEngine::aborted_blocks ( ) const

inline

Definition at line 172 of file CoreEngine.h.

◆ addAbortedBlock()

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 161 of file CoreEngine.h.

◆ dispatchWorkItem()

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 214 of file CoreEngine.cpp.

References clang::ProgramPoint::BlockEdgeKind, clang::ProgramPoint::BlockEntranceKind, clang::ProgramPoint::BlockExitKind, clang::ProgramPoint::CallEnterKind, clang::ProgramPoint::CallExitBeginKind, clang::ento::SVal::castAs(), dispatchWorkItem(), clang::ProgramPoint::EpsilonKind, clang::ento::SVal::getAs(), clang::ento::WorkListUnit::getBlock(), clang::ento::ExplodedNode::getFirstPred(), clang::ento::WorkListUnit::getIndex(), clang::ento::SVal::getKind(), clang::ento::ExplodedNode::getLocation(), clang::ento::ExplodedNode::getStackFrame(), clang::ento::ExplodedNode::hasSinglePred(), timeTraceMetadata(), and timeTraceScopeName().

Referenced by dispatchWorkItem(), and ExecuteWorkList().

◆ enqueue()

void CoreEngine::enqueue ( ExplodedNodeSet & Set )

Enqueue the given set of nodes onto the work list.

Definition at line 646 of file CoreEngine.cpp.

References clang::Set.

Referenced by ExecuteWorkList().

◆ enqueueEndOfFunction()

void CoreEngine::enqueueEndOfFunction	(	ExplodedNodeSet &	Set,
		const ReturnStmt *	RS )

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

Definition at line 657 of file CoreEngine.cpp.

References clang::StackFrame::getParent(), makeNode(), and clang::Set.

◆ enqueueStmtNode()

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

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

Definition at line 574 of file CoreEngine.cpp.

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

Referenced by enqueueStmtNodes().

◆ enqueueStmtNodes()

void CoreEngine::enqueueStmtNodes	(	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 651 of file CoreEngine.cpp.

References clang::Block, enqueueStmtNode(), and clang::Set.

◆ ExecuteWorkList()

bool CoreEngine::ExecuteWorkList	(	const StackFrame *	SF,
		unsigned	Steps,
		ProgramStateRef	InitState )

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 87 of file CoreEngine.cpp.

References dispatchWorkItem(), clang::CFGBlock::empty(), enqueue(), clang::ento::WorkListUnit::getBlockCounter(), clang::CFGBlock::getBlockID(), clang::StackFrame::getCFG(), clang::StackFrame::getDecl(), clang::ento::ExplodedNode::getLocation(), clang::ento::WorkListUnit::getNode(), clang::CFG::getNumBlockIDs(), clang::ento::ExplodedNode::getStackFrame(), clang::CFGBlock::succ_begin(), and clang::CFGBlock::succ_size().

◆ exhausted_blocks()

auto clang::ento::CoreEngine::exhausted_blocks ( ) const

inline

Definition at line 168 of file CoreEngine.h.

◆ getCTUWorkList()

WorkList * clang::ento::CoreEngine::getCTUWorkList ( ) const

inline

Definition at line 166 of file CoreEngine.h.

Referenced by REGISTER_MAP_WITH_PROGRAMSTATE().

◆ getDataTags()

DataTag::Factory & clang::ento::CoreEngine::getDataTags ( )

inline

Definition at line 215 of file CoreEngine.h.

◆ getGraph()

ExplodedGraph & clang::ento::CoreEngine::getGraph ( )

inline

getGraph - Returns the exploded graph.

Definition at line 139 of file CoreEngine.h.

◆ getWorkList()

WorkList * clang::ento::CoreEngine::getWorkList ( ) const

inline

Definition at line 165 of file CoreEngine.h.

Referenced by REGISTER_MAP_WITH_PROGRAMSTATE().

◆ hasExploredAllPaths()

bool clang::ento::CoreEngine::hasExploredAllPaths ( ) const

inline

Definition at line 154 of file CoreEngine.h.

References wasBlockAborted(), and wasBlocksExhausted().

◆ makeNode()

ExplodedNode * CoreEngine::makeNode	(	const ProgramPoint &	Loc,
		ProgramStateRef	State,
		ExplodedNode *	Pred,
		bool	MarkAsSink = false ) const

Definition at line 562 of file CoreEngine.cpp.

References clang::ento::ExplodedNode::addPredecessor().

Referenced by enqueueEndOfFunction(), enqueueStmtNode(), makeNodeWithBinding(), makePostStmtNode(), REGISTER_TRAIT_WITH_PROGRAMSTATE(), and REGISTER_TRAIT_WITH_PROGRAMSTATE().

◆ makeNodeWithBinding() [1/2]

ExplodedNode * clang::ento::CoreEngine::makeNodeWithBinding	(	ExplodedNode *	Pred,
		const Expr *	E,
		SVal	V,
		ProgramPoint::Kind	K = ProgramPoint::PostStmtKind ) const

inline

Definition at line 195 of file CoreEngine.h.

References clang::ento::ExplodedNode::getState(), makeNodeWithBinding(), clang::ProgramPoint::PostStmtKind, and V.

◆ makeNodeWithBinding() [2/2]

ExplodedNode * clang::ento::CoreEngine::makeNodeWithBinding	(	ExplodedNode *	Pred,
		const Expr *	E,
		SVal	V,
		ProgramStateRef	State,
		ProgramPoint::Kind	K = ProgramPoint::PostStmtKind ) const

inline

Definition at line 185 of file CoreEngine.h.

References clang::ProgramPoint::getProgramPoint(), clang::ento::ExplodedNode::getStackFrame(), makeNode(), clang::ProgramPoint::PostStmtKind, and V.

Referenced by makeNodeWithBinding().

◆ makePostStmtNode()

ExplodedNode * clang::ento::CoreEngine::makePostStmtNode	(	const Stmt *	S,
		ProgramStateRef	State,
		ExplodedNode *	Pred,
		bool	MarkAsSink = false ) const

inline

Definition at line 177 of file CoreEngine.h.

References clang::ento::ExplodedNode::getStackFrame(), and makeNode().

◆ operator=()

CoreEngine & clang::ento::CoreEngine::operator= ( const CoreEngine & )

delete

References CoreEngine().

◆ wasBlockAborted()

bool clang::ento::CoreEngine::wasBlockAborted ( ) const

inline

Definition at line 152 of file CoreEngine.h.

Referenced by hasExploredAllPaths().

◆ wasBlocksExhausted()

bool clang::ento::CoreEngine::wasBlocksExhausted ( ) const

inline

Definition at line 153 of file CoreEngine.h.

Referenced by hasExploredAllPaths().

◆ ExprEngine

friend class ExprEngine

friend

Definition at line 51 of file CoreEngine.h.

References ExprEngine.

Referenced by CoreEngine(), and ExprEngine.

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

include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h
lib/StaticAnalyzer/Core/CoreEngine.cpp

Public Types

Public Member Functions

Friends

Detailed Description

Member Typedef Documentation

◆ BlocksAborted

◆ BlocksExhausted

Constructor & Destructor Documentation

◆ CoreEngine() [1/2]

◆ CoreEngine() [2/2]

Member Function Documentation

◆ aborted_blocks()

◆ addAbortedBlock()

◆ dispatchWorkItem()

◆ enqueue()

◆ enqueueEndOfFunction()

◆ enqueueStmtNode()

◆ enqueueStmtNodes()

◆ ExecuteWorkList()

◆ exhausted_blocks()

◆ getCTUWorkList()

◆ getDataTags()

◆ getGraph()

◆ getWorkList()

◆ hasExploredAllPaths()

◆ makeNode()

◆ makeNodeWithBinding() [1/2]

◆ makeNodeWithBinding() [2/2]

◆ makePostStmtNode()

◆ operator=()

◆ wasBlockAborted()

◆ wasBlocksExhausted()

Friends And Related Symbol Documentation

◆ ExprEngine