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::test10() 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. We have provided Z3ExampleMgr::test1() to Z3ExampleMgr::test3() with some result validation code in test.cpp as examples to help you write your validation for the remaining test4() to test10().

2. Note that the validation code in test1() to test2() is not meant to be complete. Given a program prog and an assert Q, you are expected to (1) translate the negation of Q and check unsat of prog ∧ ¬Q to prove the non-existence of counterexamples, and (2) also evaluate individual variables’ values (e.g., a) if you know a’s value is 3. For example, z3Mgr->getEvalExpr(a) == 3. When we do the marking, we will also evaluate the values of some Z3 expressions given their string names, so it is better to name them consistently with the names of the C variables. We will not evaluate expressions that do not correspond to the original C variables.

3. For closed-world programs (value initializations are fixed and there are no inputs from externals), checking sat of prog ∧ Q is the same as checking unsat prog ∧ ¬Q

Method	Description	Marks
test1	Code statements with simple integers	10%
test2	Code statements with single-level pointers	10%
test3	Code statements with multi-level pointers	10%
test4	Code statements with array and pointers	10%
test5	Code statements with branches	10%
test6	Code statements with comparison and pointers	10%
test7	Code statements with binary operations	10%
test8	Code statements with array and branches	10%
test9	Code statements with struct and pointers	10%
test10	Code statements with calls	10%

4. Run ctest -R lab2 -VV and pass the test without any assertion by test.cpp.
5. 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.

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