Reasoning About LLVM Code Using Codewalker

David S. Hardin
(Rockwell Collins)

This paper reports on initial experiments using J Moore's Codewalker to reason about programs compiled to the Low-Level Virtual Machine (LLVM) intermediate form. Previously, we reported on a translator from LLVM to the applicative subset of Common Lisp accepted by the ACL2 theorem prover, producing executable ACL2 formal models, and allowing us to both prove theorems about the translated models as well as validate those models by testing. That translator provided many of the benefits of a pure decompilation into logic approach, but had the disadvantage of not being verified. The availability of Codewalker as of ACL2 7.0 has provided an opportunity to revisit this idea, and employ a more trustworthy decompilation into logic tool. Thus, we have employed the Codewalker method to create an interpreter for a subset of the LLVM instruction set, and have used Codewalker to analyze some simple array-based C programs compiled to LLVM form. We discuss advantages and limitations of the Codewalker-based method compared to the previous method, and provide some challenge problems for future Codewalker development.

In Matt Kaufmann and David L. Rager: Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2015), Austin, Texas, USA, 1-2 October 2015, Electronic Proceedings in Theoretical Computer Science 192, pp. 79–92.
Published: 18th September 2015.

ArXived at: http://dx.doi.org/10.4204/EPTCS.192.7 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org