EECS 742

Static Analysis

Index
Blog

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();
else
  if(!a) g();
  else f();
if(a) f();
else
  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
else
  if ~a then g
  else f
if a then f
else
  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.