Program Analysis with Binary Decision Diagrams

Dr. Whaley is from Massachusetts Institute of Technology
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.