SACTOR: LLM-Driven Correct and Idiomatic C to Rust Translation with Static Analysis and FFI-Based Verification

TL;DR

SACTOR presents a structure-aware, LLM-driven C-to-Rust translator that uses a two-stage pipeline—an unidiomatic Rust phase preserving C interfaces followed by an idiomatic Rust refinement—guided by static analysis and verified through end-to-end testing via FFI. A SPEC-driven harness generator bridges ABI gaps during the idiomatic phase, enabling robust cross-language verification. Evaluated on 200 programs across TransCoder-IR and CodeNet and on real-world bases CRust-Bench and libogg, SACTOR achieves high end-to-end correctness (up to 93%) and substantially improves idiomaticity, reducing Clippy warnings and attaining unsafe-free idiomatic Rust in many cases. The results demonstrate practical viability for migrating large C codebases to memory-safe Rust, while highlighting remaining challenges in feature coverage, model variance, and computational costs.

Abstract

Translating software written in C to Rust has significant benefits in improving memory safety. However, manual translation is cumbersome, error-prone, and often produces unidiomatic code. Large language models (LLMs) have demonstrated promise in producing idiomatic translations, but offer no correctness guarantees. We propose SACTOR, an LLM-driven C-to-Rust translation tool that employs a two-step process: an initial "unidiomatic" translation to preserve semantics, followed by an "idiomatic" refinement to align with Rust standards. To validate correctness of our function-wise incremental translation that mixes C and Rust, we use end-to-end testing via the foreign function interface. We evaluate SACTOR on 200 programs from two public datasets and on two more real-world scenarios (a 50-sample subset of CRust-Bench and the libogg library), comparing multiple LLMs. Across datasets, SACTOR delivers high end-to-end correctness and produces safe, idiomatic Rust with up to 7 times fewer Clippy warnings; On CRust-Bench, SACTOR achieves an average (across samples) of 85% unidiomatic and 52% idiomatic success, and on libogg it attains full unidiomatic and up to 78% idiomatic coverage on GPT-5.

Figures (14)

• Figure 1: Overview of the SACTOR methodology.
• Figure 2: Success rates (SR) across different LLM models for the TransCoder-IR and CodeNet datasets. SR 1-6 represent the number of attempts made to achieve a successful translation. Unid. and Idiom. denote unidiomatic and idiomatic translation steps, respectively.
• Figure 3: Example of a simple C program and its equivalent Rust program, both hand-written for illustration.
• Figure 4: Test harness used for verifying concat_str translation
• Figure 5: SACTOR translation process for atoi program