EECS 742

Static Analysis


Project 0 - Z3 Exercise

Here are the two code snippets that I presented in class that come from the Decision Procedures text:

if(!a && !b) h();
  if(!a) g();
  else f();
if(a) f();
  if(b) g();
  else h();

They represent what an optimizer might do when compiling code. We would like to show that these snippets are the same for every input. Specifically, we would like to check the validity of the optimization. I gave you the first step in translating the code into a form appropriate for checking using Z3:

if ~a /\ ~b then h
  if ~a then g
  else f
if a then f
  if b then g
  else h

Here we replaced C-like constructions && and ! with logical equivalents and replaced funnction calls with uninterpreted functions. We can also replace the if statements using the following equivalence:

(if x then y else z) == (x /\ y) \/ (~x /\ z)

You are to do this last transformation to generate a logical expression and check that logical expression for validity in Z3. This will tell is if the optimization is correct.