Assignment 4 2024 (1)

Assignment-4
University of Technology Sydney, Australia
Software Verification https://github.com/SVF-tools/Teaching-Software-Verification

Assignment 4: Quiz + A Coding Task
• One quiz (10 points)
• Static symbolic execution
• Automatic translation from code to Z3 formulas/constraints
Software Verification https://github.com/SVF-tools/Teaching-Software-Verification

Assignment 4: Quiz + A Coding Task
• One quiz (10 points)
• Static symbolic execution
• Automatic translation from code to Z3 formulas/constraints
• One coding task (15 points)
• Goal: automatically perform assertion-based verification for code using static
symbolic execution.
• Specification and code template:https://github.com/SVF-tools/ Teaching-Software-Verification/wiki/Assignment-4
• SVF Z3 APIs: https: //github.com/SVF-tools/Teaching-Software-Verification/wiki/Z3-API
You are encouraged to finish the quizzes before starting your coding task.
Software Verification https://github.com/SVF-tools/Teaching-Software-Verification

Methods to Be Implemented
You need to implement the following four functions in Assignment-4.cpp:
• SSE::translatePath
• SSE::handleNonBranch
• SSE::handleCall
• SSE::handleRet
• SSE::handleBranch
• Remember to put your previously implemented Assignment-2.cpp in place (under the Assignment-2 folder).
• The required implementation parts are indicated with TODO comments and you only need to fill up the code template if a method is partially implemented.
In the following slides, we provide several examples to assist your understanding of SSE.
Software Verification https://github.com/SVF-tools/Teaching-Software-Verification

Interprocedural Example
void foo(int* p) { *p = 1;
int main() {
int a = 0;
foo(&a); svf_assert(a == 1);
void @foo(i32* %p) { entry:
store i32 1, i32* %p
ret void }
i32 @main() { entry:
%a = alloca i32
store i32 0, i32* %a
call void @foo(i32* %a)
%0 = load i32, i32* %a
%cmp = icmp eq i32 %0, 1
call void @svf_assert(i1 zeroext %cmp) ret i32 0
Software Verification https://github.com/SVF-tools/Teaching-Software-Verification

Interprocedural Example
void foo(int* p) { *p = 1;
int main() {
int a = 0;
foo(&a); svf_assert(a == 1);
void @foo(i32* %p) {
entry: SVF
store i32 1, i32* %p ret void
i32 @main() { entry:
FunEntryICFGNode1 {fun:foo}
GlobalICFGNode0
CopyStmt: [Var1 !” Var0] i8* null AddrStmt: [Var9 !” Var10] i32 1 AddrStmt: [Var18 !” Var19] i32 0 AddrStmt: [Var4 !” Var5] foo AddrStmt: [Var12 !” Var13] main AddrStmt: [Var24 !” Var25] svf_assert
IntraICFGNode6 {fun: main} AddrStmt: [Var15 !” Var16]
%a = alloca i32
IntraICFGNode2 {fun: foo} StoreStmt: [Var7 !” Var9]
store i32 1,i32* %p
IntraICFGNode7 {fun: main}
StoreStmt: [Var15 !” Var18]
store i32 0,i32* %a
IntraICFGNode3 {fun: foo}
CallCFGNode8 {fun: main} CallPE: [Var7 !” Var15]
call void @foo(i32* %a)
0x5583fba7
RetICFGNode12 {fun:main}
FunExitICFGNode4 {fun:foo} 0x5583fba7
%a = alloca i32
store i32 0, i32* %a
call void @foo(i32* %a)
%0 = load i32, i32* %a
%cmp = icmp eq i32 %0, 1
call void @svf_assert(i1 zeroext %cmp) ret i32 0
IntraICFGNode10 {fun: main} LoadStmt: [Var21 !” Var15]
%0 = load i32, i32* %a
IntraICFGNode11 {fun: main}
CmpStmt: [Var22 !” Var21 pred32 Var9]
%cmp = icmp eq i32 %0,1
Software Verification https://github.com/SVF-tools/Teaching-Software-Verification

Interprocedural Example
GlobalICFGNode0
CopyStmt: [Var1 !” Var0] i8* null AddrStmt: [Var9 !” Var10] i32 1 AddrStmt: [Var18 !” Var19] i32 0 AddrStmt: [Var4 !” Var5] foo AddrStmt: [Var12 !” Var13] main AddrStmt: [Var24 !” Var25] svf_assert
FunEntryICFGNode1 {fun:foo}
IntraICFGNode6 {fun: main} AddrStmt: [Var15 !” Var16]
%a = alloca i32
IntraICFGNode2 {fun: foo} StoreStmt: [Var7 !” Var9]
store i32 1,i32* %p
IntraICFGNode7 {fun: main}
StoreStmt: [Var15 !” Var18]
store i32 0,i32* %a
IntraICFGNode3 {fun: foo}
CallCFGNode8 {fun: main} CallPE: [Var7 !” Var15]
call void @foo(i32* %a)
0x5583fba7
RetICFGNode12 {fun:main}
FunExitICFGNode4 {fun:foo} 0x5583fba7
IntraICFGNode10 {fun: main} LoadStmt: [Var21 !” Var15]
%0 = load i32, i32* %a
IntraICFGNode11 {fun: main}
CmpStmt: [Var22 !” Var21 pred32 Var9]
%cmp = icmp eq i32 %0,1
————-SVFVar and ObjVar25 (0x7f000019) ObjVar19 (0x7f000013) ObjVar16 (0x7f000010) ObjVar13 (0x7f00000d) ObjVar10 (0x7f00000a) ObjVar5 (0x7f000005) ValVar24
ObjVar2 ObjVar3 ValVar1 ValVar0 ValVar4 ValVar9 ValVar12 ValVar18
Value————- Value: NULL
Value: NULL
Value: NULL Value: 1
Value: NULL Value: 0x7f000019 Value: NULL Value: NULL Value: 2
Value: 0x7f000005 Value: 1
Value: 0x7f00000d Value: 0
(0x7f000002) (0x7f000003)
… ——————————————
The values of Z3 expressions for each SVFVar after analyzing GlobalICFGNode0
(use printExprValues()
to print SVFVars and their Values)
Software Verification https://github.com/SVF-tools/Teaching-Software-Verification

Interprocedural Example
GlobalICFGNode0
CopyStmt: [Var1 !” Var0] i8* null AddrStmt: [Var9 !” Var10] i32 1 AddrStmt: [Var18 !” Var19] i32 0 AddrStmt: [Var4 !” Var5] foo AddrStmt: [Var12 !” Var13] main AddrStmt: [Var24 !” Var25] svf_assert
FunEntryICFGNode1 {fun:foo}
IntraICFGNode6 {fun: main} AddrStmt: [Var15 !” Var16]
%a = alloca i32
IntraICFGNode2 {fun: foo} StoreStmt: [Var7 !” Var9]
store i32 1,i32* %p
IntraICFGNode7 {fun: main}
StoreStmt: [Var15 !” Var18]
store i32 0,i32* %a
IntraICFGNode3 {fun: foo}
CallCFGNode8 {fun: main} CallPE: [Var7 !” Var15]
call void @foo(i32* %a)
0x5583fba7
RetICFGNode12 {fun:main}
FunExitICFGNode4 {fun:foo} 0x5583fba7
IntraICFGNode10 {fun: main} LoadStmt: [Var21 !” Var15]
%0 = load i32, i32* %a
IntraICFGNode11 {fun: main}
CmpStmt: [Var22 !” Var21 pred32 Var9]
%cmp = icmp eq i32 %0,1
Algorithm 2 translatePath(path)
foreach edge ∈ path do
if IntraEdge ← dyn cast⟨IntraCFGEdge⟩(edge) then
if handleIntra(IntraEdge) == false then return false
else if CallEdge ← dyn cast⟨CallCFGEdge⟩(edge) then handleCall(CallEdge)
else if RetEdge ← dyn cast⟨RetCFGEdge⟩(edge) then handleRet(RetEdge)
assert(false &&”what other edges we have?”); Return true
Software Verification https://github.com/SVF-tools/Teaching-Software-Verification

Interprocedural Example
Algorithm 3 handleIntra(intraEdge)
if intraEdge.getCondition() && !handleBranch(intraEdge) then
return false
handleNonBranch(edge)
HandleNonBranch(intraEdge)
dst ← intraEdge.getDstNode(); src ← intraEdge.getSrcNode() foreach stmt ∈ dst.getSVFStmts() do
GlobalICFGNode0
CopyStmt: [Var1 !” Var0] i8* null AddrStmt: [Var9 !” Var10] i32 1 AddrStmt: [Var18 !” Var19] i32 0 AddrStmt: [Var4 !” Var5] foo AddrStmt: [Var12 !” Var13] main AddrStmt: [Var24 !” Var25] svf_assert
FunEntryICFGNode1 {fun:foo}
IntraICFGNode6 {fun: main} AddrStmt: [Var15 !” Var16]
%a = alloca i32
IntraICFGNode2 {fun: foo} StoreStmt: [Var7 !” Var9]
store i32 1,i32* %p
IntraICFGNode7 {fun: main}
StoreStmt: [Var15 !” Var18]
store i32 0,i32* %a
IntraICFGNode3 {fun: foo}
CallCFGNode8 {fun: main} CallPE: [Var7 !” Var15]
call void @foo(i32* %a)
0x5583fba7
RetICFGNode12 {fun:main}
FunExitICFGNode4 {fun:foo} 0x5583fba7
IntraICFGNode10 {fun: main} LoadStmt: [Var21 !” Var15]
%0 = load i32, i32* %a
IntraICFGNode11 {fun: main}
CmpStmt: [Var22 !” Var21 pred32 Var9]
%cmp = icmp eq i32 %0,1
1 2 3 4 5 6
11 12 13 14
else if copy ∈ dyn cast⟨CopyStmt⟩(stmt) then lhs ← getZ3Expr(copy.getLHSVarID()) rhs ← getZ3Expr(copy.getRHSVarID()) addToSolver(rhs == lhs)
else if load ∈ dyn cast⟨LoadStmt⟩(stmt) then lhs ← getZ3Expr(load.getLHSVarID()) rhs ← getZ3Expr(load.getRHSVarID())
addToSolver(lhs == z3Mgr.loadValue(rhs)) …
if addr ∈ dyn cast⟨AddrStmt⟩(stmt) then
obj ← getMemObjAddress(addr.getRHSVarID()) lhs ← getZ3Expr(addr.getLHSVarID()) addToSolver(obj == lhs)
Software Verification https://github.com/SVF-tools/Teaching-Software-Verification

Interprocedural Example
GlobalICFGNode0
CopyStmt: [Var1 !” Var0] i8* null AddrStmt: [Var9 !” Var10] i32 1 AddrStmt: [Var18 !” Var19] i32 0 AddrStmt: [Var4 !” Var5] foo AddrStmt: [Var12 !” Var13] main AddrStmt: [Var24 !” Var25] svf_assert
FunEntryICFGNode1 {fun:foo}
IntraICFGNode6 {fun: main} AddrStmt: [Var15 !” Var16]
%a = alloca i32
IntraICFGNode2 {fun: foo} StoreStmt: [Var7 !” Var9]
store i32 1,i32* %p
IntraICFGNode7 {fun: main}
StoreStmt: [Var15 !” Var18]
store i32 0,i32* %a
IntraICFGNode3 {fun: foo}
CallCFGNode8 {fun: main} CallPE: [Var7 !” Var15]
call void @foo(i32* %a)
0x5583fba7
RetICFGNode12 {fun:main}
FunExitICFGNode4 {fun:foo} 0x5583fba7
IntraICFGNode10 {fun: main} LoadStmt: [Var21 !” Var15]
%0 = load i32, i32* %a
IntraICFGNode11 {fun: main}
CmpStmt: [Var22 !” Var21 pred32 Var9]
%cmp = icmp eq i32 %0,1
————-SVFVar and ObjVar25 (0x7f000019) ObjVar19 (0x7f000013) ObjVar16 (0x7f000010) ObjVar13 (0x7f00000d) ObjVar10 (0x7f00000a) ObjVar5 (0x7f000005) ValVar24
Value————- Value: NULL
Value: NULL
Value: NULL Value: 1
Value: NULL Value: 0x7f000019 Value: NULL Value: NULL Value: 2
Value: 0x7f000005 Value: 1
Value: 0x7f00000d Value: 0
Value: 0x7f000010
… ——————————————
## Analyzing IntraICFGNode6 {fun: main} AddrStmt: [Var14 ← Var15]
%a = alloca i32
ObjVar2 ObjVar3 ValVar1 ValVar0 ValVar4 ValVar9 ValVar12 ValVar18 +ValVar15
(0x7f000002) (0x7f000003)
Software Verification https://github.com/SVF-tools/Teaching-Software-Verification

Interprocedural Example
Algorithm 3 handleIntra(intraEdge)
if intraEdge.getCondition() && !handleBranch(intraEdge) then
return false
handleNonBranch(edge)
HandleNonBranch(intraEdge)
dst ← intraEdge.getDstNode(); src ← intraEdge.getSrcNode()
foreach stmt ∈ dst.getSVFStmts() do …
11 12 13 14
15 16 17 18
19 20 21 22 23 24
else if load ∈ dyn cast⟨LoadStmt⟩(stmt) then lhs ← getZ3Expr(load.getLHSVarID())
rhs ← getZ3Expr(load.getRHSVarID()) addToSolver(lhs == z3Mgr.loadValue(rhs))
else if gep ∈ dyn cast⟨GepStmt⟩(stmt) then
lhs ← getZ3Expr(gep.getLHSVarID())
rhs ← getZ3Expr(gep.getRHSVarID())
offset = z3Mgr.getGepOffset(gep)
gepAddress = z3Mgr.getGepObjAddress(rhs, offset) addToSolver(lhs == gepAddress)
FunEntryICFGNode1 {fun:foo}
IntraICFGNode6 {fun: main} AddrStmt: [Var15 !” Var16]
%a = alloca i32
IntraICFGNode2 {fun: foo} StoreStmt: [Var7 !” Var9]
store i32 1,i32* %p
IntraICFGNode7 {fun: main}
StoreStmt: [Var15 !” Var18]
store i32 0,i32* %a
IntraICFGNode3 {fun: foo}
CallCFGNode8 {fun: main} CallPE: [Var7 !” Var15]
call void @foo(i32* %a)
0x5583fba7
RetICFGNode12 {fun:main}
FunExitICFGNode4 {fun:foo} 0x5583fba7
IntraICFGNode10 {fun: main} LoadStmt: [Var21 !” Var15]
%0 = load i32, i32* %a
IntraICFGNode11 {fun: main}
CmpStmt: [Var22 !” Var21 pred32 Var9]
%cmp = icmp eq i32 %0,1
GlobalICFGNode0
CopyStmt: [Var1 !” Var0] i8* null AddrStmt: [Var9 !” Var10] i32 1 AddrStmt: [Var18 !” Var19] i32 0 AddrStmt: [Var4 !” Var5] foo AddrStmt: [Var12 !” Var13] main AddrStmt: [Var24 !” Var25] svf_assert
else if store ∈ dyn cast⟨StoreStmt⟩(stmt) then lhs ← getZ3Expr(store.getLHSVarID())
rhs ← getZ3Expr(store.getRHSVarID()) z3Mgr.storeValue(lhs, rhs)
Software Verification https://github.com/SVF-tools/Teaching-Software-Verification

程序代写 CS代考加QQ: 749389476
Interprocedural Example
GlobalICFGNode0
CopyStmt: [Var1 !” Var0] i8* null AddrStmt: [Var9 !” Var10] i32 1 AddrStmt: [Var18 !” Var19] i32 0 AddrStmt: [Var4 !” Var5] foo AddrStmt: [Var12 !” Var13] main AddrStmt: [Var24 !” Var25] svf_assert
FunEntryICFGNode1 {fun:foo}
IntraICFGNode6 {fun: main} AddrStmt: [Var15 !” Var16]
%a = alloca i32
IntraICFGNode2 {fun: foo} StoreStmt: [Var7 !” Var9]
store i32 1,i32* %p
IntraICFGNode7 {fun: main}
StoreStmt: [Var15 !” Var18]
store i32 0,i32* %a
IntraICFGNode3 {fun: foo}
CallCFGNode8 {fun: main} CallPE: [Var7 !” Var15]
call void @foo(i32* %a)
0x5583fba7
RetICFGNode12 {fun:main}
FunExitICFGNode4 {fun:foo} 0x5583fba7
IntraICFGNode10 {fun: main} LoadStmt: [Var21 !” Var15]
%0 = load i32, i32* %a
IntraICFGNode11 {fun: main}
CmpStmt: [Var22 !” Var21 pred32 Var9]
%cmp = icmp eq i32 %0,1
————-SVFVar and ObjVar25 (0x7f000019) ObjVar19 (0x7f000013) ObjVar16 (0x7f000010) ObjVar13 (0x7f00000d) ObjVar10 (0x7f00000a) ObjVar5 (0x7f000005) ValVar24
ObjVar2 (0x7f000002)
ObjVar3 ValVar1 ValVar0 ValVar4 ValVar9 ValVar12 +ValVar18
Value————- Value: NULL
Value: NULL Value: 1
Value: NULL Value: 0x7f000019 Value: NULL
Value: 0x7f000010
Value: NULL Value: 2
Value: 0x7f000005 Value: 1
Value: 0x7f00000d
(0x7f000003)
… ——————————————
## Analyzing IntraICFGNode6 {fun: main} StoreStmt: [Var15 ← Var18]
store i32 0, i32 ∗ %a
Software Verification https://github.com/SVF-tools/Teaching-Software-Verification

Interprocedural Example
GlobalICFGNode0
CopyStmt: [Var1 !” Var0] i8* null AddrStmt: [Var9 !” Var10] i32 1 AddrStmt: [Var18 !” Var19] i32 0 AddrStmt: [Var4 !” Var5] foo AddrStmt: [Var12 !” Var13] main AddrStmt: [Var24 !” Var25] svf_assert
IntraICFGNode6 {fun: main} AddrStmt: [Var15 !” Var16]
%a = alloca i32
IntraICFGNode2 {fun: foo} StoreStmt: [Var7 !” Var9]
store i32 1,i32* %p
IntraICFGNode7 {fun: main}
StoreStmt: [Var15 !” Var18]
IntraICFGNode3 {fun: foo}
store i32 0,i32* %a
CallCFGNode8 {fun: main} CallPE: [Var7 !” Var15]
call void @foo(i32* %a)
RetICFGNode12 {fun:main}
FunEntryICFGNode1 {fun:foo}
FunExitICFGNode4 {fun:foo} 0x5583fba7
0x5583fba7
IntraICFGNode10 {fun: main} LoadStmt: [Var21 !” Var15]
%0 = load i32, i32* %a
IntraICFGNode11 {fun: main}
CmpStmt: [Var22 !” Var21 pred32 Var9]
%cmp = icmp eq i32 %0,1
callEdge retEdge
1 2 3 4 5 6 7
Algorithm 4 handleCall(callEdge)
callNode ← callEdge.getSrcNode(); FunEntryNode ←callEdge.getDstNode(); getSolver().push();
foreach callPE ∈ calledge.getCallPEs() do lhs ← getZ3Expr(callPE.getLHSVarID()); rhs ← getZ3Expr(callPE.getRHSVarID()); addToSolver(lhs == rhs);
return true;
Software Verification https://github.com/SVF-tools/Teaching-Software-Verification

Interprocedural Example
GlobalICFGNode0
CopyStmt: [Var1 !” Var0] i8* null AddrStmt: [Var9 !” Var10] i32 1 AddrStmt: [Var18 !” Var19] i32 0 AddrStmt: [Var4 !” Var5] foo AddrStmt: [Var12 !” Var13] main AddrStmt: [Var24 !” Var25] svf_assert
IntraICFGNode6 {fun: main} AddrStmt: [Var15 !” Var16]
%a = alloca i32
IntraICFGNode2 {fun: foo} StoreStmt: [Var7 !” Var9]
store i32 1,i32* %p
IntraICFGNode7 {fun: main}
StoreStmt: [Var15 !” Var18]
IntraICFGNode3 {fun: foo}
store i32 0,i32* %a
CallCFGNode8 {fun: main} CallPE: [Var7 !” Var15]
call void @foo(i32* %a)
RetICFGNode12 {fun:main}
FunEntryICFGNode1 {fun:foo}
FunExitICFGNode4 {fun:foo} 0x5583fba7
0x5583fba7
IntraICFGNode10 {fun: main} LoadStmt: [Var21 !” Var15]
%0 = load i32, i32* %a
IntraICFGNode11 {fun: main}
CmpStmt: [Var22 !” Var21 pred32 Var9]
%cmp = icmp eq i32 %0,1
callEdge retEdge
State of callstack after processing call edge between CallCFGNode8 and FunEntryICFGNode1
0x5583fba7
path (a sequence of ICFGNodes
represented by their IDs)
Software Verification https://github.com/SVF-tools/Teaching-Software-Verification

Interprocedural Example
Algorithm 3 handleIntra(intraEdge)
if intraEdge.getCondition() && !handleBranch(intraEdge) then
return false
handleNonBranch(edge)
HandleNonBranch(intraEdge)
dst ← intraEdge.getDstNode(); src ← intraEdge.getSrcNode()
foreach stmt ∈ dst.getSVFStmts() do …
11 12 13 14
15 16 17 18
19 20 21 22 23 24
else if load ∈ dyn cast⟨LoadStmt⟩(stmt) then lhs ← getZ3Expr(load.getLHSVarID())
rhs ← getZ3Expr(load.getRHSVarID()) addToSolver(lhs == z3Mgr.loadValue(rhs))
else if gep ∈ dyn cast⟨GepStmt⟩(stmt) then
lhs ← getZ3Expr(gep.getLHSVarID())
rhs ← getZ3Expr(gep.getRHSVarID())
offset = z3Mgr.getGepOffset(gep)
gepAddress = z3Mgr.getGepObjAddress(rhs, offset) addToSolver(lhs == gepAddress)
GlobalICFGNode0
CopyStmt: [Var1 !” Var0] i8* null AddrStmt: [Var9 !” Var10] i32 1 AddrStmt: [Var18 !” Var19] i32 0 AddrStmt: [Var4 !” Var5] foo AddrStmt: [Var12 !” Var13] main AddrStmt: [Var24 !” Var25] svf_assert
IntraICFGNode6 {fun: main} AddrStmt: [Var15 !” Var16]
%a = alloca i32
IntraICFGNode2 {fun: foo} StoreStmt: [Var7 !” Var9]
store i32 1,i32* %p
IntraICFGNode7 {fun: main}
StoreStmt: [Var15 !” Var18]
store i32 0,i32* %a
IntraICFGNode3 {fun: foo}
CallCFGNode8 {fun: main} CallPE: [Var7 !” Var15]
call void @foo(i32* %a)
else if store ∈ dyn cast⟨StoreStmt⟩(stmt) then lhs ← getZ3Expr(store.getLHSVarID())
rhs ← getZ3Expr(store.getRHSVarID()) z3Mgr.storeValue(lhs, rhs)
IntraICFGNode10 {fun: main} LoadStmt: [Var21 !” Var15]
%0 = load i32, i32* %a
IntraICFGNode11 {fun: main}
CmpStmt: [Var22 !” Var21 pred32 Var9]
%cmp = icmp eq i32 %0,1
Software Verification https://github.com/SVF-tools/Teaching-Software-Verification
FunEntryICFGNode1 {fun:foo}
0x5583fba7
RetICFGNode12 {fun:main}
FunExitICFGNode4 {fun:foo} 0x5583fba7

Interprocedural Example
GlobalICFGNode0
CopyStmt: [Var1 !” Var0] i8* null AddrStmt: [Var9 !” Var10] i32 1 AddrStmt: [Var18 !” Var19] i32 0 AddrStmt: [Var4 !” Var5] foo AddrStmt: [Var12 !” Var13] main AddrStmt: [Var24 !” Var25] svf_assert
IntraICFGNode6 {fun: main} AddrStmt: [Var15 !” Var16]
%a = alloca i32
IntraICFGNode2 {fun: foo} StoreStmt: [Var7 !” Var9]
store i32 1,i32* %p
IntraICFGNode7 {fun: main}
StoreStmt: [Var15 !” Var18]
store i32 0,i32* %a
IntraICFGNode3 {fun: foo}
CallCFGNode8 {fun: main} CallPE: [Var7 !” Var15]
call void @foo(i32* %a)
FunExitICFGNode4 {fun:foo} 0x5583fba7
RetICFGNode12 {fun:main}
IntraICFGNode10 {fun: main} LoadStmt: [Var21 !” Var15]
%0 = load i32, i32* %a
IntraICFGNode11 {fun: main}
CmpStmt: [Var22 !” Var21 pred32 Var9]
%cmp = icmp eq i32 %0,1
FunEntryICFGNode1 {fun:foo}
0x5583fba7
Algorithm 5 handleRet(retEdge)
rhs(getCtx());
if retPE ← retEdge.getRetPE() then
rhs ← getEvalExpr(getZ3Expr(retPE.getRHSVarID()));
getSolver().pop();
if retPE ← retEdge.getRetPE() then
lhs ← getZ3Expr(retPE.getLHSVarID()); addToSolver(lhs == rhs);
return true;
Software Verification https://github.com/SVF-tools/Teaching-Software-Verification

Interprocedural Example
GlobalICFGNode0
CopyStmt: [Var1 !” Var0] i8* null AddrStmt: [Var9 !” Var10] i32 1 AddrStmt: [Var18 !” Var19] i32 0 AddrStmt: [Var4 !” Var5] foo AddrStmt: [Var12 !” Var13] main AddrStmt: [Var24 !” Var25] svf_assert
IntraICFGNode6 {fun: main} AddrStmt: [Var15 !” Var16]
%a = alloca i32
IntraICFGNode2 {fun: foo} StoreStmt: [Var7 !” Var9]
store i32 1,i32* %p
IntraICFGNode7 {fun: main}
StoreStmt: [Var15 !” Var18]
store i32 0,i32* %a
IntraICFGNode3 {fun: foo}
CallCFGNode8 {fun: main} CallPE: [Var7 !” Var15]
call void @foo(i32* %a)
FunExitICFGNode4 {fun:foo} 0x5583fba7
RetICFGNode12 {fun:main}
IntraICFGNode10 {fun: main} LoadStmt: [Var21 !” Var15]
%0 = load i32, i32* %a
IntraICFGNode11 {fun: main}
CmpStmt: [Var22 !” Var21 pred32 Var9]
%cmp = icmp eq i32 %0,1
0x5583fba7
path (a sequence of ICFGNodes
represented by their IDs)
0x5583fba7
getCallICFGNode()
FunEntryICFGNode1 {fun:foo}
0x5583fba7
State of callstack while processing return edge from FunExitICFGNode4 to RetICFGNode12
Software Verification https://github.com/SVF-tools/Teaching-Software-Verification

Interprocedural Example
Algorithm 3 handleIntra(intraEdge)
if intraEdge.getCondition() && !handleBranch(intraEdge) then
return false
handleNonBranch(edge)
HandleNonBranch(intraEdge)
dst ← intraEdge.getDstNode(); src ← intraEdge.getSrcNode()
foreach stmt ∈ dst.getSVFStmts() do …
GlobalICFGNode0
CopyStmt: [Var1 !” Var0] i8* null AddrStmt: [Var9 !” Var10] i32 1 AddrStmt: [Var18 !” Var19] i32 0 AddrStmt: [Var4 !” Var5] foo AddrStmt: [Var12 !” Var13] main AddrStmt: [Var24 !” Var25] svf_assert
IntraICFGNode2 {fun: foo} StoreStmt: [Var7 !” Var9]
store i32 1,i32* %p
FunEntryICFGNode1 {fun:foo}
IntraICFGNode6 {fun: main} AddrStmt: [Var15 !” Var16]
%a = alloca i32
IntraICFGNode7 {fun: main}
StoreStmt: [Var15 !” Var18]
store i32 0,i32* %a
IntraICFGNode3 {fun: foo}
11 12 13 14
15 16 17 18
19 20 21 22 23 24
else if store ∈ dyn cast⟨StoreStmt⟩(stmt) then lhs ← getZ3Expr(store.getLHSVarID())
rhs ← getZ3Expr(store.getRHSVarID()) z3Mgr.storeValue(lhs, rhs)
else if gep ∈ dyn cast⟨GepStmt⟩(stmt) then
lhs ← getZ3Expr(gep.getLHSVarID())
rhs ← getZ3Expr(gep.getRHSVarID())
offset = z3Mgr.getGepOffset(gep)
gepAddress = z3Mgr.getGepObjAddress(rhs, offset) addToSolver(lhs == gepAddress)
else if load ∈ dyn cast⟨LoadStmt⟩(stmt) then lhs ← getZ3Expr(load.getLHSVarID())
rhs ← getZ3Expr(load.getRHSVarID()) addToSolver(lhs == z3Mgr.loadValue(rhs))
CallCFGNode8 {fun: main} CallPE: [Var7 !” Var15]
call void @foo(i32* %a)
0x5583fba7
RetICFGNode12 {fun:main}
FunExitICFGNode4 {fun:foo} 0x5583fba7
IntraICFGNode10 {fun: main} LoadStmt: [Var21 !” Var15]
%0 = load i32, i32* %a
IntraICFGNode11 {fun: main}
CmpStmt: [Var22 !” Var21 pred32 Var9]
%cmp = icmp eq i32 %0,1
Software Verification https://github.com/SVF-tools/Teaching-Software-Verification

Interprocedural Example
GlobalICFGNode0
CopyStmt: [Var1 !” Var0] i8* null AddrStmt: [Var9 !” Var10] i32 1 AddrStmt: [Var18 !” Var19] i32 0 AddrStmt: [Var4 !” Var5] foo AddrStmt: [Var12 !” Var13] main AddrStmt: [Var24 !” Var25] svf_assert
FunEntryICFGNode1 {fun:foo}
IntraICFGNode6 {fun: main} AddrStmt: [Var15 !” Var16]
%a = alloca i32
IntraICFGNode2 {fun: foo} StoreStmt: [Var7 !” Var9]
store i32 1,i32* %p
IntraICFGNode7 {fun: main}
StoreStmt: [Var15 !” Var18]
store i32 0,i32* %a
IntraICFGNode3 {fun: foo}
CallCFGNode8 {fun: main} CallPE: [Var7 !” Var15]
call void @foo(i32* %a)
0x5583fba7
RetICFGNode12 {fun:main}
FunExitICFGNode4 {fun:foo} 0x5583fba7
IntraICFGNode10 {fun: main} LoadStmt: [Var21 !” Var15]
%0 = load i32, i32* %a
IntraICFGNode11 {fun: main}
CmpStmt: [Var22 !” Var21 pred32 Var9]
%cmp = icmp eq i32 %0,1
————-SVFVar and ObjVar25 (0x7f000019) ObjVar19 (0x7f000013) ObjVar16 (0x7f000010) ObjVar13 (0x7f00000d) ObjVar10 (0x7f00000a) ObjVar5 (0x7f000005) ValVar24
ObjVar2 (0x7f000002) ValVar15
Value————- Value: NULL
Value: NULL Value: 1
Value: NULL Value: 0x7f000019 Value: 1
Value: NULL Value: 0x7f000010 Value: NULL Value: 2
Value: 0x7f000005 Value: 1
Value: 0x7f00000d Value: 0
ValVar18 ——————————————
(0x7f000003)
The assertion is successfully verified!!
START: 0 → 6 → 7 → 8 → 1 → 2 → 3 → 4 → 12 → 10 → 11 → … → END
Software Verification https://github.com/SVF-tools/Teaching-Software-Verification

Programming Help
Branch Example
int main(){
int x = 1, y = 1; int a = 1, b = 2; if (a > b) {
y++; } else { x++;
svf_assert (x == 2); }
return 0; }
%cmp = icmp sgt i32 1, 2
br i1 %cmp, label %if.then, label %if.else if.then:
%inc = add nsw i32 1, 1
br label %if.end if.else:
%inc1 = add nsw i32 1, 1
%cmp2 = icmp eq i32 %inc1, 2
call void @svf_assert(i1 zeroext %cmp2) br label %if.end
if.end: ret i32 0 }
i32 @main() { entry:
Software Verification https://github.com/SVF-tools/Teaching-Software-Verification

Branch Example
int main(){
int x = 1, y = 1; int a = 1, b = 2; if (a > b) {
y++; } else { x++;
svf_assert (x == 2); }
return 0; }
%cmp = icmp sgt i32 1, 2
IntraICFGNode2 {fun: main}
CmpStmt: [Var7 !” Var8 pred38 Var10]
%cmp = icmp eq i32 1,2
IntraICFGNode3 {fun: main}
BranchStmt: [Condition Var7]
br i1% cmp,label %if.then label %if.else
i32 @main() { entry:
br i1 %cmp, label %if.then, label %if.else if.then:
%inc = add nsw i32 1, 1
br label %if.end if.else:
%inc1 = add nsw i32 1, 1
%cmp2 = icmp eq i32 %inc1, 2
call void @svf_assert(i1 zeroext %cmp2) br label %if.end
if.end: ret i32 0 }
IntraCFGNode5 {fun: main}
BinaryOPStmt: Var16 !”(Var8 opcode13 Var8)
%inc1 = add nsw i32 1,1
CopyStmt: [Var1 !” Var0] i8* null AddrStmt: [Var8 !” Var9] i32 1 AddrStmt: [Var10 !” Var11] i32 2 AddrStmt: [Var23 !” Var24] i32 0 AddrStmt: [Var4 !” Var5] main AddrStmt: [Var19 !” Var20] svf_assert
IntraICFGNode7 {fun: main}
CmpStmt: [Var17 !” Var16 pred32 Var10]
%cmp2=icmp eq i32 %inc1,2
svf_assert(x!#2)
GlobalICFGNode0
IntraCFGNode4 {fun: main}
BinaryOPStmt: Var16 !”(Var8 opcode13 Var8)
%inc = add nsw i32 1,1
Software Verification https://github.com/SVF-tools/Teaching-Software-Verification

Branch Example
————-SVFVar and ObjVar20 (0x7f000014) ObjVar24 (0x7f000018) ObjVar11 (0x7f00000b) ObjVar9 (0x7f000009) ObjVar5 (0x7f000005) ValVar19
ObjVar2 ObjVar3 ValVar1 ValVar0 ValVar4 ValVar8 ValVar10
Value————- Value: NULL
Value: NULL Value: 0x7f000014 Value: 0
Value: NULL Value: NULL Value: 3
Value: 0x7f000005 Value: 1
(0x7f000002) (0x7f000003)
… ——————————————
The values of Z3 expressions for each SVFVar after analyzing GlobalICFGNode0
GlobalICFGNode0
CopyStmt: [Var1 !” Var0] i8* null AddrStmt: [Var8 !” Var9] i32 1 AddrStmt: [Var10 !” Var11] i32 2 AddrStmt: [Var23 !” Var24] i32 0 AddrStmt: [Var4 !” Var5] main AddrStmt: [Var19 !” Var20] svf_assert
IntraICFGNode2 {fun: main}
CmpStmt: [Var7 !” Var8 pred38 Var10]
%cmp = icmp eq i32 1,2
IntraICFGNode3 {fun: main}
BranchStmt: [Condition Var7]
br i1% cmp,label %if.then label %if.else
IntraCFGNode5 {fun: main}
BinaryOPStmt: Var16 !”(Var8 opcode13 Var8)
%inc1 = add nsw i32 1,1
IntraCFGNode4 {fun: main}
BinaryOPStmt: Var16 !”(Var8 opcode13 Var8)
%inc = add nsw i32 1,1
IntraICFGNode7 {fun: main}
CmpStmt: [Var17 !” Var16 pred32 Var10]
%cmp2=icmp eq i32 %inc1,2
svf_assert(x!#2)
Software Verification https://github.com/SVF-tools/Teaching-Software-Verification

Branch Example
## Analyzing IntraICFGNode2 {fun: main} CmpStmt: [Var7 <-- (Var8 predicate38 Var10)] %cmp = icmp sgt i32 1, 2 ==> (not (<= ValVar8 ValVar10)) ==> (= ValVar7 0)
Code for handling CmpStmt has been implemented in the HandleNonBranch() function.
GlobalICFGNode0
CopyStmt: [Var1 !” Var0] i8* null AddrStmt: [Var8 !” Var9] i32 1 AddrStmt: [Var10 !” Var11] i32 2 AddrStmt: [Var23 !” Var24] i32 0 AddrStmt: [Var4 !” Var5] main AddrStmt: [Var19 !” Var20] svf_assert
IntraICFGNode2 {fun: main}
CmpStmt: [Var7 !” Var8 pred38 Var10]
%cmp = icmp eq i32 1,2
IntraICFGNode3 {fun: main}
BranchStmt: [Condition Var7]
br i1% cmp,label %if.then label %if.else
IntraCFGNode5 {fun: main}
BinaryOPStmt: Var16 !”(Var8 opcode13 Var8)
%inc1 = add nsw i32 1,1
IntraCFGNode4 {fun: main}
BinaryOPStmt: Var16 !”(Var8 opcode13 Var8)
%inc = add nsw i32 1,1
IntraICFGNode7 {fun: main}
CmpStmt: [Var17 !” Var16 pred32 Var10]
%cmp2=icmp eq i32 %inc1,2
svf_assert(x!#2)
Software Verification https://github.com/SVF-tools/Teaching-Software-Verification

Branch Example
1 2 3 4 5 6
Algorithm 3 handleIntra(intraEdge)
if intraEdge.getCondition() && !handleBranch(intraEdge) then
return false
handleNonBranch(edge)
handleBranch(intraEdge)
cond = intraEdge.getCondition()
successorVal = intraEdge.getSuccessorCondValue() res = getEvalExpr(cond == suc)
if res.is false() then addToSolver(cond! = suc) return false
else if res.is true() then addToSolver(cond == suc) return true
return true
GlobalICFGNode0
CopyStmt: [Var1 !” Var0] i8* null AddrStmt: [Var8 !” Var9] i32 1 AddrStmt: [Var10 !” Var11] i32 2 AddrStmt: [Var23 !” Var24] i32 0 AddrStmt: [Var4 !” Var5] main AddrStmt: [Var19 !” Var20] svf_assert
IntraICFGNode2 {fun: main}
CmpStmt: [Var7 !” Var8 pred38 Var10]
%cmp = icmp eq i32 1,2
IntraICFGNode3 {fun: main}
BranchStmt: [Condition Var7]
br i1% cmp,label %if.then label %if.else
IntraCFGNode5 {fun: main}
BinaryOPStmt: Var16 !”(Var8 opcode13 Var8)
%inc1 = add nsw i32 1,1
IntraCFGNode4 {fun: main}
BinaryOPStmt: Var16 !”(Var8 opcode13 Var8)
%inc = add nsw i32 1,1
IntraICFGNode7 {fun: main}
CmpStmt: [Var17 !” Var16 pred32 Var10]
%cmp2=icmp eq i32 %inc1,2
svf_assert(x!#2)
Software Verification https://github.com/SVF-tools/Teaching-Software-Verification

程序代写 CS代考加微信: cstutorcs
Branch Example
GlobalICFGNode0
CopyStmt: [Var1 !” Var0] i8* null AddrStmt: [Var8 !” Var9] i32 1 AddrStmt: [Var10 !” Var1