Xavier Leroy and I recently submitted a paper about my recent work on a formally-verified alias analysis for CompCert at the Conference on Certified Programs and Proofs (CPP).

This paper reports on the formalization and proof of soundness, using the Coq proof assistant, of an alias analysis: a static analysis that approximates the flow of pointer values. The alias analysis considered is of the points-to kind and is intraprocedural, flow-sensitive, field-sensitive, and untyped. Its soundness proof follows the general style of abstract interpretation. The analysis is designed to fit in the CompCert C verified compiler, supporting future aggressive optimizations over memory accesses.

We tried to convey a high-level understanding of the key design decisions and their dedicated data structures and algorithms, as well as an overview of the main proof invariant and the properties it entails.

The analysis computes abstract flow-sensitive points-to information, in an intra-procedural fashion. We do not prove its termination. We prove that we can deduce non-aliasing in the appropriate setting.

We have not yet introduced the analysis into CompCert, for two reasons:

  1. My Coq code was awful. I have now almost entirely rewritten it in a new, better-organized, more segmented way. I am still a bit unsatisfied about the new implementation, but it is way better than the first.
  2. We have not yet updated the optimizing passes of the compiler to use this analysis. I have just written a dummy pass that does the analysis and pretty-prints the results.

Comments and questions are welcome.