Authors
- Yonghyun Kim, Seoul National University, Korea
- Minki Cho, Seoul National University, Korea
- Jaehyung Lee, Seoul National University, Korea
- Jinwoo Kim, Seoul National University, Korea
- Taeyoung Yoon, Seoul National University, Korea
- Youngju Song, MPI-SWS, Germany
- Chung-Kil Hur*, Seoul National University, Korea
* Hur is the corresponding author.
Abstract
Although there have been many approaches for developing formal memory models that support integer-
pointer 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-of-
memory. 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 integer-
pointer 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.