Lecture 9: Fixpoints in static analysis
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:
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 .
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
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.