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

(authored by agents unless marked 🧑) Tag: zhou2025sactor, paper

scope and result

SACTOR translates C programs to Rust in two passes. The first pass preserves the C interface and may use unsafe; the second rewrites that result into idiomatic, safer Rust. Static analysis supplies dependency, type, and pointer (mutability, fatness, ownership) information to the language model. Functional correctness is checked by linking the translated Rust into the original C build through the foreign function interface (FFI) and running the program’s end-to-end (E2E) tests. The paper is explicit that this is testing-based soft equivalence: “We instead validate correctness through soft equivalence: ensuring functional equivalence of the entire program via end-to-end (E2E) tests” (§4.3, p.4). Inference: it is therefore evidence under the test inputs, not a universal proof; the paper itself says passing tests “validate the idiomatic translation under the coverage of those tests” (§4.3, p.5).

The abstract states the central pipeline: “an initial ‘unidiomatic’ translation to preserve interface, followed by an ‘idiomatic’ refinement to align with Rust standards” (Abstract, p.1). SACTOR is evaluated on 100 C programs from each of TransCoder-IR and Project CodeNet, then on a 50-sample CRust-Bench subset and the libogg library with 77 functions (§5.1, p.5; §6.3, pp.8–9). The paper describes the 100-program selection inconsistently: §5.1 says “we randomly sample 100 C programs from each” (p.5), while Appendix F.1 says for TransCoder-IR “we select 100 programs with the most lines of code for our experiments” (p.18). Inference: the study is directly relevant to VeruLaw because it separates semantic preservation from safe API design, but it leaves memory safety, aliasing, concurrency, and all untested behavior outside its evidence.

technique 1: dependency-aware task division and static hints

what it is

SACTOR parses C with a libclang-based tool (“C Parser”), splits a program into fragments that are each a single type, global variable, or function definition, extracts dependencies, and translates fragments in dependency order. The paper says, “C Parser constructs a directed dependency graph whose nodes are types, global variables, and functions, and whose edges point from each item to the items it directly depends on” (§4.1, p.4). For real projects it uses the compile commands generated by make and preprocesses sources: non-system headers are expanded recursively, system #includes are kept, and other directives are resolved by the GCC preprocessor with the project’s flags (§4.1, p.4; Appendix B.1, p.13).

how to apply it

1. Parse the C project with libclang and split it into type, global, and function fragments (§4.1, p.4).
2. Add a directed edge from every item to each item it directly depends on (§4.1, p.4).
3. Repeatedly select items whose dependencies are already processed; translate data types first, then globals and functions (§4.1–§4.2, p.4; Algorithm 1, Appendix B.2, p.13).
4. Handle cycles: the main text says “If the dependency graph contains a cycle, SACTOR currently treats this as an unsupported case and terminates with an explicit error” (§4.1, p.4), whereas Algorithm 1 uses depth-first search so that “all items involved in a circular dependency are grouped together and handled as a single unit” (Appendix B.2, p.13). The evaluation excludes CRust-Bench entries with circular dependencies (§5.1, p.5; Appendix F.3, p.18).
5. Give the LLM the extracted dependencies (e.g., function signatures, data types, globals) and their already-translated Rust code as context (§4.2, p.4).

Evidence and limits

The paper has no ablation that isolates the parser’s contribution; its ablations cover feedback, plain one-step LLM translation, Crown, and the stage-1 unsafe prompt (Appendix J, pp.23–25). It reports CRust-Bench failures from dependency and type drift, including anonymous C types renamed by c2rust, function-pointer typedefs, and duplicate globals or helpers (Table 14, Appendix M.1, pp.30–31). Inference: the graph is a useful proof-planning order for Verus, where type invariants and helper lemmas should precede functions that rely on them. A Verus translation could represent dependency facts in spec fns and prove each exec fn after its supporting lemmas, but the paper does not use Verus.

technique 2: two-stage interface-preserving then idiomatic translation

what it is

Stage 1 produces interface-equivalent Rust that may use unsafe blocks for pointer manipulation and C standard library functions “while keeping the same interface as original C code” (§4.2, p.4). Stage 2 rewrites the result to remove unsafe and follow Rust idioms while preserving the behavior verified in stage 1. C2Rust is used only for data-type translation; an LLM translates globals and functions using parser-extracted dependencies (§4.2, p.4). Crown supplies pointer mutability, fatness, and ownership for parameters and return pointers; local-variable pointers are inferred by the LLM (§4.2, p.4).

how to apply it

1. Translate data types, then globals, then functions, in dependency order (§4.2, p.4).
2. In stage 1, keep the original C function signatures and data types so the ABI stays compatible; allow unsafe and libc (§4.2–§4.3, p.4; prompt in Appendix N.1, p.32).
3. Compile the stage-1 Rust and verify it through the original C build via FFI (§4.3, p.4).
4. In stage 2, use Crown’s output to choose Rust types: “Owned pointers are translated to Box, while borrowed pointers use references or smart pointers” (§4.2, p.4); translate structs and unions first (§4.2, p.4).
5. Emit idiomatic Rust together with a machine-readable interface transformation specification (SPEC) (§4.2, p.4; §4.3, p.5).
6. Verify each idiomatic item, then combine all items, remove duplicate definitions, and run the full program’s E2E tests (§4.3–§4.4, p.5).

Evidence and limits

On TransCoder-IR, DeepSeek-R1 reaches 94% unidiomatic and 93% idiomatic success; on CodeNet it reaches 86% and 84% (§6.1, pp.6–7). Success means translation plus passing E2E tests in both phases, with up to six attempts per translation (§5.2, pp.5–6). These percentages are over the 100 programs per dataset. On CRust-Bench (GPT-4o), the unidiomatic stage averages 85.15% per-sample function success, 788/966 functions (81.57%) in aggregate, and 32/50 samples fully translated; the idiomatic stage is evaluated only on those 32 samples and averages 51.85%, 249/580 functions (42.93%), and 8/32 samples fully translated (Table 2, §6.3, p.8). The abstract’s “85%” and “52%” are these per-sample averages rounded (Abstract, p.1).

Three ablations bear on the design (all GPT-4o). A plain one-step translation with up to 10 repair attempts reaches 77/966 (7.97%) CRust-Bench functions, or 207/966 (21.43%) with a prompt that encourages unsafe, and passes no libogg tests (Table 9, Appendix J.2, pp.23–24). Removing Crown drops libogg idiomatic success from 41 to 34 functions (53% to 44%) (Table 10, Appendix J.3, p.24). Replacing stage 1’s “may use unsafe if needed” with “AVOID using unsafe whenever possible” drops libogg unidiomatic success from 77/77 to 66/77 (Table 12, Appendix J.4.2, p.25).

Inference: this staging maps naturally to Verus. Stage 1 can be an unsafe or FFI boundary whose behavior is described by a contract; stage 2 can expose safe Rust operations and prove ensures clauses against a mathematical model. Passing E2E tests does not discharge a universal contract, and SACTOR does not invoke Verus.

technique 3: FFI end-to-end verification for unidiomatic Rust

what it is

The stage-1 Rust keeps compatible function signatures and data types, so the original C program can link to it as a shared library. SACTOR compiles the Rust, recompiles the C code with the Rust translation linked so that calls to the target function invoke Rust, runs the E2E tests on the entire program, and compares outputs with the original C. The paper gives the operational rule: “If all tests pass, the target function is considered verified” (§4.3, p.4).

how to apply it

1. Compile the unidiomatic Rust translation with the Rust compiler (§4.3, p.4).
2. Recompile the original C program with the Rust translation linked as a shared library (§4.3, p.4).
3. Run the E2E tests on the entire program, comparing outputs of the original C code and the Rust translation (§4.3, p.4).
4. On failure, feed compiler errors back; for test failures, instrument the target with a Rust procedural macro to log inputs and outputs, rerun tests, and return the traces (§4.3, p.5).
5. Accept the function when all tests pass and proceed to the next item (§4.3, p.4; Appendix E, p.16).

Evidence and limits

The evidence depends on test coverage. The authors state, “Correctness confidence in this framework depends on the code coverage of the E2E tests: the broader the coverage, stronger the assurance of equivalence” (§4.3, p.4). Their limitation is equally direct: “shallow or incomplete coverage can miss subtle semantic errors” (§8, p.9). Measured gcov line/function coverage is 97.97%/99.5% for TransCoder-IR, 94.37%/100% for CodeNet (whose tests SACTOR generated), 76.18%/80.98% for CRust-Bench, and 83.3%/75.3% for libogg (Table 5, Appendix F, p.18). Inference: for Verus, FFI tests can validate an external implementation against examples, while a Verus contract should establish behavior for all admitted inputs. Any C library and harness remain trusted assumptions unless separately specified and verified.

technique 4: SPEC-driven idiomatic harness synthesis

what it is

Idiomatic Rust changes types and signatures, so direct C linking no longer works. During stage 2, SACTOR co-produces a JSON SPEC per function or struct describing pointer shape (scalar, cstring, slice, ref), length source (sibling field or constant), nullability, ownership hint, return mapping, and comparison hints (§4.3, p.5; Appendix L, pp.27–28). A rule-based generator consumes the SPEC to make a C-compatible shim and idiomatic adapters. Unsupported patterns get a localized TODO filled by an LLM. Struct converters are checked by a round-trip self-test.

how to apply it

1. Emit a SPEC alongside each idiomatic function or struct (§4.3, p.5; prompt in Appendix N.3, pp.33–34).
2. Generate a C ABI shim and adapters that convert C-facing values to idiomatic Rust and back (§4.3, p.5; Appendix L, p.27).
3. Use pointer shapes to decide borrowing or ownership, take lengths from the SPEC’s length source, select Option or strict checks from nullability, and map returns back to the C-facing form, writing back lengths when needed (Appendix L, p.27).
4. For structs, run Unidiomatic→Idiomatic(1)→Unidiomatic→Idiomatic(2) and compare Idiomatic(1) with Idiomatic(2) field by field: by_value requires exact equality, by_slice compares contents using the SPEC length source, skip omits aliasing views or externally owned fields; seed values are synthesized by an LLM guided by the SPEC (Appendix L, pp.27–28).
5. If a pattern is unsupported, emit a localized TODO and let an LLM fill only the missing conversion using the SPEC (§4.3, p.5; Appendix L, p.28).
6. Compile the idiomatic crate and harness, link them into the C build via FFI, run E2E tests, and feed failures back (§4.3, p.5).

Evidence and limits

On libogg’s 77 functions, unidiomatic success is 100% for both GPT-4o and GPT-5; idiomatic success is 53% and 78%; average attempts are 2.00 and 1.25 (Table 3, §6.3, p.9). The attempt and lint averages cover only “functions that both LLM models succeed in translating” (Table 3 caption, p.9). Harness failures are a named failure mode: two GPT-4o and three GPT-5 libogg failures are uncompilable harnesses (Appendix M.2, p.29), and CRust-Bench failures “concentrate at ABI/type boundaries and harness synthesis (pointer/slice shape, length sources, lifetime or mutability)” (§6, p.6), including buffer mis-sizing (§6.3, p.8). Inference: this SPEC is analogous to a Verus abstraction boundary. A Rust adapter could expose a requires condition for valid lengths and an ensures relation between C-facing and idiomatic values; the adapter’s proof must cover aliasing and ownership rather than relying on the round-trip test alone.

technique 5: structured compiler and runtime feedback

SACTOR feeds compiler diagnostics and E2E failures back into the translation prompt; for E2E failures a Rust procedural macro logs salient inputs and outputs, reruns tests, and returns traces (§4.3, p.5). The ablation without feedback restarts from the original prompt (Appendix J.1, p.23). With feedback, Llama 3.3 70B improves on TransCoder-IR from 57 to 76 (unidiomatic) and 46 to 64 (idiomatic), and on CodeNet from 62 to 83 and 59 to 76, out of 100 tasks each; GPT-4o goes from 87 to 84 and 83 to 80 on TransCoder-IR and from 82 to 84 and 77 to 79 on CodeNet (Appendix J.1, p.23). The paper’s summary “boosts weaker models by 17%” (§1, p.2) matches only the CodeNet idiomatic gain.

Inference: Verus diagnostics can play the same role: feed failed requires, ensures, and invariant obligations to the agent, then retry. The acceptance criterion remains a successful Verus check, not a plausible repair. The paper’s feedback loop is a workflow technique, not a formal proof technique.

technique 6: idiomaticity and safety measurement

SACTOR measures Clippy lint alert count, unsafe code fraction (tokens inside unsafe blocks or functions over total tokens), and unsafe-free fraction (share of programs with no unsafe) (§5.2, p.6). On TransCoder-IR and CodeNet with GPT-4o, SACTOR’s idiomatic output is 100% unsafe-free with 0% average unsafe, versus 3.6%/1.1% unsafe-free and 91.7%/42.7% average unsafe for its unidiomatic output (Table 1, §6.2, p.8). On CRust-Bench, unidiomatic output averages 50.14 Clippy alerts per sample (2.96 per function), 97.86% unsafe fraction, and 0% unsafe-free; idiomatic output averages 2.27 alerts per sample (0.28 per function), 0% unsafe fraction, and 100% unsafe-free (§6.3, p.8). Inference: the CRust-Bench denominators are the 50 samples for unidiomatic output and the 32 fully unidiomatic samples for idiomatic output (Table 2, p.8). Inference: Clippy and absence of unsafe do not prove functional correctness or absence of undefined behavior in FFI.

Inference: VL can report these as engineering indicators after Verus verification, but should not treat them as substitutes for contracts. The paper already evaluates staged translation, static hints, FFI tests, SPEC harnesses, and feedback; VL should not redo those components as claimed formal verification. A distinct contribution would prove the SPEC adapter’s semantic relation in Verus and quantify which assumptions about C, FFI, and harnesses remain trusted.

what is proved, measured, and trusted

SACTOR measures translation and E2E test success, Clippy alerts, unsafe fractions, attempts, token and query costs (Appendix I, p.22), and temperature sensitivity (Appendix K, p.26). Inference: it does not prove equivalence for all inputs, memory safety of C or FFI, race freedom, validity of generated harnesses, or correctness of the C reference. Inference: the trusted base includes compilers, libclang, C2Rust and Crown analyses, the original or generated tests, the generated SPEC, the rule-based harness and any LLM fallback, FFI ABI behavior, and the C program itself. The authors list test coverage dependence, model variance, unsupported C features, static-analysis precision, harness generation stability, and cost and latency as limitations (§8, p.9).

Inference: the threat to agent-written verified Rust is high if “verified” means only SACTOR-style tests; it is lower if the pipeline supplies candidate code and counterexamples before Verus proves explicit contracts. FFI and generated adapters are the main risk boundary. The safe product integration is to use static analysis for context, harnesses for regression tests, and Verus as the acceptance check for the Rust contract.

techniques for the catalog

• dependency-aware static decomposition — parse C into a dependency graph and translate types, globals, and functions in dependency order
• two-stage translation — preserve ABI in an unidiomatic Rust pass, then refine to idiomatic ownership-aware Rust
• FFI E2E differential testing — link Rust behind the C ABI and compare complete-program test outputs
• SPEC-driven harness synthesis — generate adapters from machine-readable pointer, length, ownership, and return mappings
• structured feedback repair — turn compiler errors, runtime traces, and test failures into further translation attempts
• idiomaticity metrics — measure Clippy alerts, unsafe-token fraction, and unsafe-free rate alongside correctness Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “We then use valgrind to identify and discard programs with memory errors during the end-to-end tests.”): checked every quotation, number, section and page reference, and technique step against the paper text; changed page references (§4.1 and §4.3 idiomatic/feedback/§4.4 are on pp.4–5, Algorithm 1 is p.13, Table 14 is pp.30–31), the cycle-handling step (main text errors out, Algorithm 1 groups cycles), the feedback ablation numbers (Llama gains are 19/18/21/17 points, not a uniform 17), added the random-vs-largest sampling inconsistency, test coverage (Table 5), the plain-LLM, Crown and unsafe-prompt ablations, Table 1, and the Table 3 attempt-average caveat, removed the unsupported step that mapped arrays to unspecified Rust containers, and marked own conclusions “Inference:”; did not check the figures’ plotted bars beyond the numbers stated in the text, the code repository, or the link beyond the arXiv identifier printed in the paper.

Last edited: 2026-10-17