- English only

# Lab for Automated Reasoning and Analysis LARA

# Lecture 9: Fixpoints in static analysis

Recall formula propagation from Lecture 7. See correctness of formula propagation.

### Static analysis as equation solving in a lattice

If instead of formulas as we have elements of some lattice, this condition becomes

(where sp in now denotes operator on states and not formulas).

By properties of Galois connection, this is equivalent to

and we defined best transformer as , so this condition is equivalent to

We conclude that finding an inductive invariant expressed using elements of a lattice corresponds to finding a solution to a system of inequations for all . We next examine the existence and computation of such solutions more generally.

Note that is a function monotonic in a. Why?

So, we are solving a conjunction of inequations

where are variables ranging over a lattice (one for each control-flow graph node), and are monotonic functions on (one for each edge in the control-flow graph).

### From a system of equations to one equation

In lattice, we have that a conjunction of inequations

is equivalent to ( is least upper bound of them).

So we can write the conjunction of inequations in the previous section as a system of equations

Now, introduce a new product lattice with order iff ,\ldots, all hold. Then we have reduced the problem to finding a solution to equation

where . Function is also monotonic.

The solution of equation of the form is called a **fixed point** of function , because leaves in place.

The iterative process that we described above corresponds to picking an initial element such that and then computing , \ldots, .

- we have
- we have

If it stabilizes we have , so is a fixed point. This always happens if there are no infinite ascending chains.

What is we have arbitrary lattices? See, for example non-converging iteration in reals.

-continuity in a complete lattice is a requirement that for every chain we have

(generalizes continuity in real numbers). For continuous functions, even if there are infinite ascending chains, the fixed point iteration converges in the limit.

In general, even without -continuity we know that the fixed point exists, due to Tarski fixed point theorem.

See also lecture notes in SAV07 resource page, in particular notes by Michael Schwartzbach for the finite case and slides by David Schmidt for -continuity. You can also check papers by Cousot & Cousot:

#### Widening

When a lattice has infinite ascending chain property, applying the strongest postcondition for each program point need not converge.

- Example: interval analysis

One approach: redesign the lattice to make it have no infinite ascending chain

Another approach: change the fixpoint iteration itself so that it goes faster - widening.

The effect is as if we had a lattice with smaller height (but that still covers everything from to ) and this lattice is overlayed on top of the bigger lattice.

Example (Michael Swartzbach's notes, Section 7): define widening using a monotone operator that is composed with the fixpoint operator . The resulting composition is again monotone and the result is similar to computing in a smaller lattice.

Example widening operator: take **finite** set B of bounds such that . Usually also contains some constants that occur in the program. Then jump to the closest lower and upper bounds. The value can jump only finitely many times before reaching , but often the fixpoint can be reached before this happens.

Sometimes we first use for fixpoint iteration until we conclude that the value at some program point is not “stable” (it has not converged yet), and then we switch to

- advantage: more precise
- drawback: not monotonic (example), so more difficult to reason about

Often the operator is defined not just on the current fact but as a binary operator that takes and , denoted , with property .

#### Narrowing

Once we have reached above the fixpoint (using widening or anything else), we can always apply the fixpoint operator and improve the precision of the results.

If this is too slow, we can stop at any point or use a narrowing operator, the result is sound.

Instead of using the fixpoint operator , we can use any operator that leaves our current value above fixpoint.

See Combination of Abstractions in ASTREE, Section 8.1, define such that

- example: take as , or even some improved version

#### Reduced product

When we have multiple lattices for different properties, we can of course run both analyses independently.

If the analyses do not exchange information the result is same as running them one after the other - this corresponds to taking product of two lattices and operations on them.

To obtain more precise results, we allow analyses to exchange information.

Reduced product: Systematic Design of Program Analysis Frameworks, Section 10.1.

Key point: define by

The function improves the precision of the element of the lattice without changing its meaning. Subsequent computations with these values then give more precise results.