New Developments in Control Flow Graphs in Lean

Table of Contents:

1. Brief excursion
2. Main lesson

This is a small part 2/procedural update on the original article. Since then, I’ve been doing a lot of reading, and I have some notes to share! Or rather: there’s stuff I want to think through, so I’ll put it in writing, and I’ll publish that writing in case it can help someone else/attract the attention of someone that knows what they’re doing.

Brief excursion: CompCert

I had a call with one of my professors about the problem, where he said something that stuck with me:

Whenever there’s problems like these, my question is : “How would CompCert do this”. Did you have a look at that?

To which I had to admit that no, indeed, I didn’t think that CompCert was chill like that. Turns out that it is! Kildall’s algorithm is implemented and properties on it are verified, and a few dataflow optimization passes are proven on it. It seems Xavier Leroy et al were onto someting.

On the one hand, the fact that someone else had attempted to do this meant that I had to actually sit down to read and understand real, industry Rocq [1], but on the other, it given the cred and reputation of the project, if anyone did it right, it’s probably them.

So armed with confidence and a few hours, I started digging through the proofs, slightly souring the sweet taste of anticipation. CompCert’s soundness proof proceeds over two fronts:

• First, the implementation of Kildall’s algorithm is certified to respect postfix soundness, a requirement of the form:

  def IsForwardPostFixpointOf {A : Type} [Bot A] [Max A] (g : CFG)
      (nodeTransfer : CFGNode -> A -> A) (edgeTransfer : CFGEdge -> A -> A)
      (entryInit : A) (outF : GFact g A) : Prop :=
    ∀ n : NodeOf g,
      (nodeTransfer n.val (expectedInOf g edgeTransfer entryInit outF n)) ⊔ (outF n) = (outF n)

  This requirement is then used to show that a given abstraction is sound with respect to semantic steps. The proofs guarantee that the result returned by the algorithm satisfies the dataflow equations induced by the current abstraction. This derivation is obtained in [2].
• Then, for every optimization pass, it’s proven that an optimization driven by the result of this algorithm produces code that’s semantically equivalent to the original code pre-optimization. This is done by describing a relation R between the original and optimized code per each optimization, and then proving a diagram of this form.

      c -- R -- c_opt
      |           |
      |           |
      v*          v*
      c' - R -- c_opt'

  Abstracting away some CompCert specifics, we denote ->* the potentially multi step evaluation relation. Notably, the evaluation semantics that are being related are the same on both sides (the RTL execution semantics described in the project), and only the trace differs. This is derived once per analysis: consider [3] for constant propagation.

This means that this proof approach in particular relies on the relation between two execution states, and not between an execution state and a CFG node. This makes a lot of sense for the purposes of CompCert, as they’ll be uniquely focused on the dataflow as a means of optimization, so the dataflow can be assumed to be correct insofar as its effects on the executable code are sound. However, this means that for Uniqueness analysis, which is a static analysis study without application on the code, this approach loses some relevance.

Summary of the brief excursion:

• Their handling of algorithm soundness was a lot cleaner than mine: we had written the same theorems, but they were poorly structured and somewhat haphazard. Their approach informed a refactor of our code and proofs, and much needed vindication.
• Their approach cannot help us with our proof of correspondence :( However, that’s not a problem, as it does give some interesting points on establishing what we need.

Main lesson

Another interesting thing my professor said [slightly paraphrased]:

Your approach to showing correspondence cannot possibly work ‘cause you’re asking too much of it.

He didn’t say it like that, but that’s what it felt like. And it made a lot of sense: the CEK machine contains a lot of information that’s lost in translation, so while it’s easy to write a forgetful map from a state to any node, doing the opposite cannot happen with just a flat view of the program point. The professor’s suggestion was therefore to instrument the Control Flow Graphs with semantics, defining what it means to evaluate a CFG.

For a very high-level, theoretical overview: the idea is to consider the following execution state

structure CFGState where
  n : CFGNode
  E : Environment
  K : Continuations
  -- _ : Other Metadata?

and to define an execution relation of type CFGEval : CFGState -> CFGState -> Prop. Then, we define correspondence between a CEK state and a CFG state, using the bisimulation framework defined in the previous post but considering states instead of nodes, and we’re good! As long as we’re careful, the analysis half of the code shouldn’t need to be touched, nor should the structure of the CFG itself require any sort of particular handling.

In a way, this approach refines the one used by the CompCert developers, considering the CFG as the bytecode for a new abstract machine, and in some sense as a compilation target. There are some questions still lingering:

• One of the main gains tied to this is the ability to separate “proper” transitions, that carry semantic meaning and that have an equivalent in the CEK semantics, and “silent” transitions, to model the structural CFG requirements. What is the proper way to handle this separation?
• Introducing a new semantic wrapper over the CFGState requires some necessary form of forgetful map π : CFGState -> CFGNode to project out (infinitely) many execution states on a single CFG node. What is the best way to relate this evaluation transition system to the one already built by the edges? Is it simply possible to prove lemmas showing that a CFGEval step necessarily corresponds to an edge of appropriate type? Does the edge structure need to be taken into consideration when building CFGEval?
• In a way, it bugs me to define both semantics on the raw, unabstracted CFG structure, and node and edge transfer functions per abstraction. It kind of feels like repeated work: it might be possible to define a relation on abstracted nodes directly, use the transfer functions to automatically define semantics and proceed from there without needing intermediate correspondence. I might investigate this path in the future, but for now, I’ll choose to focus on the regular correspondence, and eventually simplify it if needed and feasible.

A first bit of research into CFG semantics didn’t yield a lot of information, but this approach shows a lot of promise and I’m confident something good will come of it eventually.

---

[1] Nothing against it per se, but after a few months of Rocq inactivity, it did require some mental fortitude and prior prep. ↩

[2] From the CompCert documentation, Kildall.v ↩

[3] From the CompCert documentation, ConstPropproofs.v ↩