一句话：提出局部内存动态分配的执行模型与精化定义，将编译器翻译验证可靠地归约为 SMT 可解的一阶逻辑查询。
端到端翻译验证需要在单次编译中验证编译器生成的可执行代码与源程序一致，而当局部内存地址可被程序观察时，动态分配的局部内存使该问题尤为困难。针对将 C 过程翻译为可执行代码的验证任务，验证器必须处理定长局部数组、被取地址的局部变量与形参、变长局部数组、过程调用实参（含可变参数）以及 alloca() 操作符。本文给出一个执行模型、精化（refinement）的定义，以及一种算法，能够可靠地将精化检查转换为现成 SMT 求解器可高效处理的一阶逻辑查询。实验对包含上述局部内存分配构造的 C 过程（最长 100+ SLOC）与其由优化编译器生成的汇编实现（最长 200+ 条指令，含复杂循环与向量化变换）进行黑盒翻译验证。
End-to-End Translation Validation is the problem of verifying the executable code generated by a compiler against the corresponding input source code for a single compilation. This becomes particularly hard in the presence of dynamically-allocated local memory where addresses of local memory may be observed by the program. In the context of validating the translation of a C procedure to executable code, a validator needs to tackle constant-length local arrays, address-taken local variables, address-taken formal parameters, variable-length local arrays, procedure-call arguments (including variadic arguments), and the alloca () operator. We provide an execution model, a definition of refinement, and an algorithm to soundly convert a refinement check into first-order logic queries that an off-the-shelf SMT solver can handle efficiently. In our experiments, we perform blackbox translation validation of C procedures (with up to 100+ SLOC), involving these local memory allocation constructs, against their corresponding assembly implementations (with up to 200+ instructions) generated by an optimizing compiler with complex loop and vectorizing transformations.
@article{paperbot2537,
title = {Modeling Dynamic (De)Allocations of Local Memory for Translation Validation},
author = {Abhishek Rose and Sorav Bansal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA1},
year = {2024},
doi = {10.1145/3649863}
}