#include <ProgSlice.h>

Public Types
typedef Set< const SVFGNode * >	SVFGNodeSet

typedef SVFGNodeSet::const_iterator	SVFGNodeSetIter

typedef SaberCondAllocator::Condition	Condition

typedef Map< const SVFGNode *, Condition >	SVFGNodeToCondMap
	map a SVFGNode to its condition during value-flow guard computation More...

typedef FIFOWorkList< const SVFGNode * >	VFWorkList
	worklist for value-flow guard computation More...

typedef FIFOWorkList< const SVFBasicBlock * >	CFWorkList
	worklist for control-flow guard computation More...

typedef SaberCondAllocator::SVFGNodeToSVFGNodeSetMap	SVFGNodeToSVFGNodeSetMap

Public Member Functions
	ProgSlice (const SVFGNode src, SaberCondAllocator pa, const SVFG *graph)
	Constructor. More...

virtual	~ProgSlice ()
	Destructor. More...

u32_t	getForwardSliceSize () const

u32_t	getBackwardSliceSize () const

void	addToForwardSlice (const SVFGNode *node)
	Forward and backward slice operations. More...

void	addToBackwardSlice (const SVFGNode *node)

bool	inForwardSlice (const SVFGNode *node)

bool	inBackwardSlice (const SVFGNode *node)

SVFGNodeSetIter	forwardSliceBegin () const

SVFGNodeSetIter	forwardSliceEnd () const

SVFGNodeSetIter	backwardSliceBegin () const

SVFGNodeSetIter	backwardSliceEnd () const

const SVFGNode *	getSource () const
	root and sink operations More...

void	addToSinks (const SVFGNode *node)

const SVFGNodeSet &	getSinks () const

SVFGNodeSetIter	sinksBegin () const

SVFGNodeSetIter	sinksEnd () const

void	setPartialReachable ()

void	setAllReachable ()

bool	setReachGlobal ()

bool	isPartialReachable () const

bool	isAllReachable () const

bool	isReachGlobal () const

bool	AllPathReachableSolve ()
	Guarded reachability solve. More...

bool	isSatisfiableForAll ()

bool	isSatisfiableForPairs ()

const CallICFGNode *	getCallSite (const SVFGEdge *edge) const
	Get callsite ID and get returnsiteID from SVFGEdge. More...

const CallICFGNode *	getRetSite (const SVFGEdge *edge) const

Condition	condAnd (const Condition &lhs, const Condition &rhs)
	Condition operations. More...

Condition	condOr (const Condition &lhs, const Condition &rhs)

Condition	condNeg (const Condition &cond)

Condition	getTrueCond () const

Condition	getFalseCond () const

std::string	dumpCond (const Condition &cond) const

std::string	evalFinalCond () const
	Evaluate final condition. More...

void	evalFinalCond2Event (GenericBug::EventStack &eventStack) const
	Add final condition to eventStack. More...

Protected Member Functions
const SVFG *	getSVFG () const

void	destroy ()
	Release memory. More...

void	clearCFCond ()
	Clear Control flow conditions before each VF computation. More...

Condition	getVFCond (const SVFGNode *node) const
	Get/set VF (value-flow) and CF (control-flow) conditions. More...

bool	setVFCond (const SVFGNode *node, const Condition &cond)

Condition	ComputeIntraVFGGuard (const SVFBasicBlock src, const SVFBasicBlock dst)
	Compute guards for value-flows. More...

Condition	ComputeInterCallVFGGuard (const SVFBasicBlock src, const SVFBasicBlock dst, const SVFBasicBlock *callBB)

Condition	ComputeInterRetVFGGuard (const SVFBasicBlock src, const SVFBasicBlock dst, const SVFBasicBlock *retBB)

bool	isEquivalentBranchCond (const Condition &lhs, const Condition &rhs) const

const SVFBasicBlock *	getSVFGNodeBB (const SVFGNode *node) const

const SVFGNode *	getCurSVFGNode () const
	Get/set current SVFG node. More...

void	setCurSVFGNode (const SVFGNode *node)

void	setFinalCond (const Condition &cond)
	Set final condition after all path reachability analysis. More...

Condition	computeInvalidCondFromRemovedSUVFEdge (const SVFGNode *cur)
	Compute invalid branch condition stemming from removed strong update value-flow edges. More...

const SVFGNodeToSVFGNodeSetMap &	getRemovedSUVFEdges () const

Private Attributes
SVFGNodeSet	forwardslice
	the forward slice More...

SVFGNodeSet	backwardslice
	the backward slice More...

SVFGNodeSet	sinks
	a set of sink nodes More...

const SVFGNode *	root
	root node on the slice More...

SVFGNodeToCondMap	svfgNodeToCondMap
	map a SVFGNode to its path condition starting from root More...

bool	partialReachable
	reachable from some paths More...

bool	fullReachable
	reachable from all paths More...

bool	reachGlob
	Whether slice reach a global. More...

SaberCondAllocator *	pathAllocator
	path condition allocator More...

const SVFGNode *	_curSVFGNode
	current svfg node during guard computation More...

Condition	finalCond
	final condition More...

const SVFG *	svfg
	SVFG. More...

Detailed Description

Definition at line 49 of file ProgSlice.h.

Member Typedef Documentation

◆ CFWorkList

typedef FIFOWorkList<const SVFBasicBlock*> SVF::ProgSlice::CFWorkList

worklist for control-flow guard computation

Definition at line 59 of file ProgSlice.h.

◆ Condition

typedef SaberCondAllocator::Condition SVF::ProgSlice::Condition

Definition at line 55 of file ProgSlice.h.

◆ SVFGNodeSet

typedef Set<const SVFGNode*> SVF::ProgSlice::SVFGNodeSet

Definition at line 53 of file ProgSlice.h.

◆ SVFGNodeSetIter

typedef SVFGNodeSet::const_iterator SVF::ProgSlice::SVFGNodeSetIter

Definition at line 54 of file ProgSlice.h.

◆ SVFGNodeToCondMap

typedef Map<const SVFGNode*, Condition> SVF::ProgSlice::SVFGNodeToCondMap

map a SVFGNode to its condition during value-flow guard computation

Definition at line 56 of file ProgSlice.h.

◆ SVFGNodeToSVFGNodeSetMap

typedef SaberCondAllocator::SVFGNodeToSVFGNodeSetMap SVF::ProgSlice::SVFGNodeToSVFGNodeSetMap

Definition at line 61 of file ProgSlice.h.

◆ VFWorkList

typedef FIFOWorkList<const SVFGNode*> SVF::ProgSlice::VFWorkList

worklist for value-flow guard computation

Definition at line 58 of file ProgSlice.h.

Constructor & Destructor Documentation

◆ ProgSlice()

SVF::ProgSlice::ProgSlice	(	const SVFGNode *	src,
		SaberCondAllocator *	pa,
		const SVFG *	graph
	)

inline

Constructor.

Definition at line 65 of file ProgSlice.h.

                                                                              :
         root(src), partialReachable(false), fullReachable(false), reachGlob(false),
         pathAllocator(pa), _curSVFGNode(nullptr), finalCond(pa->getFalseCond()), svfg(graph)
     {
     }

◆ ~ProgSlice()

virtual SVF::ProgSlice::~ProgSlice ( )

inlinevirtual

Destructor.

Definition at line 72 of file ProgSlice.h.

     {
         destroy();
     }

Member Function Documentation

◆ addToBackwardSlice()

void SVF::ProgSlice::addToBackwardSlice ( const SVFGNode * node )

inline

Definition at line 91 of file ProgSlice.h.

     {
         backwardslice.insert(node);
     }

◆ addToForwardSlice()

void SVF::ProgSlice::addToForwardSlice ( const SVFGNode * node )

inline

Forward and backward slice operations.

Definition at line 87 of file ProgSlice.h.

     {
         forwardslice.insert(node);
     }

◆ addToSinks()

void SVF::ProgSlice::addToSinks ( const SVFGNode * node )

inline

Definition at line 127 of file ProgSlice.h.

     {
         sinks.insert(node);
     }

◆ AllPathReachableSolve()

bool ProgSlice::AllPathReachableSolve ( )

Guarded reachability solve.

Compute path conditions for nodes on the backward slice path condition of each node is calculated starting from root node (source) Given a SVFGNode n, its path condition C is allocated (path_i stands for one of m program paths reaches n)

C = \bigvee Guard(path_i), 0 < i < m Guard(path_i) = \bigwedge VFGGuard(x,y), suppose (x,y) are two SVFGNode nodes on path_i

mark source node conditions to be true

clean up the control flow conditions for next round guard computation

Definition at line 43 of file ProgSlice.cpp.

 {
     const SVFGNode* source = getSource();
     VFWorkList worklist;
     worklist.push(source);
     setVFCond(source,getTrueCond());
  
     while(!worklist.empty())
     {
         const SVFGNode* node = worklist.pop();
         setCurSVFGNode(node);
  
         Condition invalidCond = computeInvalidCondFromRemovedSUVFEdge(node);
         Condition cond = getVFCond(node);
         for(SVFGNode::const_iterator it = node->OutEdgeBegin(), eit = node->OutEdgeEnd(); it!=eit; ++it)
         {
             const SVFGEdge* edge = (*it);
             const SVFGNode* succ = edge->getDstNode();
             if(inBackwardSlice(succ))
             {
                 Condition vfCond;
                 const SVFBasicBlock* nodeBB = getSVFGNodeBB(node);
                 const SVFBasicBlock* succBB = getSVFGNodeBB(succ);
                 clearCFCond();
  
                 if(edge->isCallVFGEdge())
                 {
                     vfCond = ComputeInterCallVFGGuard(nodeBB,succBB, getCallSite(edge)->getParent());
                 }
                 else if(edge->isRetVFGEdge())
                 {
                     vfCond = ComputeInterRetVFGGuard(nodeBB,succBB, getRetSite(edge)->getParent());
                 }
                 else
                     vfCond = ComputeIntraVFGGuard(nodeBB,succBB);
                 vfCond = condAnd(vfCond, condNeg(invalidCond));
                 Condition succPathCond = condAnd(cond, vfCond);
                 if(setVFCond(succ,  condOr(getVFCond(succ), succPathCond) ))
                     worklist.push(succ);
             }
  
             DBOUT(DSaber, outs() << " node (" << node->getId()  <<
                   ") --> " << "succ (" << succ->getId() << ") condition: " << getVFCond(succ) << "\n");
         }
     }
  
     return isSatisfiableForAll();
 }

◆ backwardSliceBegin()

SVFGNodeSetIter SVF::ProgSlice::backwardSliceBegin ( ) const

inline

Definition at line 111 of file ProgSlice.h.

     {
         return backwardslice.begin();
     }

◆ backwardSliceEnd()

SVFGNodeSetIter SVF::ProgSlice::backwardSliceEnd ( ) const

inline

Definition at line 115 of file ProgSlice.h.

     {
         return backwardslice.end();
     }

◆ clearCFCond()

void SVF::ProgSlice::clearCFCond ( )

inlineprotected

Clear Control flow conditions before each VF computation.

TODO: how to clean z3 memory

Definition at line 221 of file ProgSlice.h.

     {
         pathAllocator->clearCFCond();
     }

◆ ComputeInterCallVFGGuard()

Condition SVF::ProgSlice::ComputeInterCallVFGGuard	(	const SVFBasicBlock *	src,
		const SVFBasicBlock *	dst,
		const SVFBasicBlock *	callBB
	)

inlineprotected

Definition at line 256 of file ProgSlice.h.

     {
         return pathAllocator->ComputeInterCallVFGGuard(src,dst,callBB);
     }

◆ ComputeInterRetVFGGuard()

Condition SVF::ProgSlice::ComputeInterRetVFGGuard	(	const SVFBasicBlock *	src,
		const SVFBasicBlock *	dst,
		const SVFBasicBlock *	retBB
	)

inlineprotected

Definition at line 260 of file ProgSlice.h.

     {
         return pathAllocator->ComputeInterRetVFGGuard(src,dst,retBB);
     }

◆ ComputeIntraVFGGuard()

Condition SVF::ProgSlice::ComputeIntraVFGGuard	(	const SVFBasicBlock *	src,
		const SVFBasicBlock *	dst
	)

inlineprotected

Compute guards for value-flows.

Definition at line 252 of file ProgSlice.h.

     {
         return pathAllocator->ComputeIntraVFGGuard(src,dst);
     }

◆ computeInvalidCondFromRemovedSUVFEdge()

ProgSlice::Condition ProgSlice::computeInvalidCondFromRemovedSUVFEdge ( const SVFGNode * cur )

protected

Compute invalid branch condition stemming from removed strong update value-flow edges.

Compute invalid branch condition stemming from removed strong update value-flow edges

Fix issue: https://github.com/SVF-tools/SVF/issues/1306 Line 11->13 is removed due to a strong update at Line 13, which means Line 11 is unreachable to Line 13 on the value flow graph. However on the control flow graph they are still considered as reachable, making the vf guard on Line 11 -> Line 15 a true condition (should consider the infeasible branch Line 11 -> Line 13) Therefore, we collect this infeasible branch condition (condition on Line 11 -> Line 13, a == b) as an invalid condition (invalidCond), and add the negation of invalidCond when computing value flow guard starting from the source of the SU. In this example, we add a != b on Line 11 -> Line 15.

Parameters

cur	current SVFG node

Returns: invalid branch condition

Definition at line 108 of file ProgSlice.cpp.

 {
     Set<const SVFBasicBlock*> validOutBBs; // the BBs of valid successors
     for(SVFGNode::const_iterator it = cur->OutEdgeBegin(), eit = cur->OutEdgeEnd(); it!=eit; ++it)
     {
         const SVFGEdge* edge = (*it);
         const SVFGNode* succ = edge->getDstNode();
         if(inBackwardSlice(succ))
         {
             validOutBBs.insert(getSVFGNodeBB(succ));
         }
     }
     Condition invalidCond = getFalseCond();
     auto suVFEdgesIt = getRemovedSUVFEdges().find(cur);
     if (suVFEdgesIt != getRemovedSUVFEdges().end())
     {
         for (const auto &succ: suVFEdgesIt->second)
         {
             if (!validOutBBs.count(getSVFGNodeBB(succ)))
             {
                 // removed vfg node does not reside in the BBs of valid successors
                 const SVFBasicBlock *nodeBB = getSVFGNodeBB(cur);
                 const SVFBasicBlock *succBB = getSVFGNodeBB(succ);
                 clearCFCond();
                 invalidCond = condOr(invalidCond, ComputeIntraVFGGuard(nodeBB, succBB));
             }
         }
     }
     return invalidCond;
 }

◆ condAnd()

Condition SVF::ProgSlice::condAnd	(	const Condition &	lhs,
		const Condition &	rhs
	)

inline

Condition operations.

Definition at line 182 of file ProgSlice.h.

     {
         return pathAllocator->condAnd(lhs,rhs);
     }

◆ condNeg()

Condition SVF::ProgSlice::condNeg ( const Condition & cond )

inline

Definition at line 190 of file ProgSlice.h.

     {
         return pathAllocator->condNeg(cond);
     }

◆ condOr()

Condition SVF::ProgSlice::condOr	(	const Condition &	lhs,
		const Condition &	rhs
	)

inline

Definition at line 186 of file ProgSlice.h.

     {
         return pathAllocator->condOr(lhs,rhs);
     }

◆ destroy()

void ProgSlice::destroy ( )

protected

Release memory.

Definition at line 246 of file ProgSlice.cpp.

247 {

248 }

◆ dumpCond()

std::string SVF::ProgSlice::dumpCond ( const Condition & cond ) const

inline

Definition at line 202 of file ProgSlice.h.

     {
         return pathAllocator->dumpCond(cond);
     }

◆ evalFinalCond()

std::string ProgSlice::evalFinalCond ( ) const

Evaluate final condition.

Evaluate Atoms of a condition TODO: for now we only evaluate one path, evaluate every single path

Atom – a propositional variable: a, b, c Literal – an atom or its negation: a, ~a Clause – A disjunction of some literals: a \vee b CNF formula – a conjunction of some clauses: (a \vee b ) \wedge (c \vee d)

print leak path after eliminating duplicated element

Definition at line 220 of file ProgSlice.cpp.

 {
     std::string str;
     std::stringstream rawstr(str);
     Set<std::string> locations;
     NodeBS elems = pathAllocator->exactCondElem(finalCond);
  
     for(NodeBS::iterator it = elems.begin(), eit = elems.end(); it!=eit; ++it)
     {
         const ICFGNode* tinst = pathAllocator->getCondInst(*it);
         if(pathAllocator->isNegCond(*it))
             locations.insert(tinst->getSourceLoc()+"|False");
         else
             locations.insert(tinst->getSourceLoc()+"|True");
     }
  
     for(Set<std::string>::iterator iter = locations.begin(), eiter = locations.end();
             iter!=eiter; ++iter)
     {
         rawstr << "\t\t  --> (" << *iter << ") \n";
     }
  
     return rawstr.str();
 }

◆ evalFinalCond2Event()

void ProgSlice::evalFinalCond2Event ( GenericBug::EventStack & eventStack ) const

Add final condition to eventStack.

Definition at line 196 of file ProgSlice.cpp.

 {
     NodeBS elems = pathAllocator->exactCondElem(finalCond);
     for(NodeBS::iterator it = elems.begin(), eit = elems.end(); it!=eit; ++it)
     {
         const ICFGNode* tinst = pathAllocator->getCondInst(*it);
         if(pathAllocator->isNegCond(*it))
             eventStack.push_back(SVFBugEvent(
                                      SVFBugEvent::Branch|((((u32_t)false) << 4) & BRANCHFLAGMASK), tinst));
         else
             eventStack.push_back(SVFBugEvent(
                                      SVFBugEvent::Branch|((((u32_t)true) << 4) & BRANCHFLAGMASK), tinst));
     }
 }

◆ forwardSliceBegin()

SVFGNodeSetIter SVF::ProgSlice::forwardSliceBegin ( ) const

inline

Definition at line 103 of file ProgSlice.h.

     {
         return forwardslice.begin();
     }

◆ forwardSliceEnd()

SVFGNodeSetIter SVF::ProgSlice::forwardSliceEnd ( ) const

inline

Definition at line 107 of file ProgSlice.h.

     {
         return forwardslice.end();
     }

◆ getBackwardSliceSize()

u32_t SVF::ProgSlice::getBackwardSliceSize ( ) const

inline

Definition at line 81 of file ProgSlice.h.

     {
         return backwardslice.size();
     }

◆ getCallSite()

const CallICFGNode * ProgSlice::getCallSite ( const SVFGEdge * edge ) const

Get callsite ID and get returnsiteID from SVFGEdge.

Definition at line 179 of file ProgSlice.cpp.

 {
     assert(edge->isCallVFGEdge() && "not a call svfg edge?");
     if(const CallDirSVFGEdge* callEdge = SVFUtil::dyn_cast<CallDirSVFGEdge>(edge))
         return getSVFG()->getCallSite(callEdge->getCallSiteId());
     else
         return getSVFG()->getCallSite(SVFUtil::cast<CallIndSVFGEdge>(edge)->getCallSiteId());
 }

◆ getCurSVFGNode()

const SVFGNode* SVF::ProgSlice::getCurSVFGNode ( ) const

inlineprotected

Get/set current SVFG node.

Definition at line 286 of file ProgSlice.h.

     {
         return _curSVFGNode;
     }

◆ getFalseCond()

Condition SVF::ProgSlice::getFalseCond ( ) const

inline

Definition at line 198 of file ProgSlice.h.

     {
         return pathAllocator->getFalseCond();
     }

◆ getForwardSliceSize()

u32_t SVF::ProgSlice::getForwardSliceSize ( ) const

inline

Definition at line 77 of file ProgSlice.h.

     {
         return forwardslice.size();
     }

◆ getRemovedSUVFEdges()

const SVFGNodeToSVFGNodeSetMap& SVF::ProgSlice::getRemovedSUVFEdges ( ) const

inlineprotected

Definition at line 305 of file ProgSlice.h.

     {
         return pathAllocator->getRemovedSUVFEdges();
     }

◆ getRetSite()

const CallICFGNode * ProgSlice::getRetSite ( const SVFGEdge * edge ) const

Definition at line 187 of file ProgSlice.cpp.

 {
     assert(edge->isRetVFGEdge() && "not a return svfg edge?");
     if(const RetDirSVFGEdge* callEdge = SVFUtil::dyn_cast<RetDirSVFGEdge>(edge))
         return getSVFG()->getCallSite(callEdge->getCallSiteId());
     else
         return getSVFG()->getCallSite(SVFUtil::cast<RetIndSVFGEdge>(edge)->getCallSiteId());
 }

◆ getSinks()

const SVFGNodeSet& SVF::ProgSlice::getSinks ( ) const

inline

Definition at line 131 of file ProgSlice.h.

     {
         return sinks;
     }

◆ getSource()

const SVFGNode* SVF::ProgSlice::getSource ( ) const

inline

root and sink operations

Definition at line 123 of file ProgSlice.h.

     {
         return root;
     }

◆ getSVFG()

const SVFG* SVF::ProgSlice::getSVFG ( ) const

inlineprotected

Definition at line 213 of file ProgSlice.h.

     {
         return svfg;
     }

◆ getSVFGNodeBB()

const SVFBasicBlock* SVF::ProgSlice::getSVFGNodeBB ( const SVFGNode * node ) const

inlineprotected

Return the basic block where a SVFGNode resides in a SVFGNode may not in a basic block if it is not a program statement (e.g. PAGEdge is an global assignment or NullPtrSVFGNode)

Definition at line 274 of file ProgSlice.h.

     {
         const ICFGNode* icfgNode = node->getICFGNode();
         if(SVFUtil::isa<NullPtrSVFGNode>(node) == false)
         {
             return icfgNode->getBB();
         }
         return nullptr;
     }

◆ getTrueCond()

Condition SVF::ProgSlice::getTrueCond ( ) const

inline

Definition at line 194 of file ProgSlice.h.

     {
         return pathAllocator->getTrueCond();
     }

◆ getVFCond()

Condition SVF::ProgSlice::getVFCond ( const SVFGNode * node ) const

inlineprotected

Get/set VF (value-flow) and CF (control-flow) conditions.

Definition at line 229 of file ProgSlice.h.

     {
         SVFGNodeToCondMap::const_iterator it = svfgNodeToCondMap.find(node);
         if(it==svfgNodeToCondMap.end())
         {
             return getFalseCond();
         }
         return it->second;
     }

◆ inBackwardSlice()

bool SVF::ProgSlice::inBackwardSlice ( const SVFGNode * node )

inline

Definition at line 99 of file ProgSlice.h.

     {
         return backwardslice.find(node)!=backwardslice.end();
     }

◆ inForwardSlice()

bool SVF::ProgSlice::inForwardSlice ( const SVFGNode * node )

inline

Definition at line 95 of file ProgSlice.h.

     {
         return forwardslice.find(node)!=forwardslice.end();
     }

◆ isAllReachable()

bool SVF::ProgSlice::isAllReachable ( ) const

inline

Definition at line 159 of file ProgSlice.h.

     {
         return fullReachable || reachGlob;
     }

◆ isEquivalentBranchCond()

bool SVF::ProgSlice::isEquivalentBranchCond	(	const Condition &	lhs,
		const Condition &	rhs
	)		const

inlineprotected

Definition at line 266 of file ProgSlice.h.

     {
         return pathAllocator->isEquivalentBranchCond(lhs, rhs);
     };

◆ isPartialReachable()

bool SVF::ProgSlice::isPartialReachable ( ) const

inline

Definition at line 155 of file ProgSlice.h.

     {
         return partialReachable || reachGlob;
     }

◆ isReachGlobal()

bool SVF::ProgSlice::isReachGlobal ( ) const

inline

Definition at line 163 of file ProgSlice.h.

     {
         return reachGlob;
     }

◆ isSatisfiableForAll()

bool ProgSlice::isSatisfiableForAll ( )

Solve by computing disjunction of conditions from all sinks (e.g., memory leak)

Definition at line 142 of file ProgSlice.cpp.

 {
  
     Condition guard = getFalseCond();
     for(SVFGNodeSetIter it = sinksBegin(), eit = sinksEnd(); it!=eit; ++it)
     {
         guard = condOr(guard,getVFCond(*it));
     }
     setFinalCond(guard);
  
     return pathAllocator->isAllPathReachable(guard);
 }

◆ isSatisfiableForPairs()

bool ProgSlice::isSatisfiableForPairs ( )

Solve by analysing each pair of sinks (e.g., double free)

Definition at line 158 of file ProgSlice.cpp.

 {
  
     for(SVFGNodeSetIter it = sinksBegin(), eit = sinksEnd(); it!=eit; ++it)
     {
         for(SVFGNodeSetIter sit = it, esit = sinksEnd(); sit!=esit; ++sit)
         {
             if(*it == *sit)
                 continue;
             Condition guard = condAnd(getVFCond(*sit),getVFCond(*it));
             if(!isEquivalentBranchCond(guard, getFalseCond()))
             {
                 setFinalCond(guard);
                 return false;
             }
         }
     }
  
     return true;
 }

◆ setAllReachable()

void SVF::ProgSlice::setAllReachable ( )

inline

Definition at line 147 of file ProgSlice.h.

     {
         fullReachable = true;
     }

◆ setCurSVFGNode()

void SVF::ProgSlice::setCurSVFGNode ( const SVFGNode * node )

inlineprotected

Definition at line 290 of file ProgSlice.h.

     {
         _curSVFGNode = node;
         pathAllocator->setCurEvalSVFGNode(node);
     }

◆ setFinalCond()

void SVF::ProgSlice::setFinalCond ( const Condition & cond )

inlineprotected

Set final condition after all path reachability analysis.

Definition at line 297 of file ProgSlice.h.

     {
         finalCond = cond;
     }

◆ setPartialReachable()

void SVF::ProgSlice::setPartialReachable ( )

inline

Definition at line 143 of file ProgSlice.h.

     {
         partialReachable = true;
     }

◆ setReachGlobal()

bool SVF::ProgSlice::setReachGlobal ( )

inline

Definition at line 151 of file ProgSlice.h.

     {
         return reachGlob = true;
     }

◆ setVFCond()

bool SVF::ProgSlice::setVFCond	(	const SVFGNode *	node,
		const Condition &	cond
	)

inlineprotected

Definition at line 238 of file ProgSlice.h.

     {
         SVFGNodeToCondMap::iterator it = svfgNodeToCondMap.find(node);
         // until a fixed-point is reached (condition is not changed)
         if(it!=svfgNodeToCondMap.end() && isEquivalentBranchCond(it->second, cond))
             return false;
  
         svfgNodeToCondMap[node] = cond;
         return true;
     }

◆ sinksBegin()

SVFGNodeSetIter SVF::ProgSlice::sinksBegin ( ) const

inline

Definition at line 135 of file ProgSlice.h.

     {
         return sinks.begin();
     }

◆ sinksEnd()

SVFGNodeSetIter SVF::ProgSlice::sinksEnd ( ) const

inline

Definition at line 139 of file ProgSlice.h.

     {
         return sinks.end();
     }

Member Data Documentation

◆ _curSVFGNode

const SVFGNode* SVF::ProgSlice::_curSVFGNode

private

current svfg node during guard computation

Definition at line 320 of file ProgSlice.h.

◆ backwardslice

SVFGNodeSet SVF::ProgSlice::backwardslice

private

the backward slice

Definition at line 312 of file ProgSlice.h.

◆ finalCond

Condition SVF::ProgSlice::finalCond

private

final condition

Definition at line 321 of file ProgSlice.h.

◆ forwardslice

SVFGNodeSet SVF::ProgSlice::forwardslice

private

the forward slice

Definition at line 311 of file ProgSlice.h.

◆ fullReachable

bool SVF::ProgSlice::fullReachable

private

reachable from all paths

Definition at line 317 of file ProgSlice.h.

◆ partialReachable

bool SVF::ProgSlice::partialReachable

private

reachable from some paths

Definition at line 316 of file ProgSlice.h.

◆ pathAllocator

SaberCondAllocator* SVF::ProgSlice::pathAllocator

private

path condition allocator

Definition at line 319 of file ProgSlice.h.

◆ reachGlob

bool SVF::ProgSlice::reachGlob

private

Whether slice reach a global.

Definition at line 318 of file ProgSlice.h.

◆ root

const SVFGNode* SVF::ProgSlice::root

private

root node on the slice

Definition at line 314 of file ProgSlice.h.

◆ sinks

SVFGNodeSet SVF::ProgSlice::sinks

private

a set of sink nodes

Definition at line 313 of file ProgSlice.h.

◆ svfg

const SVFG* SVF::ProgSlice::svfg

private

SVFG.

Definition at line 322 of file ProgSlice.h.

◆ svfgNodeToCondMap

SVFGNodeToCondMap SVF::ProgSlice::svfgNodeToCondMap

private

map a SVFGNode to its path condition starting from root

Definition at line 315 of file ProgSlice.h.

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

/home/runner/work/SVF/SVF/svf/include/SABER/ProgSlice.h
/home/runner/work/SVF/SVF/svf/lib/SABER/ProgSlice.cpp

Public Types

Public Member Functions

Protected Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ CFWorkList

◆ Condition

◆ SVFGNodeSet

◆ SVFGNodeSetIter

◆ SVFGNodeToCondMap

◆ SVFGNodeToSVFGNodeSetMap

◆ VFWorkList

Constructor & Destructor Documentation

◆ ProgSlice()

◆ ~ProgSlice()

Member Function Documentation

◆ addToBackwardSlice()

◆ addToForwardSlice()

◆ addToSinks()

◆ AllPathReachableSolve()

◆ backwardSliceBegin()

◆ backwardSliceEnd()

◆ clearCFCond()

◆ ComputeInterCallVFGGuard()

◆ ComputeInterRetVFGGuard()

◆ ComputeIntraVFGGuard()

◆ computeInvalidCondFromRemovedSUVFEdge()

◆ condAnd()

◆ condNeg()

◆ condOr()

◆ destroy()

◆ dumpCond()

◆ evalFinalCond()

◆ evalFinalCond2Event()

◆ forwardSliceBegin()

◆ forwardSliceEnd()

◆ getBackwardSliceSize()

◆ getCallSite()

◆ getCurSVFGNode()

◆ getFalseCond()

◆ getForwardSliceSize()

◆ getRemovedSUVFEdges()

◆ getRetSite()

◆ getSinks()

◆ getSource()

◆ getSVFG()

◆ getSVFGNodeBB()

◆ getTrueCond()

◆ getVFCond()

◆ inBackwardSlice()

◆ inForwardSlice()

◆ isAllReachable()

◆ isEquivalentBranchCond()

◆ isPartialReachable()

◆ isReachGlobal()

◆ isSatisfiableForAll()

◆ isSatisfiableForPairs()

◆ setAllReachable()

◆ setCurSVFGNode()

◆ setFinalCond()

◆ setPartialReachable()

◆ setReachGlobal()

◆ setVFCond()

◆ sinksBegin()

◆ sinksEnd()

Member Data Documentation

◆ _curSVFGNode

◆ backwardslice

◆ finalCond

◆ forwardslice

◆ fullReachable

◆ partialReachable

◆ pathAllocator

◆ reachGlob

◆ root

◆ sinks

◆ svfg

◆ svfgNodeToCondMap