October 06, 2004
Hilton Suites Toronto/Markham Conference Centre
Markham, ON
Associated with CASCON 2004
(http://www.cas.ibm.com/cascon)
Taming Pointers -- A Symbolic Approach
Jianwen Zhu - University of Toronto
Parallelizing compilers often stumble on the pointer analysis
problem, or the computation of runtime pointer values at
compile time. The challenges of precise pointer
analysis stem from the need to explore an exponential number of
program execution paths, and the need to maintain program state
for every program point under all such paths.
In this talk, I will introduce a new method for constructing
scalable graph algorithms (ICCAD'02, PLDI'04), called
superposition, which solves different problem instances in an
aggregate fashion. Applying this method to pointer analysis,
different program states under different execution paths are
combined into a single Boolean function, and solved together using
the efficient, BDD-based image computation operator developed by
the formal verification community. Experimental results show that
context-sensitive, flow-insensitive analysis on programs with
billions of different calling paths can be analyzed in seconds.
The subject of this talk can be of interest to researchers in
high-performance compiler, software engineering and software security.
Presentation Slides.