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
and in the following Ph.D. thesis:
Automatically
Proving the Correctness of Program Analyses and
Transformations (Ph.D. thesis, 2006)
Sorin Lerner
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:
Automatically
Inferring Sound Dataflow Functions from Dataflow Fact Schemas (COCV
2005)
Erika Rice, Sorin Lerner, 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