software migration teams

Abstract: Lifting stripped, heavily optimized binaries to a canonical, pre-optimization LLVM intermediate representation (IR) is essential for downstream security analysis and legacy software migration when source code is unavailable. However, aggressive compiler optimizations rewrite control and data flow, remove structural metadata, and introduce type-erased low-level idioms, causing current lifters to produce malformed or semantically divergent IR. We present ATLAS, a multi-agent framework designed to reconstruct formally valid and canonical LLVM IR from optimized disassembly.ATLAS combines (i) Structure-aware, region-level retrieval, which utilizes pseudo-probe attribution to align optimized instructions with canonical IR exemplars, and (ii) a collaborative refinement loop that closes the gap between probabilistic generation and deterministic compiler constraints. Concretely, a Lift agent generates an initial IR draft conditioned on retrieved exemplars, an Advisor agent interprets LLVM verifier/compilation diagnostics and static checks to propose localized repair actions, and a Validation agent applies the edits, re-runs toolchain verification and (when available) runtime checks, and feeds the resulting diagnostics back to the Advisor. The agents iterate until the IR is verifier-clean and behaviorally consistent, or a budget limit is reached. On HumanEval-Decompile and MBPP, ATLAS outperforms seven baselines on lifting LLVM IR, achieving 91.8% re-executability and 89.4% CFG similarity across ARM, x86-64, and RISC-V binaries. Moreover, our evaluation demonstrates that ATLAS also outperforms the Binary to C to IR pipelines in pointer-flow precision and downstream analyzability. By recovering a well-formed, machine-centric representation, ATLAS enables practical cross-ISA recompilation and verifiable binary-only migration workflows.

Abstract: Producing synthetic data for comparison testing a migrated COBOL application is a major challenge that agentic migrations face today. Our prior paper, the Agentic Method for Deterministic Validation of Legacy Code Migration, presents a deterministic oracle to facilitate such migrations, the Locksmith Loop. We now propose a novel method for achieving high branch and paragraph coverage through generated synthetic end-to-end test cases, by means of entry-replay test-case certification by observing the code execution trace on a surrogate COBOL program that mocks external interactions via a chronological external-operation tape. We applied our method to a very large COBOL program with 33,429 lines of code to generate 849 synthetic end-to-end test cases covering 2,973/3,806 source branches (78.1%) and 989/1,033 main-AST paragraphs (95.7%). Using the Locksmith Loop's projected-agreement validation, the generated Java code matched the COBOL surrogate on the specified observations across all 849 certified synthetic end-to-end test cases. During the campaign we detected 61 defects and fixed the Java generator accordingly. To test whether the coding agent could silently introduce business logic bugs, we seeded 450 defects into the Java code, such as deleted writes, deleted paragraph calls, and altered rounding, to verify how many of these would be detected by the gating methodology. The gate detected 47.6%, including all deleted writes and paragraph calls in executed code, but was unable to detect the rounding and precision defects.

Abstract: Rust is increasingly adopted as a memory-safe successor to C, and transpilers such as \crust{} can migrate entire C projects while preserving their behavior. Preserving behavior, however, does not guarantee preserving performance. We study this gap on 20 real-world C projects and their \crust{} translations. On the eight projects used for analysis, the translated Rust is more than 3\% slower than the original C on 12 of 19 operations, by up to 62.2\%. By comparing execution-cost profiles, optimized LLVM IR, and compiler optimization remarks across each C--Rust pair, we trace these slowdowns to nine recurring performance issues, spanning residual runtime work, missed compiler optimizations, and C-style source patterns, and derive an optimization direction for each. We then present \ourtool{}, an LLM-based approach that encodes these issues as reusable optimization rules to recover the performance of translated Rust. \ourtool{} profiles each project to locate hot functions and matches them against rule-specific patterns. The LLM then checks each rule's rewrite preconditions against the project context before rewriting, and a rewrite is kept only if it passes both functional and performance validation. On 41 operations from twelve held-out projects, \ourtool{} preserves C outputs on all tested workloads and speeds up 40 operations over the \crust{} translations, 18 of which end up faster than the original C. It outperforms the general-purpose coding agent \codex{} on 31 of the 37 operations where both preserve C outputs, and outperforms its own variant without rule guidance on 34 of the 41 operations.

Abstract: Translating COBOL to a modern language can change what a program computes, and LLM translations carry no guarantee of equivalence. We present IRONPROOF, which parses COBOL into an intermediate representation, generates Python, encodes both as Z3 formulas over shared inputs, and emits either a machine-checkable equivalence certificate (UNSAT) or a counterexample (SAT). On 2,345 COBOL files (GnuCOBOL tests, NIST CCVS85, open-source collections, and programs we generated or wrote), 782 enter the checking path: 606 (77.5%) are proved equivalent, 101 are partially verified, none is refuted, and 75 fail inside our pipeline and stay in the denominator. On independently authored programs the rate is 52.6% (153 of 291), against 92.3% on programs we wrote. Of the 153 independent proofs, 37 cover a single execution of a program that reads input the encoder does not model, and across all 606 proofs only 14 quantify over an input that a proved output depends on. On two public business-application corpora (AWS CardDemo and IBM GenApp), the encoder models no program end to end. An April 2026 LLM-only baseline failed on 54 of 94 independently authored programs, counting translations our encoder could not verify. PIC-bounded overflow detection flags an out-of-range output in 22.1% of the programs it can analyze, an upper bound. An earlier confrontation with GnuCOBOL 3.2.0 found 24 of 49 executable independent proofs disagreeing with the runtime on a variable in the proof's domain. A proof establishes that the generated Python computes what our intermediate representation says the COBOL computes, not equivalence to a COBOL implementation.

Abstract: This technical report accompanies our EuroSys 2027 paper "Lifting the Preprocessor with Oxidize: Structure-Preserving C-to-Rust Translation" (DOI 10.1145/3842654.3848533). Oxidize is a C-to-Rust translator that retains C macros as Rust macros instead of expanding them away, so that the translated code keeps the abstractions its developers wrote. The report collects material the paper cites but has no room for: the translator's intermediate representation, pass structure and back-end emission; the details of macro typing through helper traits and the generic cast macro; the sources and pinned revisions of the nine evaluated C codebases; the per-codebase macro population and how macros are attributed to classes; a roadmap from structure-preserving translation toward safe Rust; the performance overhead study and its methodology; and the configuration and prompt used for the LLM-based baselines.

Abstract: Binary recompilation is a technique for operating directly on executable code. It promises to automate two important tasks: retrofitting security mitigations onto legacy binaries, and migrating binaries across instruction set architectures (ISAs). Yet today, there is no fully automated system that can reliably lift arbitrary binary executables to a compiler intermediate representation (IR) such as LLVM IR, or that can fully statically and reliably translate non-trivial binary executables from one ISA to another. The main underlying problem is that recovering a program's control flow graph (CFG) statically is impossible in general: computed branches can jump to targets that cannot be determined without actually running the program. Existing systems resort to runtime fallback mechanisms, requiring a significant portion of the binary translation machinery to accompany the translated program on the target machine. This article presents a fully static, whole-program binary lifting system requiring no runtime translation support on the target. Rather than attempting to distinguish code from data, we treat every byte offset as a potential branch target and lift the entire binary in a brute-force manner, constructing a superset CFG that conservatively contains all feasible control flows. Statically unresolvable computed branches are thereby reduced to lookups in a dispatch table that points to the corresponding translated control flow path. We have implemented this approach as a prototype binary recompiler from x86-64 binaries to LLVM IR, requiring no code/data heuristics. We validate it with a fully static cross-compilation to AArch64, achieved by reusing existing LLVM backends with no modification.