91 lines
5.2 KiB
Markdown
91 lines
5.2 KiB
Markdown
---
|
|
title: "Implementing and Verifying \"Static Program Analysis\" in Agda, Part 0: Intro"
|
|
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-04-12T14:23:03-07:00
|
|
draft: true
|
|
tags: ["Agda", "Programming Languages"]
|
|
---
|
|
|
|
Some years ago, when the Programming Languages research group at Oregon State
|
|
University was discussing what to read, the [_Static Program Analysis_](https://cs.au.dk/~amoeller/spa/)
|
|
lecture notes came up. The group didn't end up reading the lecture notes,
|
|
but I did. As I was going through them, I noticed that they were quite rigorous:
|
|
the first several chapters cover a little bit of [lattice theory](https://en.wikipedia.org/wiki/Lattice_(order)),
|
|
and the subsequent analyses -- and the descriptions thereof -- are quite precise.
|
|
When I went to implement the algorithms in the textbook, I realized that just
|
|
writing them down would not be enough. After all, the textbook also proves
|
|
several properties of the lattice-based analyses, which would be lost in
|
|
translation if I were to just write C++ or Haskell.
|
|
|
|
At the same time, I noticed that lots of recent papers in programming language
|
|
theory were formalizing their results in
|
|
[Agda](https://agda.readthedocs.io/en/latest/getting-started/what-is-agda.html).
|
|
Having [played]({{< relref "meaningfully-typechecking-a-language-in-idris" >}})
|
|
[with]({{< relref "advent-of-code-in-coq" >}}) [dependent]({{< relref "coq_dawn_eval" >}})
|
|
[types]({{< relref "coq_palindrome" >}}) before, I was excited to try it out.
|
|
Thus began my journey to formalize (the first few chapters of) _Static Program Analysis_
|
|
in Agda.
|
|
|
|
In all, I built a framework for static analyses, based on a tool
|
|
called _motone functions_. This framework can be used to implement and
|
|
reason about many different analyses (currently only a certain class called
|
|
_forward analyses_, but that's not hard limitation). Recently, I've proven
|
|
the _correctness_ of the algorithms my framework produces. Having reached
|
|
this milestone, I'd like to pause and talk about what I've done.
|
|
|
|
In subsequent posts in this series, will describe what I have so far.
|
|
It's not perfect, and some work is yet to be done; however, getting to
|
|
this point was no joke, and I think it's worth discussing. In all,
|
|
I envision three major topics to cover, each of which is likely going to make
|
|
for a post or two:
|
|
|
|
* __Lattices__: the analyses I'm reasoning about use an algebraic structure
|
|
called a _lattice_. This structure has certain properties that make it
|
|
amenable to describing degrees of "knowledge" about a program. In
|
|
lattice-based static program analysis, the various elements of the
|
|
lattice represent different facts or properties that we know about the
|
|
program in question; operations on the lattice help us combine these facts
|
|
and reason about them.
|
|
|
|
Interestingly, lattices can be made by combining other lattices in certain
|
|
ways. We can therefore use simpler lattices as building blocks to create
|
|
more complex ones, all while preserving the algebraic structure that
|
|
we need for program analysis.
|
|
|
|
* __The Fixed-Point Algorithm__: to analyze a program, we use information
|
|
that we already know to compute additional information. For instance,
|
|
we might use the fact that `1` is positive to compute the fact that
|
|
`1+1` is positive as well. Using that information, we can determine the
|
|
sign of `(1+1)+1`, and so on. In practice, this is often done by calling
|
|
some kind of "analyze" function over and over, each time getting closer to an
|
|
accurate characterization of the program's behavior. When the output of "analyze"
|
|
stops changing, we know we've found as much as we can find, and stop.
|
|
|
|
What does it mean for the output to stop changing? Roughly, that's when
|
|
the following equation holds: `knownInfo = analyze(knownInfo)`. In mathematics,
|
|
this is known as a [fixed point](https://mathworld.wolfram.com/FixedPoint.html).
|
|
Crucially, not all functions have fixed points; however, certain types of
|
|
functions on lattices do. The fixed-point algorithm is a way to compute these
|
|
points, and we will use this to drive our analyses.
|
|
|
|
* __Correctness__: putting together the work on lattices and the fixed-point
|
|
algorithm, we can implement a static program analyzer in Agda. However,
|
|
it's not hard to write an "analyze" function that has a fixed point but
|
|
produces an incorrect result. Thus, the next step is to prove that the results
|
|
of our analyzer accurately describe the program in question.
|
|
|
|
The interesting aspect of this step is that our program analyzer works
|
|
on [control-flow graphs](https://en.wikipedia.org/wiki/Control-flow_graph) (CFGs),
|
|
which are a relatively compiler-centric representation of programs. On the
|
|
other hand, what the language _actually does_ is defined by its
|
|
[semantics](https://en.wikipedia.org/wiki/Semantics_(computer_science)),
|
|
which is not at all compiler-centric. We need to connect these two, showing
|
|
that the CFGs we produce "make sense" for our language, and that given
|
|
CFGs that make sense, our analysis produces results that match the language's
|
|
execution.
|
|
|
|
{{< todo >}}
|
|
Once the posts are ready, link them here to add some kind of navigation.
|
|
{{< /todo >}}
|