-
Notifications
You must be signed in to change notification settings - Fork 4
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Xr0 in Rust #52
base: master
Are you sure you want to change the base?
Xr0 in Rust #52
Conversation
In the original, these returned `result` which was implicitly a Result<Value>.
@@ -1 +1 @@ | |||
7-use-after-free/400-FAIL-conditions-in-setup.x:4:3 setup preconditions must be decidable |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This PR changes one test expectation, only because I could not get the Rust parser library I chose to reproduce the (questionable) line and column information of the original! The behavior of the verifier is, as far as I know, identical.
(Actually... I made the Rust parser emit deliberately funky location information to match what the tests expect -- locations at the end of statements rather than the beginning -- but in this particular case Yacc uses an extra token of lookahead to check for else
, so setup.x:4:3
is actually the position at the end of the first token of the next statement. I decided not to go out of my way to reproduce that behavior, but just hack the test.)
} | ||
|
||
impl AstBlock { | ||
//=ast_block_create |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
These //=
comments simply mark where there's Rust code that corresponds to some C function. They help when merging C changes to Rust. There's nothing special about //=
in Rust. There's no tooling or anything that uses these comments, and not every C function has one.
No leaks!
Total heap usage, according to Valgrind, is 5% of what the original uses when verifying The original:
|
This is absolutely incredible and I am both speechless and deeply moved. We will definitely take the time to work through this.
No worries about this in the least! This is the most wonderful thing that anyone has done in all the time we've been working on Xr0. |
Genuinely amazed by this :o |
Hi, this is a peculiar thing to have done, and likely not in line with your plans, but I have ported Xr0 to safe Rust.
I did it for fun, and to see what it would be like. I decided to open a PR here for a few reasons:
This found several apparent memory leaks, double frees, and other general bugs in the C code, most of which would be pretty easy to fix in the C codebase. Search for
// Note:
in the PR.Safe Rust poses challenges of its own. Search for
// Rust note:
to see places where the port clones some data or does extra work at run time to convince Rust it's safe. I think this stuff is interesting.As you've observed, Rust isn't perfect. On the other hand, we have it now, and it has advantages. The Rust code is half as many lines of code as the original C, and it won't crash or leak. Rust has
Vec
,Result
, and safe tagged unions built in. Memory management is automatic. So ... it is worth seriously considering switching. Rust makes Xr0 safer than C!I want to be clear I'm not trying to dunk on Xr0 here or whatever. I'm a Rust fan, but mostly just enthusiastic about making our software world work better. Every effort to make C safer is welcome.