SVF::SaberCondAllocator Class Reference

#include <SaberCondAllocator.h>

Public Types
typedef Z3Expr	Condition
typedef Map< u32_t, const ICFGNode * >	IndexToTermInstMap
	z3 condition
typedef Map< u32_t, Condition >	CondPosMap
	id to instruction map for z3
typedef Map< const SVFBasicBlock *, CondPosMap >	BBCondMap
typedef Set< const SVFBasicBlock * >	BasicBlockSet
	map bb to a Condition
typedef Map< const FunObjVar *, BasicBlockSet >	FunToExitBBsMap
	map a function to all its basic blocks calling program exit
typedef Map< const SVFBasicBlock *, Condition >	BBToCondMap
	map a basic block to its condition during control-flow guard computation
typedef FIFOWorkList< const SVFBasicBlock * >	CFWorkList
	worklist for control-flow guard computation
typedef Map< const SVFGNode *, Set< const SVFGNode * > >	SVFGNodeToSVFGNodeSetMap

Public Member Functions
	SaberCondAllocator ()
	Constructor.
virtual	~SaberCondAllocator ()
	Destructor.
std::string	getMemUsage ()
	Statistics.
u32_t	getCondNum ()
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
NodeBS	exactCondElem (const Condition &cond)
	Iterator every element of the condition.
std::string	dumpCond (const Condition &cond) const
Condition	newCond (const ICFGNode *inst)
	Allocate a new condition.
void	allocate ()
	Perform path allocation.
const ICFGNode *	getCondInst (u32_t id) const
	Get/Set instruction based on Z3 expression id.
void	setCondInst (const Condition &condition, const ICFGNode *inst)
bool	isNegCond (u32_t id) const
bool	postDominate (const SVFBasicBlock *bbKey, const SVFBasicBlock *bbValue) const
bool	dominate (const SVFBasicBlock *bbKey, const SVFBasicBlock *bbValue) const
virtual Condition	ComputeIntraVFGGuard (const SVFBasicBlock *src, const SVFBasicBlock *dst)
	Guard Computation for a value-flow (between two basic blocks).
virtual Condition	ComputeInterCallVFGGuard (const SVFBasicBlock *src, const SVFBasicBlock *dst, const SVFBasicBlock *callBB)
virtual Condition	ComputeInterRetVFGGuard (const SVFBasicBlock *src, const SVFBasicBlock *dst, const SVFBasicBlock *retBB)
virtual Condition	getPHIComplementCond (const SVFBasicBlock *BB1, const SVFBasicBlock *BB2, const SVFBasicBlock *BB0)
void	clearCFCond ()
void	setCurEvalSVFGNode (const SVFGNode *node)
	Set current value for branch condition evaluation.
const SVFGNode *	getCurEvalSVFGNode () const
	Get current value for branch condition evaluation.
void	printPathCond ()
	Print out the path condition information.
bool	isSatisfiable (const Condition &condition)
	whether condition is satisfiable
bool	isAllPathReachable (Condition &condition)
	whether condition is satisfiable for all possible boolean guards
bool	isEquivalentBranchCond (const Condition &lhs, const Condition &rhs) const
	Whether lhs and rhs are equivalent branch conditions.
ICFG *	getICFG () const
bool	setCFCond (const SVFBasicBlock *bb, const Condition &cond)
	Get/Set control-flow conditions.
Condition	getCFCond (const SVFBasicBlock *bb) const
void	setNegCondInst (const Condition &condition, const ICFGNode *inst)
	mark neg Z3 expression
SVFGNodeToSVFGNodeSetMap &	getRemovedSUVFEdges ()

Protected Attributes
BBCondMap	bbConds
	map basic block to its successors/predecessors branch conditions

Private Member Functions
virtual void	allocateForBB (const SVFBasicBlock &bb)
	Allocate path condition for every basic block.
void	setBranchCond (const SVFBasicBlock *bb, const SVFBasicBlock *succ, const Condition &cond)
	Get/Set a branch condition, and its terminator instruction.
Condition	getBranchCond (const SVFBasicBlock *bb, const SVFBasicBlock *succ) const
	Get branch condition.
Condition	getEvalBrCond (const SVFBasicBlock *bb, const SVFBasicBlock *succ)
	Get a condition, evaluate the value for conditions if necessary (e.g., testNull like express).
Condition	evaluateBranchCond (const SVFBasicBlock *bb, const SVFBasicBlock *succ)
	Evaluate branch conditions.
Condition	evaluateLoopExitBranch (const SVFBasicBlock *bb, const SVFBasicBlock *succ)
	Evaluate loop exit branch.
Condition	evaluateTestNullLikeExpr (const BranchStmt *branchStmt, const SVFBasicBlock *succ)
	Return branch condition after evaluating test null like expression.
Condition	evaluateProgExit (const BranchStmt *branchStmt, const SVFBasicBlock *succ)
	Return condition when there is a branch calls program exit.
void	collectBBCallingProgExit (const SVFBasicBlock &bb)
	Collect basic block contains program exit function call.
bool	isBBCallsProgExit (const SVFBasicBlock *bb)
bool	isEQCmp (const CmpStmt *cmp) const
	Evaluate test null/not null like expressions.
bool	isNECmp (const CmpStmt *cmp) const
	Return true if the predicate of this compare instruction is not equal.
bool	isTestNullExpr (const ICFGNode *test) const
	Return true if this is a test null expression.
bool	isTestNotNullExpr (const ICFGNode *test) const
	Return true if this is a test not null expression.
bool	isTestContainsNullAndTheValue (const CmpStmt *cmp) const
	Return true if two values on the predicate are what we want.
void	destroy ()
	Release memory.
void	extractSubConds (const Condition &condition, NodeBS &support) const
	extract subexpression from a Z3 expression

Private Attributes
FunToExitBBsMap	funToExitBBsMap
	map a function to all its basic blocks calling program exit
BBToCondMap	bbToCondMap
	map a basic block to its path condition starting from root
const SVFGNode *	curEvalSVFGNode {}
	current llvm value to evaluate branch condition when computing guards
IndexToTermInstMap	idToTermInstMap
NodeBS	negConds
	key: z3 expression id, value: instruction
std::vector< Condition >	conditionVec
	bit vector for distinguish neg
SVFGNodeToSVFGNodeSetMap	removedSUVFEdges
	a counter for fresh condition

Static Private Attributes
static u32_t	totalCondNum = 0
	vector storing z3expression

Detailed Description

SaberCondAllocator allocates conditions for each basic block of a certain CFG.

Definition at line 45 of file SaberCondAllocator.h.

Member Typedef Documentation

BasicBlockSet

typedef Set<const SVFBasicBlock*> SVF::SaberCondAllocator::BasicBlockSet

map bb to a Condition

Definition at line 54 of file SaberCondAllocator.h.

BBCondMap

typedef Map<const SVFBasicBlock*, CondPosMap > SVF::SaberCondAllocator::BBCondMap

Definition at line 53 of file SaberCondAllocator.h.

BBToCondMap

typedef Map<const SVFBasicBlock*, Condition> SVF::SaberCondAllocator::BBToCondMap

map a basic block to its condition during control-flow guard computation

Definition at line 56 of file SaberCondAllocator.h.

CFWorkList

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

worklist for control-flow guard computation

Definition at line 57 of file SaberCondAllocator.h.

Condition

typedef Z3Expr SVF::SaberCondAllocator::Condition

Definition at line 50 of file SaberCondAllocator.h.

CondPosMap

typedef Map<u32_t,Condition> SVF::SaberCondAllocator::CondPosMap

id to instruction map for z3

map a branch to its Condition

Definition at line 52 of file SaberCondAllocator.h.

FunToExitBBsMap

typedef Map<const FunObjVar*, BasicBlockSet> SVF::SaberCondAllocator::FunToExitBBsMap

map a function to all its basic blocks calling program exit

Definition at line 55 of file SaberCondAllocator.h.

IndexToTermInstMap

typedef Map<u32_t, const ICFGNode*> SVF::SaberCondAllocator::IndexToTermInstMap

z3 condition

Definition at line 51 of file SaberCondAllocator.h.

SVFGNodeToSVFGNodeSetMap

typedef Map<const SVFGNode*, Set<const SVFGNode*> > SVF::SaberCondAllocator::SVFGNodeToSVFGNodeSetMap

Definition at line 58 of file SaberCondAllocator.h.

Constructor & Destructor Documentation

SaberCondAllocator()

SaberCondAllocator::SaberCondAllocator

(

)

Constructor.

Definition at line 51 of file SaberCondAllocator.cpp.

{
 
}

~SaberCondAllocator()

virtual SVF::SaberCondAllocator::~SaberCondAllocator ( )

inlinevirtual

Destructor.

Definition at line 65 of file SaberCondAllocator.h.

    {
    }

Member Function Documentation

allocate()

void SaberCondAllocator::allocate

(

)

Perform path allocation.

Allocate path condition for each branch

Definition at line 59 of file SaberCondAllocator.cpp.

{
    DBOUT(DGENERAL, outs() << pasMsg("path condition allocation starts\n"));
 
    const CallGraph* svfirCallGraph = PAG::getPAG()->getCallGraph();
    for (const auto& item: *svfirCallGraph)
    {
        const FunObjVar *func = (item.second)->getFunction();
        if (!SVFUtil::isExtCall(func))
        {
            // Allocate conditions for a program.
            for (FunObjVar::const_bb_iterator bit = func->begin(), ebit = func->end();
                    bit != ebit; ++bit)
            {
                const SVFBasicBlock* bb = bit->second;
                collectBBCallingProgExit(*bb);
                allocateForBB(*bb);
            }
        }
    }
 
    if (Options::PrintPathCond())
        printPathCond();
 
    DBOUT(DGENERAL, outs() << pasMsg("path condition allocation ends\n"));
}

allocateForBB()

void SaberCondAllocator::allocateForBB ( const SVFBasicBlock & bb )

privatevirtual

Allocate path condition for every basic block.

Allocate conditions for a basic block and propagate its condition to its successors.

TODO: handle BranchInst and SwitchInst individually here!!

Definition at line 89 of file SaberCondAllocator.cpp.

{
 
    u32_t succ_number = bb.getNumSuccessors();
 
    // if successor number greater than 1, allocate new decision variable for successors
    if (succ_number > 1)
    {
 
        //allocate log2(num_succ) decision variables
        double num = log(succ_number) / log(2);
        u32_t bit_num = (u32_t) ceil(num);
        u32_t succ_index = 0;
        std::vector<Condition> condVec;
        for (u32_t i = 0; i < bit_num; i++)
        {
            condVec.push_back(newCond(bb.back()));
        }
 
        // iterate each successor
        for (const SVFBasicBlock* svf_succ_bb : bb.getSuccessors())
        {
            Condition path_cond = getTrueCond();

 
            // for each successor decide its bit representation
            // decide whether each bit of succ_index is 1 or 0, if (three successor) succ_index is 000 then use C1^C2^C3
            // if 001 use C1^C2^negC3
            for (u32_t j = 0; j < bit_num; j++)
            {
                //test each bit of this successor's index (binary representation)
                u32_t tool = 0x01 << j;
                if (tool & succ_index)
                {
                    path_cond = condAnd(path_cond, (condNeg(condVec.at(j))));
                }
                else
                {
                    path_cond = condAnd(path_cond, condVec.at(j));
                }
            }
            setBranchCond(&bb, svf_succ_bb, path_cond);
 
            succ_index++;
        }
 
    }
}

clearCFCond()

void SVF::SaberCondAllocator::clearCFCond ( )

inline

Definition at line 176 of file SaberCondAllocator.h.

    {
        bbToCondMap.clear();
    }

collectBBCallingProgExit()

void SaberCondAllocator::collectBBCallingProgExit ( const SVFBasicBlock & bb )

private

Collect basic block contains program exit function call.

Whether this basic block contains program exit function call

Definition at line 431 of file SaberCondAllocator.cpp.

{
 
    for (const auto& icfgNode: bb.getICFGNodeList())
    {
        if (const CallICFGNode* cs = SVFUtil::dyn_cast<CallICFGNode>(icfgNode))
            if (SVFUtil::isProgExitCall(cs))
            {
                const FunObjVar* svfun = bb.getParent();
                funToExitBBsMap[svfun].insert(&bb);
            }
    }
}

ComputeInterCallVFGGuard()

SaberCondAllocator::Condition SaberCondAllocator::ComputeInterCallVFGGuard ( const SVFBasicBlock * srcBB, const SVFBasicBlock * dstBB, const SVFBasicBlock * callBB )

virtual

Compute calling inter-procedural guards between two SVFGNodes (from caller to callee) src –c1--> callBB –true--> funEntryBB –c2--> dst the InterCallVFGGuard is c1 ^ c2

Definition at line 490 of file SaberCondAllocator.cpp.

{
    const SVFBasicBlock* funEntryBB = dstBB->getParent()->getEntryBlock();
 
    Condition c1 = ComputeIntraVFGGuard(srcBB, callBB);
    setCFCond(funEntryBB, condOr(getCFCond(funEntryBB), getCFCond(callBB)));
    Condition c2 = ComputeIntraVFGGuard(funEntryBB, dstBB);
    return condAnd(c1, c2);
}

ComputeInterRetVFGGuard()

SaberCondAllocator::Condition SaberCondAllocator::ComputeInterRetVFGGuard ( const SVFBasicBlock * srcBB, const SVFBasicBlock * dstBB, const SVFBasicBlock * retBB )

virtual

Compute return inter-procedural guards between two SVFGNodes (from callee to caller) src –c1--> funExitBB –true--> retBB –c2--> dst the InterRetVFGGuard is c1 ^ c2

Definition at line 507 of file SaberCondAllocator.cpp.

{
    const FunObjVar* parent = srcBB->getParent();
    const SVFBasicBlock* funExitBB = parent->getExitBB();
 
    Condition c1 = ComputeIntraVFGGuard(srcBB, funExitBB);
    setCFCond(retBB, condOr(getCFCond(retBB), getCFCond(funExitBB)));
    Condition c2 = ComputeIntraVFGGuard(retBB, dstBB);
    return condAnd(c1, c2);
}

ComputeIntraVFGGuard()

SaberCondAllocator::Condition SaberCondAllocator::ComputeIntraVFGGuard ( const SVFBasicBlock * srcBB, const SVFBasicBlock * dstBB )

virtual

Guard Computation for a value-flow (between two basic blocks).

Compute intra-procedural guards between two SVFGNodes (inside same function)

if the dstBB is the eligible loop exit of the current basic block we can early terminate the computation

calculate the branch condition if succ post dominate bb, then we get brCond quicker by using postDT note that we assume loop exit always post dominate loop bodys which means loops are approximated only once.

Definition at line 521 of file SaberCondAllocator.cpp.

{
 
    assert(srcBB->getParent() == dstBB->getParent() && "two basic blocks are not in the same function??");
 
    if (postDominate(dstBB, srcBB))
        return getTrueCond();
 
    CFWorkList worklist;
    worklist.push(srcBB);
    setCFCond(srcBB, getTrueCond());
 
    while (!worklist.empty())
    {
        const SVFBasicBlock* bb = worklist.pop();
        Condition cond = getCFCond(bb);

        Condition loopExitCond = evaluateLoopExitBranch(bb, dstBB);
        if (!eq(loopExitCond, Condition::nullExpr()))
            return condAnd(cond, loopExitCond);
 
        for (const SVFBasicBlock* succ : bb->getSuccessors())
        {
            Condition brCond;
            if (postDominate(succ, bb))
                brCond = getTrueCond();
            else
                brCond = getEvalBrCond(bb, succ);
 
            DBOUT(DSaber, outs() << " bb (" << bb->getName() <<
                                    ") --> " << "succ_bb (" << succ->getName() << ") condition: " << brCond << "\n");
            Condition succPathCond = condAnd(cond, brCond);
            if (setCFCond(succ, condOr(getCFCond(succ), succPathCond)))
                worklist.push(succ);
        }
    }
 
    DBOUT(DSaber, outs() << " src_bb (" << srcBB->getName() <<
                            ") --> " << "dst_bb (" << dstBB->getName() << ") condition: " << getCFCond(dstBB)
          << "\n");
 
    return getCFCond(dstBB);
}

condAnd()

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

inline

Condition operations.

Definition at line 86 of file SaberCondAllocator.h.

    {
        return Condition::AND(lhs,rhs);
    }

condNeg()

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

inline

Definition at line 94 of file SaberCondAllocator.h.

    {
        return Condition::NEG(cond);
    }

condOr()

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

inline

Definition at line 90 of file SaberCondAllocator.h.

    {
        return Condition::OR(lhs,rhs);
    }

destroy()

void SVF::SaberCondAllocator::destroy ( )

inlineprivate

Release memory.

Definition at line 292 of file SaberCondAllocator.h.

    {
 
    }

dominate()

bool SVF::SaberCondAllocator::dominate ( const SVFBasicBlock * bbKey, const SVFBasicBlock * bbValue ) const

inline

Definition at line 156 of file SaberCondAllocator.h.

    {
        const FunObjVar*  keyFunc = bbKey->getParent();
        const FunObjVar*  valueFunc = bbValue->getParent();
        bool funcEq = (keyFunc == valueFunc);
        (void)funcEq; // Suppress warning of unused variable under release build
        assert(funcEq && "two basicblocks should be in the same function!");
        return keyFunc->dominate(bbKey,bbValue);
    }

dumpCond()

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

inline

Definition at line 114 of file SaberCondAllocator.h.

    {
        return Condition::dumpStr(cond);
    }

evaluateBranchCond()

SaberCondAllocator::Condition SaberCondAllocator::evaluateBranchCond ( const SVFBasicBlock * bb, const SVFBasicBlock * succ )

private

Evaluate branch conditions.

Evaluate the branch condition

(1) Evaluate a branch when it reaches a program exit (2) Evaluate a branch when it is loop exit branch (3) Evaluate a branch when it is a test null like condition

Definition at line 302 of file SaberCondAllocator.cpp.

{
    if(bb->getNumSuccessors() == 1)
    {
        return getTrueCond();
    }
 
    assert(!bb->getICFGNodeList().empty() && "bb not empty");
    if (const ICFGNode* icfgNode = bb->back())
    {
        for (const auto &svfStmt: icfgNode->getSVFStmts())
        {
            if (const BranchStmt *branchStmt = SVFUtil::dyn_cast<BranchStmt>(svfStmt))
            {
                if (branchStmt->getNumSuccessors() == 2)
                {
                    const SVFBasicBlock* succ1 = branchStmt->getSuccessor(0)->getBB();
                    const SVFBasicBlock* succ2 = branchStmt->getSuccessor(1)->getBB();
                    bool is_succ = (succ1 == succ || succ2 == succ);
                    (void)is_succ; // Suppress warning of unused variable under release build
                    assert(is_succ && "not a successor??");
                    Condition evalLoopExit = evaluateLoopExitBranch(bb, succ);
                    if (!eq(evalLoopExit, Condition::nullExpr()))
                        return evalLoopExit;
 
                    Condition evalProgExit = evaluateProgExit(branchStmt, succ);
                    if (!eq(evalProgExit, Condition::nullExpr()))
                        return evalProgExit;
 
                    Condition evalTestNullLike = evaluateTestNullLikeExpr(branchStmt, succ);
                    if (!eq(evalTestNullLike, Condition::nullExpr()))
                        return evalTestNullLike;
                    break;
                }
            }
        }
    }
 
    return getBranchCond(bb, succ);
}

evaluateLoopExitBranch()

SaberCondAllocator::Condition SaberCondAllocator::evaluateLoopExitBranch ( const SVFBasicBlock * bb, const SVFBasicBlock * dst )

private

Evaluate loop exit branch.

Evaluate loop exit branch to be true if bb is loop header and succ is the only exit basic block outside the loop (excluding exit bbs which call program exit) for all other case, we conservatively evaluate false for now

exclude exit bb which calls program exit

if the dst dominate all other loop exit bbs, then dst can certainly be reached

Definition at line 266 of file SaberCondAllocator.cpp.

{
    const FunObjVar* svffun = bb->getParent();
    assert(svffun == dst->getParent() && "two basic blocks should be in the same function");
 
    if (svffun->isLoopHeader(bb))
    {
        Set<const SVFBasicBlock* > filteredbbs;
        std::vector<const SVFBasicBlock*> exitbbs;
        svffun->getExitBlocksOfLoop(bb,exitbbs);
        for(const SVFBasicBlock* eb : exitbbs)
        {
            if(!isBBCallsProgExit(eb))
                filteredbbs.insert(eb);
        }

        bool allPDT = true;
        for (const auto &filteredbb: filteredbbs)
        {
            if (!postDominate(dst, filteredbb))
                allPDT = false;
        }
 
        if (allPDT)
            return getTrueCond();
    }
    return Condition::nullExpr();
}

evaluateProgExit()

SaberCondAllocator::Condition SaberCondAllocator::evaluateProgExit ( const BranchStmt * branchStmt, const SVFBasicBlock * succ )

private

Return condition when there is a branch calls program exit.

Evaluate condition for program exit (e.g., exit(0))

then branch calls program exit

else branch calls program exit

no branch call program exit

Definition at line 222 of file SaberCondAllocator.cpp.

{
    const SVFBasicBlock* succ1 = branchStmt->getSuccessor(0)->getBB();
    const SVFBasicBlock* succ2 = branchStmt->getSuccessor(1)->getBB();
 
    bool branch1 = isBBCallsProgExit(succ1);
    bool branch2 = isBBCallsProgExit(succ2);

    if (branch1 && !branch2)
    {
        // succ is then branch
        if (succ1 == succ)
            return getFalseCond();
        // succ is else branch
        else
            return getTrueCond();
    }
    else if (!branch1 && branch2)
    {
        // succ is else branch
        if (succ2 == succ)
            return getFalseCond();
        // succ is then branch
        else
            return getTrueCond();
    }
    // two branches both call program exit
    else if (branch1 && branch2)
    {
        return getFalseCond();
    }
    else
        return Condition::nullExpr();
 
}

evaluateTestNullLikeExpr()

SaberCondAllocator::Condition SaberCondAllocator::evaluateTestNullLikeExpr ( const BranchStmt * branchStmt, const SVFBasicBlock * succ )

private

Return branch condition after evaluating test null like expression.

Evaluate null like expression for source-sink related bug detection in SABER

Definition at line 186 of file SaberCondAllocator.cpp.

{
 
    const SVFBasicBlock* succ1 = branchStmt->getSuccessor(0)->getBB();
 
    const ValVar* condVar = SVFUtil::cast<ValVar>(branchStmt->getCondition());
    if (condVar->isConstDataOrAggDataButNotNullPtr())
    {
        // branch condition is a constant value, return nullexpr because it cannot be test null
        //  br i1 false, label %44, label %75, !dbg !7669 { "ln": 2033, "cl": 7, "fl": "re_lexer.c" }
        return Condition::nullExpr();
    }
    if (isTestNullExpr(SVFUtil::cast<ICFGNode>(condVar->getICFGNode())))
    {
        // succ is then branch
        if (succ1 == succ)
            return getFalseCond();
        // succ is else branch
        else
            return getTrueCond();
    }
    if (isTestNotNullExpr(condVar->getICFGNode()))
    {
        // succ is then branch
        if (succ1 == succ)
            return getTrueCond();
        // succ is else branch
        else
            return getFalseCond();
    }
    return Condition::nullExpr();
}

exactCondElem()

NodeBS SVF::SaberCondAllocator::exactCondElem ( const Condition & cond )

inline

Iterator every element of the condition.

Definition at line 107 of file SaberCondAllocator.h.

    {
        NodeBS elems;
        extractSubConds(cond, elems);
        return elems;
    }

extractSubConds()

void SaberCondAllocator::extractSubConds ( const Condition & condition, NodeBS & support ) const

private

extract subexpression from a Z3 expression

Definition at line 639 of file SaberCondAllocator.cpp.

{
    if (condition.getExpr().num_args() == 1 && isNegCond(condition.id()))
    {
        support.set(condition.getExpr().id());
        return;
    }
    if (condition.getExpr().num_args() == 0)
        if (!condition.getExpr().is_true() && !condition.getExpr().is_false())
            support.set(condition.getExpr().id());
    for (u32_t i = 0; i < condition.getExpr().num_args(); ++i)
    {
        Condition expr = condition.getExpr().arg(i);
        extractSubConds(expr, support);
    }
 
}

getBranchCond()

SaberCondAllocator::Condition SaberCondAllocator::getBranchCond ( const SVFBasicBlock * bb, const SVFBasicBlock * succ ) const

private

Get branch condition.

Get a branch condition

Definition at line 142 of file SaberCondAllocator.cpp.

{
    u32_t pos = bb->getBBSuccessorPos(succ);
    if(bb->getNumSuccessors() == 1)
        return getTrueCond();
    else
    {
        BBCondMap::const_iterator it = bbConds.find(bb);
        assert(it != bbConds.end() && "basic block does not have branch and conditions??");
        CondPosMap::const_iterator cit = it->second.find(pos);
        assert(cit != it->second.end() && "no condition on the branch??");
        return cit->second;
    }
}

getCFCond()

Condition SVF::SaberCondAllocator::getCFCond ( const SVFBasicBlock * bb ) const

inline

Definition at line 224 of file SaberCondAllocator.h.

    {
        BBToCondMap::const_iterator it = bbToCondMap.find(bb);
        if(it==bbToCondMap.end())
        {
            return getFalseCond();
        }
        return it->second;
    }

getCondInst()

const ICFGNode * SVF::SaberCondAllocator::getCondInst ( u32_t id ) const

inline

Get/Set instruction based on Z3 expression id.

Definition at line 127 of file SaberCondAllocator.h.

    {
        IndexToTermInstMap::const_iterator it = idToTermInstMap.find(id);
        assert(it != idToTermInstMap.end() && "this should be a fresh condition");
        return it->second;
    }

getCondNum()

u32_t SVF::SaberCondAllocator::getCondNum ( )

inline

Definition at line 78 of file SaberCondAllocator.h.

    {
        return totalCondNum;
    }

getCurEvalSVFGNode()

const SVFGNode * SVF::SaberCondAllocator::getCurEvalSVFGNode ( ) const

inline

Get current value for branch condition evaluation.

Definition at line 186 of file SaberCondAllocator.h.

    {
        return curEvalSVFGNode;
    }

getEvalBrCond()

SaberCondAllocator::Condition SaberCondAllocator::getEvalBrCond ( const SVFBasicBlock * bb, const SVFBasicBlock * succ )

private

Get a condition, evaluate the value for conditions if necessary (e.g., testNull like express).

Definition at line 157 of file SaberCondAllocator.cpp.

{
    if (getCurEvalSVFGNode() && getCurEvalSVFGNode()->getValue())
        return evaluateBranchCond(bb, succ);
    else
        return getBranchCond(bb, succ);
}

getFalseCond()

Condition SVF::SaberCondAllocator::getFalseCond ( ) const

inline

Definition at line 102 of file SaberCondAllocator.h.

    {
        return Condition::getFalseCond();
    }

getICFG()

ICFG * SVF::SaberCondAllocator::getICFG ( ) const

inline

Definition at line 207 of file SaberCondAllocator.h.

    {
        return PAG::getPAG()->getICFG();
    }

getMemUsage()

std::string SVF::SaberCondAllocator::getMemUsage ( )

inline

Statistics.

Definition at line 70 of file SaberCondAllocator.h.

    {
        u32_t vmrss, vmsize;
        if (SVFUtil::getMemoryUsageKB(&vmrss, &vmsize))
            return std::to_string(vmsize) + "KB";
        else
            return "cannot read memory usage";
    }

getPHIComplementCond()

SaberCondAllocator::Condition SaberCondAllocator::getPHIComplementCond ( const SVFBasicBlock * BB1, const SVFBasicBlock * BB2, const SVFBasicBlock * BB0 )

virtual

Get complement condition (from B1 to B0) according to a complementBB (BB2) at a phi e.g., B0: dstBB; B1:incomingBB; B2:complementBB

Get complement phi condition e.g., B0: dstBB; B1:incomingBB; B2:complementBB Assume B0 (phi node) is the successor of both B1 and B2. If B1 dominates B2, and B0 not dominate B2 then condition from B1-->B0 = neg(B1-->B2)^(B1-->B0)

avoid both BB0 and BB1 dominate BB2 (e.g., while loop), then BB2 is not necessarily a complement BB

Definition at line 470 of file SaberCondAllocator.cpp.

{
    assert(BB1 && BB2 && "expect nullptr BB here!");

    if (dominate(BB1, BB2) && ! dominate(BB0, BB2))
    {
        Condition cond = ComputeIntraVFGGuard(BB1, BB2);
        return condNeg(cond);
    }
 
    return getTrueCond();
}

getRemovedSUVFEdges()

SVFGNodeToSVFGNodeSetMap & SVF::SaberCondAllocator::getRemovedSUVFEdges ( )

inline

Definition at line 243 of file SaberCondAllocator.h.

    {
        return removedSUVFEdges;
    }

getTrueCond()

Condition SVF::SaberCondAllocator::getTrueCond ( ) const

inline

Definition at line 98 of file SaberCondAllocator.h.

    {
        return Condition::getTrueCond();
    }

isAllPathReachable()

bool SVF::SaberCondAllocator::isAllPathReachable ( Condition & condition )

inline

whether condition is satisfiable for all possible boolean guards

Definition at line 199 of file SaberCondAllocator.h.

    {
        return isEquivalentBranchCond(condition, Condition::getTrueCond());
    }

isBBCallsProgExit()

bool SaberCondAllocator::isBBCallsProgExit ( const SVFBasicBlock * bb )

private

Whether this basic block contains program exit function call

Definition at line 448 of file SaberCondAllocator.cpp.

{
    const FunObjVar* svfun = bb->getParent();
    FunToExitBBsMap::const_iterator it = funToExitBBsMap.find(svfun);
    if (it != funToExitBBsMap.end())
    {
        for (const auto &bit: it->second)
        {
            if (postDominate(bit, bb))
                return true;
        }
    }
    return false;
}

isEQCmp()

bool SaberCondAllocator::isEQCmp ( const CmpStmt * cmp ) const

private

Evaluate test null/not null like expressions.

Return true if the predicate of this compare instruction is equal

Definition at line 343 of file SaberCondAllocator.cpp.

{
    return (cmp->getPredicate() == CmpStmt::ICMP_EQ);
}

isEquivalentBranchCond()

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

Whether lhs and rhs are equivalent branch conditions.

check equal using z3 solver

Definition at line 615 of file SaberCondAllocator.cpp.

{
    Condition::getSolver().push();
    Condition::getSolver().add(lhs.getExpr() != rhs.getExpr()); 
    z3::check_result res = Condition::getSolver().check();
    Condition::getSolver().pop();
    return res == z3::unsat;
}

isNECmp()

bool SaberCondAllocator::isNECmp ( const CmpStmt * cmp ) const

private

Return true if the predicate of this compare instruction is not equal.

Definition at line 348 of file SaberCondAllocator.cpp.

{
    return (cmp->getPredicate() == CmpStmt::ICMP_NE);
}

isNegCond()

bool SVF::SaberCondAllocator::isNegCond ( u32_t id ) const

inline

Definition at line 141 of file SaberCondAllocator.h.

    {
        return negConds.test(id);
    }

isSatisfiable()

bool SaberCondAllocator::isSatisfiable

(

const Condition &

condition

)

whether condition is satisfiable

Definition at line 626 of file SaberCondAllocator.cpp.

{
    Condition::getSolver().push();
    Condition::getSolver().add(condition.getExpr());
    z3::check_result result = Condition::getSolver().check();
    Condition::getSolver().pop();
    if (result == z3::sat || result == z3::unknown)
        return true;
    else
        return false;
}

isTestContainsNullAndTheValue()

bool SaberCondAllocator::isTestContainsNullAndTheValue ( const CmpStmt * cmp ) const

private

Return true if two values on the predicate are what we want.

Return true if: (1) cmp contains a null value (2) there is an indirect/direct edge from cur evaluated SVFG node to cmp operand

e.g., indirect edge: cur svfg node -> 1. store i32* %0, i32** p, align 8, !dbg !157 cmp operand -> 2. %1 = load i32*, i32** p, align 8, !dbg !159

1. tobool = icmp ne i32* %1, null, !dbg !159
2. br i1 tobool, label if.end, label if.then, !dbg !161 There is an indirect edge 1->2 with value %0

direct edge: cur svfg node -> 1. %3 = tail call i8* @malloc(i64 16), !dbg !22 (cmp operand) 2. %4 = icmp eq i8* %3, null, !dbg !28

1. br i1 %4, label %7, label %5, !dbg !30 There is an direct edge 1->2 with value %3

Definition at line 399 of file SaberCondAllocator.cpp.

{
 
    // must be val var?
    const SVFVar* op0 = cmp->getOpVar(0);
    const SVFVar* op1 = cmp->getOpVar(1);
    if (SVFUtil::isa<ConstNullPtrValVar>(op1))
    {
        Set<const SVFVar* > inDirVal;
        inDirVal.insert(getCurEvalSVFGNode()->getValue());
        for (const auto &it: getCurEvalSVFGNode()->getOutEdges())
        {
            inDirVal.insert(it->getDstNode()->getValue());
        }
        return inDirVal.find(op0) != inDirVal.end();
    }
    else if (SVFUtil::isa<ConstNullPtrValVar>(op0))
    {
        Set<const SVFVar* > inDirVal;
        inDirVal.insert(getCurEvalSVFGNode()->getValue());
        for (const auto &it: getCurEvalSVFGNode()->getOutEdges())
        {
            inDirVal.insert(it->getDstNode()->getValue());
        }
        return inDirVal.find(op1) != inDirVal.end();
    }
    return false;
}

isTestNotNullExpr()

bool SaberCondAllocator::isTestNotNullExpr ( const ICFGNode * test ) const

private

Return true if this is a test not null expression.

Definition at line 366 of file SaberCondAllocator.cpp.

{
    if(!test) return false;
    for(const SVFStmt* stmt : PAG::getPAG()->getSVFStmtList(test))
    {
        if(const CmpStmt* cmp = SVFUtil::dyn_cast<CmpStmt>(stmt))
        {
            return isTestContainsNullAndTheValue(cmp) && isNECmp(cmp);
        }
    }
    return false;
}

isTestNullExpr()

bool SaberCondAllocator::isTestNullExpr ( const ICFGNode * test ) const

private

Return true if this is a test null expression.

Definition at line 353 of file SaberCondAllocator.cpp.

{
    if(!test) return false;
    for(const SVFStmt* stmt : PAG::getPAG()->getSVFStmtList(test))
    {
        if(const CmpStmt* cmp = SVFUtil::dyn_cast<CmpStmt>(stmt))
        {
            return isTestContainsNullAndTheValue(cmp) && isEQCmp(cmp);
        }
    }
    return false;
}

newCond()

SaberCondAllocator::Condition SaberCondAllocator::newCond

(

const ICFGNode *

inst

)

Allocate a new condition.

Definition at line 602 of file SaberCondAllocator.cpp.

{
    u32_t condCountIdx = totalCondNum++;
    Condition expr = Condition::getContext().bool_const(("c" + std::to_string(condCountIdx)).c_str());
    Condition negCond = Condition::NEG(expr);
    setCondInst(expr, inst);
    setNegCondInst(negCond, inst);
    conditionVec.push_back(expr);
    conditionVec.push_back(negCond);
    return expr;
}

postDominate()

bool SVF::SaberCondAllocator::postDominate ( const SVFBasicBlock * bbKey, const SVFBasicBlock * bbValue ) const

inline

Definition at line 146 of file SaberCondAllocator.h.

    {
        const FunObjVar*  keyFunc = bbKey->getParent();
        const FunObjVar*  valueFunc = bbValue->getParent();
        bool funcEq = (keyFunc == valueFunc);
        (void)funcEq; // Suppress warning of unused variable under release build
        assert(funcEq && "two basicblocks should be in the same function!");
        return keyFunc->postDominate(bbKey,bbValue);
    }

printPathCond()

void SaberCondAllocator::printPathCond

(

)

Print out the path condition information.

Print path conditions

Definition at line 575 of file SaberCondAllocator.cpp.

{
 
    outs() << "print path condition\n";
 
    for (const auto &bbCond: bbConds)
    {
        const SVFBasicBlock* bb = bbCond.first;
        for (const auto &cit: bbCond.second)
        {
            u32_t i = 0;
            for (const SVFBasicBlock* succ: bb->getSuccessors())
            {
                if (i == cit.first)
                {
                    Condition cond = cit.second;
                    outs() << bb->getName() << "-->" << succ->getName() << ":";
                    outs() << dumpCond(cond) << "\n";
                    break;
                }
                i++;
            }
        }
    }
}

setBranchCond()

void SaberCondAllocator::setBranchCond ( const SVFBasicBlock * bb, const SVFBasicBlock * succ, const Condition & cond )

private

Get/Set a branch condition, and its terminator instruction.

Set branch condition

Set a branch condition

we only care about basic blocks have more than one successor

FIXME: llvm getNumSuccessors allows duplicated block in the successors, it makes this assertion fail In this case we may waste a condition allocation, because the overwrite of the previous cond

Definition at line 168 of file SaberCondAllocator.cpp.

{
    assert(bb->getNumSuccessors() > 1 && "not more than one successor??");
    u32_t pos = bb->getBBSuccessorPos(succ);
    CondPosMap& condPosMap = bbConds[bb];

    //assert(condPosMap.find(pos) == condPosMap.end() && "this branch has already been set ");
 
    condPosMap[pos] = cond;
}

setCFCond()

bool SVF::SaberCondAllocator::setCFCond ( const SVFBasicBlock * bb, const Condition & cond )

inline

Get/Set control-flow conditions.

Definition at line 214 of file SaberCondAllocator.h.

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

setCondInst()

void SVF::SaberCondAllocator::setCondInst ( const Condition & condition, const ICFGNode * inst )

inline

Definition at line 134 of file SaberCondAllocator.h.

    {
        assert(idToTermInstMap.find(condition.id()) == idToTermInstMap.end() && "this should be a fresh condition");
        idToTermInstMap[condition.id()] = inst;
    }

setCurEvalSVFGNode()

void SVF::SaberCondAllocator::setCurEvalSVFGNode ( const SVFGNode * node )

inline

Set current value for branch condition evaluation.

Definition at line 181 of file SaberCondAllocator.h.

    {
        curEvalSVFGNode = node;
    }

setNegCondInst()

void SVF::SaberCondAllocator::setNegCondInst ( const Condition & condition, const ICFGNode * inst )

inline

mark neg Z3 expression

Definition at line 237 of file SaberCondAllocator.h.

    {
        setCondInst(condition, inst);
        negConds.set(condition.id());
    }

Member Data Documentation

bbConds

BBCondMap SVF::SaberCondAllocator::bbConds

protected

map basic block to its successors/predecessors branch conditions

Definition at line 311 of file SaberCondAllocator.h.

bbToCondMap

BBToCondMap SVF::SaberCondAllocator::bbToCondMap

private

map a basic block to its path condition starting from root

Definition at line 302 of file SaberCondAllocator.h.

conditionVec

std::vector<Condition> SVF::SaberCondAllocator::conditionVec

private

bit vector for distinguish neg

Definition at line 306 of file SaberCondAllocator.h.

curEvalSVFGNode

const SVFGNode* SVF::SaberCondAllocator::curEvalSVFGNode {}

private

current llvm value to evaluate branch condition when computing guards

Definition at line 303 of file SaberCondAllocator.h.

{};         

funToExitBBsMap

FunToExitBBsMap SVF::SaberCondAllocator::funToExitBBsMap

private

map a function to all its basic blocks calling program exit

Definition at line 301 of file SaberCondAllocator.h.

idToTermInstMap

IndexToTermInstMap SVF::SaberCondAllocator::idToTermInstMap

private

Definition at line 304 of file SaberCondAllocator.h.

negConds

NodeBS SVF::SaberCondAllocator::negConds

private

key: z3 expression id, value: instruction

Definition at line 305 of file SaberCondAllocator.h.

removedSUVFEdges

SVFGNodeToSVFGNodeSetMap SVF::SaberCondAllocator::removedSUVFEdges

private

a counter for fresh condition

Definition at line 308 of file SaberCondAllocator.h.

totalCondNum

u32_t SaberCondAllocator::totalCondNum = 0

staticprivate

vector storing z3expression

Definition at line 307 of file SaberCondAllocator.h.

---

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

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