Reasoning About LLVM Code Using Codewalker

TL;DR

This paper explores using Codewalker to reason about LLVM-compiled programs, offering a more trustworthy decompilation into logic compared to previous methods, and demonstrates its application on simple array-based C programs.

Contribution

It introduces a new approach employing Codewalker for analyzing LLVM code, improving trustworthiness over prior unverified translation methods.

Findings

Codewalker can create an interpreter for LLVM subset

Analysis of simple array-based C programs is feasible

Discussion of advantages and limitations of Codewalker-based reasoning

Abstract

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.