Automatically Inferring Sound Dataflow Functions from Dataflow
Fact Schemas
COCV 2005, Edinburgh, UK, April 3, 2005
Erika Rice,
Sorin Lerner, and
Craig Chambers
In previous work, we presented a language called Rhodium for writing
program analyses and transformations that could be checked for
soundness automatically. In this work, we present an algorithm for
automatically inferring sound flow func- tions given only a set of
dataflow fact schemas. By generating the flow functions mechanically,
our approach reduces the burden on compiler writers. This paper
presents a detailed description of our algorithm and shows how it
works on several examples. We have run our algorithm by hand on all
the statements of a simple C-like intermediate language for an
is-constant fact schema, a points-to fact schema, and a
variable-equality fact schema. Our algorithm generated a total of 71
rules for these cases. It generated all but one of the rules we had
written by hand for these dataflow fact schemas, and it also generated
new useful rules that we had not thought of previously.
Download: [PDF | PS]