在具有效果的即时编译器中进行形式验证的本地代码生成，或者：将CompCert后端转换为形式验证的即时编译器
摘要：现代即时编译器（JIT）通常使用多种机制来执行程序。为了更快地启动和观察执行的初始行为，可以先使用解释器。但是，一段时间后，JIT会动态生成常执行部分的原生代码。尽管编译动态代码需要花费一些时间，但这种机制使得程序的剩余部分执行速度更快。这些编译器是复杂的软件，有多个组件，并且极大地依赖于正在执行的不同语言之间的精确互操作，包括堆栈替换。传统的静态编译器（如CompCert）已经在证明助手中被机械化，但是JIT迄今为止很少被正式化，部分原因是它们的非纯性质和众多的组件。本研究在Coq中提出了一个模型JIT，其中包括动态生成原生代码的实现和正式验证。尽管JIT的某些部分无法在Coq中写入，但我们提出了一种证明方法，以确定、规定和推理JIT的非纯效果。我们认为，正式验证完整JIT的艰巨任务应该借鉴现有的原生代码生成证明。为此，我们的研究在动态编译过程中成功地重新使用了CompCert及其正确性证明。最后，我们的原型可以被提取和执行。
作者：Aur`ele Barri`ere (EPICURE), Sandrine Blazy (EPICURE), David Pichardie
论文ID：2212.03129
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-12-07