Publications
Detailed Information
An SMT Encoding of LLVMs Memory Model for Bounded Translation Validation
Cited 4 time in
Web of Science
Cited 3 time in Scopus
- Authors
- Issue Date
- 2021-01
- Publisher
- Springer Verlag
- Citation
- Lecture Notes in Computer Science, Vol.12760, pp.752-776
- Abstract
- © 2021, The Author(s).Several automatic verification tools have been recently developed to verify subsets of LLVMs optimizations. However, none of these tools has robust support to verify memory optimizations. In this paper, we present the first SMT encoding of LLVMs memory model that 1) is sufficiently precise to validate all of LLVMs 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 IRs official specification document (LangRef) and fixed LLVMs code and the document so they are in agreement.
- ISSN
- 0302-9743
- Files in This Item:
- There are no files associated with this item.
Item View & Download Count
Items in S-Space are protected by copyright, with all rights reserved, unless otherwise indicated.