Ph.D. Theses

High-Level Static Analysis for Generic Libraries

By Douglas Gregor
Advisor: Sibylle Schupp
April 13, 2004

Software developers are increasingly reliant on well-tested, reusable software libraries that can rapidly decrease development time by eliminating the need to reimplement standard algorithms and data structures. Generic software libraries in particular, such as the C++ Standard Template Library (STL), provide efficient, reusable solutions that can be customized for nearly any computing environment.

Generic software libraries introduce a large number of abstractions, such as subroutines and classes, which simplify the task of a software developer. These abstractions, however, complicate static analyses, causing traditional static analysis techniques to produce poor, imprecise results. In contrast, a higher-level static analysis exploits these same abstractions to produce precise program analysis information at the library's level of abstraction, enabling library-level optimization and verification.

This thesis introduces a higher-level static analysis that employs executable specifications of software libraries to reduce the complexities of library analysis and improve analysis precision. Moreover, our analysis exploits object-oriented abstractions to improve the precision of analysis for a very important class of iterator movement problems. Other abstractions, such as subroutine abstractions and pointers, are effectively handled with symbolic analysis methods, even in program loops with nontraditional induction variables.

This thesis also introduces an organization methodology for extensible specifications for generic software libraries based on algorithm concepts. This methodology minimizes the effort required to introduce new algorithms, data structures, and semantic properties into generic library specifications.

The methodologies and analyses presented are implemented in the STLlint static checker. STLlint is able to detect errors in the use of the Standard Template Library within C++ user programs, including semantic checks of the abstract properties of STL algorithms. Our experiments have shown that STLlint achieves a low false positive rate and is capable of diagnosing common STL usage errors.

Return to main PhD Theses page