Objective

Quanton is an interprocedural static program analysis framework being developed at the University of Toronto. The primary objective is to investigate the use of symbolic techniques, binary decision diagrams (BDDs) in particular, to scale precise pointer analysis to large programs. The secondary objective is to generalize the framework into other difficult analysis problems, and explore emerging applications enabled by such a scalable solution.

Background

The pointer construct is arguably one of the most important factors that led to the success of C and its derivatives. Unfortunately, in the software world it is also the major source of abuses, bugs, and security vulnerabilities. In the high performance computing world, where programs are compiled onto supercomputers, and in the hardware world, where programs are compiled into silicon, the pointer construct is again the bottleneck for finding parallelism. The pointer analysis problem has therefore attracted considerable amount of efforts over the past three decades. Despite an extremely rich literature, a scalable solution for the most precise form of analysis has not been reported.

Ideas

The major difficulty of scalable pointer analysis comes from the size of program state, which is traditionally represented by point-to graph. This is particularly pronounced in flow sensitive analysis, when program states at every program point need to be represented, as well as context sensitive analysis, where program state of a procedure under different calling paths need to be represented. Our first idea is by noting the tremendous amount of spacial redundancies within and across the program states, and the use of BDDs to eliminate such redundancies. Our second idea is by noting tremendous amount of computational redundancies during the solutions of different program states, and employ the strategy of superposition to solve them collectively, in a way reminiscent of quantum computing.

Results

We reported the BDD-based method, a wide departure from the traditional approach, first at ICCAD'02. We later showed that invocation graph (due to Emami, Ghiya and Hendren), a necessity for context sensitivity, can be constructed symbolically in polynomial time and space at PLDI'04, which scale the analyzable programs to those with billions of contexts. We have made a step forward towards a scalable solution of context sensitive, flow sensitive analysis at DAC'05. We are working towards a full solution of flow, path, and iteration sensitive analysis.

Publications

[1]      

Jianwen Zhu, ``Towards scalable flow and context-sensitive symbolic pointer analysis,'' in Proceedings of the Design Automation Conference (DAC), Anaheim, California, June 2005.

[2]      

Jianwen Zhu and Silvian Calman, ``Context-sensitive symbolic pointer analysis,'' IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 24, no. 4, Apr. 2005.

[3]      

Silvian Calman, ``Context sensitive symbolic pointer analysis,'' M.S. thesis, Department of Electrical and Computer Engineering, University of Toronto, Toronto, Jan. 2005.

[4]      

Jianwen Zhu and Silvian Calman, ``Symbolic pointer analysis revisited,'' in Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Washington DC, June 2004.

[5]      

Jianwen Zhu, ``Symbolic pointer analysis,'' in Proceedings of the International Conference on Computer Aided Design (ICCAD), San Jose, California, November 2002.

Other Interesting Works in BDD-based Pointer Analysis

[1]      

Marc Berndl, Ondrej Lhoták, Feng Qian, Laurie Hendren, and Navindra Umanee, ``Point-to analysis using BDD,'' in Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, San Diego, June 2003.

[2]      

Ondrej Lhoták and Laurie Hendren, ``Jedd: A BDD-based relational extension of Java,'' in Proceedings of SIGPLAN Conference on Programming Language Design and Implementation, June 2004.

[3]      

John Whaley and Monica Lam, ``Cloning-based context-sensitive pointer alias analysis using binary decision diagrams,'' in Proceedings of SIGPLAN Conference on Programming Language Design and Implementation, June 2004.

Contributors

Toronto Synthesis Group

Silvian Calman	Jianwen Zhu

Web

http://www.eecg.toronto.edu/~jzhu/quanton.html