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:
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
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 and in the following Ph.D. thesis: Automatically Proving the Correctness of Program Analyses and Transformations (Ph.D. thesis, 2006)
We have also done work on automatically inferring analyses written in the Rhodium language. Users who write analyses in Rhodium are required to provide semantic meanings for the dataflow facts they define. These meanings can be used to automatically determine the best analysis rules. However, those rules cannot always be expressed directly in Rhodium. We have an algorithm which finds the best analysis rule and transforms it to an analysis rule which can be expressed in Rhodium but may be less precise than the original.
Our approach can infer about half of the rules we had written by hand; some rules are lost because of the transformation heuristics we have chose. Our approach also infers many rules which were not covered by the handwritten rules.
The details of an early version of this algorithm can be found in the
following COCV 05 workshop paper:
Inferring Sound Dataflow Functions from Dataflow Fact Schemas (COCV
Erika Rice, Sorin Lerner, and Craig Chambers
Also, the following PLDI 03 paper describes Cobalt,
the predecessor to Rhodium:
Proving the Correctness of Compiler Optimizations
Sorin Lerner, Todd Millstein, and Craig Chambers