Modeling Dynamic (De)Allocations of Local Memory for Translation Validation
<|reference_start|>Modeling Dynamic (De)Allocations of Local Memory for Translation Validation: 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.<|reference_end|>
@article{rose2024modeling,
    title={Modeling Dynamic (De)Allocations of Local Memory for Translation
  Validation},
    author={Abhishek Rose and Sorav Bansal},
    journal={arXiv preprint arXiv:2403.05302},
    year={2024},
    doi={10.1145/3649863},
    archivePrefix={arXiv},
    eprint={2403.05302},
    primaryClass={cs.PL}
}