Syzygy: Dual Code-Test C to (safe) Rust Translation using LLMs and Dynamic Analysis

TL;DR

Syzygy introduces a dual code-test translation pipeline that converts medium-to-large C codebases to safe Rust by combining LLM-driven code generation with dynamic specification mining and test-based equivalence checks. The approach translates code incrementally along the program dependency graph, guided by dynamic analysis to recover types, aliasing, and allocation sizes, while generating intermediate tests to validate each translation unit. Empirical evaluation on Zopfli and UrlParser demonstrates scalable translation and high equivalence, albeit with some runtime overhead and the need for manual repair in complex macros. The work provides a practical, test-driven path toward memory-safety guarantees in Rust for legacy C code, and outlines future directions for improving efficiency, handling more complex C constructs, and refining safety criteria.

Abstract

Despite extensive usage in high-performance, low-level systems programming applications, C is susceptible to vulnerabilities due to manual memory management and unsafe pointer operations. Rust, a modern systems programming language, offers a compelling alternative. Its unique ownership model and type system ensure memory safety without sacrificing performance. In this paper, we present Syzygy, an automated approach to translate C to safe Rust. Our technique uses a synergistic combination of LLM-driven code and test translation guided by dynamic-analysis-generated execution information. This paired translation runs incrementally in a loop over the program in dependency order of the code elements while maintaining per-step correctness. Our approach exposes novel insights on combining the strengths of LLMs and dynamic analysis in the context of scaling and combining code generation with testing. We apply our approach to successfully translate Zopfli, a high-performance compression library with ~3000 lines of code and 98 functions. We validate the translation by testing equivalence with the source C program on a set of inputs. To our knowledge, this is the largest automated and test-validated C to safe Rust code translation achieved so far.

Figures (16)

• Figure 1: Overview of our Syzygy translation approach: Slicer decomposes the codebase into translation units, CodeGenerator performs translation for that unit, and EqTester checks for equivalence of the generated Rust code with the original C code. ArgTranslator maps the C and Rust function arguments allowing appropriate equivalence checks in EqTester. SpecMiner, our dynamic analysis module mines (property and I/O) specifications for intermediate C functions using top-level tests. These specifications later assist our LLM-driven dual code-test translation. In particular, our identified properties (nullability, aliasing, types) guide LLM to generate appropriate target Rust signature. Similarly, our collected I/O specifications allow EqTester module to provide correctness assurances on incremental translations generating our Invariant.
• Figure 2: Translation Pipeline for a C function : Given a C function and tests for the C codebase, first, the SpecMiner uses dynamic analysis to mine input-output (I/O) and property specifications for the translation. These properties (e.g., nullability and aliasing) guide a CodeGenerator to generate a candidate Rust translation of . Given the translated signature and the collected C I/O, the ArgTranslator generates an translateArgs function that constructs aligned Rust inputs and expected outputs. Finally, the EqTester generates an equivalence test that executes the candidate translation, along with the previously generated Rust code, and checks whether the outputs match the expected values. If the equivalence checks pass, the translated function is committed to the Rust codebase; otherwise, error feedback is provided for multi-round repair.
• Figure 3: Dynamic Specification Mining: An example C code snippet which features dynamic allocations (in and ), function pointers (in ), aliasing between arguments (in the -- -- call chain). While this information can greatly assist CodeGenerator and EqTester, inferring it statically is challenging. We use a combination of dynamic analyses (see §\ref{['subsubsec:c-prop-spec']}).
• Figure 4: Struct field choices induce function signatures higher in the call chain. Left: C struct and a function dependent on the struct. Middle: two choices for the field in the struct. Right: a dependency graph showing relation of with other functions.
• Figure 5: Nullability information guides Rust function signature. The arguments , , of function can be . However, the LLM cannot infer these properties from function context and generates an incorrect signature without , failing equivalence. Property specifications inferred using our dynamic analysis allow LLM to generate the correct signature on the right (using ).