xr0-org / xr0

The Xr0 Verifier for C
https://xr0.dev
Apache License 2.0
173 stars 4 forks source link

Xr0 in Rust #52

Open jorendorff opened 4 months ago

jorendorff commented 4 months ago

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:

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.

jorendorff commented 4 months ago

No leaks!

$ valgrind --fullpath-after=`pwd`/src/ --leak-check=full xr0-rs/target/debug/0v -I libx tests/99-program/100-lex/parse.x | grep "total heap usage"
==52548== Memcheck, a memory error detector
==52548== Copyright (C) 2002-2022, and GNU GPL'd, by Julian Seward et al.
==52548== Using Valgrind-3.21.0 and LibVEX; rerun with -h for copyright info
==52548== Command: xr0-rs/target/debug/0v -I libx tests/99-program/100-lex/parse.x
==52548== 
==52548== 
==52548== HEAP SUMMARY:
==52548==     in use at exit: 0 bytes in 0 blocks
==52548==   total heap usage: 528,925 allocs, 528,925 frees, 20,235,554 bytes allocated
==52548== 
==52548== All heap blocks were freed -- no leaks are possible
==52548== 
==52548== For lists of detected and suppressed errors, rerun with: -s
==52548== ERROR SUMMARY: 0 errors from 0 contexts (suppressed: 0 from 0)

Total heap usage, according to Valgrind, is 5% of what the original uses when verifying 100-lex/parse.x, but I'm guessing that's just the use of realloc every time it grows an array. Easily fixed in C.

The original:

==52571==   total heap usage: 643,804 allocs, 488,882 frees, 396,578,811 bytes allocated
akiarie commented 4 months ago

This is absolutely incredible and I am both speechless and deeply moved.

We will definitely take the time to work through this.

I want to be clear I'm not trying to dunk on Xr0 here or whatever.

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.

claude-betz commented 4 months ago

Genuinely amazed by this :o Second everything Amisi said.. Seeing your engagement with the project is insanely encouraging. Thank you!