Assignment 4

Assignment 4: Static Symbolic Execution

Assignment 4 implements an assertion-based verifier. It traverses every context-sensitive ICFG path from the program entry to a call of assert, svf_assert, or sink, translates the path into Z3 constraints, discards infeasible paths, and checks whether the assertion can fail.

Before starting, complete the ungraded Lab Z3 warm-up to practise writing the corresponding Z3 expressions by hand.

Folder layout

Assignment-4
|-- Assignment-4.cpp
|-- Assignment-4.h
|-- CMakeLists.txt
|-- Tests
|   `-- testcases
|       `-- sse
|           |-- test1.c
|           |-- test1.ll
|           |-- test2.c
|           |-- test2.ll
|           |-- test3.c
|           |-- test3.ll
|           |-- test4.c
|           `-- test4.ll
|-- Z3Mgr.cpp
|-- Z3Mgr.h
|-- Z3SSEMgr.cpp
|-- Z3SSEMgr.h
`-- test-sse.cpp

1. Configure Assignment 4

Make sure you have the latest code, then switch the VS Code launch target to:

"program": "${workspaceFolder}/bin/ass4",
"args": ["${workspaceFolder}/Assignment-4/Tests/testcases/sse/test1.ll"]

The executable accepts LLVM bitcode (.ll) as input. The matching .c files are provided to make each test easier to understand.

2. Task

Implement the TODOs in Assignment-4.cpp:

Method	Description
SVF::SSE::reachability(const ICFGEdge*, const ICFGNode*)	Traverse context-sensitive ICFG paths from the GlobalICFGNode to each assertion. Match calls with returns and visit a loop or recursive expansion only once per active path so the traversal terminates.
SVF::SSE::collectAndTranslatePath()	Record each completed path, translate it, check its assertion when feasible, and reset the solver and translation context before processing the next path.
SVF::SSE::handleCall(const CallCFGEdge*)	Translate actual-to-formal parameter assignments and update callingCtx.
SVF::SSE::handleRet(const RetCFGEdge*)	Translate the return-to-receiver assignment, when present, and restore callingCtx.
SVF::SSE::handleBranch(const IntraCFGEdge*)	Add the selected branch condition to Z3 and return whether that branch remains feasible.
SVF::SSE::handleNonBranch(const IntraCFGEdge*)	Translate AddrStmt, CopyStmt, LoadStmt, StoreStmt, GepStmt, and integer CmpStmt operations into Z3 constraints.

BinaryOPStmt, SelectStmt, PhiStmt, path dispatch in translatePath, and assertion checking are already provided. Do not reimplement them.

For CmpStmt, handle the integer predicates listed in the source comments: ICMP_EQ, ICMP_NE, unsigned and signed <, <=, >, and >=. This assignment assumes integer arithmetic does not overflow.

You only need to modify Assignment-4.cpp. Your submission will also be evaluated with non-public tests, so add your own small .c and .ll cases when checking edge conditions.

Useful references:

• Z3 API used by Assignment 4
• SVF C++ API
• Assignment-4.h, which provides the solver, path, and calling-context helpers

3. Build and test

Build Assignment 4 from the repository root:

cmake .
make ass4 -j8

Run all public Assignment 4 tests:

ctest -R '^ass4-cpp/' -VV

Run one test directly:

./bin/ass4 Assignment-4/Tests/testcases/sse/test1.ll

The public tests exercise the following features:

Test	Main features
test1	Arrays, GEP, interprocedural calls, loads, and stores
test2	Division, remainder, branches, and Phi statements
test3	Interprocedural pointer updates and return handling
test4	Branch feasibility and comparison constraints

A correct implementation verifies every reachable assertion without triggering a C++ assertion and exits successfully.