Supporting register pairs in CompCert

Abstract

Software correctness is crucial in safety-critical fields like aviation and the automotiveindustry. Performing verification only at the source-code level does not provide sufficient guarantees as the compiler might introduce bugs during the translation to machine-code.Unlike ordinary compilers, the CompCert formally-verified C compiler ensures correct translation to the target’s modeled assembly language, therefore making additional verification redundant.We present CompCertp , an extension of the CompCert compiler that models register pairs, a feature found in 32-bit processors to implement double-precision floating-pointarithmetic. Two hardware registers are grouped into a register pair that can be used as an operand of machine instructions to pass 64-bit values.By supporting register pairs in the backend of the compiler, we can correctly model the floating-point semantics of the compiler’s Arm target. This allows us to implement thecorrect calling conventions for floating-point arguments and be compatible with libraries compiled with different compilers. Moreover, we can omit one of the unverified passes of CompCert increasing the trust in CompCertp ’s correctness proof.We adapt the proofs for all supported architectures of CompCert and show that CompCertpeither improves on CompCert or performs similarly in terms of code size at the cost of a slight increase in compile time. For the Arm target, we evaluate CompCertp onwell-known benchmark suites and tests generated by a fuzzer, showing an improvement of up to 10% in code size.