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 {\tt 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.

翻译：端到端翻译验证是指在单次编译过程中验证编译器生成的可执行代码是否与对应的输入源代码一致。当存在动态分配的局部内存且程序可能观察到这些局部内存的地址时，该问题会变得尤为困难。在验证C过程到可执行代码的翻译正确性时，验证工具需要处理定长局部数组、取地址局部变量、取地址形参、变长局部数组、过程调用参数（包括可变参数）以及{\tt alloca()}运算符。我们提出了一种执行模型、精化定义，以及将精化检查可靠转换为一阶逻辑查询的算法，使得现成的SMT求解器能够高效处理该问题。在实验中，我们对C过程（最长100+行源代码）及其对应汇编实现（最长200+条指令）进行了黑盒翻译验证，这些汇编代码由包含复杂循环和向量化变换的优化编译器生成，并涉及上述局部内存分配结构。