Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Compiling C to Safe Rust, Formalized

arxiv.org

Post reply on HN
Print view View original

41–50 of 173 posts

Re: Compiling C to Safe Rust, Formalized

#41

Post by oneshtein »

pizlonator wrote: post #19
pornel wrote: post #17

Earlier quoted context omitted.

Rust's ownership model is close enough for translating C. It's just more explicit and strongly typed, so the translation needs to figure out what a more free-form C code is trying to do, and map that to Rust's idioms. For example, C's buffers obviously have lengths, but in C the length isn't explicitly tied to a pointer, so the translator has to deduce how the C program tracks the length to convert that into a slice.…

Rust’s ownership model forbids things like doubly linked lists, which C programs use a lot. That’s just one example of how C code is nowhere near meeting Rust’s requirements. There are lots of others.

Rus's ownership model doesn't forbid doubly linked lists. It forbids doubly owned lists, or, in other words, «use after free» bug.

Re: Compiling C to Safe Rust, Formalized

#42

Post by Animats »

quuxplusone wrote: post #31
orf wrote: post #23

Earlier quoted context omitted.

> Rust’s ownership model forbids things like doubly linked lists, which C programs use a lot. It’s literally in the standard library https://doc.rust-lang.org/std/collections/struct.LinkedList....

But it's not in C's standard library. So the exercise isn't merely to auto-translate one language's standard library to another language's standard library (say, replacing C++ std::list with Rust LinkedList) — which would already be very hard. The exercise here is to auto-identify-and-refactor idioms open-coded in one language, into idioms suited for the other language's already-written standard library. Imagine refa…

> The exercise here is to auto-identify-and-refactor idioms open-coded in one language, into idioms suited for the other language's already-written standard library.

That's what LLMs are for - idiom translation. You can't trust them to do it right, though.

[Pan et al . 2024] find that while GPT-4 generates code that is more idiomatic than C2Rust, only 61% of it is correct (i.e., compiles and produces the expected result), compared to 95% for C2Rust.

This problem needs both AI-type methods to help with the idioms and formal methods to insure that the guessed idioms correctly capture the semantics.

A big advance in this project is that they can usually translate C pointer arithmetic into Rust slices. That's progress on of one of the hardest parts of the problem. C2Rust did not do that. That system just generates unsafe raw pointer arithmetic, yielding ugly Rust code that replicates C pointer semantics using function calls.

DARPA is funding research in this area under the TRACTOR program. Program awards in April 2025, so this is just getting started. It's encouraging to see so much progress already. This looks do-able.

Re: Compiling C to Safe Rust, Formalized

#43

Post by oneshtein »

andrewflnr wrote: post #33
orf wrote: post #28

Earlier quoted context omitted.

Safe rust isn’t “rust code with absolutely 0 unsafe blocks in any possible code path, ever”. Rc uses unsafe code every time you construct one, for example. Unsafe blocks are an escape hatch where you promise that some invariants the compiler cannot verify are in fact true. If the translated code were to use that collection, via its safe interfaces, it would still be “safe rust”. More generally: it’s incorrect to say…

No one here is confused about what unsafe means. The point is, they're not implemented by following Rust's ownership model, because Rust's ownership model does in fact forbid that kind of thing. You can nitpick the meaning of "forbids", but as far as the current context is concerned, if you translate code that implements a doubly linked list (as opposed to using one from a library) into Rust, it's not going to work w…

It's easy to implement doubly linked lists in safe Rust. Just ensure that every element has one OWNER, to avoid «use after free» bugs, or use a garbage collector, like a reference counter.

Unlike C++ or Rust, C has no references, only pointers, so developer must release memory manually at some arbitrary point. This is the problem and source of bugs.

Re: Compiling C to Safe Rust, Formalized

#46

Post by zxvkhkxvdvbdxz »

ActorNightly wrote: post #26

[flagged]

With rust having recently entered the Linux kernel, Windows 11, qemu among others where Haskell never took a hold, I really fail to see where you feel the wind is blowing.

The thing is, rust is used today in more and more places because it's reliable. We're not going to switch out the ground we are standing on every time something shiny comes along and that's why this is such an interesting development.

Re: Compiling C to Safe Rust, Formalized

#47

Post by thunkingdeep »

LPisGood wrote: post #34
tonetegeatinst wrote: post #30

Earlier quoted context omitted.

What is the main difference? Can compiler flags force compliance?

My understanding is that formal verification is a tough goal to achieve and that it usually requires designing the program or the language to be a specific way. The problem with transpiling C to rust is that unsafe and unverified behavior can be a key property of the behavior resulting program, so there isn’t an obvious way to spit out a sort of rustified (CRustified?) binary that matches the behavior of the C progra…

Typical term is “Oxidized”. I think they feel clever when they do the RiiR thing and say that.

Re: Compiling C to Safe Rust, Formalized

#48

Post by smolder »

pornel wrote: post #17
pizlonator wrote: post #12

Compiling a tiny subset of C, that is. It might be so tiny as to be useless in practice. I have low hopes for this kind of approach; it’s sure to hit the limits of what’s possible with static analysis of C code. Also, choosing Rust as the target makes the problem unnecessarily hard because Rust’s ownership model is so foreign to how real C programs work.

Rust's ownership model is close enough for translating C. It's just more explicit and strongly typed, so the translation needs to figure out what a more free-form C code is trying to do, and map that to Rust's idioms. For example, C's buffers obviously have lengths, but in C the length isn't explicitly tied to a pointer, so the translator has to deduce how the C program tracks the length to convert that into a slice.…

It's not that simple. In fact it's impossible in some cases if you don't sprinkle unsafe everywhere and defeat the purpose. Rusts restrictions are so that it can be statically analyzed to guarantee safety. The superset of all allowable C program behaviors includes lots of things that are impossible to guarantee the safety of through static analysis.

Formally verified C involves sticking to a strict subset of the capabilities of C that is verifiable, much like Rust enforces, so it makes sense that programs meeting that standard could be translated.

Re: Compiling C to Safe Rust, Formalized

#49

Post by saghm »

Animats wrote: post #42
quuxplusone wrote: post #31

Earlier quoted context omitted.

But it's not in C's standard library. So the exercise isn't merely to auto-translate one language's standard library to another language's standard library (say, replacing C++ std::list with Rust LinkedList) — which would already be very hard. The exercise here is to auto-identify-and-refactor idioms open-coded in one language, into idioms suited for the other language's already-written standard library. Imagine refa…

> The exercise here is to auto-identify-and-refactor idioms open-coded in one language, into idioms suited for the other language's already-written standard library. That's what LLMs are for - idiom translation. You can't trust them to do it right, though. [Pan et al . 2024] find that while GPT-4 generates code that is more idiomatic than C2Rust, only 61% of it is correct (i.e., compiles and produces the expected res…

Oh god, I can't even imagine trying to have formally-verified LLM-generated code. It's not surprising that even incremental progress for that would require quite a lot of ingenuity.

Re: Compiling C to Safe Rust, Formalized

#50

Post by fuhsnn »

Animats wrote: post #42
quuxplusone wrote: post #31

Earlier quoted context omitted.

But it's not in C's standard library. So the exercise isn't merely to auto-translate one language's standard library to another language's standard library (say, replacing C++ std::list with Rust LinkedList) — which would already be very hard. The exercise here is to auto-identify-and-refactor idioms open-coded in one language, into idioms suited for the other language's already-written standard library. Imagine refa…

> The exercise here is to auto-identify-and-refactor idioms open-coded in one language, into idioms suited for the other language's already-written standard library. That's what LLMs are for - idiom translation. You can't trust them to do it right, though. [Pan et al . 2024] find that while GPT-4 generates code that is more idiomatic than C2Rust, only 61% of it is correct (i.e., compiles and produces the expected res…

>That's what LLMs are for - idiom translation. You can't trust them to do it right, though.

Optimizing C compilers also happened to be good at idiom recognition, and we can probably trust them a little more. The OP paper does mention future plan to use clang as well: >We have plans for a libclang-based frontend that consume actual C syntax.

If such transformation can be done at IR level it might be more efficient to be to C-IR > idiom transform to Rust-IR > run safe-checks in Rust-IR > continue compilation in C-IR or Rust-IR or combining both for better optimization properties.

Post reply on HN