Strictly Declarative Specification of Sophisticated Points-to Analyses
Speaker: Martin Bravenboer, University of Massachusetts, Amherst
Location: Warren Weaver Hall 1302
Date: March 30, 2009, 11:30 a.m.
Host: Michael Overton
We present the Doop framework for points-to analysis of Java programs. Pointer analysis is the most fundamental program analysis and has a long and rich history of research and application. Doop builds on the idea of specifying pointer analysis algorithms declaratively, using Datalog: a logic-based language for defining (recursive) relations. We carry the declarative approach further than past work by describing the full end-to-end analysis in Datalog, which was thought to be impossible. The pointer analysis specifications are optimized aggressively through exposition of the representation of relations (e.g. indexing) to the Datalog language level and a novel technique that takes into account Datalog incremental evaluation.
As a result, Doop achieves a full order of magnitude improvement in runtime over the current state of the art in context-sensitive pointer analysis. Additionally, Doop scales to very precise analyses that are impossible with previous pointer analysis algorithms, directly addressing open problems in past literature. Finally, our implementation is modular and can be easily configured to analyses with a wide range of characteristics, largely due to its declarativeness.
Our work is a strong data point in support of declarative languages: we believe that humans cannot implement and optimize well complex mutually-recursive definitions at an operational level of abstraction, but can do so using declarative specifications. The work also demonstrates that representing relations using binary decision diagrams, as in past precise pointer analysis work, is not essential for the most important configurations, and even detrimental to performance.
In-person attendance only available to those with active NYU ID cards. All individuals must show the Daily Screener green pass in order to gain entry to the building.