  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.
