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.

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