使用Codewalker推理LLVM代码

本文报告了使用J Moore的Codewalker对编译为低级虚拟机(LLVM)中间形式的程序进行推理的初步实验。此前，我们报告了一个从LLVM到ACL2定理证明器所接受的Common Lisp应用子集的翻译器，该翻译器生成可执行的ACL2形式化模型，并使我们既能证明关于翻译后模型的定理，也能通过测试验证这些模型。该翻译器提供了纯逻辑反编译方法的诸多好处，但具有未经验证的缺点。自ACL2 7.0起Codewalker的可用性提供了一个重新审视该想法并采用更可信的逻辑反编译工具的机会。因此，我们采用Codewalker方法为LLVM指令集的一个子集创建了解释器，并使用Codewalker分析了某些编译为LLVM形式的简单基于数组的C程序。我们讨论了基于Codewalker的方法相较于先前方法的优势与局限，并提供了一些供未来Codewalker开发的挑战问题。