Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Translating Large-Scale C Repositories to Idiomatic Rust

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

result

  • Rustine: 5-stage pipeline, whole C repo to Rust
    • preprocess, refactor, dependence analysis, LLM translate, test-based validate/debug
  • 23 C programs, 27–13,200 LOC
    • 100% compile, no human help
    • 87% assertions pass (1,063,099/1,221,192) after automated + manual debugging
    • 10 projects fully equivalent automatically (2 have no assertion results in Table 2)
    • human fixed 11 remaining to 100% in 4.5h avg
    • 3.92h and $0.48 per translation
  • evidence is tests, not proof; output retains unsafe
    • raw pointer decl/deref 4,080/2,045 (C) to 198/126 (Rust)
    • 243 new pointer-arithmetic cases in 14 projects C-side preparation
  • run C preprocessor first: expand headers, macros, #ifdef
  • refactor C to ease translation, revert if tests fail
    • unary inc/dec to assignments
    • pointer arithmetic to integer index + array access
      • claimed semantics-preservation proof is in an absent appendix
    • constness via data flow, steers to &T vs &mut T
    • function over 50% of context window split into helper_<fn>_<block> translation order and context
  • context-sensitive dependence graph, SCCs via Tarjan become translation units
    • reverse topological order, compilable skeleton
  • core lib calls: retrieve Linux API docs; external libs: bindgen FFI two-tier LLM loop
  • base model (DeepSeek-V3) with fixed idiomatic ICL example + compiler feedback
  • after 8 failed re-prompts, reasoning model (DeepSeek-R1) with adaptive ICL
    • example picked by Rust error code + embedding similarity, or generated by o4-mini
    • e.g. E0499 fixed via split_at_mut test-based debugging
  • count assertions, not test exits
  • disable failing assertions, re-enable one by one
  • shortlist top stack functions, reasoning LLM proposes fix from C + Rust + stderr
  • accept only if target passes and nothing regresses; heuristic, can miss culprits Verus relevance (inference)
  • refactorings and translation each need equivalence lemmas; tests miss unexecuted inputs
  • FFI/OS calls stay trusted

Last edited: