CSE 501: Principles and Applications of Program Analysis Homework 2

Hello, if you have any need, please feel free to consult us, this is my wechat: wx91due

Homework 2: Axiomatic Semantics and Program Verification

Objective

The goal of this assignment is to familiarize yourself with using an automated verifier to check verification conditions. Verification conditions are mechanistic formalization of weakest preconditions that we discussed in lecture.

Background

In this assignment, you will be writing verification conditions for a few programs, and using an SMT solver (Z3) to check the validity of your solutions. The purpose of this exercise is to get you familiarized with the Z3 solver and its input language, SMT-LIB2, which is the standard format for specifying Satisfiability Modulo Theories (SMT) problems.

Details

For the problem set, you need to download Z3 and build (by running the included configure script followed by make). You can either use your own machine or the department cluster (recycle, bicycle, etc). An alternative is to use the Z3 web interface.

We have successfully built the latest version of Z3 (4.4.0) out of the box on the department cluster and will only support that platform. If you use other platforms, feel free to post questions on the discussion board in case others can help.

The Z3 homepage contains a very clear documentation describing the SMT-LIB2 language and how to use Z3. While that page has way more than what you need for this assignment, it might be a good idea to look through a few examples there to get a sense of the input SMT-LIB2 language. Below is a small example to help you get started.

Example of using Z3

;; ";" starts a comment line
;; define a scalar (enumerated) type person. Variables of type person can only 
;; be equal to joe, jane, tim or tina.
(declare-datatypes () ((person joe jane tim tina)) )

;; define two variables p1 and p2 of type person
(declare-const p1 person)
(declare-const p2 person)

;; We declare-const two variables for the money owned by person p1 and the person p2
(declare-const p1money Int)
(declare-const p2money Int)

;; Person 1 has more money than person 2
(assert (> p1money  p2money))

;; money amounts are positive
(assert (and (< 0  p1money) (< 0  p2money)))

;; Person 1 can not be the same as person 2
(assert (not (= p1 p2)))
;; Jane must have more money than everyone else.
(assert (=> (= p1 jane) (> p1money p2money)))
(assert (=> (= p2 jane) (> p2money p1money)))

;; find a solution
(check-sat)

;; Tell Z3 that we actually want to see the result,
;; not just to tell us whether it's sat or unsat
(get-model)

sat
(model (define-fun p2money () Int 1)
       (define-fun p1 () person tim)
       (define-fun p2 () person joe)
       (define-fun p1money () Int 2)
)

        
;; an unfeasible constraint
(assert (= p2 jane))

unsat

Problem 1: Fun with Z3 (15 pts)

You are going to use Z3 to answer the following puzzle (courtesy of mathisfun.com):

You have three crates, one has only apples, one has only oranges, and one has both apples and oranges. However, someone has maliciously relabeled the crates, and all you know is that all the labels have been shuffled, i.e., none of the crates has the right label. The goal is to infer the right label by picking a single fruit from one of the crates.

(a) (5 pts) Suppose you picked a fruit out of the crate labeled "Mixed", and it happened to be an apple. Write a Z3 formula involving the variables realApple, realOrange and realMixed, such that the variable realOrange will tell you the real contents of the crate labeled "orange", the variable realApple will tell you the real contents of the crate labeled "apple", and similarly for realMixed. The values of these three variables should be consistent with the fact that you picked an apple from the mixed crate.

(b) (5 pts) Use the solver to prove that there is only one possible assignment for the labels given the information that you picked an apple from the mixed crate.

(c) (5 pts) If you had picked an apple from the crate labeled "orange" instead, would that information had been enough to uniquely determine the solution? Provide a formula that can answer this question.

Problem 2: Solving Verification Conditions in Z3 (30 pts)

Consider the following 4 verification problems. For each of them, hand-code the verification conditions in Z3, and show that they are correct (i.e., the post-condition is true given the precondition and the verification conditions). We are only concerned with partial correctness in these problems so you do not need to provide ranking functions for the loops.

Since we are not looking for a satisfying assignment or model (as in problem 1) in program verification, the usual strategy is to assert the preconditions to be true, and then assert that the negated verification condition is not satisfiable, and hence the original verification condition is true (this is also known as refutation-based proving). This is especially important for first-order logic with quantifications, as that is undecidable in general. It might take some time before the solver will come back with a satisfiable model.

Recall from lecture what we need to show for a program containing loops. Given pre-condition PRE before entering the loop, post-condition POST assuming the loop terminates, and loop invariant I, we need to show that:

1. the loop invariant is initially true before entering the loop: PRE → I
2. the loop invariant is preserved if the loop continues: I ∧ loop condition is true → wp(c, I), where wp(c, I) is the weakest precondition of the body of the loop with I as the post-condition
3. the loop invariant implies the post condition if the loop terminates: I ∧ loop condition is false → POST

One way to structure your proof script is the following:

; declare any variable that you might need
(declare-const ...)

; preconditions
(assert ...)

; verification condition given the post-condition
(assert (not (....)))

(check-sat)

// precondition: {y = y0 ∧ k = k0 ∧ t = y0 - k0} // invariant: {t = y - k0 ∧ k = k0} while (t > 0) {
  y = y - 1;
  t = t - 1;
} // postcondition: {y ≤ k0} 

// precondition: {y < len ∧ Err = 0} // invariant: {y < len ∧ Err = 0} while (q < y) {
  if (q > len) { Err = 1; } 
  q = q + 1;
} // postcondition: {Err = 0} 

// precondition: {s = 0 ∧ x0 ≥ 0 ∧ x = x0} // invariant: ?? while (x ≠ 0) {
  s = s + x;
  x = x - 1;
} // postcondition: {s = Σi = 0 → x0 i} 

// precondition: {m = 0 ∧ x = x0 ∧ t = t0 ∧ t0 > 0 ∧ x0 ≥ 0} // outer loop invariant: ?? while (t > 0) { // inner loop invariant: ?? while (x > 0) {
    m = m + 1;
    x = x - 1;
  }

  t = t - 1;
} // postcondition: {m = x0} 

Submitting Bugs

• a description of the bug.
• a minimal test case that reproduces the bug.

Grading and What to Submit

Please submit a separate Z3 proof script for each problem. For problem 1, you can submit all parts in the same file if you prefer. We will grade your proofs based on whether they are correct (obviously), and whether you have set up the proof correctly.

In a separate readme file, describe how long it took you to complete this assignment, and any comments regarding difficulty, usefulness, etc.