When to Stop Going Down the Rabbit Hole: Taming Context-Sensitivity on the Fly
Authors: 
Julian Erhard, Johanna Franziska Schinabeck, Michael Schwarz, Helmut SeidlAuthors Info & Claims
Pages 35 - 44
Abstract
Context-sensitive analysis of programs containing recursive procedures may be expensive, in particular, when using expressive domains, rendering the set of possible contexts large or even infinite. Here, we present a general framework for context-sensitivity that allows formalizing not only known approaches such as full context or call strings but also combinations of these. We propose three generic lifters in this framework to bound the number of encountered contexts on the fly. These lifters are implemented within the abstract interpreter Goblint and compared to existing approaches to context-sensitivity on the SV-COMP benchmark suite. On a subset of recursive benchmarks, all proposed lifters manage to reduce the number of stack overflows and timeouts compared to a full context approach, with one of them improving the number of correct verdicts by 31% and showing promising results on the considered SV-COMP categories.
References
[1]
Kalmer Apinis. 2014. Frameworks for analyzing multi-threaded C. Ph. D. Dissertation. Technical University Munich. https://nbn-resolving.org/urn:nbn:de:bvb:91-diss-20140606-1189191-0-9
[2]
Kalmer Apinis, Helmut Seidl, and Vesal Vojdani. 2012. Side-Effecting Constraint Systems: A Swiss Army Knife for Program Analysis. In Programming Languages and Systems - 10th Asian Symposium, APLAS 2012, Kyoto, Japan, December 11-13, 2012. Proceedings, Ranjit Jhala and Atsushi Igarashi (Eds.) (Lecture Notes in Computer Science, Vol. 7705). Springer, 157–172. https://doi.org/10.1007/978-3-642-35182-2_12
[3]
Kalmer Apinis, Helmut Seidl, and Vesal Vojdani. 2013. How to combine widening and narrowing for non-monotonic systems of equations. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’13, Seattle, WA, USA, June 16-19, 2013, Hans-Juergen Boehm and Cormac Flanagan (Eds.). ACM, 377–386. https://doi.org/10.1145/2491956.2462190
[4]
Dirk Beyer. 2016. Reliable and Reproducible Competition Results with BenchExec and Witnesses (Report on SV-COMP 2016). In Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, Marsha Chechik and Jean-François Raskin (Eds.) (Lecture Notes in Computer Science, Vol. 9636). Springer, 887–904. https://doi.org/10.1007/978-3-662-49674-9_55
[5]
Dirk Beyer. 2023. Competition on Software Verification and Witness Validation: SV-COMP 2023. In Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part II, Sriram Sankaranarayanan and Natasha Sharygina (Eds.) (Lecture Notes in Computer Science, Vol. 13994). Springer, 495–522. https://doi.org/10.1007/978-3-031-30820-8_29
[6]
François Bourdoncle. 1992. Abstract Interpretation by Dynamic Partitioning. J. Funct. Program., 2, 4 (1992), 407–423. https://doi.org/10.1017/S0956796800000496
[7]
David Bühler. 2017. Structuring an Abstract Interpreter through Value and State Abstractions: EVA, an Evolved Value Analysis for Frama-C. Ph. D. Dissertation. University of Rennes 1, France. https://tel.archives-ouvertes.fr/tel-01664726
[8]
Patrick Cousot and Radhia Cousot. 1992. Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation. In Programming Language Implementation and Logic Programming, 4th International Symposium, PLILP’92, Leuven, Belgium, August 26-28, 1992, Proceedings, Maurice Bruynooghe and Martin Wirsing (Eds.) (Lecture Notes in Computer Science, Vol. 631). Springer, 269–295. https://doi.org/10.1007/3-540-55844-6_142
[9]
Ben Hardekopf, Ben Wiedermann, Berkeley R. Churchill, and Vineeth Kashyap. 2014. Widening for Control-Flow. In Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings, Kenneth L. McMillan and Xavier Rival (Eds.) (Lecture Notes in Computer Science, Vol. 8318). Springer, 472–491. https://doi.org/10.1007/978-3-642-54013-4_26
[10]
Behnaz Hassanshahi, Raghavendra Kagalavadi Ramesh, Padmanabhan Krishnan, Bernhard Scholz, and Yi Lu. 2017. An efficient tunable selective points-to analysis for large codebases. In Proceedings of the 6th ACM SIGPLAN International Workshop on State of the Art in Program Analysis. 13–18. https://doi.org/10.1145/3088515.3088519
[11]
Mathias Hedenborg, Jonas Lundberg, and Welf Löwe. 2021. Memory efficient context-sensitive program analysis. Journal of Systems and Software, 177 (2021), 110952. https://doi.org/10.1016/J.JSS.2021.110952
[12]
Mathias Hedenborg, Jonas Lundberg, Welf Löwe, and Martin Trapp. 2015. Approximating Context-Sensitive Program Information. In Programmiersprachen und Grundlagen der Programmierung KPS 2015.
[13]
Mathias Hedenborg, Jonas Lundberg, Welf Löwe, and Martin Trapp. 2022. A framework for memory efficient context-sensitive program analysis. Theory of Computing Systems, 66, 5 (2022), 911–956. https://doi.org/10.1007/S00224-022-10093-W
[14]
Kihong Heo, Hakjoo Oh, and Kwangkeun Yi. 2017. Selective conjunction of context-sensitivity and octagon domain toward scalable and precise global static analysis. Software: Practice and Experience, 47, 11 (2017), 1677–1705. https://doi.org/10.1002/SPE.2493
[15]
Swati Jaiswal, Uday P. Khedker, and Alan Mycroft. 2022. A Unified Model for Context-Sensitive Program Analyses: : The Blind Men and the Elephant. ACM Comput. Surv., 54, 6 (2022), 114:1–114:37. https://doi.org/10.1145/3456563
[16]
Minseok Jeon, Myungho Lee, and Hakjoo Oh. 2020. Learning graph-based heuristics for pointer analysis without handcrafting application-specific features. Proceedings of the ACM on Programming Languages, 4, OOPSLA (2020), 1–30. https://doi.org/10.1145/3428247
[17]
Sehun Jeong, Minseok Jeon, Sungdeok Cha, and Hakjoo Oh. 2017. Data-driven context-sensitivity for points-to analysis. Proceedings of the ACM on Programming Languages, 1, OOPSLA (2017), 1–28. https://doi.org/10.1145/3133924
[18]
Jacques-Henri Jourdan. 2016. Verasco: a formally verified C static analyzer. Ph. D. Dissertation. Universite Paris Diderot-Paris VII. https://tel.archives-ouvertes.fr/tel-01327023
[19]
Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie. 2015. A formally-verified C static analyzer. Acm Sigplan Notices, 50, 1 (2015), 247–259. https://doi.org/10.1145/2676726.2676966
[20]
George Kastrinis and Yannis Smaragdakis. 2013. Hybrid context-sensitivity for points-to analysis. ACM SIGPLAN Notices, 48, 6 (2013), 423–434. https://doi.org/10.1145/2491956.2462191
[21]
Uday P Khedker and Bageshri Karkare. 2008. Efficiency, precision, simplicity, and generality in interprocedural data flow analysis: Resurrecting the classical call strings method. In Compiler Construction: 17th International Conference, CC 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings 17. 213–228. https://doi.org/10.1007/978-3-540-78791-4_15
[22]
Sorin Lerner, Todd D. Millstein, Erika Rice, and Craig Chambers. 2005. Automated soundness proofs for dataflow analyses and transformations via local rules. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005, Jens Palsberg and Martín Abadi (Eds.). ACM, 364–377. https://doi.org/10.1145/1040305.1040335
[23]
Ondřej Lhoták and Laurie Hendren. 2006. Context-sensitive points-to analysis: is it worth it? In International Conference on Compiler Construction. 47–64. https://doi.org/10.1007/11688839_5
[24]
Yue Li, Tian Tan, Anders Møller, and Yannis Smaragdakis. 2018. Precision-guided context sensitivity for pointer analysis. Proceedings of the ACM on Programming Languages, 2, OOPSLA (2018), 1–29. https://doi.org/10.1145/3276511
[25]
Yue Li, Tian Tan, Anders Møller, and Yannis Smaragdakis. 2018. Scalability-first pointer analysis with self-tuning context-sensitivity. In Proceedings of the 2018 26th ACM joint meeting on european software engineering conference and symposium on the foundations of software engineering. 129–140. https://doi.org/10.1145/3236024.3236041
[26]
Yue Li, Tian Tan, Anders Møller, and Yannis Smaragdakis. 2020. A principled approach to selective context sensitivity for pointer analysis. ACM Transactions on Programming Languages and Systems (TOPLAS), 42, 2 (2020), 1–40. https://doi.org/10.1145/3381915
[27]
Jingbo Lu, Dongjie He, and Jingling Xue. 2021. Eagle: CFL-reachability-based precision-preserving acceleration of object-sensitive pointer analysis with partial context sensitivity. ACM Transactions on Software Engineering and Methodology (TOSEM), 30, 4 (2021), 1–46. https://doi.org/10.1145/3450492
[28]
Wenjie Ma, Shengyuan Yang, Tian Tan, Xiaoxing Ma, Chang Xu, and Yue Li. 2023. Context Sensitivity without Contexts: A Cut-Shortcut Approach to Fast and Precise Pointer Analysis. Proceedings of the ACM on Programming Languages, 7, PLDI (2023), 539–564. https://doi.org/10.1145/3591242
[29]
Ravi Mangal, Mayur Naik, and Hongseok Yang. 2014. A correspondence between two approaches to interprocedural analysis in the presence of join. In European Symposium on Programming Languages and Systems. 513–533. https://doi.org/10.1007/978-3-642-54833-8_27
[30]
Florian Martin. 1999. Experimental comparison of call string and functional approaches to interprocedural analysis. In International Conference on Compiler Construction. 63–75. https://doi.org/10.1007/978-3-540-49051-7_5
[31]
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. 1–11. https://doi.org/10.1145/566172.566174
[32]
Ana Milanova, Atanas Rountev, and Barbara G Ryder. 2005. Parameterized object sensitivity for points-to analysis for Java. ACM Transactions on Software Engineering and Methodology (TOSEM), 14, 1 (2005), 1–41. https://doi.org/10.1145/1044834.1044835
[33]
Ana L. Milanova, Atanas Rountev, and Barbara G. Ryder. 2005. Parameterized object sensitivity for points-to analysis for Java. ACM Trans. Softw. Eng. Methodol., 14, 1 (2005), 1–41. https://doi.org/10.1145/1044834.1044835
[34]
Benoît Montagu and Thomas P. Jensen. 2021. Trace-based control-flow analysis. In PLDI ’21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021, Stephen N. Freund and Eran Yahav (Eds.). ACM, 482–496. https://doi.org/10.1145/3453483.3454057
[35]
Hakjoo Oh, Wonchan Lee, Kihong Heo, Hongseok Yang, and Kwangkeun Yi. 2014. Selective context-sensitivity guided by impact pre-analysis. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation. 475–484. https://doi.org/10.1145/2594291.2594318
[36]
Hakjoo Oh, Wonchan Lee, Kihong Heo, Hongseok Yang, and Kwangkeun Yi. 2015. Selective x-sensitive analysis guided by impact pre-analysis. ACM Transactions on Programming Languages and Systems (TOPLAS), 38, 2 (2015), 1–45. https://doi.org/10.1145/2821504
[37]
Hakjoo Oh, Hongseok Yang, and Kwangkeun Yi. 2015. Learning a strategy for adapting a program analysis via bayesian optimisation. In Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2015). Association for Computing Machinery, New York, NY, USA. 572–588. isbn:9781450336895 https://doi.org/10.1145/2814270.2814309
[38]
Jihyeok Park, Hongki Lee, and Sukyoung Ryu. 2021. A survey of parametric static analysis. ACM Computing Surveys (CSUR), 54, 7 (2021), 1–37. https://doi.org/10.1145/3464457
[39]
Thomas Reps, Susan Horwitz, and Mooly Sagiv. 1995. Precise interprocedural dataflow analysis via graph reachability. In Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 49–61. https://doi.org/10.1145/199448.199462
[40]
Noam Rinetzky and Shmuel Sagiv. 2001. Interprocedural Shape Analysis for Recursive Programs. In Compiler Construction, 10th International Conference, CC 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings, Reinhard Wilhelm (Ed.) (Lecture Notes in Computer Science, Vol. 2027). Springer, 133–149. https://doi.org/10.1007/3-540-45306-7_10
[41]
Xavier Rival and Bor-Yuh Evan Chang. 2011. Calling context abstraction with shapes. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, Thomas Ball and Mooly Sagiv (Eds.). ACM, 173–186. https://doi.org/10.1145/1926385.1926406
[42]
Michael Schwarz, Julian Erhard, Vesal Vojdani, Simmo Saan, and Helmut Seidl. 2023. When Long Jumps Fall Short: Control-Flow Tracking and Misuse Detection for Non-local Jumps in C. In Proceedings of the 12th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis, SOAP 2023, Orlando, FL, USA, 17 June 2023, Pietro Ferrara and Liana Hadarean (Eds.). ACM, 20–26. https://doi.org/10.1145/3589250.3596140
[43]
Michael Schwarz, Simmo Saan, Helmut Seidl, Kalmer Apinis, Julian Erhard, and Vesal Vojdani. 2021. Improving Thread-Modular Abstract Interpretation. In Static Analysis - 28th International Symposium, SAS 2021, Chicago, IL, USA, October 17-19, 2021, Proceedings, Cezara Dragoi, Suvam Mukherjee, and Kedar S. Namjoshi (Eds.) (Lecture Notes in Computer Science, Vol. 12913). Springer, 359–383. https://doi.org/10.1007/978-3-030-88806-0_18
[44]
Michael Schwarz, Simmo Saan, Helmut Seidl, Julian Erhard, and Vesal Vojdani. 2023. Clustered relational thread-modular abstract interpretation with local traces. In European Symposium on Programming. 28–58. https://doi.org/10.1007/978-3-031-30044-8_2
[45]
Helmut Seidl and Ralf Vogler. 2021. Three improvements to the top-down solver. Math. Struct. Comput. Sci., 31, 9 (2021), 1090–1134. https://doi.org/10.1017/S0960129521000499
[46]
Micha Sharir and Amir Pnueli. 1978. Two approaches to interprocedural data flow analysis. New York University. Courant Institute of Mathematical Sciences.
[47]
Olin Grigsby Shivers. 1991. Control-flow analysis of higher-order languages or taming lambda. Ph. D. Dissertation. Carnegie Mellon University.
[48]
Yannis Smaragdakis, Martin Bravenboer, and Ondrej Lhoták. 2011. Pick your contexts well: understanding object-sensitivity. In Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 17–30. https://doi.org/10.1145/1926385.1926390
[49]
Yannis Smaragdakis, George Kastrinis, and George Balatsouras. 2014. Introspective analysis: context-sensitivity, across the board. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation. 485–495. https://doi.org/10.1145/2594291.2594320
[50]
Tian Tan, Yue Li, Xiaoxing Ma, Chang Xu, and Yannis Smaragdakis. 2021. Making pointer analysis more precise by unleashing the power of selective context sensitivity. Proceedings of the ACM on Programming Languages, 5, OOPSLA (2021), 1–27. https://doi.org/10.1145/3485524
[51]
Tian Tan, Yue Li, Xiaoxing Ma, Chang Xu, and Yannis Smaragdakis. 2021. Making pointer analysis more precise by unleashing the power of selective context sensitivity. Proc. ACM Program. Lang., 5, OOPSLA (2021), Article 147, oct, 27 pages. https://doi.org/10.1145/3485524
[52]
Tian Tan, Yue Li, and Jingling Xue. 2016. Making k-object-sensitive pointer analysis more precise with still k-limiting. In International Static Analysis Symposium. 489–510. https://doi.org/10.1007/978-3-662-53413-7_24
[53]
Tian Tan, Yue Li, and Jingling Xue. 2017. Efficient and precise points-to analysis: modeling the heap by merging equivalent automata. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. 278–291. https://doi.org/10.1145/3062341.3062360
[54]
Manas Thakur and V. Krishna Nandivada. 2020. Mix your contexts well: opportunities unleashed by recent advances in scaling context-sensitivity. In Proceedings of the 29th International Conference on Compiler Construction (CC 2020). Association for Computing Machinery, New York, NY, USA. 27–38. isbn:9781450371209 https://doi.org/10.1145/3377555.3377902
[55]
Vesal Vojdani, Kalmer Apinis, Vootele Rõtov, Helmut Seidl, Varmo Vene, and Ralf Vogler. 2016. Static race detection for device drivers: the Goblint approach. In Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, ASE 2016, Singapore, September 3-7, 2016, David Lo, Sven Apel, and Sarfraz Khurshid (Eds.). ACM, 391–402. https://doi.org/10.1145/2970276.2970337
[56]
Shiyi Wei and Barbara G Ryder. 2015. Adaptive context-sensitive analysis for JavaScript. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). https://doi.org/10.4230/LIPICS.ECOOP.2015.712
[57]
John Whaley and Monica S. Lam. 2004. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation 2004, Washington, DC, USA, June 9-11, 2004, William W. Pugh and Craig Chambers (Eds.). ACM, 131–144. https://doi.org/10.1145/996841.996859
Index Terms
- When to Stop Going Down the Rabbit Hole: Taming Context-Sensitivity on the Fly
Recommendations
Context transformations for pointer analysis
PLDI 2017: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and ImplementationPoints-to analysis for Java benefits greatly from context sensitivity. CFL-reachability and k-limited context strings are two approaches to obtaining context sensitivity with different advantages: CFL-reachability allows local reasoning about data-value ...
Context transformations for pointer analysis
PLDI '17Points-to analysis for Java benefits greatly from context sensitivity. CFL-reachability and k-limited context strings are two approaches to obtaining context sensitivity with different advantages: CFL-reachability allows local reasoning about data-value ...
Tracking pointers with path and context sensitivity for bug detection in C programs
This paper proposes a pointer alias analysis for automatic error detection. State-of-the-art pointer alias analyses are either too slow or too imprecise for finding errors in real-life programs. We propose a hybrid pointer analysis that tracks actively ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
June 2024
66 pages
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 20 June 2024
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
- DFG
Conference
SOAP '24
Sponsor:
SOAP '24: 13th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis
June 25, 2024
Copenhagen, Denmark
Acceptance Rates
Overall Acceptance Rate 11 of 11 submissions, 100%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 200Total Downloads
- Downloads (Last 12 months)200
- Downloads (Last 6 weeks)38
Reflects downloads up to 23 Nov 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in