In this assignment you shall experiment with and extend the material
from Chapter 2 of Nielson, Nielson and Hankin, mainly by
doing a selection of the exercises similar to those in the book.
The various parts are largely independent, and I have indicated when
you have the necessary information to complete the assignment.
The assignment may be done alone or, preferably, in pairs.
Every student should be able to explain orally and clearly
every part of the assignment he hands in. The lecturer has the freedom
to ask this explanation at any time, meaning that you might not be warned
Not all of the components below are worth the same number of grade point:
Part 1 to 5 are weighted at 10, 20, 20, 25 and 25 percent.
The goal of the assignment
A large part of the chapter is devoted to developing a dataflow
analysis framework for an imperative language. To get a thorough
understanding of what is really happening underneath all that notation
you shall work on the following subjects:
- How to develop the transfer functions for a given analysis
- How chaotic iteration should be performed
- How to develop transfer functions for new language constructs and instantiate these for a specific analysis
- How to prove a soundness result for an analysis
- How to deal with the extension for procedures
Sometimes I ask you to give an illustrative, but small example.
The idea is that your example should be as varied and broad as possible,
but on the other hand should be as concise as possible. For instance,
in the case of Strongly Live Variables (see below), I expect an example
where a variable is strongly live, one which is not, one which is strongly live
but not live, and maybe you can think of other cases. The bottom line is that
your example is an alternative for a soundness proof, so the more convincing
your example, the more convinced people will be (actually, a proof also only
does the job when it is convincing).
The general rule is: Motivate your answers
The various parts of the assignment
Part 1: developing a new analysis within the framework (after Week 1)
Do Exercise 2.4 for Strongly Live Variable Analysis
on page 133 of NNH, formulate your answer
similar to Table 2.4 on page 48.
Part 2: performing chaotic iteration (after Week 1)
Design a While program of at least five blocks which well
illustrates the Strongly Live Variable Analysis (it should contain
at least one while loop).
Apply Chaotic Iteration to the
corresponding monotone framework instance, showing also intermediate
values for the iterations (similar to what I do in the slides for
Available Expressions). Indicate how SLV is different for this example
from the standard LV (and make sure that your example allows you to
illustrate this fact).
Part 3: adding new constructs to the While language (after Week 1)
Add the following three programming constructs to the While
language. Describe, in general, what has to change to accommodate
each of the constructs.
(Hint: sometimes it is sufficient to add new transfer functions, sometimes
a change has to be made to a different parameter of the monotone framework.
Deciding this is, of course, up to you.)
print a statement where
a is an arithmetic
expression. Show how to adapt the Strongly Live Analysis to accommodate
programs which contain
print statements. Devise a small
program which shows that your extension works as expected. (You do not
need to perform Chaotic Iteration. What you should do is give the
equations for your program, propose a good (preferably the best)
solution, indicate why you think this is a reasonable solution
and verify that it fulfills the equations).
- Simultaneous assignments: a simultaneous assignment is of the form
v1, ..., vn := a1, ..., an, which assigns the value of
v2 and so on. The semantics of such a statement is that first
the sequence of expressions
is evaluated, and when this is done, the resulting values are stored
in the corresponding variables in left to right order.
Add simultaneous assignments to the While language and show how
to adapt the Strongly Live Variable Analysis to accomodate it.
Illustrate that your solution works by giving an example.
Part 4: prove a soundness result (after Week 2)
Do Mini Project 2.2 on page 131.
Part 5: procedures and context (after Week 2)
Do Exercise 2.18 for the Live Variable analysis.
Work out the fibonacci example of Example 2.42 (page 101)
by giving the resulting embellished monotone framework
with context being call strings bounded by length k=2.
(Beware: there are a few snakes in the grass here.)
Remark: you do not have to work out the iteration itself.
Be very precise when you give the transfer functions, especially
those for call and return.
What, how and when to submit
Details can be found here
In whatever fashion you hand things in make sure things are clear and
readable and on time. Make sure that you motivate
Experiences from last year
The main problems and a large part of the work lie in Part 4 and 5
of this assignment.
Part four is one many students find difficult to do.
Do not be fooled to believe that the
proof is a copy of that in the book: it follows the same line, but
what you actually have to prove is quite different, and asks for
a different point of view. In practice it turned out that most students
did this well.
Part five is quite difficult, and people tend to forget quite a few details
here. The main complication I guess is how to simulate scoping.
- 15 Apr 2005