Variable Range Analysis for Example Program

The general form of abstract interpretation of the collecting semantics is analogous to collecting semantics, but replaces operations on sets with operations on the lattice:  Here will be except at the entry into our control-flow graph, where it approximates the set of initial states at the entry point.

Abstract Analysis Domain

In Collecting Semantics for Example Program we had representation for all possible sets of states: Here we have representation of only certain states, namely intervals: The meaning of domain elements is given by a monotonic concretization function : From monotonicity and it follows and thus We try to define to be as small as possible while satisfying this condition.

Define abstraction function such that

• if those values exist (set is bounded from below and above)
• if there is lower but no upper bound
• if there is upper but no lower bound
• if there is no upper and no lower bound
• Lemma: The pair form a Galois Connection.

By property of Galois Connection, the condition is equivalent to To make as small as possible, we let the equality hold, defining For example, Abstract Postcondition

We had: Now we have: For correctness, the condition from Abstract Interpretation Recipe is that for each and each command : We would like to be as small as possible so that this condition holds

By property of Galois Connection, the condition is equivalent to Because we want to be as small as possible (to obtain correct result), we let equality hold: Because we know , we can compute the value of by simplifying certain expressions involving sets of states.

Example: for we have: For an integer constant and , we have Note that for every command given by relation , we have Abstract Semantic Function for the Program Here we have: Solving Abstract Function

Doing the analysis means computing for : Note the approximation (especially in the last step) compared to Collecting Semantics for Example Program.

Correctness

We are talking about overapproximating analysis.

In Lecture 05 we discussed that a sufficient condition is to have When we talk about the transition relation, then we need a big , which maps states including program counter. We define it by The soundness condition is then: where is defined pointwise for each component of the tuple. By definition of , , and , this reduces to pointwise conditions.

For example, we need to ensure that To show this, we can start from left hand side and push outside, obtaining larger and larger sets.

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 for such program.

Exercise 2

Consider the program that manipulates two integer variables .

Consider any assignment , where is a linear combination of integer variables, for example, Consider an interval analysis that maps each variable to its value.

Describe an algorithm that will, given a syntax tree of and intervals for (denoted ) and (denoted ) find the new interval for 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 for the following statements , where 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 analysis that stores one interval for each variable.

• Define the domain of lattice elements that are computed for each program point.
• Give the definition for statement 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 at each program point, until you reach a fixpoint.

What are the fixpoint values at program points and ?