Exercise 07 - Abstract Interpretation

Exercise 1

Consider an analysis that has two integer variables, for which we track intervals, and one boolean variable, whose value we track exactly.

Give the type of $F^{\#}$ for such program. $F^{\#}$ is the post function for the collecting semantics.

Exercise 2

Consider the program that manipulates two integer variables $x,y$ .

Consider any assignment $x=e$ , where $e$ is a linear combination of integer variables, for example,

$\begin{equation*} x = 2*x - 5*y \end{equation*}$

Consider an interval analysis that maps each variable to its value.

Describe an algorithm that will, given a syntax tree of $x=e$ and intervals for $x$ (denoted $[a_x,b_x]$ ) and $y$ (denoted $[a_y,b_y]$ ) find the new interval $[a,b]$ for $x$ after the assignment statement.

Exercise 3

a)

For a program whose state is one integer variable and whose abstraction is an interval, derive general transfer functions $sp^\#(a,c)$ for the following statements $c$ , where $K$ is an arbitrary compile-time constant known in the program:

x= K;
x= x + K;
assume(x ⇐ K)
assume(x >= K)

b)

Consider a program with two integer variables, x,y. Consider an analysis that stores one interval for each variable.

Define the domain of lattice elements $a$ that are computed for each program point.
Give the definition for statement $sp^{\#}(a,y=x+y+K)$

c)

Draw the control-flow graph for the following program.

// v0
x := 0;
// v1
while (x < 10) {
  // v2
  x := x + 3;
}
// v3
if (x >= 0) {
  if (x <= 15) {
    a[x]=7; // made sure index is within range
  } else {
    // v4
    error;
  }
} else {
  // v5
  error;
}

Run abstract interpretation that maintains an interval for $x$ at each program point, until you reach a fixpoint.

What are the fixpoint values at program points $v_4$ and $v_5$ ?

Available Expressions Analysis

This classical dataflow analysis determines for each program point, which expressions must have already been computed, and not later modified, on all paths to the program point.

This information can be used to avoid re-computation of an expression. Consider the example program

1: x = a + b
2: y = a * b
3: while (y > a + b) {
4:   a = a + 1
5:   x = a + b
6: }

It is clear, that the expression a + b is always available at the test of the while loop, so it need not be recomputed.

An expression is killed in statement if any of the variables used in the expression are modified in the statement.
A generated expression is one that is evaluated in a statement and where none of the variables used in the expression are later modified in the statement.

The analysis tracks the killed and generated expressions at each program point.

a)

Define the lattice, including join.

b)

Give the definition of sp#

c)

Run the analysis on the example above. For this, you may want to write down the equations for each program first.