blog-static/content/blog/07_spa_agda_semantics_and_cfg/index.md

---
title: "Implementing and Verifying \"Static Program Analysis\" in Agda, Part 7: Connecting Semantics and Control Flow Graphs"
series: "Static Program Analysis in Agda"
description: "In this post, I prove that the Control Flow Graphs from the previous sections are sound according to our language's semantics"
date: 2024-11-28T20:32:00-07:00
tags: ["Agda", "Programming Languages"]
---

In the previous two posts, I covered two ways of looking at programs in
my little toy language:

* [In part 5]({{< relref "05_spa_agda_semantics" >}}), I covered the
  __formal semantics__ of the programming language. These are precise rules
  that describe how programs are executed. These serve as the source of truth
  for what each statement and expression does.

  Because they are the source of truth, they capture all information about
  how programs are executed. To determine that a program starts in one
  environment and ends in another (getting a judgement \(\rho_1, s \Rightarrow \rho_2\)),
  we need to actually run the program. In fact, our Agda definitions
  encoding the semantics actually produce proof trees, which contain every
  single step of the program's execution.
* [In part 6]({{< relref "06_spa_agda_cfg" >}}), I covered
  __Control Flow Graphs__ (CFGs), which in short arranged code into a structure
  that represents how execution moves from one statement or expression to the
  next.

  Unlike the semantics, CFGs do not capture a program's entire execution;
  they merely contain the possible orders in which statements can be evaluated.
  Instead of capturing the exact number of iterations performed by a `while`
  loop, they encode repetition as cycles in the graph. Because they are
  missing some information, they're more of an approximation of a program's
  behavior.

Our analyses operate on CFGs, but it is our semantics that actually determine
how a program behaves. In order for our analyses to be able to produce correct
results, we need to make sure that there isn't a disconnect between the
approximation and the truth. In the previous post, I stated the property I will
use to establish the connection between the two perspectives:

> For each possible execution of a program according to its semantics,
> there exists a corresponding path through the graph.

By ensuring this property, we will guarantee that our Control Flow Graphs
account for anything that might happen. Thus, a correct analysis built on top
of the graphs will produce results that match reality.

### Traces: Paths Through a Graph
A CFG contains each "basic" statement in our program, by definition; when we're
executing the program, we are therefore running code in one of the CFG's nodes.
When we switch from one node to another, there ought to be an edge between the
two, since edges in the CFG encode possible control flow. We keep doing this
until the program terminates (if ever).

Now, I said that there "ought to be edges" in the graph that correspond to
our program's execution. Moreover, the endpoints of these edges have to line
up, since we can only switch which basic block / node we're executing by following
an edge. As a result, if our CFG is correct, then for every program execution,
there is a path between the CFG's nodes that matches the statements that we
were executing.

Take the following program and CFG from the previous post as an example.

{{< sidebyside >}}
{{% sidebysideitem weight="0.55" %}}
```
x = 2;
while x {
  x = x - 1;
}
y = x;
```
{{% /sidebysideitem %}}
{{< sidebysideitem weight="0.5" >}}
{{< figure src="while-cfg.png" label="CFG for simple `while` code." class="small" >}}
{{< /sidebysideitem >}}
{{< /sidebyside >}}

We start by executing `x = 2`, which is the top node in the CFG. Then, we execute
the condition of the loop, `x`. This condition is in the second node from
the top; fortunately, there exists an edge between `x = 2` and `x` that
allows for this possibility. Once we computed `x`, we know that it's nonzero,
and therefore we proceed to the loop body. This is the statement `x = x - 1`,
contained in the bottom left node in the CFG. There is once again an edge
between `x` and that node; so far, so good. Once we're done executing the
statement, we go back to the top of the loop again, following the edge back to
the middle node. We then execute the condition, loop body, and condition again.
At that point we have reduced `x` to zero, so the condition produces a falsey
value. We exit the loop and execute `y = x`, which is allowed by the edge from
the middle node to the bottom right node.

We will want to show that every possible execution of the program (e.g.,
with different variable assignments) corresponds to a path in the CFG. If one
doesn't, then our program can do something that our CFG doesn't account for,
which means that our analyses will not be correct.

I will define a `Trace` datatype, which will be an embellished
path through the graph. At its core, a path is simply a list of indices
together with edges that connect them. Viewed another way, it's a list of edges,
where each edge's endpoint is the next edge's starting point. We want to make
illegal states unrepresentable, and therefore use the type system to assert
that the edges are compatible. The easiest way to do this is by making
our `Trace` indexed by its start and end points. An empty trace, containing
no edges, will start and end in the same node; the `::` equivalent for the trace
will allow prepending one edge, starting at node `i1` and ending in `i2`, to
another trace which starts in `i2` and ends in some arbitrary `i3`. Here's
an initial stab at that:

```Agda
module _ {g : Graph} where
    open Graph g using (Index; edges; inputs; outputs)

    data Trace : Index → Index → Set where
        Trace-single : ∀ {idx : Index} → Trace idx idx
        Trace-edge : ∀ {idx₁ idx₂ idx₃ : Index} →
                     (idx₁ , idx₂) ∈ edges →
                     Trace idx₂ idx₃ → Trace idx₁ idx₃
```

This isn't enough, though. Suppose you had a function that takes an evaluation
judgement and produces a trace, resulting in a signature like this:

```Agda
buildCfg-sufficient : ∀ {s : Stmt} {ρ₁ ρ₂ : Env} → ρ₁ , s ⇒ˢ ρ₂ →
                      let g = buildCfg s
                      in Σ (Index g × Index g) (λ (idx₁ , idx₂) → Trace {g} idx₁ idx₂)
```

What's stopping this function from returning _any_ trace through the graph,
including one that doesn't even include the statements in our program `s`?
We need to narrow the type somewhat to require that the nodes it visits have
some relation to the program execution in question.

We could do this by indexing the `Trace` data type by a list of statements
that we expect it to match, and requiring that for each constructor, the
statements of the starting node be at the front of that list. We could compute
the list of executed statements in order using
{{< sidenote "right" "full-execution=note" "a recursive function on the `_,_⇒ˢ_` data type." >}}
I mentioned earlier that our encoding of the semantics is actually defining
a proof tree, which includes every step of the computation. That's why we can
write a function that takes the proof tree and extracts the executed statements.
{{< /sidenote >}}

That would work, but it loses a bit of information. The execution judgement
contains not only each statement that was evaluated, but also the environments
before and after evaluating it. Keeping those around will be useful: eventually,
we'd like to state the invariant that at every CFG node, the results of our
analysis match the current program environment. Thus, instead of indexing simply
by the statements of code, I chose to index my `Trace` by the
starting and ending environment, and to require it to contain evaluation judgements
for each node's code. The judgements include the statements that were evaluated,
which we can match against the code in the CFG node. However, they also assert
that the environments before and after are connected by that code in the
language's formal semantics. The resulting definition is as follows:

{{< codelines "Agda" "agda-spa/Language/Traces.agda" 10 18 >}}

The `g [ idx ]` and `g [ idx₁ ]` represent accessing the basic block code at
indices `idx` and `idx₁` in graph `g`.

### Trace Preservation by Graph Operations

Our proofs of trace existence will have the same "shape" as the functions that
build the graph. To prove the trace property, we'll assume that evaluations of
sub-statements correspond to traces in the sub-graphs, and use that to prove
that the full statements have corresponding traces in the full graph. We built
up graphs by combining sub-graphs for sub-statements, using `_∙_` (overlaying
two graphs), `_↦_` (sequencing two graphs) and `loop` (creating a zero-or-more
loop in the graph). Thus, to make the jump from sub-graphs to full graphs,
we'll need to prove that traces persist through overlaying, sequencing,
and looping.

Take `_∙_`, for instance; we want to show that if a trace exists in the left
operand of overlaying, it also exists in the final graph. This leads to
the following statement and proof:

{{< codelines "Agda" "agda-spa/Language/Properties.agda" 88 97 >}}

There are some details there to discuss.
* First, we have to change the
  indices of the returned `Trace`. That's because they start out as indices
  into the graph `g₁`, but become indices into the graph `g₁ ∙ g₂`. To take
  care of this re-indexing, we have to make use of the `↑ˡ` operators,
  which I described in [this section of the previous post]({{< relref "06_spa_agda_cfg#fin-reindexing" >}}).
* Next, in either case, we need to show that the new index acquired via `↑ˡ`
  returns the same basic block in the new graph as the old index returned in
  the original graph. Fortunately, the Agda standard library provides a proof
  of this, `lookup-++ˡ`.  The resulting equality is the following:

  ```Agda
  g₁ [ idx₁ ] ≡ (g₁ ∙ g₂) [ idx₁ ↑ˡ Graph.size g₂ ]
  ```

  This allows us to use the evaluation judgement in each constructor for
  traces in the output of the function.
* Lastly, in the `Trace-edge` case, we have to additionally return a proof that the
  edge used by the trace still exists in the output graph. This follows
  from the fact that we include the edges from `g₁` after re-indexing them.

  ```Agda
      ; edges = (Graph.edges g₁ ↑ˡᵉ Graph.size g₂) List.++
                (Graph.size g₁ ↑ʳᵉ Graph.edges g₂)

  ```

  The `↑ˡᵉ` function is just a list `map` with `↑ˡ`. Thus, if a pair of edges
  is in the original list (`Graph.edges g₁`), as is evidenced by `idx₁→idx`,
  then its re-indexing is in the mapped list. To show this, I use the utility
  lemma `x∈xs⇒fx∈fxs`. The mapped list is the left-hand-side of a `List.++`
  operator, so I additionally use the lemma `∈-++⁺ˡ` that shows membership is
  preserved by list concatenation.

The proof of `Trace-∙ʳ`, the same property but for the right-hand operand `g₂`,
is very similar, as are the proofs for sequencing. I give their statements,
but not their proofs, below.

{{< codelines "Agda" "agda-spa/Language/Properties.agda" 99 101 >}}
{{< codelines "Agda" "agda-spa/Language/Properties.agda" 139 141 >}}
{{< codelines "Agda" "agda-spa/Language/Properties.agda" 150 152 >}}
{{< codelines "Agda" "agda-spa/Language/Properties.agda" 175 176 >}}

Preserving traces is unfortunately not quite enough. The thing that we're missing
is looping: the same sub-graph can be re-traversed several times as part of
execution, which suggests that we ought to be able to combine multiple traces
through a loop graph into one. Using our earlier concrete example, we might
have traces for evaluating `x` then `x = x -1` with the variable `x` being
mapped first to `2` and then to `1`. These traces occur back-to-back, so we
will put them together into a single trace. To prove some properties about this,
I'll define a more precise type of trace.

### End-To-End Traces
The key way that traces through a loop graph are combined is through the
back-edges. Specifically, our `loop` graphs have edges from each of the `output`
nodes to each of the `input` nodes. Thus, if we have two paths, both
starting at the beginning of the graph and ending at the end, we know that
the first path's end has an edge to the second path's beginning. This is
enough to combine them.

This logic doesn't work if one of the paths ends in the middle of the graph,
and not on one of the `output`s. That's because there is no guarantee that there
is a connecting edge.

To make things easier, I defined a new data type of "end-to-end" traces, whose
first nodes are one of the graph's `input`s, and whose last nodes are one
of the graph's `output`s.

{{< codelines "Agda" "agda-spa/Language/Traces.agda" 27 36 >}}

We can trivially lift the proofs from the previous section to end-to-end traces.
For example, here's the lifted version of the first property we proved:

{{< codelines "Agda" "agda-spa/Language/Properties.agda" 110 121 >}}

The other lifted properties are similar.

For looping, the proofs get far more tedious, because of just how many
sources of edges there are in the output graph --- they span four lines:

{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 84 94 "hl_lines=5-8" >}}

I therefore made use of two helper lemmas. The first is about list membership
under concatenation. Simply put, if you concatenate a bunch of lists, and
one of them (`l`) contains some element `x`, then the concatenation contains
`x` too.

{{< codelines "Agda" "agda-spa/Utils.agda" 82 85 >}}

I then specialized this lemma for concatenated groups of edges.

{{< codelines "Agda" "agda-spa/Language/Properties.agda" 162 172 "hl_lines=9-11" >}}

Now we can finally prove end-to-end properties of loop graphs. The simplest one is
that they allow the code within them to be entirely bypassed
(as when the loop body is evaluated zero times). I called this
`EndToEndTrace-loop⁰`. The "input" node of the loop graph is index `zero`,
while the "output" node of the loop graph is index `suc zero`. Thus, the key
step is to show that an edge between these two indices exists:

{{< codelines "Agda" "agda-spa/Language/Properties.agda" 227 240 "hl_lines=5-6" >}}

The only remaining novelty is the `trace` field of the returned `EndToEndTrace`.
It uses the trace concatenation operation `++⟨_⟩`. This operator allows concatenating
two traces, which start and end at distinct nodes, as long as there's an edge
that connects them:

{{< codelines "Agda" "agda-spa/Language/Traces.agda" 21 25 >}}

The expression on line 239 of `Properties.agda` is simply the single-edge trace
constructed from the edge `0 -> 1` that connects the start and end nodes of the
loop graph. Both of those nodes is empty, so no code is evaluated in that case.

The proof for combining several traces through a loop follows a very similar
pattern. However, instead of constructing a single-edge trace as we did above,
it concatenates two traces from its arguments. Also, instead of using
the edge from the first node to the last, it instead uses an edge from the
last to the first, as I described at the very beginning of this section.

{{< codelines "Agda" "agda-spa/Language/Properties.agda" 209 225 "hl_lines=8-9" >}}

### Proof of Sufficiency

We now have all the pieces to show each execution of our program has a corresponding
trace through a graph. Here is the whole proof:

{{< codelines "Agda" "agda-spa/Language/Properties.agda" 281 296 >}}

We proceed by 
{{< sidenote "right" "derivation-note" "checking what inference rule was used to execute a particular statement," >}}
Precisely, we proceed by induction on the derivation of \(\rho_1, s \Rightarrow \rho_2\).
{{< /sidenote >}}
because that's what tells us what the program did in that particular moment.

* When executing a basic statement, we know that we constructed a singleton
  graph that contains one node with that statement. Thus, we can trivially
  construct a single-step trace without any edges.
* When executing a sequence of statements, we have two induction hypotheses.
  These state that the sub-graphs we construct for the first and second statement
  have the trace property. We also have two evaluation judgements (one for each
  statement), which means that we can apply that property to get traces. The
  `buildCfg` function sequences the two graphs, and we can sequence
  the two traces through them, resulting in a trace through the final output.
* For both the `then` and `else` cases of evaluating an `if` statement,
  we observe that `buildCfg` overlays the sub-graphs of the two branches using
  `_∙_`. We also know that the two sub-graphs have the trace property.
  * In the `then` case, since we have an evaluation judgement for
    `s₁` (in variable `ρ₁,s₁⇒ρ₂`), we conclude that there's a correct trace
    through the `then` sub-graph. Since that graph is the left operand of
    `_∙_`, we use `EndToEndTrace-∙ˡ` to show that the trace is preserved in the full graph.
  * In the `else` case things are symmetric. We are evaluating `s₂`, with
    a judgement given by `ρ₁,s₂⇒ρ₂`. We use that to conclude that there's a
    trace through the graph built from `s₂`. Since this sub-graph is the right
    operand of `_∙_`, we use `EndToEndTrace-∙ʳ` to show that it's preserved in
    the full graph.
* For the `true` case of `while`, we have two evaluation judgements: one
  for the body and one for the loop again, this time
  in a new environment. They are stored in `ρ₁,s⇒ρ₂` and `ρ₂,ws⇒ρ₃`, respectively.
  The statement being evaluated by `ρ₂,ws⇒ρ₃` is actually the exact same statement
  that's being evaluated at the top level of the proof. Thus, we can use
  `EndToEndTrace-loop²`, which sequences two traces through the same graph.

  We also use `EndToEndTrace-loop` to lift the trace through `buildCfg s` into
  a trace through `buildCfg (while e s)`.
* For the `false` case of the `while`, we don't execute any instructions,
  and finish evaluating right away. This corresponds to the do-nothing trace,
  which we have established exists using `EndToEndTrace-loop⁰`.

That's it! We have now validated that the Control Flow Graphs we construct
match the semantics of the programming language, which makes them a good
input to our static program analyses. We can finally start writing those!

### Defining and Verifying Static Program Analyses

We have all the pieces we need to define a formally-verified forward analysis:

* We have used the framework of lattices to encode the precision of program
  analysis outputs. Smaller elements in a lattice are more specific,
  meaning more useful information.
* We have [implemented fixed-point algorithm]({{< relref "04_spa_agda_fixedpoint" >}}),
  which finds the smallest solutions to equations in the form \(f(x) = x\)
  for monotonic functions over lattices. By defining our analysis as such a function,
  we can apply the algorithm to find the most precise steady-state description
  of our program.
* We have defined how our programs are executed, which is crucial for defining
  "correctness".

Here's how these pieces will fit together. We will construct a
finite-height lattice. Every single element of this lattice will contain
information about each variable at each node in the Control Flow Graph. We will
then define a monotonic function that updates this information using the
structure encoded in the CFG's edges and nodes. Then, using the fixed-point algorithm,
we will find the least element of the lattice, which will give us a precise
description of all program variables at all points in the program. Because
we have just validated our CFGs to be faithful to the language's semantics,
we'll be able to prove that our algorithm produces accurate results.

The next post or two will be the last stretch; I hope to see you there!