research-article

Anchor: Fast and Precise Value-flow Analysis for Containers via Memory Orientation

Authors:

Chengpeng Wang,

Charles ZhangAuthors Info & Claims

ACM Transactions on Software Engineering and Methodology, Volume 32, Issue 3

Article No.: 66, Pages 1 - 39

https://doi.org/10.1145/3565800

Published: 26 April 2023 Publication History

Abstract

Containers are ubiquitous data structures that support a variety of manipulations on the elements, inducing the indirect value flows in the program. Tracking value flows through containers is stunningly difficult, because it depends on container memory layouts, which are expensive to be discovered.

This work presents a fast and precise value-flow analysis framework called Anchor for the programs using containers. We introduce the notion of anchored containers and propose the memory orientation analysis to construct a precise value-flow graph. Specifically, we establish a combined domain to identify anchored containers and apply strong updates to container memory layouts. Anchor finally conducts a demand-driven reachability analysis in the value-flow graph for a client. Experiments show that it removes 17.1% spurious statements from thin slices and discovers 20 null pointer exceptions with 9.1% as its false-positive ratio, while the smashing-based analysis reports 66.7% false positives. Anchor scales to millions of lines of code and checks the program with around 5.12 MLoC within 5 hours.

References

[1]

Microsoft. 2022. Containers-C++ Reference. Retrieved September 7, 2022 from https://www.cplusplus.com/reference/stl/.

[2]

Oracle. 2022. Collections Framework Overview. Retrieved from September 7, 2022 from https://docs.oracle.com/javase/8/docs/technotes/guides/collections/overview.html.

[3]

JavaEE. 2022. Java EE 8 Specification APIs. Retrieved September 7, 2022 from https://javaee.github.io/javaee-spec/javadocs/.

[4]

Manu Sridharan, Stephen J. Fink, and Rastislav Bodík. 2007. Thin slicing. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, Jeanne Ferrante and Kathryn S. McKinley (Eds.). ACM, 112–122. DOI:

Digital Library

[5]

Susan Horwitz, Thomas W. Reps, and David W. Binkley. 1990. Interprocedural slicing using dependence graphs. ACM Trans. Program. Lang. Syst. 12, 1 (1990), 26–60. DOI:

Digital Library

[6]

Roman Manevich, Manu Sridharan, Stephen Adams, Manuvir Das, and Zhe Yang. 2004. PSE: Explaining program failures via postmortem static analysis. In Proceedings of the 12th ACM SIGSOFT International Symposium on Foundations of Software Engineering, Richard N. Taylor and Matthew B. Dwyer (Eds.). ACM, 63–72. DOI:

Digital Library

[7]

V. Benjamin Livshits and Monica S. Lam. 2005. Finding security vulnerabilities in Java applications with static analysis. In Proceedings of the 14th USENIX Security Symposium, Patrick D. McDaniel (Ed.). USENIX Association.

Digital Library

[8]

Omer Tripp, Marco Pistoia, Stephen J. Fink, Manu Sridharan, and Omri Weisman. 2009. TAJ: Effective taint analysis of web applications. In Proceedings of the SIGPLAN Conference on Programming Language Design and Implementation (PLDI’09), Michael Hind and Amer Diwan (Eds.). ACM, 87–97. DOI:

Digital Library

[9]

Sam Blackshear, Bor-Yuh Evan Chang, and Manu Sridharan. 2013. Thresher: Precise refutations for heap reachability. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’13), Hans-Juergen Boehm and Cormac Flanagan (Eds.). ACM, 275–286. DOI:

Digital Library

[10]

Zhiqiang Zuo, John Thorpe, Yifei Wang, Qiuhong Pan, Shenming Lu, Kai Wang, Guoqing Harry Xu, Linzhang Wang, and Xuandong Li. 2019. Grapple: A graph system for static finite-state property checking of large-scale systems code. In Proceedings of the 14th EuroSys Conference, George Candea, Robbert van Renesse, and Christof Fetzer (Eds.). ACM, 38:1–38:17. DOI:

Digital Library

[11]

Zhiqiang Zuo, Yiyu Zhang, Qiuhong Pan, Shenming Lu, Yue Li, Linzhang Wang, Xuandong Li, and Guoqing Harry Xu. 2021. Chianina: An evolving graph system for flow- and context-sensitive analyses of million lines of C code. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI’21), Stephen N. Freund and Eran Yahav (Eds.). ACM, 914–929. DOI:

Digital Library

[12]

Mark Marron, Cesar Sanchez, and Zhendong Su. 2010. High-level heap abstractions for debugging programs.

[13]

Hiralal Agrawal. 1991. Towards Automatic Debugging of Computer Programs. Ph.D. Dissertation. Purdue University.

[14]

Bor-Yuh Evan Chang, Cezara Dragoi, Roman Manevich, Noam Rinetzky, and Xavier Rival. 2020. Shape analysis. Found. Trends Program. Lang. 6, 1–2 (2020), 1–158. DOI:

[15]

Yu Feng, Xinyu Wang, Isil Dillig, and Thomas Dillig. 2015. Bottom-up context-sensitive pointer analysis for Java. In Proceedings of the 13th Asian Symposium on Programming Languages and Systems (APLAS’15),Lecture Notes in Computer Science, Xinyu Feng and Sungwoo Park (Eds.), Vol. 9458. Springer, 465–484. DOI:

[16]

Minseok Jeon, Sehun Jeong, and Hakjoo Oh. 2018. Precise and scalable points-to analysis via data-driven context tunneling. Proc. ACM Program. Lang. 2 (2018), 140:1–140:29. DOI:

Digital Library

[17]

Yue Li, Tian Tan, Anders Møller, and Yannis Smaragdakis. 2020. A principled approach to selective context sensitivity for pointer analysis. ACM Trans. Program. Lang. Syst. 42, 2 (2020), 10:1–10:40. DOI:

Digital Library

[18]

Bertrand Jeannet and Antoine Miné. 2009. Apron: A library of numerical abstract domains for static analysis. In Proceedings of the 21st International Conference on Computer Aided Verification (CAV’09),Lecture Notes in Computer Science, Ahmed Bouajjani and Oded Maler (Eds.), Vol. 5643. Springer, 661–667. DOI:

Digital Library

[19]

Bill McCloskey, Thomas W. Reps, and Mooly Sagiv. 2010. Statically inferring complex heap, array, and numeric invariants. In Proceedings of the 17th International Symposium, on Static Analysis (SAS’10),Lecture Notes in Computer Science, Radhia Cousot and Matthieu Martel (Eds.), Vol. 6337. Springer, 71–99. DOI:

[20]

Jiangchao Liu and Xavier Rival. 2015. Abstraction of optional numerical values. In Proceedings of the 13th Asian Symposium on Programming Languages and Systems (APLAS’15),Lecture Notes in Computer Science, Xinyu Feng and Sungwoo Park (Eds.), Vol. 9458. Springer, 146–166. DOI:

[21]

Aske Simon Christensen, Anders Møller, and Michael I. Schwartzbach. 2003. Precise analysis of string expressions. In Proceedings of the 10th International Symposium on Static Analysis (SAS’03),Lecture Notes in Computer Science, Radhia Cousot (Ed.), Vol. 2694. Springer, 1–18. DOI:

[22]

Adam Kiezun, Vijay Ganesh, Shay Artzi, Philip J. Guo, Pieter Hooimeijer, and Michael D. Ernst. 2012. HAMPI: A solver for word equations over strings, regular expressions, and context-free grammars. ACM Trans. Softw. Eng. Methodol. 21, 4 (2012), 25:1–25:28. DOI:

Digital Library

[23]

Pieter Hooimeijer and Margus Veanes. 2011. An evaluation of automata algorithms for string analysis. In Proceedings of the 12th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’11),Lecture Notes in Computer Science, Ranjit Jhala and David A. Schmidt (Eds.), Vol. 6538. Springer, 248–262. DOI:

[24]

Xiaofei Xie, Yang Liu, Wei Le, Xiaohong Li, and Hongxu Chen. 2015. S-looper: Automatic summarization for multipath string loops. In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA’15), Michal Young and Tao Xie (Eds.). ACM, 188–198. DOI:

Digital Library

[25]

Arlen Cox, Bor-Yuh Evan Chang, and Xavier Rival. 2014. Automatic analysis of open objects in dynamic language programs. In Proceedings of the 21st International Symposium on Static Analysis (SAS’14),Lecture Notes in Computer Science, Markus Müller-Olm and Helmut Seidl (Eds.), Vol. 8723. Springer, 134–150. DOI:

[26]

Arlen Cox, Bor-Yuh Evan Chang, and Xavier Rival. 2015. Desynchronized multi-state abstractions for open programs in dynamic languages. In Proceedings of the 24th European Symposium on Programming (ESOP’15), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS’15),Lecture Notes in Computer Science, Jan Vitek (Ed.), Vol. 9032. Springer, 483–509. DOI:

Digital Library

[27]

Henry Gordon Rice. 1953. Classes of recursively enumerable sets and their decision problems. Trans. Am. Math. Soc. 74, 2 (1953), 358–366.

[28]

David L. Heine and Monica S. Lam. 2006. Static detection of leaks in polymorphic containers. In Proceedings of the 28th International Conference on Software Engineering (ICSE’06), Leon J. Osterweil, H. Dieter Rombach, and Mary Lou Soffa (Eds.). ACM, 252–261. DOI:

Digital Library

[29]

Steven Arzt, Siegfried Rasthofer, Christian Fritz, Eric Bodden, Alexandre Bartel, Jacques Klein, Yves Le Traon, Damien Octeau, and Patrick D. McDaniel. 2014. FlowDroid: Precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for Android apps. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’14), Michael F. P. O’Boyle and Keshav Pingali (Eds.). ACM, 259–269. DOI:

Digital Library

[30]

Johannes Späth, Karim Ali, and Eric Bodden. 2017. IDE^al: Efficient and precise alias-aware dataflow analysis. Proc. ACM Program. Lang. 1 (2017), 99:1–99:27. DOI:

Digital Library

[31]

Pratik Fegade and Christian Wimmer. 2020. Scalable pointer analysis of data structures using semantic models. In Proceedings of the 29th International Conference on Compiler Construction (CC’20), Louis-Noël Pouchet and Alexandra Jimborean (Eds.). ACM, 39–50. DOI:

Digital Library

[32]

Anastasios Antoniadis, Nikos Filippakis, Paddy Krishnan, Raghavendra Ramesh, Nicholas Allen, and Yannis Smaragdakis. 2020. Static analysis of Java enterprise applications: Frameworks and caches, the elephants in the room. In Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI’20), Alastair F. Donaldson and Emina Torlak (Eds.). ACM, 794–807. DOI:

Digital Library

[33]

Jie Wang, Yunguang Wu, Gang Zhou, Yiming Yu, Zhenyu Guo, and Yingfei Xiong. 2020. Scaling static taint analysis to industrial SOA applications: A case study at Alibaba. In Proceedings of the 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE’20), Prem Devanbu, Myra B. Cohen, and Thomas Zimmermann (Eds.). ACM, 1477–1486. DOI:

Digital Library

[34]

Isil Dillig, Thomas Dillig, and Alex Aiken. 2010. Fluid updates: Beyond strong vs. weak updates. In Proceedings of the 19th European Symposium on Programming (ESOP’10), Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS’10),Lecture Notes in Computer Science, Andrew D. Gordon (Ed.), Vol. 6012. Springer, 246–266. DOI:

Digital Library

[35]

Isil Dillig, Thomas Dillig, and Alex Aiken. 2011. Precise reasoning for programs using containers. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’11), Thomas Ball and Mooly Sagiv (Eds.). ACM, 187–200. DOI:

Digital Library

[36]

Huisong Li, Francois Berenger, Bor-Yuh Evan Chang, and Xavier Rival. 2017. Semantic-directed clumping of disjunctive abstract states. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL’17), Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 32–45. DOI:

Digital Library

[37]

Isil Dillig, Thomas Dillig, and Alex Aiken. 2009. Cuts from proofs: A complete and practical technique for solving linear inequalities over integers. In Proceedings of the 21st International Conference on Computer Aided Verification (CAV’09),Lecture Notes in Computer Science, Ahmed Bouajjani and Oded Maler (Eds.), Vol. 5643. Springer, 233–247. DOI:

Digital Library

[38]

Patrick Cousot and Radhia Cousot. 1979. Systematic design of program analysis frameworks. In Conference Record of the 6th Annual ACM Symposium on Principles of Programming Languages, Alfred V. Aho, Stephen N. Zilles, and Barry K. Rosen (Eds.). ACM Press, 269–282. DOI:

Digital Library

[39]

Donglin Liang and Mary Jean Harrold. 2001. Efficient computation of parameterized pointer information for interprocedural analyses. In Proceedings of the 8th International Symposium on Static Analysis (SAS’01),Lecture Notes in Computer Science, Patrick Cousot (Ed.), Vol. 2126. Springer, 279–298. DOI:

[40]

Yulei Sui, Sen Ye, Jingling Xue, and Jie Zhang. 2014. Making context-sensitive inclusion-based pointer analysis practical for compilers using parameterised summarisation. Softw. Pract. Exp. 44, 12 (2014), 1485–1510. DOI:

Digital Library

[41]

Qingkai Shi, Xiao Xiao, Rongxin Wu, Jinguo Zhou, Gang Fan, and Charles Zhang. 2018. Pinpoint: Fast and precise sparse value flow analysis for million lines of code. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’18), Jeffrey S. Foster and Dan Grossman (Eds.). ACM, 693–706. DOI:

Digital Library

[42]

Qingkai Shi, Rongxin Wu, Gang Fan, and Charles Zhang. 2020. Conquering the extensional scalability problem for value-flow analysis frameworks. In Proceedings of the 42nd International Conference on Software Engineering (ICSE’20), Gregg Rothermel and Doo-Hwan Bae (Eds.). ACM, 812–823. DOI:

Digital Library

[43]

OWASP. 2022. Open Web Application Security Project. Retrieved September 7, 2022 from http://www.owasp.org/.

[44]

Anchor. 2022. Bug reports of Anchor. Retrieved September 7, 2022 from https://containeranalyzer.github.io/.

[45]

Yulei Sui and Jingling Xue. 2016. SVF: Interprocedural static value-flow analysis in LLVM. In Proceedings of the 25th International Conference on Compiler Construction (CC’16), Ayal Zaks and Manuel V. Hermenegildo (Eds.). ACM, 265–266. DOI:

Digital Library

[46]

Ron Cytron, Jeanne Ferrante, Barry K. Rosen, Mark N. Wegman, and F. Kenneth Zadeck. 1991. Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13, 4 (1991), 451–490. DOI:

Digital Library

[47]

Timotej Kapus, Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, and Cristian Cadar. 2019. Computing summaries of string loops in C for better testing and refactoring. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’19), Kathryn S. McKinley and Kathleen Fisher (Eds.). ACM, 874–888. DOI:

Digital Library

[48]

Qingkai Shi, Peisen Yao, Rongxin Wu, and Charles Zhang. 2021. Path-sensitive sparse analysis without path conditions. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI’21), Stephen N. Freund and Eran Yahav (Eds.). ACM, 930–943. DOI:

Digital Library

[49]

Yulei Sui and Jingling Xue. 2016. SVF: Interprocedural static value-flow analysis in LLVM. In Proceedings of the 25th International Conference on Compiler Construction (CC’16), Ayal Zaks and Manuel V. Hermenegildo (Eds.). ACM, 265–266. DOI:

Digital Library

[50]

Vini Kanvar and Uday P. Khedker. 2016. Heap abstractions for static analysis. ACM Comput. Surv. 49, 2 (2016), 29:1–29:47. DOI:

Digital Library

[51]

Sumit Gulwani, Tal Lev-Ami, and Mooly Sagiv. 2009. A combination framework for tracking partition sizes. In Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’09), Zhong Shao and Benjamin C. Pierce (Eds.). ACM, 239–251. DOI:

Digital Library

[52]

Sumit Gulwani and Ashish Tiwari. 2006. Combining abstract interpreters. ACM SIGPLAN Not. 41, 6 (2006), 376–386.

Digital Library

[53]

Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the 4th ACM Symposium on Principles of Programming Languages, Robert M. Graham, Michael A. Harrison, and Ravi Sethi (Eds.). ACM, 238–252. DOI:

Digital Library

[54]

Peisen Yao, Jinguo Zhou, Xiao Xiao, Qingkai Shi, Rongxin Wu, and Charles Zhang. 2021. Efficient path-sensitive data-dependence analysis. arXiv:2109.07923. Retrieved from https://arxiv.org/abs/2109.07923.

[55]

Thomas W. Reps. 1997. Program analysis via graph reachability. In Proceedings of the International Symposium on Logic Programming, Jan Maluszynski (Ed.). MIT Press, 5–19.

[56]

Shmuel Sagiv, Thomas W. Reps, and Susan Horwitz. 1996. Precise interprocedural dataflow analysis with applications to constant propagation. Theor. Comput. Sci. 167, 1&2 (1996), 131–170. DOI:

Digital Library

[57]

Stephen J. Fink, Eran Yahav, Nurit Dor, G. Ramalingam, and Emmanuel Geay. 2006. Effective typestate verification in the presence of aliasing. In Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis (ISSTA’06), Lori L. Pollock and Mauro Pezzè (Eds.). ACM, 133–144. DOI:

Digital Library

[58]

Sigmund Cherem, Lonnie Princehouse, and Radu Rugina. 2007. Practical memory leak detection using guarded value-flow analysis. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, Jeanne Ferrante and Kathryn S. McKinley (Eds.). ACM, 480–491. DOI:

Digital Library

[59]

Gang Fan, Rongxin Wu, Qingkai Shi, Xiao Xiao, Jinguo Zhou, and Charles Zhang. 2019. Smoke: Scalable path-sensitive memory leak detection for millions of lines of code. In Proceedings of the 41st International Conference on Software Engineering (ICSE’19), Joanne M. Atlee, Tevfik Bultan, and Jon Whittle (Eds.). IEEE/ACM, 72–82. DOI:

Digital Library

[60]

Yu Feng, Saswat Anand, Isil Dillig, and Alex Aiken. 2014. Apposcopy: Semantics-based detection of Android malware through static analysis. In Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE’22), Shing-Chi Cheung, Alessandro Orso, and Margaret-Anne D. Storey (Eds.). ACM, 576–587. DOI:

Digital Library

[61]

Ondrej Lhoták and Laurie J. Hendren. 2008. Evaluating the benefits of context-sensitive points-to analysis using a BDD-based implementation. ACM Trans. Softw. Eng. Methodol. 18, 1 (2008), 3:1–3:53. DOI:

Digital Library

[62]

Yannis Smaragdakis, George Kastrinis, and George Balatsouras. 2014. Introspective analysis: Context-sensitivity, across the board. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’14), Michael F. P. O’Boyle and Keshav Pingali (Eds.). ACM, 485–495. DOI:

Digital Library

[63]

Leonardo Mendonça de Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’08), Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS’08),Lecture Notes in Computer Science, C. R. Ramakrishnan and Jakob Rehof (Eds.), Vol. 4963. Springer, 337–340. DOI:

[64]

Ohad Shacham, Martin T. Vechev, and Eran Yahav. 2009. Chameleon: Adaptive selection of collections. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’09), Michael Hind and Amer Diwan (Eds.). ACM, 408–418. DOI:

Digital Library

[65]

Rong Gu, Zhiqiang Zuo, Xi Jiang, Han Yin, Zhaokang Wang, Linzhang Wang, Xuandong Li, and Yihua Huang. 2021. Towards efficient large-scale interprocedural program static analysis on distributed data-parallel computation. IEEE Trans. Parallel Distrib. Syst. 32, 4 (2021), 867–883. DOI:

Digital Library

[66]

Chengpeng Wang, Peisen Yao, Wensheng Tang, Qingkai Shi, and Charles Zhang. 2022. Complexity-guided container replacement synthesis. Proc. ACM Program. Lang. 6 (2022), 1–31. DOI:

Digital Library

[67]

Yichen Xie and Alexander Aiken. 2005. Scalable error detection using boolean satisfiability. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’05), Jens Palsberg and Martín Abadi (Eds.). ACM, 351–363. DOI:

Digital Library

[68]

Yue Li, Tian Tan, Yifei Zhang, and Jingling Xue. 2016. Program tailoring: Slicing by sequential criteria. In Proceedings of the 30th European Conference on Object-Oriented Programming (ECOOP’16),LIPIcs, Shriram Krishnamurthi and Benjamin S. Lerner (Eds.), Vol. 56. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 15:1–15:27. DOI:

[69]

Facebook. 2022. Infer Static Analyzer. Retrieved September 7, 2022 from https://fbinfer.com/.

[70]

Dino Distefano, Manuel Fähndrich, Francesco Logozzo, and Peter W. O’Hearn. 2019. Scaling static analyses at Facebook. Commun. ACM 62, 8 (2019), 62–70. DOI:

Digital Library

[71]

David A. Tomassi and Cindy Rubio-González. 2021. On the real-world effectiveness of static bug detectors at finding null pointer exceptions. In Proceedings of the 36th IEEE/ACM International Conference on Automated Software Engineering (ASE’21). IEEE, 292–303. DOI:

Digital Library

[72]

David Mitchel Perry, Andrea Mattavelli, Xiangyu Zhang, and Cristian Cadar. 2017. Accelerating array constraints in symbolic execution. In Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, Tevfik Bultan and Koushik Sen (Eds.). ACM, 68–78. DOI:

Digital Library

[73]

Jan Eberhardt, Samuel Steffen, Veselin Raychev, and Martin T. Vechev. 2019. Unsupervised learning of API aliasing specifications. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’19), Kathryn S. McKinley and Kathleen Fisher (Eds.). ACM, 745–759. DOI:

Digital Library

[74]

Apache Commons. 2022. Commons Collections. Retrieved September 7, 2022 from https://commons.apache.org/proper/commons-collections/.

[75]

Trove. 2022. High Speed Object and Primitive Collections for Java. Retrieved September 7, 2022 from http://trove.starlight-systems.com/.

[76]

Guava. 2022. Google Core Libraries for Java. Retrieved September 7, 2022 from https://github.com/google/guava.

[77]

Manu Sridharan, Denis Gopan, Lexin Shan, and Rastislav Bodík. 2005. Demand-driven points-to analysis for Java. In Proceedings of the 20th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA’05), Ralph E. Johnson and Richard P. Gabriel (Eds.). ACM, 59–76. DOI:

Digital Library

[78]

Johannes Späth, Lisa Nguyen Quang Do, Karim Ali, and Eric Bodden. 2016. Boomerang: Demand-driven flow- and context-sensitive pointer analysis for Java. In Proceedings of the 30th European Conference on Object-Oriented Programming (ECOOP’16), (LIPIcs), Shriram Krishnamurthi and Benjamin S. Lerner (Eds.), Vol. 56. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 22:1–22:26. DOI:

[79]

Shmuel Sagiv, Thomas W. Reps, and Reinhard Wilhelm. 2002. Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24, 3 (2002), 217–298. DOI:

Digital Library

[80]

Bertrand Jeannet, Alexey Loginov, Thomas W. Reps, and Mooly Sagiv. 2010. A relational approach to interprocedural shape analysis. ACM Trans. Program. Lang. Syst. 32, 2 (2010), 5:1–5:52. DOI:

Digital Library

[81]

Jiangchao Liu, Liqian Chen, and Xavier Rival. 2018. Automatic verification of embedded system code manipulating dynamic structures stored in contiguous regions. IEEE Trans. Comput. Aided Des. Integr. Circ. Syst. 37, 11 (2018), 2311–2322. DOI:

[82]

Thomas W. Reps. 1997. Program analysis via graph reachability. In Proceedings of the International Symposium on Logic Programming, Jan Maluszynski (Ed.). MIT Press, 5–19.

[83]

Shmuel Sagiv, Thomas W. Reps, and Susan Horwitz. 1996. Precise interprocedural dataflow analysis with applications to constant propagation. Theor. Comput. Sci. 167, 1&2 (1996), 131–170. DOI:

Digital Library

[84]

Eric Bodden. 2012. Inter-procedural data-flow analysis with IFDS/IDE and Soot. In Proceedings of the ACM SIGPLAN International Workshop on State of the Art in Java Program analysis (SOAP’12), Eric Bodden, Laurie J. Hendren, Patrick Lam, and Elena Sherman (Eds.). ACM, 3–8. DOI:

Digital Library

[85]

Thomas W. Reps. 1995. Shape analysis as a generalized path problem. In Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation. 1–11. DOI:

Digital Library

[86]

Thomas W. Reps, Mooly Sagiv, and Reinhard Wilhelm. 2007. Shape analysis and applications. In The Compiler Design Handbook: Optimizations and Machine Code Generation, Second Edition, Y. N. Srikant and Priti Shankar (Eds.). CRC Press, 12.

[87]

Cristiano Calcagno, Dino Distefano, Peter W. O’Hearn, and Hongseok Yang. 2011. Compositional shape analysis by means of Bi-abduction. J. ACM 58, 6 (2011), 26:1–26:66. DOI:

Digital Library

[88]

Stephen Magill, Ming-Hsien Tsai, Peter Lee, and Yih-Kuen Tsay. 2010. Automatic numeric abstractions for heap-manipulating programs. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’10), Manuel V. Hermenegildo and Jens Palsberg (Eds.). ACM, 211–222. DOI:

Digital Library

[89]

Kuat Yessenov, Ruzica Piskac, and Viktor Kuncak. 2010. Collections, cardinalities, and relations. In Proceedings of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’10),Lecture Notes in Computer Science, Gilles Barthe and Manuel V. Hermenegildo (Eds.), Vol. 5944. Springer, 380–395. DOI:

Digital Library

[90]

Tianhan Lu, Pavol Cerný, Bor-Yuh Evan Chang, and Ashutosh Trivedi. 2019. Type-directed bounding of collections in reactive programs. In Proceedings of the 20th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’19)Lecture Notes in Computer Science, Constantin Enea and Ruzica Piskac (Eds.), Vol. 11388. Springer, 275–296. DOI:

[91]

Tuan-Hung Pham, Minh-Thai Trinh, Anh-Hoang Truong, and Wei-Ngan Chin. 2011. FixBag: A fixpoint calculator for quantified bag constraints. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV’11),Lecture Notes in Computer Science, Ganesh Gopalakrishnan and Shaz Qadeer (Eds.), Vol. 6806. Springer, 656–662. DOI:

[92]

Arlen Cox, Bor-Yuh Evan Chang, and Sriram Sankaranarayanan. 2013. QUIC graphs: Relational invariant generation for containers. In Proceedings of the 27th European Conference Object-Oriented Programming (ECOOP’13),Lecture Notes in Computer Science, Giuseppe Castagna (Ed.), Vol. 7920. Springer, 401–425. DOI:

Digital Library

[93]

Zhoulai Fu. 2014. Targeted update–Aggressive memory abstraction beyond common sense and its application on static numeric analysis. In Proceedings of the 23rd European Symposium on Programming (ESOP’14), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS’14),Lecture Notes in Computer Science, Zhong Shao (Ed.), Vol. 8410. Springer, 534–553. DOI:

Digital Library

[94]

Zhoulai Fu. 2014. Modularly combining numeric abstract domains with points-to analysis, and a scalable static numeric analyzer for Java. In Proceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’14),Lecture Notes in Computer Science, Kenneth L. McMillan and Xavier Rival (Eds.), Vol. 8318. Springer, 282–301. DOI:

Digital Library

[95]

Karen Zee, Viktor Kuncak, and Martin C. Rinard. 2008. Full functional verification of linked data structures. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, Rajiv Gupta and Saman P. Amarasinghe (Eds.). ACM, 349–361. DOI:

Digital Library

[96]

Deokhwan Kim and Martin C. Rinard. 2011. Verification of semantic commutativity conditions and inverse operations on linked data structures. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’11), Mary W. Hall and David A. Padua (Eds.). ACM, 528–541. DOI:

Digital Library

[97]

Ruzica Piskac, Thomas Wies, and Damien Zufferey. 2014. GRASShopper - complete heap verification with mixed specifications. In Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’14), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS’14),Lecture Notes in Computer Science, Erika Ábrahám and Klaus Havelund (Eds.), Vol. 8413. Springer, 124–139. DOI:

[98]

Osbert Bastani, Rahul Sharma, Alex Aiken, and Percy Liang. 2018. Active learning of points-to specifications. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI.18), Jeffrey S. Foster and Dan Grossman (Eds.). ACM, 678–692. DOI:

Digital Library

[99]

Michail Basios, Lingbo Li, Fan Wu, Leslie Kanthan, and Earl T. Barr. 2018. Darwinian data structure selection. In Proceedings of the 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. 118–128.

Digital Library

[100]

Jianhui Chen and Fei He. 2018. Control flow-guided SMT solving for program verification. In Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering (ASE’18), Marianne Huchard, Christian Kästner, and Gordon Fraser (Eds.). ACM, 351–361. DOI:

Digital Library

[101]

Peisen Yao, Qingkai Shi, Heqing Huang, and Charles Zhang. 2020. Fast bit-vector satisfiability. In Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA’20), Sarfraz Khurshid and Corina S. Pasareanu (Eds.). ACM, 38–50. DOI:

Digital Library

[102]

Hongyu Fan, Weiting Liu, and Fei He. 2022. Interference relation-guided SMT solving for multi-threaded program verification. In Proceedings of the 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP’22), Jaejin Lee, Kunal Agrawal, and Michael F. Spear (Eds.). ACM, 163–176. DOI:

Digital Library

[103]

Ziqi Shuai, Zhenbang Chen, Yufeng Zhang, Jun Sun, and Ji Wang. 2021. Type and interval aware array constraint solving for symbolic execution. In Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA’21), Cristian Cadar and Xiangyu Zhang (Eds.). ACM, 361–373.

Digital Library

[104]

Dongpeng Xu, Binbin Liu, Weijie Feng, Jiang Ming, Qilong Zheng, Jing Li, and Qiaoyan Yu. 2021. Boosting SMT solver performance on mixed-bitwise-arithmetic expressions. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI’21), Stephen N. Freund and Eran Yahav (Eds.). ACM, 651–664. DOI:

Digital Library

Cited By

Xu RChen LZhang RZhang YXiao WZhou HMao X(2024)Accelerating Static Null Pointer Dereference Detection with Parallel ComputingProceedings of the 15th Asia-Pacific Symposium on Internetware10.1145/3671016.3671385(135-144)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1145/3671016.3671385
Tang WDong DLi SWang CYao PZhou JZhang C(2024) Octopus: Scaling Value-Flow Analysis via Parallel Collection of Realizable Path ConditionsACM Transactions on Software Engineering and Methodology10.1145/363274333:3(1-33)Online publication date: 24-Jan-2024
https://dl.acm.org/doi/10.1145/3632743
Xu RMao XXiao W(2023)Accelerating High-Precision Vulnerability Detection in C Programs with Parallel Graph Summarization2023 6th International Conference on Software Engineering and Computer Science (CSECS)10.1109/CSECS60003.2023.10428132(1-6)Online publication date: 22-Dec-2023
https://doi.org/10.1109/CSECS60003.2023.10428132
Show More Cited By

Index Terms

Anchor: Fast and Precise Value-flow Analysis for Containers via Memory Orientation
1. Software and its engineering
  1. Software organization and properties
    1. Extra-functional properties
      1. Software safety
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program analysis

Recommendations

Practical memory leak detection using guarded value-flow analysis
PLDI '07: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation

This paper presents a practical inter-procedural analysis algorithm for detecting memory leaks in C programs. Our algorithm tracks the flow of values from allocation points to deallocation points using a sparse representation of the program consisting ...
Precise and scalable context-sensitive pointer analysis via value flow graph
ISMM '13: Proceedings of the 2013 international symposium on memory management

In this paper, we propose a novel method for context-sensitive pointer analysis using the value flow graph (VFG) formulation. We achieve context-sensitivity by simultaneously applying function cloning and computing context-free language reachability (...
Precise and scalable context-sensitive pointer analysis via value flow graph
ISMM '13: Proceedings of the 2013 international symposium on memory management

In this paper, we propose a novel method for context-sensitive pointer analysis using the value flow graph (VFG) formulation. We achieve context-sensitivity by simultaneously applying function cloning and computing context-free language reachability (...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Software Engineering and Methodology

ACM Transactions on Software Engineering and Methodology Volume 32, Issue 3

May 2023

937 pages

ISSN:1049-331X

EISSN:1557-7392

DOI:10.1145/3594533

Editor:
Mauro Pezzè
USI Università della Svizzera italiana and SIT Schaffhausen Institute of Technology, Switzerland

Issue’s Table of Contents

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 26 April 2023

Online AM: 04 October 2022

Accepted: 06 September 2022

Revised: 15 July 2022

Received: 08 March 2022

Published in TOSEM Volume 32, Issue 3

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Hong Kong Research Grant Council and the Innovation and Technology Commission, Ant Group

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
546
Total Downloads

Downloads (Last 12 months)243
Downloads (Last 6 weeks)8

Reflects downloads up to 24 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Xu RChen LZhang RZhang YXiao WZhou HMao X(2024)Accelerating Static Null Pointer Dereference Detection with Parallel ComputingProceedings of the 15th Asia-Pacific Symposium on Internetware10.1145/3671016.3671385(135-144)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1145/3671016.3671385
Tang WDong DLi SWang CYao PZhou JZhang C(2024) Octopus: Scaling Value-Flow Analysis via Parallel Collection of Realizable Path ConditionsACM Transactions on Software Engineering and Methodology10.1145/363274333:3(1-33)Online publication date: 24-Jan-2024
https://dl.acm.org/doi/10.1145/3632743
Xu RMao XXiao W(2023)Accelerating High-Precision Vulnerability Detection in C Programs with Parallel Graph Summarization2023 6th International Conference on Software Engineering and Computer Science (CSECS)10.1109/CSECS60003.2023.10428132(1-6)Online publication date: 22-Dec-2023
https://doi.org/10.1109/CSECS60003.2023.10428132
Xu RMao XChen L(2023)P-DATA: A Task-Level Parallel Framework for Dependency-Aware Value Flow Taint Analysis2023 30th Asia-Pacific Software Engineering Conference (APSEC)10.1109/APSEC60848.2023.00035(249-258)Online publication date: 4-Dec-2023
https://doi.org/10.1109/APSEC60848.2023.00035

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Full Text

View this article in Full Text.

HTML Format

View this article in HTML Format.

Media

Figures

Other

Tables

View full text|Download PDF

View Issue’s Table of Contents