Modeling Register Pairs in CompCert

Abstract

The CompCert C compiler is a moderately optimizing, formally verified compiler that ensures the preservation of the input program’s semantics through a machine-checkable correctness proof. We introduce CompCert, an extension of the CompCert compiler, which incorporates the modeling of register pairs. This enhancement targets 32-bit architectures, such as the 32-bit Arm, which combine two registers to support 64-bit operands. So far, CompCert abstracts register pairs as 64-bit registers and allocates the entire pair when operating on 32-bit values, effectively cutting the number of available registers for 32-bit computations in half. This creates a harder register allocation problem and the emitted code requires post-processing outside of the formally verified compiler to comply with calling conventions. Our enhancement models all of Arm’s registers, improving register allocation and the generated code’s size. Additionally, it models the correct calling conventions for floating-point arguments within the formal semantics, eliminating the need for unverified modifications and therefore decreasing the trusted computing base (TCB). We adapt the proofs for all CompCert-supported architectures and demonstrate that, despite a slight increase in compile time, CompCert generates code that is either smaller or comparable in size to that produced by the original CompCert.