Tools for automatic program analysis promise to improve programmer productivity by searching and summarizing large bodies of code. However, the phenomenon of aliasing -- different names being used to refer to the same data -- reduces the effectiveness of simple textual analyses. This dissertation describes the design of a system, Ajax, that addresses this problem by using semantics-based program analysis as the basis for a number of different tools to aid Java programmers.

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.

294 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu