Formal verification of weak topological orderings and dataflow analysis

Overview & Synopsis

Dataflow analysis is a static analysis technique that determines information on the propagation of data throughout the execution of a computer program, without actually executing the program. This information can notably be used to optimize the program at compile-time. Performing dataflow analysis usually consists in solving a system of equations. Besides the traditional methods used to solve such systems, other techniques have been developed in the static analysis community. One of them, proposed by Bourdoncle in 1993, consists in pre-computing a solving strategy in order to solve the system more efficiently. This thesis aims at the development of formally verified dataflow solvers that are based on this solving technique. First, we provide a rigorous formalization for the notion of Weak Topological Ordering (WTO), which captures the pre-computed solving strategy. Then, we implement and formally verify in the Rocq proof assistant two flavors of WTO-based solving strategies introduced by Bourdoncle, known as the iterative and the recursive strategy, along with the most commonly used algorithm to compute a WTO. Our development is entirely integrated inside the formally verified compiler CompCert. Finally, we evaluate experimentally our implementations, comparing them to CompCert's dataflow solvers and to an untrusted computation of the WTO.