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

Translating All C to Rust (TRACTOR)

darpa.mil

Post reply on HN
Print view View original

161–170 of 403 posts

Re: Translating All C to Rust (TRACTOR)

#161

Post by nanolith »

PhilipRoman wrote: post #153
nanolith wrote: post #126

Earlier quoted context omitted.

> No chance. CBMC is amazing, but have you actually tried formally verifying a "real" program? Yes. Every day. It's actually quite easy to do. Write shadow methods covering the resources and function contracts of called functions, then verify the function. Repeat all of the way up and down the stack. It adds about 30% overhead over just TDD development.

Last time I tried CBMC, it ended up running out of memory for relatively small programs, do you encounter any resource usage issues with it? I'm learning Frama-C and I find it more predictable, although the non-determinism of solvers shocked me when I first tried to prove non-trivial programs. I guess ideally I would like something even more explicit than Frama-C.

CBMC works best on functions, not programs. You want to isolate an individual function, then provide shadows of the functions it calls. The shadows should have nondeterministic behavior (cover every possible error condition) and otherwise follow the same memory and resource rules as the original function. For instance, if shadowing a function that reads a buffer, the shadow should ensure full buffer access as part of its assertions.

The biggest issue you will run into with bounded model checking is recursion and looping. In these cases, you want to refactor the code to make it easier to formally verify outside of the loop. Capture and assert on loop variants / invariants, and feed these forward in assertions on code.

There's no way I can capture all of this in an HN comment, but to get CBMC to work, you need to break down your code.

Re: Translating All C to Rust (TRACTOR)

#163

Post by jcranmer »

Animats wrote: post #155
jcranmer wrote: post #112

Earlier quoted context omitted.

I once tried to use c2rust as a starting point for rustification of code and... it's not even good at that. The code is just too freakishly literal to the original C semantics that you can't even take the non-pointery bits and strip off the unsafe block and use that as a basis. (To give you a sense, it translates something like a + 1 to a.unwrapped_add(1i32), and my recollection is that for (int i = 0; i In general,…

That doesn't mention the affine type problem. Rust references are restricted to single ownership. If A has a reference to B, B can't have a reference to A. Bi-directional references are not only a common idiom in C, they're an inherent part of C++ objects. Rust has to use reference counts in such situations. You have an Rc wrapped around structs, sometimes a RefCell, and .borrow() calls that panic when you have a con…

I'd lump that analysis somewhere in the d-g, because you have to remember that &mut is also noalias and work out downstream implications of that. It's probably presumptive of me to assume a particular workflow for reconstructing the ownership model to express in Rust, and dividing that into the steps I did isn't the only way to do it.

In any case, it's the difficulty of that reconstruction step that leaves me thinking that automated conversion of whole-application to Rust is a near-impossibility. Conversion of an individual function that works on plain-old-data structures is probably doable, if somewhat challenging.

An off-the-cuff idea I just had is to implement a semi-automated transformation, where the user has to input what a final conversion of a struct type should look like (including all Cell/Rc/whatever wrappers as needed), and the tool can use that to work out the rest of the translation. There's probably a lot of ways that can go horribly wrong, but it seems more feasible than trying to figure out all of the wrappers need to be.

Re: Translating All C to Rust (TRACTOR)

#164

Post by saagarjha »

programd wrote: post #64
Calavar wrote: post #47

Earlier quoted context omitted.

> today cars drive themselves You can attach about a hundred asterisks to that. If anything, I think self the failure to hit L5 driving after billions of dollars and millions of man hours invested is probably reflective of how automatic C to Rust translation will go. We'll cruise 90% of the way, but the last 10% will prove insurmountable with current technology. Think about the number of C programs in the wild that r…

> > today cars drive themselves > You can attach about a hundred asterisks to that. Not in San Francisco. There are about 300 Waymo cars safely driving in one of the most difficult urban environments around (think steep hills, fog, construction, crazy traffic, crazy drivers, crazier pedestrians). Five years ago this was "someday" science-fiction. Frankly I trust them much more then human drivers and envision a future…

San Francisco, for all its challenges, mostly has traffic laws that people follow. This is not true throughout the world.

Re: Translating All C to Rust (TRACTOR)

#166

Post by warkdarrior »

9659 wrote: post #159
reaperducer wrote: post #154

Earlier quoted context omitted.

in this case it seems to me the hard task that DARPA has chosen is to get me to forget how much they spent on pushing Ada. You hate jumbo jets, high-speed trains, air traffic control, and satellites?

Do you know what fear is? Getting in an airplane where the flight controls use NPM.

   npm ERR! install Couldn't read dependencies
   npm ERR! package.json ENOENT, open '/boeing/787-9/flaps-up.json'
   npm ERR! package.json This is most likely not a problem with npm itself.
   npm ERR! package.json npm can't find a package.json file in your current directory.

Re: Translating All C to Rust (TRACTOR)

#167

Post by PhilipRoman »

nanolith wrote: post #161
PhilipRoman wrote: post #153

Earlier quoted context omitted.

Last time I tried CBMC, it ended up running out of memory for relatively small programs, do you encounter any resource usage issues with it? I'm learning Frama-C and I find it more predictable, although the non-determinism of solvers shocked me when I first tried to prove non-trivial programs. I guess ideally I would like something even more explicit than Frama-C.

CBMC works best on functions, not programs. You want to isolate an individual function, then provide shadows of the functions it calls. The shadows should have nondeterministic behavior (cover every possible error condition) and otherwise follow the same memory and resource rules as the original function. For instance, if shadowing a function that reads a buffer, the shadow should ensure full buffer access as part of…

Thanks, that was really helpful. Relying on getting shadow functions right does seem icky, but I guess the improved productivity of CBMC should make up for it. Definitely going to give it another chance!

Re: Translating All C to Rust (TRACTOR)

#168

Post by rectang »

Someone wrote: post #152
rectang wrote: post #120

Earlier quoted context omitted.

I have to imagine that in the general case it will be a translation to unsafe Rust, with occasional isolated leaf nodes being translated to safe Rust. If you think it's hard wrestling with the borrow checker, just imagine how much harder it is to write automatic translation to borrow-checker-approved code that accounts for all the possible program space of C and all it's celebrated undefined behavior. A classic probl…

> have to imagine that in the general case it will be a translation to unsafe Rust, with occasional isolated leaf nodes being translated to safe Rust. That’s not what they are aiming for. FTA: “The goal is to achieve the same quality and style that a skilled Rust developer would produce” > just imagine how much harder it is to write automatic translation to borrow-checker-approved code that accounts for all the possi…

> undefined behavior gives the compiler leeway in deciding what a program does, so the more undefined behavior a C program invokes, the easier it is to translate its code to rust.

That's the kind of language lawyer approach that caused a rebellion in the last decade amongst C programmers against irresponsible compiler optimizations. "Who cares if your program actually works as intended? My optimization is legal according to the standard, it's your program that's written to exploit loopholes".

I don't see any evidence that that's the attitude being taken by TRACTOR — I sure hope it isn't. But hell, even if the result is unreliable in practice, I suppose that if somebody gets to claim "it works" then the incentives are aligned to produce garbage.

Re: Translating All C to Rust (TRACTOR)

#169

Post by warkdarrior »

plasticeagle wrote: post #149

If 1) Rust contains no memory bugs 2) C can be automatically translated to it Then all memory bugs can be fixed automatically, which is almost certainly untrue. This task is very likely completely impossible in the general case.

Since you did not specify that you wish to preserve all behaviors of the C code, there are trivial solutions to this problem. For example, one could replace all dynamic memory allocations with fixed buffers (set at translation time), and reject all inputs that do not fit in those buffers.

Re: Translating All C to Rust (TRACTOR)

#170

Post by estebank »

PreInternet01 wrote: post #18
keybored wrote: post #7

Earlier quoted context omitted.

You linked an interpreter for some kind of internal compiler representation that the Rust compiler uses. What on Earth do you mean?

> What on Earth do you mean? That documented use of safe Rust can easily lead to UB, which this infernal 'internal compiler representation' demonstrates. I'm not even sure what is even remotely confusing about that?

> That documented use of safe Rust can easily lead to UB

The only thing that comes to mind that this could be referring to are the open bugs at https://github.com/rust-lang/rust/issues?q=is%3Aopen+is%3Ais.... Are these what you're referring to?

> this infernal 'internal compiler representation'

What makes MIR "infernal"?

> I'm not even sure what is even remotely confusing about that?

You posted a link to a tool that executes pure rust libraries and evaluates memory accesses (both from safe and unsafe rust code) to assert whether they conform to the rust memory model. It sits in the same space as valgrind. You left it open to interpretation with really no other context. We can be excused for not knowing what you were trying to say. I personally still don't.

Post reply on HN