Lab Exercise 2

Lab-Exercise-2 folder layout

$tree Lab-Exercise-2
├── Z3ExampleMgr.cpp
├── Z3ExampleMgr.h
├── Z3Mgr.cpp
├── Z3Mgr.h
├── CMakeLists.txt
├── test.cpp

1. Get the latest Lab-Exercise-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 coding.

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.

1.1 launch.json

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

2. Lab-Exercise-2 task

1. Implement methods from Z3ExampleMgr::test1() to Z3ExampleMgr::test7() in class Z3ExampleMgr in Z3ExampleMgr.cpp to translate C code into Z3 logic expressions and solve them to prove assertions. SVF Z3Mgr APIs to help with your implementation SVF Z3Mgr API.

Method	Description	Marks
test1	Code statements with simple integers	12%
test2	Code statements with single-level pointers	12%
test3	Code statements with multi-level pointers	12%
test4	Code statements with array and pointers	12%
test5	Code statements with struct and pointers	12%
test6	Code statements with branches	20%
test7	Code statements with calls	20%

2. Run ctest -R lab2 -VV and pass the test without any assertion by test.cpp.
3. Upload Z3Example.cpp to UNSW WebCMS for your submission when you are finished with this lab. Your implementation will be evaluated against our internal tests. You will get the full marks if your code can pass them all. We have provided Z3ExampleMgr::test0() in Test3.cpp as an example to help get started.

*You will be working on Z3Mgr.cpp only and there is NO need to modify other files under the Lab-Exercise-2 folder

3. Debugging

If you try to check the value of z3Expr, you can use to_string() to see the value. For example,

#include <iostream>
#include <z3++.h>  

int main() {
    z3::context c;
    z3::expr x = c.int_const("x");
    z3::expr y = c.int_const("y");
    z3::expr formula = x > y;
    std::string expr_as_string = formula.to_string();
    std::cout << "The expression is: " << expr_as_string << std::endl;
    return 0;
}