Lab Exercise 2 - SVF-tools/Software-Security-Analysis GitHub Wiki

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%
  1. Run ctest -R lab2 -VV and pass the test without any assertion by test.cpp.
  2. 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;
}
⚠️ **GitHub.com Fallback** ⚠️