In-class exercise: Z3 (optional)

High-level goal

The high-level goal of this exercise is to learn about automated theorem provers (Z3 in particular), and how they can be used to model programs, prove program properties, and generate test cases.

This exercise is optional and extra credit. It is intended to make up for a missing in-class exercise or to replace a previous in-class exercise where you lost points. Completing this exercise can only improve your overall score.

Set up

  1. Team up in groups of size 2.

  2. Assign yourself to the correct (in-class-z3) group on Canvas. (You may work and submit alone, but you must still self-assign to a group on Canvas!)

  3. Download and unzip the in-class-z3.zip archive.

  4. Open the Z3 web interface (or this or this) in your browser. (Alternatively, download the latest Z3 release.)

  5. Check out the Z3 Tutorial if you want more background. You should be able to do most of this exercise with targeted queries as opposed to reading the entirety of it.

Instructions

The in-class-z3.zip archive contains four folders (three pairs and one set of programs). Each pair contains the original program, a mutated program, and z3 starter code for comparing the two. The set contains the original program, a set of four mutants, and z3 starter code.

Your primary goal for each program and its mutant(s) is to determine if they are equivalent. You will do this by:

  • Modeling both an original (O) and a mutated (M) program in Z3 by defining a constraint system that represents program behavior based on inputs.

  • Asserting that the outputs of O and M differ for the same inputs.

  • Asking Z3 check satisfiability of the constraint system ((check-sat)).

    • If Z3 returns sat, it means it found a set of inputs for which the outputs differ. This proves non-equivalence, and (get-model) provides the set of inputs that witness non-equivalence.

    • If Z3 returns unsat, it means that there are no inputs for which the outputs differ. This proves equivalence, under the given constraint system.

  1. Examine the original and mutated program in the pair1 directory.

    Are they equivalent? (You will answer this formally in Question 1 below after using Z3).

  2. Complete Z3startercode.pair1.smt2 (see hints below!).

    Your completed code should either prove equivalence of the two programs or generates a model (inputs) that proves non-equivalence.

  3. Test your code by running it with Z3.

    Run the .smt2 file with Z3. You can copy the entire contents of the file into the web interface and run it there. Observe if the result is sat or unsat.

  4. Repeat steps 2 and 3 for the pair2 and pair3 directories.

    Note that we are using width-8 BitVecs instead of the normal width-32 BitVec. This is for ease of reading/writing/reasoning: the principals we care about are the same, but are a little easier to grok at this lower precision. Also, recall the BitVec operators (e.g., bvadd, bvsgt, bvmul, etc), which replace Int operators such as +, >, *, etc. See the BitVector section of the tutorial.

  5. Familiarize yourself with Z3 scopes.

  6. Examine the four mutants in the set1 directory.

  7. Use scopes to complete Z3startercode.set1.smt2.

    Your completed code should, for each mutant, either prove equivalence or generates a model (test case) that proves non-equivalence. By using scopes, you can leverage the fact that much of the execution is identical between the original program and the mutant programs. (See Question 2 and 3)

  8. Test your code by running it with Z3.

Questions

  1. Which of the mutants in pair1, pair2, and pair3 are equivalent to their respective original programs? For each non-equivalent mutant, provide the test case (the model showing differing inputs/outputs) generated by Z3 from the (get-model) instruction in your smt2 code. If they are equivalent, state they are unsat and thus equivalent.

  2. Which of the four mutants in set1 are equivalent to the original program? For each non-equivalent mutant, provide the test case (the model showing differing inputs/outputs) generated by Z3 from the (get-model) instruction in your smt2 code. If they are equivalent, state they are unsat and thus equivalent.

  3. Briefly explain how scopes work in Z3 (e.g., (push) and (pop)) and when they are useful.

Deliverables

  1. A plain-text file with your answers to the three questions above. Please list all group members.
  2. Your final versions of the four Z3startercode.<xyz>.smt2 templates.

Steps for turn-in

One team member should upload the deliverables to Canvas.

Hints

When modifying the .smt2 templates, only modify what is between the following two lines. Do not alter anything that is not between the following two lines, including the lines themselves!

;;;;;;;;;;;;;;;;; START STUDENT CODE ;;;;;;;;;;;;;;;

and

;;;;;;;;;;;;;;;;; END STUDENT CODE ;;;;;;;;;;;;;;;

These anchor lines are used for grading.