Formally Verified Compilation for Aligned Memory Copies

In compiled programs, memory copy operations are either explicitly requested, or inserted by the compiler for implementing data structure copying.Consecutive copies may be merged into larger block copies to improve performance and reduce code size. Block copies are in turn expanded into sequences and/or loops of word-size atomic operations.We address both points—merging and expansion—in a formally verified setting. We improve upon CompCert, which does not perform merges, and performs expansions through trusted code without formal proof. Along the way, we identified and fixed weaknesses in CompCert's memory model.To our knowledge, generic merging of memory copies is a novel optimisation, even compared to mainstream, unverified compilers. Our improvements in code size and speed now make it feasible to use CompCert in a safety-critical embedded system where it did not previously satisfy industrial requirements.