Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting

Abstract

Although there have been many approaches for developing formal memory models that support integerpointer casts, previous approaches share the drawback that they are not designed for end-to-end verification ,failing to support some important source-level coding patterns, justify some backend optimizations, or lack a source-level logic for program verification. This paper presents Archmage, a framework for integer-pointer casting designed for end-to-end verification,supporting a wide range of source-level coding patterns, backend optimizations, and a formal notion of out-ofmemory. To facilitate end-to-end verification via Archmage, we also present two systems based on Archmage: CompCertCast, an extension of CompCert with Archmage to bring a full verified compilation chain to integer-pointer casting programs, and Archmage logic, a source-level logic for reasoning about integerpointer casts. We design CompCertCast such that the overhead from formally supporting integer-pointer casts is mitigated, and illustrate the effectiveness of Archmage logic by verifying an xor-based linked-list implementation, Together, our paper presents the first practical end-to-end verification chain for programs containing integer-pointer casts.