Computer Science Department
School of Computer Science, Carnegie Mellon University
Generalized Aliasing as a Basis for Program Analysis Tools
To enable the construction of many tools, Ajax imposes a clean separation between analysis engines that produce alias information and tools that consume it. Analyses are treated as "black boxes" satisfying a simple, formal specification given in terms of the semantics of Java bytecode. Knowing only this specification, one can build many different tools with only a small amount of code. The thesis explores the flexibility and efficiency of the design by describing the construction and evaluation of several different tools: tools to find dead code, resolve Java virtual method calls, statically check Java downcasts, search for accesses to objects, and build object models. To support these tools, Ajax includes a novel static analysis engine for Java called SEMI, based on type inference with polymorphic recursion. SEMI provides fully context sensitive analysis of large programs. Using SEMI with the downcast checking tool, Ajax can prove the safety of more than 50% of the downcast instructions in some real-life Java programs, such as Sun's bytecode disassembler and the JavaCC parser generator. Ajax is the first system to address this particular task.
One of the key goals of this thesis is to study issues bearing on the practical utility of static analysis tools for programmers. This document describes some of the challenges involved in building an analysis system for off-the-shelf Java applications, and suggests some possible avenues for future research.