240 lines
12 KiB
Markdown
240 lines
12 KiB
Markdown
---
|
|
title: "Implementing and Verifying \"Static Program Analysis\" in Agda, Part 4: The Fixed-Point Algorithm"
|
|
series: "Static Program Analysis in Agda"
|
|
description: "In this post, I give a top-level overview of my work on formally verified static analyses"
|
|
date: 2024-08-10T17:37:42-07:00
|
|
tags: ["Agda", "Programming Languages"]
|
|
draft: true
|
|
---
|
|
|
|
In the preivous post we looked at lattices of finite height, which are a crucial
|
|
ingredient to our static analyses. In this post, I will describe the specific
|
|
algorithm that makes use of these lattices that will be at the core of it all.
|
|
|
|
Lattice-based static analyses tend to operate by iteratively combining facts
|
|
from the program into new ones. For instance, when analyzing `y = 1 + 2`, we
|
|
take the (trivial) facts that the numbers one and two are positive, and combine
|
|
them into the knowledge that `y` is positive as well. If another line of code
|
|
reads `x = y + 1`, we then apply our new knowledge of `y` to determine the sign
|
|
of `x`, too. Combining facs in this manner gives us more information, which we
|
|
can then continue to apply to learn more about the program.
|
|
|
|
A static program analyzer, however, is a very practical thing. Although in
|
|
mathemaitics we may allow ourselves to delve into infinite algorithms, we have
|
|
no such luxury while trying to, say, compile some code. As a result, after
|
|
a certain point, we need to stop our iterative (re)combination of facts. In
|
|
an ideal world, that point would be when we know we have found out everything we
|
|
could about the program. A corollary to that would be that this point must
|
|
be guaranteed to eventually occur, lest we keep looking for it indenfinitely.
|
|
|
|
The fixed-point algorithm does this for us. If we describe our analysis as
|
|
a monotonic function over a finite-height lattice, this algorithm gives
|
|
us a surefire way to find out facts about our program that constitute "complete"
|
|
information that can't be re-inspected to find out more. The algorithm is guaranteed
|
|
to terminate, which means that we will not get stuck in an infinite loop.
|
|
|
|
### The Algorithm
|
|
Take a lattice \(L\) and a monotonic function \(f\). We've
|
|
[talked about monotonicity before]({{< relref "01_spa_agda_lattices#define-monotonicity" >}}),
|
|
but it's easy to re-state. Specifically, a function is monotonic if the following
|
|
rule holds true:
|
|
|
|
{{< latex >}}
|
|
\textbf{if}\ a \le b\ \textbf{then}\ f(a) \le f(b)
|
|
{{< /latex >}}
|
|
|
|
Recall that the less-than relation on lattices in our case
|
|
[encodes specificity]({{< relref "01_spa_agda_lattices#specificity" >}}).
|
|
In particular, if elements of our lattice describe our program, than smaller
|
|
elements should provide more precise descriptions (where "`x` is potive"
|
|
is more precise than "`x` has any sign", for example). Viewed through this
|
|
lens, monotonicity means that more specific inputs produce more specific outputs.
|
|
That seems reasonable.
|
|
|
|
Now, let's start with the least element of our lattice, denoted \(\bot\).
|
|
A lattice of finite height is guaranteed to have such an element. If it didn't,
|
|
we could always extend chains by tacking on a smaller element to their bottom,
|
|
and then the lattice wouldn't have a finite height anymore.
|
|
|
|
Now, apply \(f\) to \(\bot\) to get \(f(\bot)\). Since \(\bot\) is the least
|
|
element, it must be true that \(\bot \le f(\bot)\). Now, if it's "less than or equal",
|
|
is it "less than", or is "equal")? If it's the latter, we have \(\bot = f(\bot)\).
|
|
This means we've found a fixed point: given our input \(\bot\) our analysis \(f\)
|
|
produced no new information, and we're done. Otherwise, we are not done, but we
|
|
know that \(\bot < f(\bot)\), which will be helpful shortly.
|
|
|
|
Continuing the "less than" case, we can apply \(f\) again, this time to \(f(\bot)\).
|
|
This gives us \(f(f(\bot))\). Since \(f\) is monotonic and \(\bot \le f(\bot)\), we know
|
|
also that \(f(\bot) \le f(f(\bot))\). Again, ask "which is it?", and as before, if
|
|
\(f(\bot) = f(f(\bot))\), we have found a fixed point. Otherwise, we know that
|
|
\(f(\bot) < f(f(\bot))\).
|
|
|
|
We can keep doing this. Notice that with each step, we are either done
|
|
(having found a fixed point) or we have a new inequality in our hands. We can
|
|
arrange the ones we've seen so far into a chain:
|
|
|
|
{{< latex >}}
|
|
\bot < f(\bot) < f(f(\bot)) < ...
|
|
{{< /latex >}}
|
|
|
|
Each time we fail to find a fixed point, we add one element to our chain, growing
|
|
it. But if our lattice \(L\) has a finite height, that means eventually this
|
|
process will have to stop; the chain can't grow forever; eventually, we will
|
|
have to find a value such that \(v = f(v)\). Thus, our algorithm is guaranteed
|
|
to terminate, and give a fixed point.
|
|
|
|
I implemented the iterative process of applying \(f\) using a recursive function.
|
|
Agda has a termination checker, to which the logic above --- which proves that
|
|
iteration will eventually finish --- is not at all obvious. The trick to
|
|
getting it to work was to use a notion of "gas": an always-decreasing value
|
|
that serves as one of the functions' arguments. Since the value is always decreasing
|
|
in size, the termination checker is satisfied.
|
|
|
|
This works by observing that we already have a rough idea of the maximum number
|
|
of times our function will recurse; that would be the height of the lattice.
|
|
After that, we would be building an impossibly long chain. So, we'll give the
|
|
function a "budget" of that many iterations, plus one more. Since the chain
|
|
increases once each time the budget shrinks (indicating recursion), running
|
|
out of our "gas" will mean that we built an impossibly long chain --- it
|
|
will provably never happen.
|
|
|
|
In all, the recursive function is as follows:
|
|
|
|
{{< codelines "Agda" "agda-spa/Fixedpoint.agda" 53 64 >}}
|
|
|
|
The first case handles running out of gas, arguing by bottom-elimination (contradiction).
|
|
The second case follows the algorithm I've described pretty closely; it
|
|
applies \(f\) to an existing value, checks if the result is equal (equivalent)
|
|
to the original, and if it isn't, it grows the existing chain of elements
|
|
and invokes the step function rescurisvely with the grown chain and less gas.
|
|
|
|
The recursive function implements a single "step" of the process (applying `f`,
|
|
comparing for equality, returning the fixed point if one was found). All that's
|
|
left is to kick off the process using \(\bot\). This is what `fix` does:
|
|
|
|
{{< codelines "Agda" "agda-spa/Fixedpoint.agda" 66 67 >}}
|
|
|
|
This functions is responsible for providing gas to `doStep`; as I mentioned above,
|
|
it provides just a bit more gas than the maximum-length chain, which means that
|
|
if the gas is exhausted, we've certainly arrived at a contradiction. It also
|
|
provides an initial chain onto which `doStep` will keep tacking on new inequalities
|
|
as it finds them. Since we haven't found any yet, this is the single-element
|
|
chain of \(\bot\). The last thing is does is set up the reursion invariant
|
|
(that the sum of the gas and the chain length is constant), and provides
|
|
a proof that \(\bot \le f(\bot)\). This function always returns a fixed point.
|
|
|
|
### Least Fixed Point
|
|
Functions can have many fixed points. Take the identity function that simply
|
|
returns its argument unchanged; this function has a fixed point for every
|
|
element in its domain, since, for example, \(\text{id}(1) = 1\), \(\text{id}(2) = 2\), etc.
|
|
The fixed point found by our algorithm above is somewhat special among the
|
|
possible fixed points of \(f\): it is the _least fixed point_ of the function.
|
|
Call our fixed point \(a\); if there's another point \(b\) such that \(b=f(b)\),
|
|
then the fixed point we found must be less than or equal to \(b\) (that is,
|
|
\(a \le b\)). This is important given our interpretation of "less than" as "more specific":
|
|
the fixedpoint algorithm produces the most specific possible information about
|
|
our program given the rules of our analysis.
|
|
|
|
The proof is simple; suppose that it took \(k\) iterations of calling \(f\)
|
|
to arrive at our fixed point. This gives us:
|
|
|
|
{{< latex >}}
|
|
a = \underbrace{f(f(...(f(}_{k\ \text{times}}\bot)))) = f^k(\bot)
|
|
{{< /latex >}}
|
|
|
|
Now, take our other fixed point \(b\). Since \(\bot\) is the least element of
|
|
the lattice, we have \(\bot \le b\).
|
|
|
|
{{< latex >}}
|
|
\begin{array}{ccccccccr}
|
|
& & \bot & \le & & & b \quad \implies & \text{(monotonicity of $f$)}\\
|
|
& & f(\bot) & \le & f(b) & = & b \quad \implies & \text{($b$ is a fixed point, monotonicity of $f$)}\\
|
|
& & f^2(\bot) & \le & f(b) & = & b \quad \implies & \text{($b$ is a fixed point, monotonicity of $f$)}\\
|
|
\\
|
|
& & \vdots & & \vdots & & \vdots & \\
|
|
\\
|
|
a & = & f^k(\bot) & \le & f(b) & = & b &
|
|
\end{array}
|
|
{{< /latex >}}
|
|
|
|
Because of the monotonicity of \(f\), each time we apply it, it preserves the
|
|
less-than relationship that started with \(\bot \le b\). Doing that \(k\) times,
|
|
we verify that \(a\) is our fixed point.
|
|
|
|
To convince Agda of this proof, we once again get in an argument with the termination
|
|
checker, which ends the same way it did last time: with us using the notion of 'gas'
|
|
to ensure that the repeated application of \(f\) eventually ends. Since we're
|
|
interested in verifying that `doStep` producdes the least fixed point, we formulate
|
|
the proof in terms of `doStep` applied to various arguments.
|
|
|
|
{{< codelines "Agda" "agda-spa/Fixedpoint.agda" 76 84 >}}
|
|
|
|
As with `doStep`, this function takes as arguments the amount of gas `g` and
|
|
a partially-built chain `c`, which gets appended to for each failed equality
|
|
comparison. In addition, however, this function takes another arbitrary fixed
|
|
point `b`, which is greater than the current input to `doStep` (which is
|
|
a value \(f^i(\bot\)\) for some \(i\)). It then proves that when `doStep` terminates
|
|
(which will be with a value in the form \(f^k(\bot)\)), this value will still
|
|
be smaller than `b`. Since it is a proof about `doStep`, `stepPreservesLess`
|
|
proceeds by the same case analysis as its subject, and has a very similar (albeit
|
|
simpler) structure. In short, though, it encodes the relatively informal proof
|
|
I gave above.
|
|
|
|
Just like with `doStep`, I define a helper function for `stepPreservesLess` that
|
|
kicks off its recursive invocations.
|
|
|
|
{{< codelines "Agda" "agda-spa/Fixedpoint.agda" 86 87 >}}
|
|
|
|
Above, `aᶠ` is the output of `fix`:
|
|
|
|
{{< codelines "Agda" "agda-spa/Fixedpoint.agda" 69 70 >}}
|
|
|
|
### What is a Program?
|
|
With the fixed point algorithm in hand, we have all the tools we need to define
|
|
static program analyses:
|
|
|
|
1. We've created a collection of "lattice builders", which allow us to combine
|
|
various lattice building blocks into more complicated structures; these
|
|
structures are advanced enough to represent the information about our programs.
|
|
2. We've figured out a way (our fixed point algorithm) to repeatedly apply
|
|
an inference function to our programs and eventually produce results.
|
|
This algorithm requires some additional properties from our latttices.
|
|
3. We've proven that our lattice builders create lattices with these properties,
|
|
making it possible to use them to construct functions fit for our fixed point
|
|
algorithm.
|
|
|
|
All that's left is to start defining monotonic functions over lattices! Except,
|
|
what are we analyzing? We've focused a fair bit on the theory of lattices,
|
|
but we haven't yet defined even a tiny piece of the language that our programs
|
|
will be analyzing. We will start with programs like this:
|
|
|
|
```
|
|
x = 42
|
|
y = 1
|
|
if y {
|
|
x = -1;
|
|
} else {
|
|
x = -2;
|
|
}
|
|
```
|
|
|
|
We will need to model these programs in Agda by describing them as trees
|
|
([Abstract Syntax Trees](https://en.wikipedia.org/wiki/Abstract_syntax_tree), to be
|
|
precise). We will also need to specify how to evaluate these programs (provide
|
|
the [semantics](https://en.wikipedia.org/wiki/Semantics_(computer_science)) of
|
|
our language). We will use big-step (also known as "natural") operational semantics
|
|
to do so; here's an example rule:
|
|
|
|
{{< latex >}}
|
|
\frac{\rho_1, e \Downarrow z \quad \neg (z = 0) \quad \rho_1,s_1 \Downarrow \rho_2}
|
|
{\rho_1, \textbf{if}\ e\ \textbf{then}\ s_1\ \textbf{else}\ s_2\ \Downarrow\ \rho_2}
|
|
{{< /latex >}}
|
|
|
|
The above reads:
|
|
|
|
> If the condition of an `if`-`else` statement evaluates to a nonzero value,
|
|
> then to evaluate the statement, you evaluate its `then` branch.
|
|
|
|
In the next post, we'll talk more about how these rules work, and define
|
|
the remainder of them to give our language life. See you then!
|