The next 700 compiler correctness theorems (functional pearl)

Compositional compiler verification is a difficult problem that focuses on separate compilation of program components with possibly different verified compilers. Logical relations are widely used in proving correctness of program transformations in higher-order languages; however, they do not scale to compositional verification of multi-pass compilers due to their lack of transitivity. The only known technique to apply to compositional verification of multi-pass compilers for higher-order languages is parametric inter-language simulations (PILS), which is however significantly more complicated than traditional proof techniques for compiler correctness. In this paper, we present a novel verification framework for lightweight compositional compiler correctness . We demonstrate that by imposing the additional restriction that program components are compiled by pipelines that go through the same sequence of intermediate representations , logical relation proofs can be transitively composed in order to derive an end-to-end compositional specification for multi-pass compiler pipelines. Unlike traditional logical-relation frameworks, our framework supports divergence preservation—even when transformations reduce the number of program steps. We achieve this by parameterizing our logical relations with a pair of relational invariants . We apply this technique to verify a multi-pass, optimizing middle-end pipeline for CertiCoq, a compiler from Gallina (Coq’s specification language) to C. The pipeline optimizes and closure-converts an untyped functional intermediate language (ANF or CPS) to a subset of that language without nested functions, which can be easily code-generated to low-level languages. Notably, our pipeline performs more complex closure-allocation optimizations than the state of the art in verified compilation. Using our novel verification framework, we prove an end-to-end theorem for our pipeline that covers both termination and divergence and applies to whole-program and separate compilation, even when different modules are compiled with different optimizations. Our results are mechanized in the Coq proof assistant.

Download Full-text

Trace-Relating Compiler Correctness and Secure Compilation

10.26226/morressier.604907f41a80aac83ca25d46 ◽

2021 ◽

Author(s):

Carmine Abate

Keyword(s):

Compiler Correctness

Download Full-text

A constructive approach to compiler correctness

Semantics-Directed Compiler Generation - Lecture Notes in Computer Science ◽

10.1007/3-540-10250-7_23 ◽

1980 ◽

pp. 189-210 ◽

Cited By ~ 6

Author(s):

Peter Mosses

Keyword(s):

Constructive Approach ◽

Compiler Correctness

Download Full-text

Trace-Relating Compiler Correctness and Secure Compilation

Programming Languages and Systems - Lecture Notes in Computer Science ◽

10.1007/978-3-030-44914-8_1 ◽

2020 ◽

pp. 1-28

Author(s):

Carmine Abate ◽

Roberto Blanco ◽

Ștefan Ciobâcă ◽

Adrien Durier ◽

Deepak Garg ◽

...

Keyword(s):

Target Property ◽

Compiler Correctness ◽

Fine Grained ◽

Side Channels ◽

Source Program ◽

Target Values ◽

Resource Exhaustion ◽

Target Languages ◽

Trace Property

AbstractCompiler correctness is, in its simplest form, defined as the inclusion of the set of traces of the compiled program into the set of traces of the original program, which is equivalent to the preservation of all trace properties. Here traces collect, for instance, the externally observable events of each execution. This definition requires, however, the set of traces of the source and target languages to be exactly the same, which is not the case when the languages are far apart or when observations are fine-grained. To overcome this issue, we study a generalized compiler correctness definition, which uses source and target traces drawn from potentially different sets and connected by an arbitrary relation. We set out to understand what guarantees this generalized compiler correctness definition gives us when instantiated with a non-trivial relation on traces. When this trace relation is not equality, it is no longer possible to preserve the trace properties of the source program unchanged. Instead, we provide a generic characterization of the target trace property ensured by correctly compiling a program that satisfies a given source property, and dually, of the source trace property one is required to show in order to obtain a certain target property for the compiled code. We show that this view on compiler correctness can naturally account for undefined behavior, resource exhaustion, different source and target values, side-channels, and various abstraction mismatches. Finally, we show that the same generalization also applies to many secure compilation definitions, which characterize the protection of a compiled program against linked adversarial code.

Download Full-text