Differential Testing of a Verification Framework for Compiler Optimizations (Experience Paper)

TL;DR

This paper applies differential testing techniques to validate that formal models of compiler optimization phases accurately reflect the actual Java code in GraalVM, ensuring correctness of complex graph transformations.

Contribution

It introduces a differential testing approach to verify the alignment between formal models and real Java code in compiler optimizations.

Findings

Multiple differential testing methods successfully identified discrepancies.

The approach enhances confidence in the correctness of compiler optimizations.

Techniques are applicable to other projects with formal models of real-world code.

Abstract

We want to verify the correctness of optimization phases in the GraalVM compiler, which consist of many thousands of lines of complex Java code performing sophisticated graph transformations. We have built high-level models of the data structures and operations of the code using the Isabelle/HOL theorem prover, and can formally verify the correctness of those high-level operations. But the remaining challenge is: how can we be sure that those high-level operations accurately reflect what the Java is doing? This paper addresses that issue by applying several different kinds of differential testing to validate that the formal model and the Java code have the same semantics. Many of these validation techniques should be applicable to other projects that are building formal models of real-world code.