Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Ownership guided C to Rust translation

Hanliang Zhang, Cristina David, Yijun Yu, Meng Wang

TL;DR

The paper addresses safely translating large C codebases to Rust by inferring and enforcing Rust-compatibility ownership models. It introduces Crown, a pipeline that starts from c2rust-generated Rust, applies a scalable, flow- and field-sensitive ownership analysis, and retypes and rewrites pointers to produce safe Rust code validated by the Rust compiler. Key contributions include the formalization of ownership constraints, the novel ownership monotonicity concept, and a prototype tool that scales to hundreds of thousands of lines of code while outperforming the prior state-of-the-art in pointer safety conversion. The work has practical impact by enabling safer migration of legacy C software, reduces unsafe usage, and provides a foundation for future enhancements in handling real-world C idioms and memory management.

Abstract

Dubbed a safer C, Rust is a modern programming language that combines memory safety and low-level control. This interesting combination has made Rust very popular among developers and there is a growing trend of migrating legacy codebases (very often in C) to Rust. In this paper, we present a C to Rust translation approach centred around static ownership analysis. We design a suite of analyses that infer ownership models of C pointers and automatically translate the pointers into safe Rust equivalents. The resulting tool, Crown, scales to real-world codebases (half a million lines of code in less than 10 seconds) and achieves a high conversion rate.

Ownership guided C to Rust translation

TL;DR

The paper addresses safely translating large C codebases to Rust by inferring and enforcing Rust-compatibility ownership models. It introduces Crown, a pipeline that starts from c2rust-generated Rust, applies a scalable, flow- and field-sensitive ownership analysis, and retypes and rewrites pointers to produce safe Rust code validated by the Rust compiler. Key contributions include the formalization of ownership constraints, the novel ownership monotonicity concept, and a prototype tool that scales to hundreds of thousands of lines of code while outperforming the prior state-of-the-art in pointer safety conversion. The work has practical impact by enabling safer migration of legacy C software, reduces unsafe usage, and provides a foundation for future enhancements in handling real-world C idioms and memory management.

Abstract

Dubbed a safer C, Rust is a modern programming language that combines memory safety and low-level control. This interesting combination has made Rust very popular among developers and there is a growing trend of migrating legacy codebases (very often in C) to Rust. In this paper, we present a C to Rust translation approach centred around static ownership analysis. We design a suite of analyses that infer ownership models of C pointers and automatically translate the pointers into safe Rust equivalents. The resulting tool, Crown, scales to real-world codebases (half a million lines of code in less than 10 seconds) and achieves a high conversion rate.
Paper Structure (35 sections, 3 theorems, 4 figures, 2 tables)

This paper contains 35 sections, 3 theorems, 4 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Background
  3. Rust ownership model
  4. Pointer types in Rust
  5. Unsafe Rust
  6. Overview
  7. Pushing into a singly-linked list
  8. Freeing an argument list in bzip2
  9. Architecture
  10. Ownership Analysis
  11. Ownership and aliasing
  12. Generation of ownership constraints
  13. Solving ownership constraints
  14. Discussion on ownership monotonicity
  15. C to Rust Translation
  16. ...and 20 more sections

Key Result

theorem thmcountertheorem

If ownership is transferred from $w$ to $v$, then, by the ASSIGN rule and ownership monotonicity, ownership also transfers between corresponding pointers on all access paths $p$ and $q$: $\mathbb{O}_{p'} =\mathbb{O}_{q}$ and $\mathbb{O}_{q'}=0$. (proof in Appendix sec:proof-of-transfer)

Figures (4)

  • Figure 1: Pushing into a singly-linked list
  • Figure 2: Freeing an argument list
  • Figure 3: Ownership constraint generation for assignment
  • Figure 4: Selected ownership rules

Theorems & Definitions (7)

  • definition thmcounterdefinition: Ownership monotonicity
  • theorem thmcountertheorem: Ownership transfer
  • theorem thmcountertheorem: Soundness of ASSIGN under ownership monotonicity
  • definition thmcounterdefinition: Ownership constraint system
  • theorem thmcountertheorem: Complexity of the ownership constraint solving
  • proof
  • proof