Homework 2

Upload your answers as a PDF file. If you want to draw the lattices by hand and hand in a scanned version of that, that is fine. You may also draw the lattices using a program of your choice. Latex, in particular, has great support for drawing lattices.

1.

Show the full lattice for the "bitwise" abstract domain where an abstract value is a vector of abstract bits. An abstract bit is either 0, 1, or unknown. This domain does not track correlations between bits. Show the lattice for 2-bit integers.

Your lattice must include the top element (whose concretization is the set of all concrete values) but you may omit the bottom element.

2.

Again for the bitwise abstract domain with width 2, show the entire transfer function for unsigned addition. Overflows should wrap around. Each of the 81 entries should be the most precise one.

3. 

Show the full lattice for the interval abstract domain where an abstract value is a pair (low, high). Again, make sure to show the top element, but you may omit the bottom element. Do this for 3-bit unsigned integers.

4.

In the programming language of your choice, implement the abstract transfer function for unsigned subtraction for 4-bit abstract values in the interval abstract domain. Overflows should wrap around. Your transfer function should always return the most precise possible result. Include a collection of test cases demonstrating that your transfer function is correct and precise.

Do not include your code in the PDF that you hand in, but rather include a link to your code, which can be in github, on your personal home page, or whatever.