40 using namespace SVFUtil;
63 for (
const auto&
item: *svfirCallGraph)
73 collectBBCallingProgExit(*bb);
98 double num = log(succ_number) / log(2);
100 u32_t succ_index = 0;
101 std::vector<Condition> condVec;
102 for (
u32_t i = 0; i < bit_num; i++)
105 condVec.push_back(newCond(svfInst));
118 for (
u32_t j = 0; j < bit_num; j++)
121 u32_t tool = 0x01 << j;
122 if (tool & succ_index)
124 path_cond = condAnd(path_cond, (condNeg(condVec.at(j))));
128 path_cond = condAnd(path_cond, condVec.at(j));
131 setBranchCond(&bb, svf_succ_bb, path_cond);
146 return getTrueCond();
149 BBCondMap::const_iterator it = bbConds.find(bb);
150 assert(it != bbConds.end() &&
"basic block does not have branch and conditions??");
151 CondPosMap::const_iterator cit = it->second.find(pos);
152 assert(cit != it->second.end() &&
"no condition on the branch??");
159 if (getCurEvalSVFGNode() && getCurEvalSVFGNode()->getValue())
160 return evaluateBranchCond(bb, succ);
162 return getBranchCond(bb, succ);
179 condPosMap[pos] = cond;
192 if (isTestNullExpr(SVFUtil::cast<ICFGNode>(condVar->
getGNode())))
196 return getFalseCond();
199 return getTrueCond();
201 if (isTestNotNullExpr(SVFUtil::cast<ICFGNode>(condVar->
getGNode())))
205 return getTrueCond();
208 return getFalseCond();
210 return Condition::nullExpr();
221 bool branch1 = isBBCallsProgExit(succ1);
222 bool branch2 = isBBCallsProgExit(succ2);
225 if (branch1 && !branch2)
229 return getFalseCond();
232 return getTrueCond();
235 else if (!branch1 && branch2)
239 return getFalseCond();
242 return getTrueCond();
245 else if (branch1 && branch2)
247 return getFalseCond();
251 return Condition::nullExpr();
263 assert(svffun == dst->
getParent() &&
"two basic blocks should be in the same function");
268 std::vector<const SVFBasicBlock*> exitbbs;
273 if(!isBBCallsProgExit(eb))
274 filteredbbs.insert(eb);
279 for (
const auto &filteredbb: filteredbbs)
281 if (!postDominate(dst, filteredbb))
286 return getTrueCond();
288 return Condition::nullExpr();
300 return getTrueCond();
306 for (
const auto &svfStmt: icfgNode->getSVFStmts())
308 if (
const BranchStmt *branchStmt = SVFUtil::dyn_cast<BranchStmt>(svfStmt))
310 if (branchStmt->getNumSuccessors() == 2)
312 const SVFBasicBlock* succ1 = branchStmt->getSuccessor(0)->getBB();
313 const SVFBasicBlock* succ2 = branchStmt->getSuccessor(1)->getBB();
314 bool is_succ = (succ1 == succ || succ2 == succ);
316 assert(is_succ &&
"not a successor??");
317 Condition evalLoopExit = evaluateLoopExitBranch(bb, succ);
318 if (!eq(evalLoopExit, Condition::nullExpr()))
321 Condition evalProgExit = evaluateProgExit(branchStmt, succ);
322 if (!eq(evalProgExit, Condition::nullExpr()))
325 Condition evalTestNullLike = evaluateTestNullLikeExpr(branchStmt, succ);
326 if (!eq(evalTestNullLike, Condition::nullExpr()))
327 return evalTestNullLike;
334 return getBranchCond(bb, succ);
349 if(!test)
return false;
352 if(
const CmpStmt* cmp = SVFUtil::dyn_cast<CmpStmt>(stmt))
354 return isTestContainsNullAndTheValue(cmp) && isEQCmp(cmp);
362 if(!test)
return false;
365 if(
const CmpStmt* cmp = SVFUtil::dyn_cast<CmpStmt>(stmt))
367 return isTestContainsNullAndTheValue(cmp) && isNECmp(cmp);
398 if (SVFUtil::isa<SVFConstantNullPtr>(op1))
401 inDirVal.insert(getCurEvalSVFGNode()->getValue());
402 for (
const auto &it: getCurEvalSVFGNode()->getOutEdges())
404 inDirVal.insert(it->getDstNode()->getValue());
406 return inDirVal.find(op0) != inDirVal.end();
408 else if (SVFUtil::isa<SVFConstantNullPtr>(op0))
411 inDirVal.insert(getCurEvalSVFGNode()->getValue());
412 for (
const auto &it: getCurEvalSVFGNode()->getOutEdges())
414 inDirVal.insert(it->getDstNode()->getValue());
416 return inDirVal.find(op1) != inDirVal.end();
429 if (
const CallICFGNode* cs = SVFUtil::dyn_cast<CallICFGNode>(icfgNode))
433 funToExitBBsMap[svfun].insert(&bb);
444 FunToExitBBsMap::const_iterator it = funToExitBBsMap.find(svfun);
445 if (it != funToExitBBsMap.end())
447 for (
const auto &bit: it->second)
449 if (postDominate(bit, bb))
465 assert(BB1 && BB2 &&
"expect nullptr BB here!");
468 if (dominate(BB1, BB2) && ! dominate(BB0, BB2))
470 Condition cond = ComputeIntraVFGGuard(BB1, BB2);
471 return condNeg(cond);
474 return getTrueCond();
488 Condition c1 = ComputeIntraVFGGuard(srcBB, callBB);
489 setCFCond(funEntryBB, condOr(getCFCond(funEntryBB), getCFCond(callBB)));
490 Condition c2 = ComputeIntraVFGGuard(funEntryBB, dstBB);
491 return condAnd(c1, c2);
505 Condition c1 = ComputeIntraVFGGuard(srcBB, funExitBB);
506 setCFCond(retBB, condOr(getCFCond(retBB), getCFCond(funExitBB)));
507 Condition c2 = ComputeIntraVFGGuard(retBB, dstBB);
508 return condAnd(c1, c2);
517 assert(srcBB->
getParent() == dstBB->
getParent() &&
"two basic blocks are not in the same function??");
519 if (postDominate(dstBB, srcBB))
520 return getTrueCond();
523 worklist.
push(srcBB);
524 setCFCond(srcBB, getTrueCond());
526 while (!worklist.
empty())
533 Condition loopExitCond = evaluateLoopExitBranch(bb, dstBB);
534 if (!eq(loopExitCond, Condition::nullExpr()))
535 return condAnd(cond, loopExitCond);
544 if (postDominate(succ, bb))
545 brCond = getTrueCond();
547 brCond = getEvalBrCond(bb, succ);
550 ") --> " <<
"succ_bb (" << succ->getName() <<
") condition: " << brCond <<
"\n");
551 Condition succPathCond = condAnd(cond, brCond);
552 if (setCFCond(succ, condOr(getCFCond(succ), succPathCond)))
558 ") --> " <<
"dst_bb (" << dstBB->
getName() <<
") condition: " << getCFCond(dstBB)
561 return getCFCond(dstBB);
571 outs() <<
"print path condition\n";
573 for (
const auto &bbCond: bbConds)
576 for (
const auto &cit: bbCond.second)
584 outs() << bb->
getName() <<
"-->" << succ->getName() <<
":";
585 outs() << dumpCond(cond) <<
"\n";
597 u32_t condCountIdx = totalCondNum++;
598 Condition expr = Condition::getContext().bool_const((
"c" + std::to_string(condCountIdx)).c_str());
599 Condition negCond = Condition::NEG(expr);
600 setCondInst(expr, inst);
601 setNegCondInst(negCond, inst);
602 conditionVec.push_back(expr);
603 conditionVec.push_back(negCond);
611 Condition::getSolver().push();
613 z3::check_result res = Condition::getSolver().check();
614 Condition::getSolver().pop();
615 return res == z3::unsat;
621 Condition::getSolver().add(condition.
getExpr());
622 z3::check_result result = Condition::getSolver().check();
623 Condition::getSolver().pop();
624 if (result == z3::sat || result == z3::unknown)
633 if (condition.
getExpr().num_args() == 1 && isNegCond(condition.
id()))
638 if (condition.
getExpr().num_args() == 0)
639 if (!condition.
getExpr().is_true() && !condition.
getExpr().is_false())
641 for (
u32_t i = 0; i < condition.
getExpr().num_args(); ++i)
644 extractSubConds(expr, support);
#define DBOUT(TYPE, X)
LLVM debug macros, define type of your DBUG model of each pass.
const ICFGNode * getSuccessor(u32_t i) const
const SVFVar * getCondition() const
Return the condition.
u32_t getPredicate() const
static u32_t maximumCxtLen
static u32_t maximumPathLen
static u64_t maximumBudget
bool push(const Data &data)
virtual const SVFBasicBlock * getBB() const
Return the basic block of this ICFGNode.
const SVFVar * getOpVar(u32_t pos) const
Operand SVFVars.
static const Option< bool > PrintPathCond
const std::vector< const ICFGNode * > & getICFGNodeList() const
const std::vector< const SVFBasicBlock * > & getSuccessors() const
u32_t getBBSuccessorPos(const SVFBasicBlock *succbb)
const ICFGNode * back() const
u32_t getNumSuccessors() const
const SVFFunction * getParent() const
const_iterator end() const
const_iterator begin() const
void getExitBlocksOfLoop(const SVFBasicBlock *bb, BBList &exitbbs) const
const SVFBasicBlock * getEntryBlock() const
std::vector< const SVFBasicBlock * >::const_iterator const_iterator
const SVFBasicBlock * getExitBB() const
bool isLoopHeader(const SVFBasicBlock *bb) const
PTACallGraph * getCallGraph()
static SVFIR * getPAG(bool buildFromFile=false)
Singleton design here to make sure we only have one instance during any analysis.
const std::string & getName() const
const SVFValue * getValue() const
Get/has methods of the components.
void allocate(const SVFModule *module)
Perform path allocation.
virtual void allocateForBB(const SVFBasicBlock &bb)
Allocate path condition for every basic block.
Condition newCond(const ICFGNode *inst)
Allocate a new condition.
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.
bool isTestContainsNullAndTheValue(const CmpStmt *cmp) const
Return true if two values on the predicate are what we want.
bool isTestNullExpr(const ICFGNode *test) const
Return true if this is a test null expression.
void printPathCond()
Print out the path condition information.
SaberCondAllocator()
Constructor.
void setBranchCond(const SVFBasicBlock *bb, const SVFBasicBlock *succ, const Condition &cond)
Get/Set a branch condition, and its terminator instruction.
virtual Condition getPHIComplementCond(const SVFBasicBlock *BB1, const SVFBasicBlock *BB2, const SVFBasicBlock *BB0)
static u32_t totalCondNum
vector storing z3expression
bool isSatisfiable(const Condition &condition)
whether condition is satisfiable
Condition getBranchCond(const SVFBasicBlock *bb, const SVFBasicBlock *succ) const
Get branch condition.
virtual Condition ComputeInterRetVFGGuard(const SVFBasicBlock *src, const SVFBasicBlock *dst, const SVFBasicBlock *retBB)
void collectBBCallingProgExit(const SVFBasicBlock &bb)
Collect basic block contains program exit function call.
bool isBBCallsProgExit(const SVFBasicBlock *bb)
void extractSubConds(const Condition &condition, NodeBS &support) const
extract subexpression from a Z3 expression
Map< u32_t, Condition > CondPosMap
id to instruction map for z3
bool isEquivalentBranchCond(const Condition &lhs, const Condition &rhs) const
Whether lhs and rhs are equivalent branch conditions.
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.
Condition evaluateBranchCond(const SVFBasicBlock *bb, const SVFBasicBlock *succ)
Evaluate branch conditions.
Condition evaluateLoopExitBranch(const SVFBasicBlock *bb, const SVFBasicBlock *succ)
Evaluate loop exit branch.
bool isTestNotNullExpr(const ICFGNode *test) const
Return true if this is a test not null expression.
Condition getEvalBrCond(const SVFBasicBlock *bb, const SVFBasicBlock *succ)
Get a condition, evaluate the value for conditions if necessary (e.g., testNull like express)
virtual Condition ComputeInterCallVFGGuard(const SVFBasicBlock *src, const SVFBasicBlock *dst, const SVFBasicBlock *callBB)
virtual Condition ComputeIntraVFGGuard(const SVFBasicBlock *src, const SVFBasicBlock *dst)
Guard Computation for a value-flow (between two basic blocks)
const SVFBaseNode * getGNode() const
const z3::expr & getExpr() const
const SVFFunction * getFunction(const std::string &name)
Get the corresponding Function based on its name.
bool isExtCall(const SVFFunction *fun)
std::string pasMsg(const std::string &msg)
Print each pass/phase message by converting a string into blue string output.
bool isProgExitCall(const CallICFGNode *cs)
std::ostream & outs()
Overwrite llvm::outs()
std::unordered_set< Key, Hash, KeyEqual, Allocator > Set