Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers

TL;DR

The paper addresses how to perform formally verified yet efficient static analysis within formally verified compilers by examining design choices, data structures, and verification strategies. It combines insights from CompCert and Astrée to discuss non-relational and data-flow analyses, fixed-point invariants, and symbolic execution for optimization correctness, while proposing practical efficiency techniques such as hash-consing and pointer-based shortcuts. The work highlights a balanced approach that uses untrusted oracles with verified checkers, examines trust boundaries, and demonstrates that substantial verified optimizations are feasible, albeit with careful management of proof effort and performance. Overall, the study provides concrete guidance for building scalable, formally verified static analyses integrated into verified compilers, with implications for safety-critical software where correctness and efficiency are both paramount.

Abstract

Formally verified compilers and formally verified static analyzers are a solution to the problem that certain industries face when they have to demonstrate to authorities that the object code they run truly corresponds to its source code and that it satisfies certain properties. From a scientific and technological point of view, they are a challenge: not only a number of nontrivial invariants and algorithms must be proved to be correct, but also the implementation must be reasonably effective so that the tools operate within reasonable time. Many optimizations in compilers rely on static analysis, and thus a formally verified compiler entails formally verified static analyses.In this article, we explain some difficulties, possible solutions, design choices and trade-offs pertaining to verified static analysis, in particular when the solution of the analysis is expressed as some form of tree, map or set.

Figures (3)

• Figure 1: Pointer equality can distinguish between two equal values
• Figure 2: Using Boulmé's monad system DBLP:books/hal/Boulme21DBLP:conf/vstte/FouilheB14, a pointer equality ("physical equality") operator is declared over a tree datatype, inside a "may return" monad with Boolean return type (). The axiom states that if this operator has returned true, then the two values are semantically equal.
• Figure 3: A simple tree datatype with a naive equality test and a fast "shortcut" equality test, using the pointer equality defined in Fig. \ref{['fig:phys_eq']}. It is possible to prove that the two coincide (below) and that they implement equality testing.