-
Notifications
You must be signed in to change notification settings - Fork 10
Assignment 2
Yulei Sui edited this page Jul 12, 2024
·
19 revisions
$tree Assignment-2
├── Assignment-2.cpp
├── Assignment-2.h
├── CMakeLists.txt
└── Tests
├── CMakeLists.txt
├── test-sse.cpp
└── testcases
└── sse
├── test1.ll
├── test1.c
├── test2.ll
├── test2.c
├── test3.ll
└── test3.c
* Before coding, please type cd $HOME/Software-Security-Analysis
and git pull
in your terminal to make sure you always have the latest version of the code template before each assignment.
If git pull
fails due to the conflict with your local changes, type git stash
to store your current code in a temporal branch and type git pull
again. If you want to retrieve your code back, type git stash pop
.
Make sure to switch your program to ass2
before coding.
- Implement the following methods of class SSE
in Assignment-2.cpp
Method | Description | Marks |
---|---|---|
SSE::reachability |
Control-flow reachability analysis starting from the entry (GlobalICFGNode) of the program. The method differs from Assignment-1 only in the first argument which is ICFGEdge* rather than ICFGNode*
|
10% |
SSE::collectAndTranslatePath |
Collect each program path from the entry to each assertion of the program. In this function, you will need to (1) add each path into the paths set, (2) call translatePath to convert each path into Z3 expressions. Note that translatePath returns true if the path is feasible, infeasible otherwise. (3) If a path is feasible, you will need to call assertchecking to verify the assertion (which is the last ICFGNode of this path). |
20% |
SSE::handleCall |
Translate callPE and return true if the path is feasible, otherwise infeasible (returning false) | 10% |
SSE::handleRet |
Translate retPE and return true if the path is feasible, otherwise infeasible (returning false) | 10% |
SSE::handleBranch |
Translate branch intraICFGEdge and evaluate the branch condition and return true if the branch evaluated is feasible, otherwise infeasible | 20% |
SSE::handleNonBranch |
Translate AddrStmt , CopyStmt , LoadStmt , StoreStmt , GepStmt , CmpStmt into constraints |
30% (5% each) |
- Run ctest -R ass2 -VV
Pass the test without any assertion by test-sse.cpp
.
- Upload Assignment-2.cpp
to UNSW WebCMS
for your submission when you are finished with this assignment. Your implementation will be evaluated against our internal tests. You will get full marks if your code can pass them all. Unfortunately, our internal tests are publicly unavailable. Here, we only provided limited test cases 3 test cases under `Assignment-2/Tests/testcases/sse
`. You are encouraged to add more test cases by yourself to validate the correctness of your implementation.
*You will be working on Assignment-2.cpp
only and there is NO need to modify other files under the Assignment-2 folder
SVF APIs to help with your implementation SVF Z3 API.
To enable debugging and running, switch your executable by setting the program
and args
fields as described here or follow the below screenshot.
Visualize ICFG by following here