Due: Friday, February 3, 2017 at 4:59pm, via Canvas
You may do this assignment in pairs; sign up your pairs on Canvas. Your partner should be in a different project group than you.
The goal of this assignment is to solidify your understanding of abstract interpretation. Doing so will enable you to better understand automated tools, and to better reason manually when necessary.
Try to do the assignment with just your partner at first. If you need to review material from the Internet or discuss with other people, you may do so, but you may not take any written notes and at least 30 minutes must pass before you write anything down. The purpose of this is to ensure that you have internalized and understood the information rather than just copying it, which would be a bad use of your time.
Consider the copy propagation problem.
Copy propagation replaces uses of one variable by another that is equal to it.
For example, if x and y are equal, then uses of y can be replaced by x.
Copy propagation by itself isn't of much benefit: changing a line from z = 3 + y to z = 3 + x doesn't make the code faster. The benefit is that the live range of y can be reduced, or the variable y can be eliminated altogether. We won't consider that, but it's good to understand the purpose of what you are doing.
Write an abstract interpretation for copy propagation. The hardest part is deciding the abstract domain, so first think about what sort of questions a client of the analysis wants to answer, and design a data structure that can answer the question.
Include, at the end of your writeup, an example of how your analysis running on the following code. Structure it like we did on the board, showing the abstract state between each pair of statements (including before the first one and after the last one). This example is straight-line code, but make sure that your abstract interpretation can also handle loops, if statements, etc.
a := x * x b := 3 c := x d := c * c e := b * 2 f := a + d g := e * f
Show the code changed to replace some variable uses and delete the no-longer-necessary assignments.
Describe a simple change you can make to your analysis that would also enable you to eliminate the b := 3 line.
Given a use of a variable, it is helpful to know where the variable was last assigned. The set of possible definitions that "reach" the use gives information about the variable's value at the use site.
More precisely, the expression x = y + z is a definition of x and a use of both y and z.
A definition reaches a use if the value that was written by that definition may be read at the use.
For example, consider the code
s = 0 a = 4 i = 0 if k == 0 b = 1 else b = 2 while i < n s = s + a * b i = i + 1 return s
in the statement s = s + a * b, there is just one reaching definition for a (and from this definition we know that a is constant), but there are two reaching definitions for b.
Design an abstract interpretation for the reaching definition problem.
Execute your analysis on the above example. You may want to re-draw the program as a control flow graph.
Upload file(s) with your results to Canvas. You may typeset them, or use plain text, or draw them on a computer, or draw them longhand and scan them. Formatting is not important, but comprehensibility does matter, and that requires clear thinking, completeness, and neatness.