EECS 742

Static Analysis


Project 2 - Reaching analysis

For this exercise you will generalize Project 1 by constructing a translator from arbitrary IMP programs to a Z3 reaching analysis model. Recall the factorial program from Project 1:

Y := X;
Z := 1;
while 1<Y do
  Z := Z * Y;
  Y := Y - 1;
Y := 0

You wrote a model Z3 model by hand that allowed checking a number of properties related to variable assignment. For this project you will generate that model automatically.

The input to your solution should be an abstract syntax representation of an IMP program. You are welcome to write or use an existing parser to generate your abstract syntax, but this is not a requirement.

Your abstract syntax should represent the following IMP language:

aexp ::= Nat | aexp + aexp | aexp - aexp | Var
bexp ::= aexp <= aexp | isZero aexp | bexp or bexp | not bexp
com ::= skip | while bexp do com | if bexp then com else com | Var := aexp | com ; com

If you choose you may add parenthesis as needed.

Your first task is to identify IMP statements that impact variable values or sequence code. We know from class that assignment and while are examples of such statements, but there are others. Remember that only statements that impact variable values or flow of control matter in reaching analysis.

Your second task is to identify templates for each statement in your model. In Project 1 you wrote custom Z3 definitions describing how each statement impacts reaching definitions. Generalize those and create templates for other statements identified as impacting reaching definitions.

Your third task is to implement IMP as an AST and develop code that generates your Z3 model from it. I strongly encourage you to remember how you processed code in programming language and compilers courses. Specifically, defining a recursive interpreter that processes each AST element as one case in case or match statement.

You are free to use any of the languages that support a Z3 interface. However, you do not need to do this. One solution is to walk your code a simply generate a text file containing Z3 syntax without making any calls to Z3 from your analysis tool.

The output of your tool should be a valid Z3 program and a reaching definition model generated by Z3 using (get-model). While it should be easy to create a script that calls your tool and calls Z3 on the result, I am okay with calling Z3 by hand.

Your project submission should include source code for your analysis tool, necessary documentation for running your tool, and a collection of test cases. Start with factorial since we know what the model looks like.