Solver Utilize CFLData. More...

#include <CFLSolver.h>

Inheritance diagram for SVF::POCRSolver:

Public Types
typedef std::map< const Label, NodeBS >	TypeMap

typedef std::unordered_map< NodeID, TypeMap >	DataMap

typedef DataMap::iterator	iterator

typedef DataMap::const_iterator	const_iterator

Public Types inherited from SVF::CFLSolver
typedef FIFOWorkList< const CFLEdge * >	WorkList
	Define worklist. More...

typedef CFGrammar::Production	Production

typedef CFGrammar::Symbol	Symbol

Public Member Functions
virtual void	clear ()

const_iterator	begin () const

const_iterator	end () const

iterator	begin ()

iterator	end ()

DataMap &	getSuccMap ()

DataMap &	getPredMap ()

TypeMap &	getSuccMap (const NodeID key)

TypeMap &	getPredMap (const NodeID key)

NodeBS &	getSuccs (const NodeID key, const Label ty)

NodeBS &	getPreds (const NodeID key, const Label ty)

bool	addEdge (const NodeID src, const NodeID dst, const Label ty)

NodeBS	addEdges (const NodeID src, const NodeBS &dstData, const Label ty)
	add edges and return the set of added edges (dst) for src More...

NodeBS	addEdges (const NodeBS &srcData, const NodeID dst, const Label ty)
	add edges and return the set of added edges (src) for dst More...

bool	hasEdge (const NodeID src, const NodeID dst, const Label ty)
	find src -> find src[ty] -> find dst in set More...

void	clearEdges (const NodeID key)

	POCRSolver (CFLGraph _graph, CFGrammar _grammar)

virtual	~POCRSolver ()
	Destructor. More...

virtual void	processCFLEdge (const CFLEdge *Y_edge)
	Process CFLEdge. More...

virtual void	buildCFLData ()
	Init CFLData. More...

virtual void	initialize ()
	Initialize worklist. More...

Public Member Functions inherited from SVF::CFLSolver
	CFLSolver (CFLGraph _graph, CFGrammar _grammar)

virtual	~CFLSolver ()

virtual void	solve ()
	Start solving. More...

const CFLGraph *	getGraph () const
	Return CFL Graph. More...

const CFGrammar *	getGrammar () const
	Return CFL Grammar. More...

virtual bool	pushIntoWorklist (const CFLEdge *item)

virtual bool	isWorklistEmpty ()

Protected Member Functions
bool	addPred (const NodeID key, const NodeID src, const Label ty)

bool	addSucc (const NodeID key, const NodeID dst, const Label ty)

bool	addPreds (const NodeID key, const NodeBS &data, const Label ty)

bool	addSuccs (const NodeID key, const NodeBS &data, const Label ty)

Protected Member Functions inherited from SVF::CFLSolver
const CFLEdge *	popFromWorklist ()
	Worklist operations. More...

bool	isInWorklist (const CFLEdge *item)

Protected Attributes
DataMap	succMap

DataMap	predMap

const NodeBS	emptyData

NodeBS	diff

Protected Attributes inherited from SVF::CFLSolver
CFLGraph *	graph

CFGrammar *	grammar

WorkList	worklist
	Worklist for resolution. More...

Additional Inherited Members
Static Public Attributes inherited from SVF::CFLSolver
static double	numOfChecks = 0

Detailed Description

Solver Utilize CFLData.

Definition at line 116 of file CFLSolver.h.

Member Typedef Documentation

◆ const_iterator

typedef DataMap::const_iterator SVF::POCRSolver::const_iterator

Definition at line 122 of file CFLSolver.h.

◆ DataMap

typedef std::unordered_map<NodeID, TypeMap> SVF::POCRSolver::DataMap

Definition at line 120 of file CFLSolver.h.

◆ iterator

typedef DataMap::iterator SVF::POCRSolver::iterator

Definition at line 121 of file CFLSolver.h.

◆ TypeMap

typedef std::map<const Label, NodeBS> SVF::POCRSolver::TypeMap

Definition at line 119 of file CFLSolver.h.

Constructor & Destructor Documentation

◆ POCRSolver()

SVF::POCRSolver::POCRSolver	(	CFLGraph *	_graph,
		CFGrammar *	_grammar
	)

inline

Definition at line 269 of file CFLSolver.h.

                                                       : CFLSolver(_graph, _grammar)
     {
         buildCFLData();
     }

◆ ~POCRSolver()

virtual SVF::POCRSolver::~POCRSolver ( )

inlinevirtual

Destructor.

Definition at line 274 of file CFLSolver.h.

275 {

276 }

Member Function Documentation

◆ addEdge()

bool SVF::POCRSolver::addEdge	(	const NodeID	src,
		const NodeID	dst,
		const Label	ty
	)

inline

Definition at line 215 of file CFLSolver.h.

     {
         addSucc(src, dst, ty);
         return addPred(dst, src, ty);
     }

◆ addEdges() [1/2]

NodeBS SVF::POCRSolver::addEdges	(	const NodeBS &	srcData,
		const NodeID	dst,
		const Label	ty
	)

inline

add edges and return the set of added edges (src) for dst

Definition at line 235 of file CFLSolver.h.

     {
         NodeBS newSrcs;
         if (addPreds(dst, srcData, ty))
         {
             for (const NodeID datum: srcData)
                 if (addSucc(datum, dst, ty))
                     newSrcs.set(datum);
         }
         return newSrcs;
     }

◆ addEdges() [2/2]

NodeBS SVF::POCRSolver::addEdges	(	const NodeID	src,
		const NodeBS &	dstData,
		const Label	ty
	)

inline

add edges and return the set of added edges (dst) for src

Definition at line 222 of file CFLSolver.h.

     {
         NodeBS newDsts;
         if (addSuccs(src, dstData, ty))
         {
             for (const NodeID datum: dstData)
                 if (addPred(datum, src, ty))
                     newDsts.set(datum);
         }
         return newDsts;
     }

◆ addPred()

bool SVF::POCRSolver::addPred	(	const NodeID	key,
		const NodeID	src,
		const Label	ty
	)

inlineprotected

Definition at line 131 of file CFLSolver.h.

     {
         return predMap[key][ty].test_and_set(src);
     };

◆ addPreds()

bool SVF::POCRSolver::addPreds	(	const NodeID	key,
		const NodeBS &	data,
		const Label	ty
	)

inlineprotected

Definition at line 141 of file CFLSolver.h.

     {
         if (data.empty())
             return false;
         return predMap[key][ty] |= data;                            // union of sparsebitvector (add to LHS)
     }

◆ addSucc()

bool SVF::POCRSolver::addSucc	(	const NodeID	key,
		const NodeID	dst,
		const Label	ty
	)

inlineprotected

Definition at line 136 of file CFLSolver.h.

     {
         return succMap[key][ty].test_and_set(dst);
     };

◆ addSuccs()

bool SVF::POCRSolver::addSuccs	(	const NodeID	key,
		const NodeBS &	data,
		const Label	ty
	)

inlineprotected

Definition at line 148 of file CFLSolver.h.

     {
         if (data.empty())
             return false;
         return succMap[key][ty] |= data;                            // // union of sparsebitvector (add to LHS)
     }

◆ begin() [1/2]

iterator SVF::POCRSolver::begin ( )

inline

Definition at line 173 of file CFLSolver.h.

     {
         return succMap.begin();
     }

◆ begin() [2/2]

const_iterator SVF::POCRSolver::begin ( ) const

inline

Definition at line 163 of file CFLSolver.h.

     {
         return succMap.begin();
     }

◆ buildCFLData()

void POCRSolver::buildCFLData ( )

virtual

Init CFLData.

Definition at line 132 of file CFLSolver.cpp.

 {
     for (CFLEdge* edge: graph->getCFLEdges())
         addEdge(edge->getSrcID(), edge->getDstID(), edge->getEdgeKind());
 }

◆ clear()

virtual void SVF::POCRSolver::clear ( )

inlinevirtual

Definition at line 157 of file CFLSolver.h.

     {
         succMap.clear();
         predMap.clear();
     }

◆ clearEdges()

void SVF::POCRSolver::clearEdges ( const NodeID key )

inline

Definition at line 262 of file CFLSolver.h.

     {
         succMap[key].clear();
         predMap[key].clear();
     }

◆ end() [1/2]

iterator SVF::POCRSolver::end ( )

inline

Definition at line 178 of file CFLSolver.h.

     {
         return succMap.end();
     }

◆ end() [2/2]

const_iterator SVF::POCRSolver::end ( ) const

inline

Definition at line 168 of file CFLSolver.h.

     {
         return succMap.end();
     }

◆ getPredMap() [1/2]

DataMap& SVF::POCRSolver::getPredMap ( )

inline

Definition at line 188 of file CFLSolver.h.

     {
         return predMap;
     }

◆ getPredMap() [2/2]

TypeMap& SVF::POCRSolver::getPredMap ( const NodeID key )

inline

Definition at line 198 of file CFLSolver.h.

     {
         return predMap[key];
     }

◆ getPreds()

NodeBS& SVF::POCRSolver::getPreds	(	const NodeID	key,
		const Label	ty
	)

inline

Definition at line 208 of file CFLSolver.h.

     {
         return predMap[key][ty];
     }

◆ getSuccMap() [1/2]

DataMap& SVF::POCRSolver::getSuccMap ( )

inline

Definition at line 183 of file CFLSolver.h.

     {
         return succMap;
     }

◆ getSuccMap() [2/2]

TypeMap& SVF::POCRSolver::getSuccMap ( const NodeID key )

inline

Definition at line 193 of file CFLSolver.h.

     {
         return succMap[key];
     }

◆ getSuccs()

NodeBS& SVF::POCRSolver::getSuccs	(	const NodeID	key,
		const Label	ty
	)

inline

Definition at line 203 of file CFLSolver.h.

     {
         return succMap[key][ty];
     }

◆ hasEdge()

bool SVF::POCRSolver::hasEdge	(	const NodeID	src,
		const NodeID	dst,
		const Label	ty
	)

inline

find src -> find src[ty] -> find dst in set

Definition at line 248 of file CFLSolver.h.

     {
         const_iterator iter1 = succMap.find(src);
         if (iter1 == succMap.end())
             return false;
  
         auto iter2 = iter1->second.find(ty);
         if (iter2 == iter1->second.end())
             return false;
  
         return iter2->second.test(dst);
     }

◆ initialize()

void POCRSolver::initialize ( )

virtual

Initialize worklist.

Foreach production X -> epsilon add X(i,i) if not exist to E and to worklist

Reimplemented from SVF::CFLSolver.

Reimplemented in SVF::POCRHybridSolver.

Definition at line 192 of file CFLSolver.cpp.

 {
     for(auto edge : graph->getCFLEdges())
     {
         pushIntoWorklist(edge);
     }
  
     for(const Production& prod : grammar->getEpsilonProds())
     {
         for(auto IDMap : getSuccMap())
         {
             Symbol X = grammar->getLHSSymbol(prod);
             if (addEdge(IDMap.first, IDMap.first, X))
             {
                 CFLNode* i = graph->getGNode(IDMap.first);
                 const CFLEdge* newEdge = graph->addCFLEdge(i, i, X);
                 pushIntoWorklist(newEdge);
             }
         }
     }
 }

◆ processCFLEdge()

void POCRSolver::processCFLEdge ( const CFLEdge * Y_edge )

virtual

Process CFLEdge.

For each production X -> Y add X(i,j) if not exist to E and to worklist

For each production X -> Y Z Foreach outgoing edge Z(j,k) from node j do add X(i,k) if not exist to E and to worklist

For each production X -> Z Y Foreach incoming edge Z(k,i) to node i do add X(k,j) if not exist to E and to worklist

Reimplemented from SVF::CFLSolver.

Reimplemented in SVF::POCRHybridSolver.

Definition at line 138 of file CFLSolver.cpp.

 {
     CFLNode* i = Y_edge->getSrcNode();
     CFLNode* j = Y_edge->getDstNode();
  
     Symbol Y = Y_edge->getEdgeKind();
     if (grammar->hasProdsFromSingleRHS(Y))
         for(const Production& prod : grammar->getProdsFromSingleRHS(Y))
         {
             Symbol X = grammar->getLHSSymbol(prod);
             numOfChecks++;
             if (addEdge(i->getId(), j->getId(), X))
             {
                 const CFLEdge* newEdge = graph->addCFLEdge(Y_edge->getSrcNode(), Y_edge->getDstNode(), X);
                 pushIntoWorklist(newEdge);
             }
  
         }
  
     if (grammar->hasProdsFromFirstRHS(Y))
         for(const Production& prod : grammar->getProdsFromFirstRHS(Y))
         {
             Symbol X = grammar->getLHSSymbol(prod);
             NodeBS diffDsts = addEdges(i->getId(), getSuccMap(j->getId())[grammar->getSecondRHSSymbol(prod)], X);
             numOfChecks += getSuccMap(j->getId())[grammar->getSecondRHSSymbol(prod)].count();
             for (NodeID diffDst: diffDsts)
             {
                 const CFLEdge* newEdge = graph->addCFLEdge(i, graph->getGNode(diffDst), X);
                 pushIntoWorklist(newEdge);
             }
         }
  
     if(grammar->hasProdsFromSecondRHS(Y))
         for(const Production& prod : grammar->getProdsFromSecondRHS(Y))
         {
             Symbol X = grammar->getLHSSymbol(prod);
             NodeBS diffSrcs = addEdges(getPredMap(i->getId())[grammar->getFirstRHSSymbol(prod)], j->getId(), X);
             numOfChecks += getPredMap(i->getId())[grammar->getFirstRHSSymbol(prod)].count();
             for (NodeID diffSrc: diffSrcs)
             {
                 const CFLEdge* newEdge = graph->addCFLEdge(graph->getGNode(diffSrc), j, X);
                 pushIntoWorklist(newEdge);
             }
         }
 }

Member Data Documentation

◆ diff

NodeBS SVF::POCRSolver::diff

protected

Definition at line 128 of file CFLSolver.h.

◆ emptyData

const NodeBS SVF::POCRSolver::emptyData

protected

Definition at line 127 of file CFLSolver.h.

◆ predMap

DataMap SVF::POCRSolver::predMap

protected

Definition at line 126 of file CFLSolver.h.

◆ succMap

DataMap SVF::POCRSolver::succMap

protected

Definition at line 125 of file CFLSolver.h.

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

/home/runner/work/SVF/SVF/svf/include/CFL/CFLSolver.h
/home/runner/work/SVF/SVF/svf/lib/CFL/CFLSolver.cpp

Public Types

Public Member Functions

Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ const_iterator

◆ DataMap

◆ iterator

◆ TypeMap

Constructor & Destructor Documentation

◆ POCRSolver()

◆ ~POCRSolver()

Member Function Documentation

◆ addEdge()

◆ addEdges() [1/2]

◆ addEdges() [2/2]

◆ addPred()

◆ addPreds()

◆ addSucc()

◆ addSuccs()

◆ begin() [1/2]

◆ begin() [2/2]

◆ buildCFLData()

◆ clear()

◆ clearEdges()

◆ end() [1/2]

◆ end() [2/2]

◆ getPredMap() [1/2]

◆ getPredMap() [2/2]

◆ getPreds()

◆ getSuccMap() [1/2]

◆ getSuccMap() [2/2]

◆ getSuccs()

◆ hasEdge()

◆ initialize()

◆ processCFLEdge()

Member Data Documentation

◆ diff

◆ emptyData

◆ predMap

◆ succMap