wasp mascot


Washington Advanced Systems for Programming

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:

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


Sorin Lerner, Todd Millstein, Erika Rice, and Craig Chambers