Juneyoung Lee, Dongjoo Kim, Chung-Kil Hur, Nuno P. Lopes
Several automatic verification tools have been recently developed to verify subsets of LLVM's optimizations. However, none of these tools has robust support to verify memory optimizations.
In this paper, we present the first SMT encoding of LLVM's memory model that 1) is sufficiently precise to validate all of LLVM's intra-procedural memory optimizations, and 2) enables bounded translation validation of programs with up to hundreds of thousands of lines of code.
We implemented our new encoding in Alive2, a bounded translation validation tool, and used it to uncover 21 new bugs in LLVM memory optimizations, 10 of which have been already fixed. We also found several inconsistencies in LLVM IR's official specification document (LangRef) and fixed LLVM's code and the document so they are in agreement.
J. Lee, D. Kim, C. Hur, N. P. Lopes. An SMT Encoding of LLVM's Memory Model for Bounded Translation Validation. In Proc. of the 33rd International Conference on Computer-Aided Verification (CAV), July 2021.
@inproceedings{alive2-mem-cav21,
title = {An {SMT} Encoding of {LLVM}'s Memory Model for Bounded Translation Validation},
author = {Juneyoung Lee and Dongjoo Kim and Chung-Kil Hur and Nuno P. Lopes},
booktitle = {Proc. of the 33rd International Conference on Computer-Aided Verification (CAV)},
doi = {10.1007/978-3-030-81688-9_35},
month = jul,
year = 2021
}
© The Authors, 2021. Licensed under the Creative Commons Attribution 4.0 International License.