McGill UniversitySchool of Computer ScienceSable Research GroupPoints-to Analysis using BDDsSable Technical Report No. 2002-10Marc Berndl, Ondˇrej Lhot´ak, Feng Qian, Laurie Hendren and Navindra UmaneeNovember 18, 2002w w w . s a b l e . m c g i l l . c aContents1 Introduction 32 BDD Background 43 Points-to Algorithm with BDDs 63.1 BDD Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 Performance Tuning 84.1 Experimental Setup . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84.2 Variable Ordering . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94.3 Incrementalization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115 Full Experimental Results 135.1 Performance of BDDs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 135.2 Notes on Measuring Memory Usage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 136 Applications 147 Related Work 158 Conclusions and Future Work 16A BuDDy Code to implement the BDD-based Points-to Solver 191List of Figures1 Example code fragment. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 BDDs for points-to relation {(a,A),(a,B),(b,A),(b,B),(c,A),(c,B),(c,C)} (a) unreduced using or-deringV1V0H1H0, (b) reducedusing orderingV1V0H1H0, (c) reducedusing alternative orderingH0V0H1V153 (a) BDD for initial points-to set {(a, A), (b, B), (c,C)} (b) BDD for edge set {(a → b), (b → a),(b →c)} (c) result of relprod((a),(b),V1)(the points-to set {(a,B),(b,A),(c,B)}) (d) result of replace((c),V2ToV1)(e) result of (a)∪(d) (the points-to set {(a,A),(a,B),(b,A),(b,B),(c,B),(c,C)} . . . . . . . . . . . . 54 The four types of pointer statements (constraints). . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 Inference rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66 The basic BDD algorithm for points-to analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 Effect of domain arrangement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108 Effect of interleaving domains . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 119 Incremental modification to rule (1) of algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12List of TablesI Effect of variable ordering on performance (N/C means the solver does not complete the run in 4 hours.) 10II Analysis time improvement due to incrementalization . . . . . . . . . . . . . . . . . . . . . . . . . . 12III Performance and live data of BDD solver. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 142AbstractThis paper reports on a new approach to solving a subset-based points-to analysis for Java using Binary DecisionDiagrams (BDDs). In the model checking community, BDDs have been shown very effective for representing largesets and solving very large verification problems. Our work shows that BDDs can also be very effective for developinga points-to analysis that is simple to implement and that scales well, in both space and time, to large programs.The paper first introduces BDDs and operations on BDDs using some simple points-to examples. Then, a com-plete subset-based points-to algorithm is presented, expressed completely using BDDs and BDD operations. Thisalgorithm is then refined by finding appropriate variable orderings and by making the algorithm incremental, in orderto arrive at a very efficient algorithm. Experimental results are given to justify the choice of variable ordering, todemonstrate the improvement due to incrementalization, and to compare the performance of the BDD-based solverto an efficient hand-coded graph-based solver. Finally, based on the results of the BDD-based solver, a variety ofBDD-based queries are presented, including the points-to query.1 IntroductionIn this paper, we take a well-known problem from the compiler optimization community, points-to analysis, and weshow how to solve this problem efficiently using reduced ordered binary decision diagrams (ROBDDs)1which havebeen shown to be very effective in the model checking community.Whole program analyses, such as points-to analysis, require approaches that can scale well to large programs. Twopopular approaches to flow-insensitive points-to analysis have been pursued in the past, equality-based approacheslike those pioneered by Steensgaard [29], and subset-based approaches like the analysis first suggested by Andersen[4]. The subset-based approaches give more accurate results, but they also lead to greater challenges for efficientimplementations [8,11,13,18,24,27,31].2For this paper, we have chosen to implement a subset-based points-to analysis for Java. At a very high level,one can see this problem as finding the allocation sites that reach a variable in the program. Consider an allocationstatement S : a = new A();. If a variable x is used in some other part of the program, then one would like toknow whether x can refer to (point-to) an object allocated at S. A key problem in developing efficient solvers forthe subset-based points-to analysis is that for large programs there are many points-to sets, and each points-to set canbecome very large. This problem has been attacked previously by collapsing equivalent variables [11,23] or designingnew representations for sets [12,17].Since BDDs …
View Full Document