Program Analysis with Binary Decision Diagrams

March 17, 2005
John Whaley | Stanford

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¹⁴ 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.

Speaker Details

John Whaley graduated from MIT in 1999 with a Bachelors and Masters in Electrical Engineering and Computer Science, and will be receiving his Ph.D. in Computer Science from Stanford University in June 2005. He has worked at IBM Watson Research on the Jalapeno Java virtual machine and at IBM Tokyo Research Laboratory on the JIT compiler for the IBM Java Development Kit. John is the author of many open source projects, including joeq, a virtual machine and compiler infrastructure used by researchers around the world and for the compilers course at Stanford University. He is the winner of Best Paper Awards at OOPSLA 2001 and PLDI 2004, and a SIGSOFT Distinguished Paper Award at ISSTA 2002. His primary research interests are in program analysis, compilers, and virtual machines.