Homework # 11 (corrected 2006/12/13)
due December 19
Read section 4.2 on widening.
For each of the following analysis lattices, explain whether each is
finite and/or satisfies the ascending chain condition:
- Set of states: each state maps a variable to an integer.
(Hint: this is the collecting semantics lattice.)
- Set of sign states: each sign state maps a variable to
one of POSITIVE,NEGATIVE,ZERO.
- Abstract sign state: each variable is mapped to a sign lattice
value (one of the eight).
- Set state: each variable is mapped to a set of integers.
(Hint: this is different than (a).)
- Range state: each variable is mapped to a pair of integers,
representing lower and upper bounds.
Then compare the lattices: which is more abstract than which and which
are incomparably abstract. In the first case, give an abstraction
function. To show incomparability, show two
incomparable lattice values--in which each describe incomparable
collecting states. Every pair of lattices should either be in an
abstraction relation or be incomparable.
Implement an analysis using the union lattice over
elements from AB completed in
Example 4.39 on page 255. The analysis will only concern itself with two
variables. It should, however, be able to intelligently handle
conditions such as x < y-1 and statements such as
y = y + 1. Try to be general.
Assume integer overflow ``never'' happens.
As a test case, implement a main program that takes
three strings: one for the while program file, one for the first
variable and one for the second variable and runs the analysis.
This program is the most complex one I've asked of you all semester.
Start at first with a very simple analysis (using the correct lattice) and add precision incrementally so that you always have something working.
Even a partial working solution will enable you to make progress on the discussion questions.
Here are some of the classes I used for the solution:
- Sign
- The Sign class from Homework #2 was renamed
Signs and a new enumeration was created with three values: POSITIVE, NEGATIVE and ZERO.
- Range
- A Range enumeration was created with five values: MUCHLESS, ONELESS, EQUAL, ONEMORE,
MUCHMORE.
- AB
- A AB enumeration was created with 29 values.
Each was given two signs and a range. Helper functions for locating values were defined.
- IntegerBitSetLattice
- A utility class for creating lattices
using integer values to represent sets of no more than 32 elements.
These are provided on the web page.
Answer the following questions:
- Is your transfer function as precise as
? If so, I'm impressed. If not,
give an example of where your transfer function loses precision.
- This lattice was designed to be used for
checking array references. How could it be used for this purpose?
- What aspects of the abstraction are useful for
array bounds checking?
- What aspects of the abstraction are rather a hindrance:
do not help with array bounds checking?
- What are its limitations? How should be extended to
do real array bound checking?
Please turn in your homework on paper at the
beginning of lecture. You may send the code by email if you wish.
About this document
John Boyland
2006-12-13