Tuesday, March 15, 2005, 12-1, 4760 Boelter Hall
Program Analysis with Binary Decision Diagrams
John Whaley
Stanford, http://www.stanford.edu/~jwhaley
Binary decision diagrams (BDDs) are a data structure that can efficiently
represent large relations and provide efficient set operations. BDDs have
traditionally been used for model checking, formal verification, optimizing
circuit diagrams, etc. My research applies BDDs to the area of program
analysis. In this talk, I will describe a scalable context-sensitive,
inclusion-based pointer alias analysis for Java programs. My approach to
context sensitivity is to create a clone of a method for every context of
interest, and run a context-insensitive algorithm over the expanded call
graph to get context-sensitive results. Normally, this formulation is
hopelessly intractable as a call graph often has 10^14 acyclic paths or
more. I show that these exponential relations can be computed efficiently
using BDDs. I applied my algorithm to the most popular applications
available on Sourceforge and found that even the largest programs can be
analyzed in under 20 minutes.
Using BDDs for program analysis also allows us to specify program analyses
at a higher level. The pointer analysis, along with many other algorithms,
can be described succinctly and declaratively using Datalog, a logic
programming language. I have developed a system called "bddbddb" that
automatically translates Datalog programs into highly efficient BDD
implementations. I and others have used bddbddb to develop a variety of
context-sensitive algorithms, including side effect analysis, escape
analysis, external lock analysis, and analyses to detect and prevent various
security vulnerabilities in C and Java programs. Experiments have shown
that the code generated by bddbddb is up to five times faster than a
hand-coded, hand-tuned solver.
Host: Jens Palsberg