Daniel's Blog

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; this algorithm will be at the core of this series.

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.

Take a lattice $L$ and a monotonic function $f$. We’ve talked about monotonicity before, but it’s easy to re-state. Specifically, a function is monotonic if the following rule holds true:

Recall that the less-than relation on lattices in our case encodes 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:

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:

53
54
55
56
57
58
59
60
61
62
63
64

    doStep : ∀ (g hᶜ : ℕ) (a₁ a₂ : A) (c : ChainA.Chain a₁ a₂ hᶜ) (g+hᶜ≡h : g + hᶜ ≡ suc h) (a₂≼fa₂ : a₂ ≼ f a₂) → Σ A (λ a → a ≈ f a)
    doStep 0 hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n boundedᴬ c)
    doStep (suc g') hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite sym (+-suc g' hᶜ)
        with ≈-dec a₂ (f a₂)
    ...   | yes a₂≈fa₂ = (a₂ , a₂≈fa₂)
    ...   | no  a₂̷≈fa₂ = doStep g' (suc hᶜ) a₁ (f a₂) c' g+hᶜ≡sh (Monotonicᶠ a₂≼fa₂)
                where
                    a₂≺fa₂ : a₂ ≺ f a₂
                    a₂≺fa₂ = (a₂≼fa₂ , a₂̷≈fa₂)

                    c' : ChainA.Chain a₁ (f a₂) (suc hᶜ)
                    c' rewrite +-comm 1 hᶜ = ChainA.concat c (ChainA.step a₂≺fa₂ ≈-refl (ChainA.done (≈-refl {f a₂})))

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:

66
67

    fix : Σ A (λ a → a ≈ f a)
    fix = doStep (suc h) 0 ⊥ᴬ ⊥ᴬ (ChainA.done ≈-refl) (+-comm (suc h) 0) (⊥ᴬ≼ (f ⊥ᴬ))

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 recursion 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.

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:

Now, take our other fixed point $b$. Since $\bot$ is the least element of the lattice, we have $\bot \le b$.

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 least 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.

76
77
78
79
80
81
82
83
84

    stepPreservesLess : ∀ (g hᶜ : ℕ) (a₁ a₂ b : A) (b≈fb : b ≈ f b) (a₂≼a : a₂ ≼ b)
                     (c : ChainA.Chain a₁ a₂ hᶜ) (g+hᶜ≡h : g + hᶜ ≡ suc h)
                     (a₂≼fa₂ : a₂ ≼ f a₂) →
                     proj₁ (doStep g hᶜ a₁ a₂ c g+hᶜ≡h a₂≼fa₂) ≼ b
    stepPreservesLess 0 _ _ _ _ _ _ c g+hᶜ≡sh _ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n boundedᴬ c)
    stepPreservesLess (suc g') hᶜ a₁ a₂ b b≈fb a₂≼b c g+hᶜ≡sh a₂≼fa₂ rewrite sym (+-suc g' hᶜ)
        with ≈-dec a₂ (f a₂)
    ...   | yes _ = a₂≼b
    ...   | no  _ = stepPreservesLess g' _ _ _ b b≈fb (≼-cong ≈-refl (≈-sym b≈fb) (Monotonicᶠ a₂≼b)) _ _ _

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.

86
87

aᶠ≼ : ∀ (a : A) → a ≈ f a → aᶠ ≼ a
aᶠ≼ a a≈fa = stepPreservesLess (suc h) 0 ⊥ᴬ ⊥ᴬ a a≈fa (⊥ᴬ≼ a) (ChainA.done ≈-refl) (+-comm (suc h) 0) (⊥ᴬ≼ (f ⊥ᴬ))

Above, aᶠ is the output of fix:

69
70

aᶠ : A
aᶠ = proj₁ fix

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, to be precise). We will also need to specify how to evaluate these programs (provide the semantics of our language). We will use big-step (also known as “natural”) operational semantics to do so; here’s an example rule:

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!