Compiling C to Safe Rust, Formalized
#論文
https://arxiv.org/abs/2412.15042
C で書かれたプログラムを safe Rust にコンパイルする。
入力は任意の C コードではなく、mini-C と呼ばれる C のサブセット。
We present Mini-C (Figure 1), a data-oriented subset of C that is expressive enough to handle a large class of applications. Types comprise value, pointer and struct types.
ポインタ演算もできる。Rust の split_at_mut を使う。
What Rust provides instead is a primitive named split_at_mut (or split_at for immutable slices), which allows the programmer to relinquish ownership of a slice, and obtain in exchange two sub slices that split the original slice at the given index. This permits some restricted notion of pointer arithmetic, while preserving Rust’s invariant that mutable data should have a unique owner: to regain ownership of the original slice, the programmer must give up the sub slices.
分割した配列を管理するために Split Tree というデータ構造を使う。
C はスタックを指すポインタとヒープを指すポインタを区別しないが、Rust では明確に区別している。基本的には Box に変換するっぽい。
評価に使われたプログラムは HACL* とよばれる暗号ライブラリ。 Low* とよばれる、 C 互換かつ F* のサブセットである言語で書かれている。C に変換すると 95,000 行。提案手法によって safe Rust に変換することができた。