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

You need to set the "program" to be the executable file of Lab 2, i.e., "${workspaceFolder}/bin/lab2" and "args" to include one of the tests, e.g., ["test1"] in launch.json in order to run and debug

{
  "version": "0.2.0",
  "configurations": [
    {
      "name": "(gdb) Launch",
      "type": "cppdbg",
      "request": "launch",
      "program": "${workspaceFolder}/bin/lab2",
      "args": ["test1"],
      "stopAtEntry": false,
      "cwd": "${workspaceFolder}",
      "environment": [],
      "MIMode": "gdb",
      "setupCommands": [
        {
          "description": "Enable pretty-printing for gdb",
          "text": "-enable-pretty-printing",
          "ignoreFailures": true
        }
      ],
      "preLaunchTask": "C/C++: cpp build active file"
    }
  ]
}

2. Lab-Exercise-2 task

1. Implement methods from Z3ExampleMgr::test1() to Z3ExampleMgr::test7() in class Z3ExampleMgr in Z3ExampleMgr.cpp
2. Run ctest -R lab2 -VV and pass the test without any assertion by test.cpp.
3. Submit Z3Mgr.cpp to UNSW WebCMS or give. Your implementation will be evaluated against our 7 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

SVF Z3Mgr APIs to help with your implementation SVF Z3Mgr API.

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;
}