Hakjoo Oh
Abstract
We present a method for selectively applying context-sensitivity during interprocedural program analysis. Our method applies context-sensitivity only when and where doing so is likely to improve the precision that matters for resolving given queries. The idea is to use a pre-analysis to estimate the impact of context-sensitivity on the main analysis’s precision, and to use this information to find out when and where the main analysis should turn on or off its context-sensitivity. We formalize this approach and prove that the analysis always benefits from the pre-analysis--guided context-sensitivity. We implemented this selective method for an existing industrial-strength interval analyzer for full C. The method reduced the number of (false) alarms by 24.4% while increasing the analysis cost by 27.8% on average.
The use of the selective method is not limited to context-sensitivity. We demonstrate this generality by following the same principle and developing a selective relational analysis and a selective flow-sensitive analysis. Our experiments show that the method cost-effectively improves the precision in the these analyses as well.
- Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 238--252. Google Scholar
Digital Library
- Patrick Cousot and Radhia Cousot. 1992. Abstract interpretation frameworks. Journal of Logic and Computation 2, 4, 511--547.Google ScholarCross Ref
- Alain Deutsch. 1997. On the complexity of escape analysis. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’97). ACM, New York, NY, 358--371. DOI:http://dx.doi.org/10.1145/263699.263750 Google ScholarDigital Library
- Azadeh Farzan and Zachary Kincaid. 2012. Verification of parameterized concurrent programs by modular reasoning about data and control. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 297--308. Google ScholarDigital Library
- Samuel Z. Guyer and Calvin Lin. 2003. Client-driven pointer analysis. In Proceedings of the International Symposium on Static Analysis. 214--236. Google ScholarDigital Library
- Williams L. Harrison III. 1989. The interprocedural analysis and automatic parallelization of scheme programs. LISP and Symbolic Computation 2, 3, 179--396.Google ScholarCross Ref
- Nevin Heintze and Olivier Tardieu. 2001. Demand-driven pointer analysis. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. 24--34. Google ScholarDigital Library
- Yungbum Jung, Jaehwang Kim, Jaeho Shin, and Kwangkeun Yi. 2005. Taming false alarms from a domain-unaware C analyzer by a Bayesian statistical post analysis. In Proceedings of the International Symposium on Static Analysis. 203--217. Google ScholarDigital Library
- George Kastrinis and Yannis Smaragdakis. 2013. Hybrid context-sensitivity for points-to analysis. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. 423--434. Google ScholarDigital Library
- Woosuk Lee, Wonchan Lee, and Kwangkeun Yi. 2012. Sound non-statistical clustering of static analysis alarms. In Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, Vol. 7148. Springer, 299--314. Google ScholarDigital Library
- Percy Liang, Omer Tripp, and Mayur Naik. 2011. Learning minimal abstractions. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 31--42. Google ScholarDigital Library
- Ana Milanova, Atanas Rountev, and Barbara G. Ryder. 2002. Parameterized object sensitivity for points-to and side-effect analyses for Java. In Proceedings of the 2002 ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA’02). 1--11. Google ScholarDigital Library
- A. Miné. 2006. The octagon abstract domain. Higher-Order and Symbolic Computation 19, 1, 31--100. Google ScholarDigital Library
- Mayur Naik, Hongseok Yang, Ghila Castelnuovo, and Mooly Sagiv. 2012. Abstractions from tests. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 373--386. Google ScholarDigital Library
- Hakjoo Oh, Wonchan Lee, Kihong Heo, Hongseok Yang, and Kwangkeun Yi. 2014. Selective context-sensitivity guided by impact pre-analysis. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. 475--484. Google ScholarDigital Library
- Hakjoo Oh, Kihong Heo, Wonchan Lee, Woosuk Lee, and Kwangkeun Yi. 2012. Design and implementation of sparse global analyses for C-like languages. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. 229--238. Google ScholarDigital Library
- Hakjoo Oh, Kihong Heo, Wonchan Lee, Woosuk Lee, and Kwangkeun Yi. 2015. Sparrow. Retrieved November 30, 2015, from http://ropas.snu.ac.kr/sparrow.Google Scholar
- Hakjoo Oh and Kwangkeun Yi. 2010. An algorithmic mitigation of large spurious interprocedural cycles in static analysis. Software: Practice and Experience 40, 8, 585--603. DOI:http://dx.doi.org/10.1002/spe.969 Google ScholarCross Ref
- Hakjoo Oh and Kwangkeun Yi. 2013. Access-based abstract memory localization in static analysis. Science of Computer Programming 78, 9, 1701--1727.Google ScholarCross Ref
- Rohan Padhye and Uday P. Khedker. 2013. Interprocedural data flow analysis in soot using value contexts. In Proceedings of the 2nd ACM SIGPLAN International Workshop on State of the Art in Java Program Analysis (SOAP’13). ACM, New York, NY, 31--36. DOI:http://dx.doi.org/10.1145/2487568.2487569 Google ScholarDigital Library
- John Plevyak and Andrew A. Chien. 1994. Precise concrete type inference for object-oriented languages. In Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications. 324--340. Google ScholarDigital Library
- Thomas Reps, Susan Horwitz, and Mooly Sagiv. 1995. Precise interprocedural dataflow analysis via graph reachability. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 49--61. Google ScholarDigital Library
- Xavier Rival and Laurent Mauborgne. 2007. The trace partitioning abstract domain. ACM Transactions on Programming Languages and Systems 29, 5, 26--51. Google ScholarDigital Library
- Micha Sharir and Amir Pnueli. 1981. Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications. Prentice-Hall, Englewood Cliffs, NJ, 189--234.Google Scholar
- Olin Grigsby Shivers. 1991. Control-Flow Analysis of Higher-Order Languages—or—Taming Lambda. Ph.D. Dissertation. Carnegie Mellon University, Pittsburgh, PA.Google Scholar
- Yannis Smaragdakis, Martin Bravenboer, and Ondrej Lhoták. 2011. Pick your contexts well: Understanding object-sensitivity. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 17--30. Google ScholarDigital Library
- Manu Sridharan and Rastislav Bodík. 2006. Refinement-based context-sensitive points-to analysis for Java. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. 387--400. Google ScholarDigital Library
- Manu Sridharan, Denis Gopan, Lexin Shan, and Rastislav Bodík. 2005. Demand-driven points-to analysis for Java. In Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications. 59--76. Google ScholarDigital Library
- Xin Zhang, Ravi Mangal, Radu Grigore, Mayur Naik, and Hongseok Yang. 2014. On abstraction refinement for program analyses in datalog. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. 239--248. Google ScholarDigital Library
- Xin Zhang, Mayur Naik, and Hongseok Yang. 2013. Finding optimum abstractions in parametric dataflow analysis. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. 365--376. Google ScholarDigital Library
Index Terms
- Selective X-Sensitive Analysis Guided by Impact Pre-Analysis
Recommendations
Selective context-sensitivity guided by impact pre-analysis
PLDI '14: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and ImplementationWe present a method for selectively applying context-sensitivity during interprocedural program analysis. Our method applies context-sensitivity only when and where doing so is likely to improve the precision that matters for resolving given queries. ...
Selective context-sensitivity guided by impact pre-analysis
PLDI '14We present a method for selectively applying context-sensitivity during interprocedural program analysis. Our method applies context-sensitivity only when and where doing so is likely to improve the precision that matters for resolving given queries. ...
A relational approach to interprocedural shape analysis
This article addresses the verification of properties of imperative programs with recursive procedure calls, heap-allocated storage, and destructive updating of pointer-valued fields, that is, interprocedural shape analysis. The article makes three ...
Comments