Learning Effective BDD Variable Orders for BDD-based Program Analysis

Software reliability and security are in jeopardy. As software has become ubiquitous and its capabilities have become more complex, code quality has been sacrificed in the race for the next ”killer app.” In response, program analysis researchers have mounted a revolution; they have developed new tools and methods, underpinned by traditional compilation techniques, in order to save software from its downward spiral. However, because these tools and analyses have also become more sophisticated, they too have suffered from scalability, reliability and complexity issues.
Just as program analysis researchers have set out to solve the problems of software developers, we have set out to solve the problems of program analysis researchers. The bddbddb (Binary Decision Diagram-Based Deductive DataBase) system has recently made possible many advanced, context-sensitive program analyses. Such analyses can be expressed in bddbddb as Datalog queries, which are quantifiably easier to write than a traditional implementation. The bddbddb system’s unique compilation mechanisms also yield analyses of exceptional performance. The key to this performance is the use of Binary Decision Diagrams (BDDs), a compact representation that exploits repeated patterns in data, to represent the principle elements of an analysis. However, finding efficient BDD representations (i.e., BDD variable orders) for a particular analysis is nearly impossible to accomplish manually and, in some cases, is without a solution given an analysis and its formulation.
This thesis presents an algorithm that helps automate the discovery of efficient BDD representations. Our technique reformulates the search for BDD variable orders as an active learning process over the space of BDD variable orders and their execution times. This technique revolves around an iterative process of carefully sampling new orders and then reducing the search space by extracting features from high performance orders. The dominant features of the sampled variable orders can then be used to generate new orders, refine existing orders, or even revise analysis formulations. The variable orders generated by our algorithm outperform those obtained after months of manual exploration. And, more importantly, our results make bddbddb a viable and valuable tool for program analysis researchers in their quest for better quality code.