Skip to content

Assignment 2 Python

Jump to bottom
bjjwwang edited this page May 7, 2025 · 5 revisions 
../Assignment-2
|-- CPP
|   |-- Assignment-2.cpp
|   |-- Assignment-2.h
|   |-- CMakeLists.txt
|   |-- Z3SSEMgr.cpp
|   |-- Z3SSEMgr.h
|   `-- test-sse.cpp
|-- Python
|   |-- Ass2_helper.py
|   |-- Assignment2.py
|   |-- CMakeLists.txt
|   |-- Main.py
|   `-- Test.py
`-- Tests
    `-- testcases
        `-- sse
            |-- test1.c
            |-- test1.ll
            |-- test2.c
            |-- test2.ll
            |-- test3.c
            `-- test3.ll

1. Get the latest assignment-2 code template

* 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.

2. Assignment 2 task

- Implement the following methods of class SSE in Assignment-2.py

Method Description
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
collect_and_translate_path 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 translate_path to convert each path into Z3 expressions. Note that translate_path returns true if the path is feasible, infeasible otherwise. (3) If a path is feasible, you will need to call assert_checking to verify the assertion (which is the last ICFGNode of this path).
handle_call Translate callPE and return true if the path is feasible, otherwise infeasible (returning false)
handle_ret Translate retPE and return true if the path is feasible, otherwise infeasible (returning false)
handle_branch Translate branch intraICFGEdge and evaluate the branch condition and return true if the branch evaluated is feasible, otherwise infeasible
handle_intra Translate AddrStmt, CopyStmt, LoadStmt, StoreStmt, GepStmt, CmpStmt,BinaryOPStmt,PhiStmt into constraints

- Run Test Pass the test without any assertion by Test.py.

- Upload Assignment2.py to UNSW WebCMS for your submission when you are finished with this assignment.

Your implementation will be evaluated against X number of our internal tests. If you pass Y tests, you will receive Y/X * 100% marks. 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.py 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.

3. Configuration, Debug and visualize ICFG

To enable debugging and running, switch your executable by setting the program and args fields as described here or follow the below screenshot.

Clone this wiki locally