Corrode: Automatic semantics-preserving translation from C to Rust
This program reads a C source file and prints an equivalent module in Rust syntax. It's intended to be useful for two different purposes:
Partial automation for migrating legacy code that was implemented in C. (This tool does not fully automate the job because its output is only as safe as the input was; you should clean up the output afterward to use Rust features and idioms where appropriate.)
A new, complementary approach to static analysis for C programs. If this program can't translate your C source to equivalent Rust, you might consider whether your program is too complicated and hiding bugs. Or, if translation succeeds, the Rust compiler may report warnings and errors that your C compiler misses, or you may be able to use a custom Rust linter to detect project-specific problems.
As of now, there are no pre-built binaries available, so you need to build the
project yourself, but don't let that scare you away; clone the project,
into it and follow along :)
If you're using Windows, start by running
Ensure that you have GHC and the
cabal-install tool installed by following
the directions on haskell.org.
You'll also need to have the
alex tools available in order to
corrode: you can install them with the
cabal-install tool, as well.
Once you have installed the
cabal-install tool, you can build
navigating to the
corrode directory, installing the
and then building and installing the
cabal install happy cabal install alex cabal install
This puts the
corrode executable in
~/.cabal/bin, so ensure that that
location is in your
Alternately, you can use the Haskell Stack tool for Haskell development. If you don't have it, head over to their website and follow the instructions for installing it on your machine.
Install the Glasgow Haskell Compiler using
stack setup. You can skip this
step if you already have a version of GHC installed on your system.
You can then build and install
corrode by navigating to the
directory and running:
Stack will build and install
~/.local/bin. For ease of use, make
sure that directory is in your
You can now run
corrode, giving it any options that
corrode -Wall filename.c -I/usr/local/include -lm
It will only use the options that are relevant to the C pre-processor,
-D, but since it accepts and ignores any other options,
you can usually hack it into existing build systems just by setting
However, unlike a real C compiler, Corrode does not produce an object
file or executable! Instead, if you ask it to process
generates equivalent Rust source code in
filename.rs. At the moment,
it's up to you to invoke
rustc on the output with appropriate options
to finish compilation.
To experiment with the project itself, you can build it using
then run the executable:
stack exec -- corrode -Wall filename.c -I/usr/local/include -lm
Corrode aims to produce Rust source code which behaves exactly the same way that the original C source behaved, if the input is free of undefined and implementation-defined behavior.
At the same time, Corrode should produce code which is recognizably structured like the original. Every statement and every expression should be represented in the output—in the same order, where possible. If a programmer went to the trouble to put something in, I want it in the translated output; if it's not necessary, we can let the Rust compiler warn about it.
In the presence of undefined behavior, I've tried to pick a behavior
that isn't too surprising and preserves the structure of the input
program. For example, if a signed addition might overflow (which is
undefined behavior in C), Corrode just translates it to Rust's
operator, which panics on overflow in debug builds.
So far, Corrode has primarily been tested by generating random C programs using csmith, fixing Corrode until it can handle all syntax used in that particular program, and verifying that the resulting Rust module compiles without errors.
Because the project is still in its early phases, it is not yet possible to translate most real C programs or libraries. But if you have one you particularly want to try out, I'd love to get pull requests implementing more of C!
If this seems cool and you'd like to help complete it, welcome! There are quite a few fundamental pieces of the C standard which are not yet implemented. I'm trying to keep track of good starting projects as issues with the 'Easy' label.
"Easy" is, of course, a relative term in a project mashing together C's complicated semantics with Rust's not-fully-documented semantics and all implemented in Haskell. I'd love to chat with you if you're not quite sure how to get started! You can e-mail me at firstname.lastname@example.org.
A Rust module that exactly captures the semantics of a C source file is
a Rust module that doesn't look very much like Rust. ;-) I would like to
build a companion tool which rewrites parts of a valid Rust program in
ways that have the same result but make use of Rust idioms. I think it
should be separate from this tool because I expect it to be useful for
other folks, not just users of Corrode. I propose to call that program
"idiomatic", and I think it should be written in Rust using the Rust AST
Verifying that the translated output is equivalent to the input is not
trivial. One approach I think is worth trying is to use the Galois
Software Analysis Workbench to prove that the
LLVM bitcode generated from
clang on a C source file is equivalent to
the LLVM bitcode generated from
rustc on a Rust source file from
Corrode. SAW uses a symbolic simulator over LLVM bitcode to extract
logical formulas representing the behavior of each function, and then
uses an SMT solver to prove equivalence between pairs of formulas.
Generating large numbers of random C programs using csmith and then
proving the translation results equivalent for each one should give
pretty good confidence in the implementation.