Skip to content

Commit 492d4ef

Browse files
yuleisuiyuleisui
committed
release Lab-2 and Assignment-2
1 parent 4679abc commit 492d4ef

File tree

8 files changed

+374
-133
lines changed

8 files changed

+374
-133
lines changed

‎Assignment-2/Assignment-2.cpp‎

Lines changed: 106 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -42,9 +42,11 @@ void SSE::reachability(const ICFGEdge* curEdge, const ICFGNode* snk) {
4242
}
4343

4444
/// TODO: collect each path once this method is called during reachability analysis, and
45-
/// add each path (a sequence of node IDs) as a string into std::set<std::string> paths
46-
/// in the format "START->1->2->4->5->END", where -> indicate an ICFGEdge connects two ICFGNode IDs
47-
void SSE::collectICFGPath() {
45+
/// Collect each program path from the entry to each assertion of the program. In this function,
46+
/// you will need (1) add each path into the paths set, (2) call translatePath to convert each path into Z3 expressions.
47+
/// Note that translatePath returns true if the path is feasible, infeasible otherwise. (3) If a path is feasible,
48+
/// you will need to call assertchecking to verify the assertion (which is the last ICFGNode of this path).
49+
void SSE::collectAndTranslatePath() {
4850
/// TODO: your code starts from here
4951
}
5052

@@ -69,11 +71,107 @@ bool SSE::handleBranch(const IntraCFGEdge* edge) {
6971
return true;
7072
}
7173

72-
/// TODO: Implement handling of non-branch statement inside a function
73-
/// including handling of (1) AddrStmt, (2) CopyStmt, (3) LoadStmt, (4) StoreStmt, (5) GepStmt and (6) any other types
74-
/// of intra SVFStmts Return true means a feasible path, false otherwise
74+
/// TODO: Translate AddrStmt, CopyStmt, LoadStmt, StoreStmt, GepStmt and CmpStmt
75+
/// Translate AddrStmt, CopyStmt, LoadStmt, StoreStmt, GepStmt, BinaryOPStmt, CmpStmt, SelectStmt, and PhiStmt
7576
bool SSE::handleNonBranch(const IntraCFGEdge* edge) {
76-
/// TODO: your code starts from here
77+
const ICFGNode* dstNode = edge->getDstNode();
78+
const ICFGNode* srcNode = edge->getSrcNode();
79+
DBOP(if(!SVFUtil::isa<CallICFGNode>(dstNode) && !SVFUtil::isa<RetICFGNode>(dstNode)) std::cout << "\n## Analyzing "<< dstNode->toString() << "\n");
80+
81+
for (const SVFStmt *stmt : dstNode->getSVFStmts())
82+
{
83+
if (const AddrStmt *addr = SVFUtil::dyn_cast<AddrStmt>(stmt))
84+
{
85+
// TODO: implement AddrStmt handler here
86+
}
87+
else if (const CopyStmt *copy = SVFUtil::dyn_cast<CopyStmt>(stmt))
88+
{
89+
// TODO: implement CopyStmt handler her
90+
}
91+
else if (const LoadStmt *load = SVFUtil::dyn_cast<LoadStmt>(stmt))
92+
{
93+
// TODO: implement LoadStmt handler here
94+
}
95+
else if (const StoreStmt *store = SVFUtil::dyn_cast<StoreStmt>(stmt))
96+
{
97+
// TODO: implement StoreStmt handler here
98+
}
99+
else if (const GepStmt *gep = SVFUtil::dyn_cast<GepStmt>(stmt))
100+
{
101+
// TODO: implement GepStmt handler here
102+
}
103+
else if (const CmpStmt *cmp = SVFUtil::dyn_cast<CmpStmt>(stmt))
104+
{
105+
// TODO: implement CmpStmt handler here
106+
}
107+
else if (const BinaryOPStmt *binary = SVFUtil::dyn_cast<BinaryOPStmt>(stmt))
108+
{
109+
expr op0 = getZ3Expr(binary->getOpVarID(0));
110+
expr op1 = getZ3Expr(binary->getOpVarID(1));
111+
expr res = getZ3Expr(binary->getResID());
112+
switch (binary->getOpcode())
113+
{
114+
case BinaryOperator::Add:
115+
addToSolver(res == op0 + op1);
116+
break;
117+
case BinaryOperator::Sub:
118+
addToSolver(res == op0 - op1);
119+
break;
120+
case BinaryOperator::Mul:
121+
addToSolver(res == op0 * op1);
122+
break;
123+
case BinaryOperator::SDiv:
124+
addToSolver(res == op0 / op1);
125+
break;
126+
case BinaryOperator::SRem:
127+
addToSolver(res == op0 % op1);
128+
break;
129+
case BinaryOperator::Xor:
130+
addToSolver(int2bv(32, res) == (int2bv(32, op0) ^ int2bv(32, op1)));
131+
break;
132+
case BinaryOperator::And:
133+
addToSolver(int2bv(32, res) == (int2bv(32, op0) & int2bv(32, op1)));
134+
break;
135+
case BinaryOperator::Or:
136+
addToSolver(int2bv(32, res) == (int2bv(32, op0) | int2bv(32, op1)));
137+
break;
138+
case BinaryOperator::AShr:
139+
addToSolver(int2bv(32, res) == ashr(int2bv(32, op0), int2bv(32, op1)));
140+
break;
141+
case BinaryOperator::Shl:
142+
addToSolver(int2bv(32, res) == shl(int2bv(32, op0), int2bv(32, op1)));
143+
break;
144+
default:
145+
assert(false && "implement this part");
146+
}
147+
}
148+
else if (const BranchStmt *br = SVFUtil::dyn_cast<BranchStmt>(stmt))
149+
{
150+
DBOP(std::cout << "\t skip handled when traversal Conditional IntraCFGEdge \n");
151+
}
152+
else if (const SelectStmt *select = SVFUtil::dyn_cast<SelectStmt>(stmt)) {
153+
expr res = getZ3Expr(select->getResID());
154+
expr tval = getZ3Expr(select->getTrueValue()->getId());
155+
expr fval = getZ3Expr(select->getFalseValue()->getId());
156+
expr cond = getZ3Expr(select->getCondition()->getId());
157+
addToSolver(res == ite(cond == getCtx().int_val(1), tval, fval));
158+
}
159+
else if (const PhiStmt *phi = SVFUtil::dyn_cast<PhiStmt>(stmt)) {
160+
expr res = getZ3Expr(phi->getResID());
161+
bool opINodeFound = false;
162+
for(u32_t i = 0; i < phi->getOpVarNum(); i++){
163+
assert(srcNode && "we don't have a predecessor ICFGNode?");
164+
if (srcNode->getFun()->postDominate(srcNode->getBB(),phi->getOpICFGNode(i)->getBB()))
165+
{
166+
expr ope = getZ3Expr(phi->getOpVar(i)->getId());
167+
addToSolver(res == ope);
168+
opINodeFound = true;
169+
}
170+
}
171+
assert(opINodeFound && "predecessor ICFGNode of this PhiStmt not found?");
172+
}
173+
}
174+
77175
return true;
78176
}
79177

@@ -108,4 +206,4 @@ void SSE::analyse() {
108206
resetSolver();
109207
}
110208
}
111-
}
209+
}

‎Assignment-2/Assignment-2.h‎

Lines changed: 5 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -50,13 +50,13 @@ namespace SVF {
5050
delete z3Mgr;
5151
}
5252

53-
/// Identify source node on ICFG
53+
/// Identify source which is the program entry ICFGNode (GlobalICFGNode)
5454
std::set<const ICFGNode*>& identifySources() {
5555
sources.insert(icfg->getGlobalICFGNode());
5656
return sources;
5757
}
5858

59-
/// Identify the sink node which is an assertion call on ICFG
59+
/// Identify the sink nodes which are assertion ICFGNodes
6060
std::set<const ICFGNode*>& identifySinks() {
6161
for (const CallICFGNode* cs : svfir->getCallSiteSet()) {
6262
const SVFFunction* fun = SVFUtil::getCallee(cs->getCallSite());
@@ -78,7 +78,7 @@ namespace SVF {
7878
}
7979

8080
/// TODO: Implementing the collection the ICFG paths
81-
virtual void collectICFGPath();
81+
virtual void collectAndTranslatePath();
8282

8383
/// Depth-first-search ICFGTraversal on ICFG from src node to snk node
8484
void reachability(const ICFGEdge* curNode, const ICFGNode* snk);
@@ -100,6 +100,8 @@ namespace SVF {
100100
return handleNonBranch(edge);
101101
}
102102
}
103+
bool handleNonBranch(const IntraCFGEdge* edge);
104+
bool handleBranch(const IntraCFGEdge* edge);
103105

104106
/// Encode the path into Z3 constraints and return true if the path is feasible, false otherwise.
105107
bool translatePath(std::vector<const ICFGEdge*>& path);
@@ -130,10 +132,6 @@ namespace SVF {
130132
}
131133
}
132134

133-
134-
bool handleNonBranch(const IntraCFGEdge* edge);
135-
bool handleBranch(const IntraCFGEdge* edge);
136-
137135
std::set<std::string> getPaths() {
138136
return paths;
139137
}

0 commit comments

Comments
 (0)