 |
UCSD Programming Systems |
The Rhodium language for writing program analyses and transformations
Rhodium is a domain specific language for expressing program analyses and transformations. By providing natural abstractions for declaratively specifying analyses and transformations, Rhodium makes it easier for humans to write and reason about various kinds of program analysis tools, for example compilers, static checkers, static bug finders and source-to-source program translators. But more importantly, Rhodium will make it possible for a computer to effectively understand, process and reason about program analyses and transformations. Here are some examples of goals we hope to achieve once program analysis tools are expressed in Rhodium:
- reason statically about various properties of analyses and transformations;
- automatically combine separately written compiler optimizations, while still enabling them to interact in mutually beneficial ways;
- efficiently stage compiler optimizations;
- write various kinds of useful Rhodium transformers.
By providing better support for writing program analyses and transformations, Rhodium can provide a foundation for user-extensible program analysis tools, whether it be compilers, static bug finders or type-checkers.
As a first step, we have focused on reasoning statically about
the safety of Rhodium analyses and transformations. An analysis
is safe if the information it computes correctly characterizes
the behavior of the program being analyzed. A transformation is
safe if for any input program P, the
transformation produces an output program P' that is
semantically equivalent to P. We have implemented a
static safety checker that can verify the safety of Rhodium analyses
and transformations, before they are even run once.
The details of our approach can be found in the
following POPL 05 paper:
Automated Soundness Proofs for Dataflow Analyses and
Transformations via Local Rules (POPL 2005)
Sorin Lerner, Todd Millstein,
Erika Rice, and Craig Chambers
Also, the following PLDI 03 paper describes Cobalt,
the predecessor to Rhodium:
Automatically
Proving the Correctness of Compiler Optimizations
(PLDI 2003)
Sorin Lerner, Todd Millstein, and Craig Chambers