#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

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

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

typedef SaberCondAllocator::SVFGNodeToSVFGNodeSetMap	SVFGNodeToSVFGNodeSetMap

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

virtual	~ProgSlice ()
	Destructor.

u32_t	getForwardSliceSize () const

u32_t	getBackwardSliceSize () const

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

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

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.

bool	isSatisfiableForAll ()

bool	isSatisfiableForPairs ()

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

const CallICFGNode *	getRetSite (const SVFGEdge *edge) const

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

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.

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

Protected Member Functions
const SVFG *	getSVFG () const

void	destroy ()
	Release memory.

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

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

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

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

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.

void	setCurSVFGNode (const SVFGNode *node)

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

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

const SVFGNodeToSVFGNodeSetMap &	getRemovedSUVFEdges () const

Private Attributes
SVFGNodeSet	forwardslice
	the forward slice

SVFGNodeSet	backwardslice
	the backward slice

SVFGNodeSet	sinks
	a set of sink nodes

const SVFGNode *	root
	root node on the slice

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

bool	partialReachable
	reachable from some paths

bool	fullReachable
	reachable from all paths

bool	reachGlob
	Whether slice reach a global.

SaberCondAllocator *	pathAllocator
	path condition allocator

const SVFGNode *	_curSVFGNode
	current svfg node during guard computation

Condition	finalCond
	final condition

const SVFG *	svfg
	SVFG.

Detailed Description

Definition at line 48 of file ProgSlice.h.

Member Typedef Documentation

◆ CFWorkList

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

worklist for control-flow guard computation

Definition at line 58 of file ProgSlice.h.

◆ Condition

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

Definition at line 54 of file ProgSlice.h.

◆ SVFGNodeSet

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

Definition at line 52 of file ProgSlice.h.

◆ SVFGNodeSetIter

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

Definition at line 53 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 55 of file ProgSlice.h.

◆ SVFGNodeToSVFGNodeSetMap

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

Definition at line 60 of file ProgSlice.h.

◆ VFWorkList

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

worklist for value-flow guard computation

Definition at line 57 of file ProgSlice.h.

Constructor & Destructor Documentation

◆ ProgSlice()

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

inline

Constructor.

Definition at line 64 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 71 of file ProgSlice.h.

    {
        destroy();
    }

Member Function Documentation

◆ addToBackwardSlice()

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

inline

Definition at line 90 of file ProgSlice.h.

    {
        backwardslice.insert(node);
    }

◆ addToForwardSlice()

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

inline

Forward and backward slice operations.

Definition at line 86 of file ProgSlice.h.

    {
        forwardslice.insert(node);
    }

◆ addToSinks()

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

inline

Definition at line 126 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 110 of file ProgSlice.h.

    {
        return backwardslice.begin();
    }

◆ backwardSliceEnd()

SVFGNodeSetIter SVF::ProgSlice::backwardSliceEnd ( ) const

inline

Definition at line 114 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 220 of file ProgSlice.h.

    {
        pathAllocator->clearCFCond();
    }

◆ ComputeInterCallVFGGuard()

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

inlineprotected

Definition at line 255 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 259 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 251 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 181 of file ProgSlice.h.

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

◆ condNeg()

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

inline

Definition at line 189 of file ProgSlice.h.

    {
        return pathAllocator->condNeg(cond);
    }

◆ condOr()

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

inline

Definition at line 185 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 201 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 102 of file ProgSlice.h.

    {
        return forwardslice.begin();
    }

◆ forwardSliceEnd()

SVFGNodeSetIter SVF::ProgSlice::forwardSliceEnd ( ) const

inline

Definition at line 106 of file ProgSlice.h.

    {
        return forwardslice.end();
    }

◆ getBackwardSliceSize()

u32_t SVF::ProgSlice::getBackwardSliceSize ( ) const

inline

Definition at line 80 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 285 of file ProgSlice.h.

    {
        return _curSVFGNode;
    }

◆ getFalseCond()

Condition SVF::ProgSlice::getFalseCond ( ) const

inline

Definition at line 197 of file ProgSlice.h.

    {
        return pathAllocator->getFalseCond();
    }

◆ getForwardSliceSize()

u32_t SVF::ProgSlice::getForwardSliceSize ( ) const

inline

Definition at line 76 of file ProgSlice.h.

    {
        return forwardslice.size();
    }

◆ getRemovedSUVFEdges()

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

inlineprotected

Definition at line 304 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 130 of file ProgSlice.h.

    {
        return sinks;
    }

◆ getSource()

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

inline

root and sink operations

Definition at line 122 of file ProgSlice.h.

    {
        return root;
    }

◆ getSVFG()

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

inlineprotected

Definition at line 212 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. SVFStmt is an global assignment or NullPtrSVFGNode)

Definition at line 273 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 193 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 228 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 98 of file ProgSlice.h.

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

◆ inForwardSlice()

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

inline

Definition at line 94 of file ProgSlice.h.

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

◆ isAllReachable()

bool SVF::ProgSlice::isAllReachable ( ) const

inline

Definition at line 158 of file ProgSlice.h.

    {
        return fullReachable || reachGlob;
    }

◆ isEquivalentBranchCond()

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

inlineprotected

Definition at line 265 of file ProgSlice.h.

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

◆ isPartialReachable()

bool SVF::ProgSlice::isPartialReachable ( ) const

inline

Definition at line 154 of file ProgSlice.h.

    {
        return partialReachable || reachGlob;
    }

◆ isReachGlobal()

bool SVF::ProgSlice::isReachGlobal ( ) const

inline

Definition at line 162 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 146 of file ProgSlice.h.

    {
        fullReachable = true;
    }

◆ setCurSVFGNode()

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

inlineprotected

Definition at line 289 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 296 of file ProgSlice.h.

    {
        finalCond = cond;
    }

◆ setPartialReachable()

void SVF::ProgSlice::setPartialReachable ( )

inline

Definition at line 142 of file ProgSlice.h.

    {
        partialReachable = true;
    }

◆ setReachGlobal()

bool SVF::ProgSlice::setReachGlobal ( )

inline

Definition at line 150 of file ProgSlice.h.

    {
        return reachGlob = true;
    }

◆ setVFCond()

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

inlineprotected

Definition at line 237 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 134 of file ProgSlice.h.

    {
        return sinks.begin();
    }

◆ sinksEnd()

SVFGNodeSetIter SVF::ProgSlice::sinksEnd ( ) const

inline

Definition at line 138 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 319 of file ProgSlice.h.

◆ backwardslice

SVFGNodeSet SVF::ProgSlice::backwardslice

private

the backward slice

Definition at line 311 of file ProgSlice.h.

◆ finalCond

Condition SVF::ProgSlice::finalCond

private

final condition

Definition at line 320 of file ProgSlice.h.

◆ forwardslice

SVFGNodeSet SVF::ProgSlice::forwardslice

private

the forward slice

Definition at line 310 of file ProgSlice.h.

◆ fullReachable

bool SVF::ProgSlice::fullReachable

private

reachable from all paths

Definition at line 316 of file ProgSlice.h.

◆ partialReachable

bool SVF::ProgSlice::partialReachable

private

reachable from some paths

Definition at line 315 of file ProgSlice.h.

◆ pathAllocator

SaberCondAllocator* SVF::ProgSlice::pathAllocator

private

path condition allocator

Definition at line 318 of file ProgSlice.h.

◆ reachGlob

bool SVF::ProgSlice::reachGlob

private

Whether slice reach a global.

Definition at line 317 of file ProgSlice.h.

◆ root

const SVFGNode* SVF::ProgSlice::root

private

root node on the slice

Definition at line 313 of file ProgSlice.h.

◆ sinks

SVFGNodeSet SVF::ProgSlice::sinks

private

a set of sink nodes

Definition at line 312 of file ProgSlice.h.

◆ svfg

const SVFG* SVF::ProgSlice::svfg

private

SVFG.

Definition at line 321 of file ProgSlice.h.

◆ svfgNodeToCondMap

SVFGNodeToCondMap SVF::ProgSlice::svfgNodeToCondMap

private

map a SVFGNode to its path condition starting from root

Definition at line 314 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