Document Open Access Logo

Accumulation Analysis

Authors Martin Kellogg, Narges Shadab, Manu Sridharan, Michael D. Ernst

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2022.10.pdf
  • Filesize: 0.95 MB
  • 30 pages

Document Identifiers

Author Details

Martin Kellogg
  • University of Washington, Seattle, WA, USA
Narges Shadab
  • University of California, Riverside, CA, USA
Manu Sridharan
  • University of California, Riverside, CA, USA
Michael D. Ernst
  • University of Washington, Seattle, WA, USA

Funding

This research was supported in part by the National Science Foundation under grants CCF-2007024 and CCF-2005889, DARPA contract FA8750-20-C-0226, a gift from Oracle Labs, and a Google Research Award.

Acknowledgements

Thanks to Max Willsey, Gus Smith, and the anonymous reviewers for their helpful feedback on early drafts.

Cite AsGet BibTex

Martin Kellogg, Narges Shadab, Manu Sridharan, and Michael D. Ernst. Accumulation Analysis. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 10:1-10:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ECOOP.2022.10

Abstract

A typestate specification indicates which behaviors of an object are permitted in each of the object’s states. In the general case, soundly checking a typestate specification requires precise information about aliasing (i.e., an alias or pointer analysis), which is computationally expensive. This requirement has hindered the adoption of sound typestate analyses in practice. This paper identifies accumulation typestate specifications, which are the subset of typestate specifications that can be soundly checked without any information about aliasing. An accumulation typestate specification can be checked instead by an accumulation analysis: a simple, fast dataflow analysis that conservatively approximates the operations that have been performed on an object. This paper formalizes the notions of accumulation analysis and accumulation typestate specification. It proves that accumulation typestate specifications are exactly those typestate specifications that can be checked soundly without aliasing information. Further, 41% of the typestate specifications that appear in the research literature are accumulation typestate specifications.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
Keywords
  • Typestate
  • finite-state property

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Stephen Adams, Thomas Ball, Manuvir Das, Sorin Lerner, Sriram K. Rajamani, Mark Seigle, and Westley Weimer. Speeding up dataflow analysis using flow-insensitive pointer analysis. In International Static Analysis Symposium, pages 230-246. Springer, 2002. Google Scholar
  2. Jonathan Aldrich, Joshua Sunshine, Darpan Saini, and Zachary Sparks. Typestate-oriented programming. In Proceedings of the 24th ACM SIGPLAN conference companion on Object oriented programming systems languages and applications, pages 1015-1022, 2009. Google Scholar
  3. Matthew Arnold, Martin Vechev, and Eran Yahav. Qvm: An efficient runtime for detecting defects in deployed systems. In Proceedings of the 23rd ACM SIGPLAN conference on Object-oriented programming systems languages and applications, pages 143-162, 2008. Google Scholar
  4. Nels E. Beckman, Duri Kim, and Jonathan Aldrich. An empirical study of object protocols in the wild. In European Conference on Object-Oriented Programming, pages 2-26. Springer, 2011. Google Scholar
  5. Kevin Bierhoff and Jonathan Aldrich. Lightweight object specification with typestates. ACM SIGSOFT Software Engineering Notes, 30(5):217-226, 2005. Google Scholar
  6. Kevin Bierhoff and Jonathan Aldrich. Modular typestate checking of aliased objects. ACM SIGPLAN Notices, 42(10):301-320, 2007. Google Scholar
  7. Kevin Bierhoff, Nels E. Beckman, and Jonathan Aldrich. Practical API protocol checking with access permissions. In European Conference on Object-Oriented Programming, pages 195-219. Springer, 2009. Google Scholar
  8. Eric Bodden. Efficient hybrid typestate analysis by determining continuation-equivalent states. In 2010 ACM/IEEE 32nd International Conference on Software Engineering, volume 1, pages 5-14. IEEE, 2010. Google Scholar
  9. Eric Bodden, Laurie Hendren, and Ondřej Lhoták. A staged static program analysis to improve the performance of runtime monitoring. In European Conference on Object-Oriented Programming, pages 525-549. Springer, 2007. Google Scholar
  10. Eric Bodden, Patrick Lam, and Laurie Hendren. Finding programming errors earlier by evaluating runtime monitors ahead-of-time. In Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering, pages 36-47, 2008. Google Scholar
  11. Eric Bodden, Andreas Sewe, Jan Sinschek, Hela Oueslati, and Mira Mezini. Taming reflection: Aiding static analysis in the presence of reflection and custom class loaders. In 2011 33rd International Conference on Software Engineering (ICSE), pages 241-250. IEEE, 2011. Google Scholar
  12. Miguel Castro, Manuel Costa, Jean-Philippe Martin, Marcus Peinado, Periklis Akritidis, Austin Donnelly, Paul Barham, and Richard Black. Fast byte-granularity software fault isolation. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, pages 45-58, 2009. Google Scholar
  13. Sigmund Cherem, Lonnie Princehouse, and Radu Rugina. Practical memory leak detection using guarded value-flow analysis. In Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 480-491, 2007. Google Scholar
  14. Dave Clarke, Johan Östlund, Ilya Sergey, and Tobias Wrigstad. Ownership types: A survey. In Aliasing in Object-Oriented Programming. Types, Analysis and Verification. Springer, Berlin, Heidelberg, 2013. Google Scholar
  15. Manuvir Das, Sorin Lerner, and Mark Seigle. ESP: Path-sensitive program verification in polynomial time. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, pages 57-68, 2002. Google Scholar
  16. Markus Degen, Peter Thiemann, and Stefan Wehr. Tracking linear and affine resources with Java(X). In European Conference on Object-Oriented Programming, pages 550-574. Springer, 2007. Google Scholar
  17. Robert DeLine and Manuel Fähndrich. Enforcing high-level protocols in low-level software. In Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, pages 59-69, 2001. Google Scholar
  18. Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. Patterns in property specifications for finite-state verification. In International Conference on Software Engineering, pages 411-420, 1999. Google Scholar
  19. Matthew B. Dwyer, Madeline Diep, and Sebastian Elbaum. Reducing the cost of path property monitoring through sampling. In 2008 23rd IEEE/ACM International Conference on Automated Software Engineering, pages 228-237. IEEE, 2008. Google Scholar
  20. Matthew B. Dwyer and Rahul Purandare. Residual dynamic typestate analysis exploiting static analysis: results to reformulate and reduce the cost of dynamic analysis. In Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, pages 124-133, 2007. Google Scholar
  21. Michael Emmi, Liana Hadarean, Ranjit Jhala, Lee Pike, Nicolás Rosner, Martin Schäf, Aritra Sengupta, and Willem Visser. RAPID: Checking API usage for the cloud in the cloud. In Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pages 1416-1426, 2021. Google Scholar
  22. Manuel Fähndrich and K. Rustan M. Leino. Heap monotonic typestates. In IWACO 2003: International Workshop on Aliasing, Confinement and Ownership in object-oriented programming, pages 58-72, Darmstadt, Germany, July 2003. Google Scholar
  23. John Field, Deepak Goyal, G. Ramalingam, and Eran Yahav. Typestate verification: Abstraction techniques and complexity results. In International Static Analysis Symposium, pages 439-462. Springer, 2003. Google Scholar
  24. Stephen J. Fink, Eran Yahav, Nurit Dor, G. Ramalingam, and Emmanuel Geay. Effective typestate verification in the presence of aliasing. ACM Transactions on Software Engineering and Methodology (TOSEM), 17(2):1-34, 2008. Google Scholar
  25. Jeffrey S. Foster, Tachio Terauchi, and Alex Aiken. Flow-sensitive type qualifiers. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, pages 1-12, 2002. Google Scholar
  26. Asya Frumkin, Yotam M. Y. Feldman, Ondřej Lhoták, Oded Padon, Mooly Sagiv, and Sharon Shoham. Property directed reachability for proving absence of concurrent modification errors. In International Conference on Verification, Model Checking, and Abstract Interpretation, pages 209-227. Springer, 2017. Google Scholar
  27. Mark Gabel and Zhendong Su. Testing mined specifications. In Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering, pages 1-11, 2012. Google Scholar
  28. Qi Gao, Wenbin Zhang, Zhezhe Chen, Mai Zheng, and Feng Qin. 2ndStrike: toward manifesting hidden concurrency typestate bugs. ACM Sigplan Notices, 46(3):239-250, 2011. Google Scholar
  29. Ronald Garcia, Éric Tanter, Roger Wolff, and Jonathan Aldrich. Foundations of typestate-oriented programming. ACM Transactions on Programming Languages and Systems (TOPLAS), 36(4):1-44, 2014. Google Scholar
  30. Christian Haack and Erik Poll. Type-based object immutability with flexible initialization. In European Conference on Object-Oriented Programming, pages 520-545. Springer, 2009. Google Scholar
  31. Graham Higman. Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society, 3(1):326-336, 1952. Google Scholar
  32. Jeff Huang, Qingzhou Luo, and Grigore Rosu. GPredict: Generic predictive concurrency analysis. In 2015 IEEE/ACM 37th IEEE International Conference on Software Engineering, volume 1, pages 847-857. IEEE, 2015. Google Scholar
  33. Dongyun Jin, Patrick O'Neil Meredith, Dennis Griffith, and Grigore Rosu. Garbage collection for monitoring parametric properties. ACM SIGPLAN Notices, 46(6):415-424, 2011. Google Scholar
  34. Pallavi Joshi and Koushik Sen. Predictive typestate checking of multithreaded Java programs. In 2008 23rd IEEE/ACM International Conference on Automated Software Engineering, pages 288-296. IEEE, 2008. Google Scholar
  35. Martin Kellogg, Manli Ran, Manu Sridharan, Martin Schäf, and Michael D. Ernst. Verifying object construction. In ICSE 2020, Proceedings of the 42nd International Conference on Software Engineering, pages 1447-1458, Seoul, Korea, May 2020. Google Scholar
  36. Martin Kellogg, Martin Schäf, Serdar Tasiran, and Michael D. Ernst. Continuous compliance. In ASE 2020: Proceedings of the 35th Annual International Conference on Automated Software Engineering, pages 511-523, Melbourne, Australia, September 2020. Google Scholar
  37. Martin Kellogg, Narges Shadab, Manu Sridharan, and Michael D. Ernst. Lightweight and modular resource leak verification. In ESEC/FSE 2021: The ACM 29th joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), Athens, Greece, August 2021. Google Scholar
  38. Naoki Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In Proceedings of the 36th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 416-428, 2009. Google Scholar
  39. Goh Kondoh and Tamiya Onodera. Finding bugs in Java Native Interface programs. In Proceedings of the 2008 international symposium on Software testing and analysis, pages 109-118, 2008. Google Scholar
  40. Viktor Kuncak, Patrick Lam, and Martin Rinard. Role analysis. In Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 17-32, 2002. Google Scholar
  41. William Landi and Barbara G. Ryder. Pointer-induced aliasing: A problem classification. In POPL '91: Proceedings of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, pages 93-103, Orlando, FL, January 1991. Google Scholar
  42. Wei Le and Mary Lou Soffa. Marple: Detecting faults in path segments using automatically generated analyses. ACM Transactions on Software Engineering and Methodology (TOSEM), 22(3):1-38, 2013. Google Scholar
  43. Junhee Lee, Seongjoon Hong, and Hakjoo Oh. Memfix: static analysis-based repair of memory deallocation errors for C. In Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pages 95-106, 2018. Google Scholar
  44. Yue Li, Tian Tan, Yifei Zhang, and Jingling Xue. Program tailoring: Slicing by sequential criteria. In 30th European Conference on Object-Oriented Programming (ECOOP 2016). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2016. Google Scholar
  45. Filipe Militao, Jonathan Aldrich, and Luís Caires. Rely-guarantee protocols. In European Conference on Object-Oriented Programming, pages 334-359. Springer, 2014. Google Scholar
  46. Nomair A. Naeem and Ondrej Lhoták. Typestate-like analysis of multiple interacting objects. ACM Sigplan Notices, 43(10):347-366, 2008. Google Scholar
  47. Mangala Gowri Nanda, Christian Grothoff, and Satish Chandra. Deriving object typestates in the presence of inter-object references. In Proceedings of the 20th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, pages 77-96, 2005. Google Scholar
  48. Matthew M. Papi, Mahmood Ali, Telmo Luis Correa Jr., Jeff H. Perkins, and Michael D. Ernst. Practical pluggable types for Java. In ISSTA 2008, Proceedings of the 2008 International Symposium on Software Testing and Analysis, pages 201-212, Seattle, WA, USA, July 2008. Google Scholar
  49. Hila Peleg, Sharon Shoham, Eran Yahav, and Hongseok Yang. Symbolic automata for static specification mining. In International Static Analysis Symposium, pages 63-83. Springer, 2013. Google Scholar
  50. Goran Piskachev, Tobias Petrasch, Johannes Späth, and Eric Bodden. AuthCheck: Program-state analysis for access-control vulnerabilities. In International Symposium on Formal Methods, pages 557-572. Springer, 2019. Google Scholar
  51. Michael Pradel, Ciera Jaspan, Jonathan Aldrich, and Thomas R. Gross. Statically checking API protocol conformance with mined multi-object specifications. In 2012 34th International Conference on Software Engineering (ICSE), pages 925-935. IEEE, 2012. Google Scholar
  52. Rahul Purandare, Matthew B. Dwyer, and Sebastian Elbaum. Monitor optimization via stutter-equivalent loop transformation. In Proceedings of the ACM international conference on Object oriented programming systems languages and applications, pages 270-285, 2010. Google Scholar
  53. Rahul Purandare, Matthew B. Dwyer, and Sebastian Elbaum. Optimizing monitoring of finite state properties through monitor compaction. In Proceedings of the 2013 International Symposium on Software Testing and Analysis, pages 280-290, 2013. Google Scholar
  54. Xin Qi and Andrew C. Myers. Masked types for sound object initialization. ACM SIGPLAN Notices, 44(1):53-65, 2009. Google Scholar
  55. Rust team. Rust programming language. https://www.rust-lang.org/, 2021. Accessed 30 November 2021.
  56. Sharon Shoham, Eran Yahav, Stephen J. Fink, and Marco Pistoia. Static specification mining using automata-based abstractions. IEEE Transactions on Software Engineering, 34(5):651-666, 2008. Google Scholar
  57. Johannes Späth, Karim Ali, and Eric Bodden. IDEal: Efficient and precise alias-aware dataflow analysis. Proceedings of the ACM on Programming Languages, 1(OOPSLA):1-27, 2017. Google Scholar
  58. Robert E. Strom and Shaula Yemini. Typestate: A programming language concept for enhancing software reliability. IEEE TSE, SE-12(1):157-171, January 1986. Google Scholar
  59. Joshua Sunshine, Karl Naden, Sven Stork, Jonathan Aldrich, and Éric Tanter. First-class state change in Plaid. In OOPSLA 2011, Object-Oriented Programming Systems, Languages, and Applications, pages 713-732, Portland, OR, USA, October 2011. Google Scholar
  60. Tian Tan, Yue Li, Xiaoxing Ma, Chang Xu, and Yannis Smaragdakis. Making pointer analysis more precise by unleashing the power of selective context sensitivity. Proceedings of the ACM on Programming Languages, 5(OOPSLA):1-27, 2021. Google Scholar
  61. Jesse A. Tov and Riccardo Pucella. Practical affine types. ACM SIGPLAN Notices, 46(1):447-458, 2011. Google Scholar
  62. Cláudio Vasconcelos and António Ravara. From object-oriented code with assertions to behavioural types. In Proceedings of the Symposium on Applied Computing, pages 1492-1497, 2017. Google Scholar
  63. Haowei Wu, Shengqian Yang, and Atanas Rountev. Static detection of energy defect patterns in android applications. In Proceedings of the 25th International Conference on Compiler Construction, pages 185-195, 2016. Google Scholar
  64. Tianyong Wu, Jierui Liu, Zhenbo Xu, Chaorong Guo, Yanli Zhang, Jun Yan, and Jian Zhang. Light-weight, inter-procedural and callback-aware resource leak detection for android apps. IEEE Transactions on Software Engineering, 42(11):1054-1076, 2016. Google Scholar
  65. Xusheng Xiao, Gogul Balakrishnan, Franjo Ivančić, Naoto Maeda, Aarti Gupta, and Deepak Chhetri. Arc++: effective typestate and lifetime dependency analysis. In Proceedings of the 2014 International Symposium on Software Testing and Analysis, pages 116-126, 2014. Google Scholar
  66. Guoqing Xu, Nick Mitchell, Matthew Arnold, Atanas Rountev, Edith Schonberg, and Gary Sevitsky. Scalable runtime bloat detection using abstract dynamic slicing. ACM Transactions on Software Engineering and Methodology (TOSEM), 23(3):1-50, 2014. Google Scholar
  67. Greta Yorsh, Eran Yahav, and Satish Chandra. Generating precise and concise procedure summaries. In Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 221-234, 2008. Google Scholar
  68. Hengbiao Yu, Zhenbang Chen, Ji Wang, Zhendong Su, and Wei Dong. Symbolic verification of regular properties. In 2018 IEEE/ACM 40th International Conference on Software Engineering (ICSE), pages 871-881. IEEE, 2018. Google Scholar
  69. Lu Zhang and Chao Wang. Runtime prevention of concurrency related type-state violations in multithreaded applications. In Proceedings of the 2014 International Symposium on Software Testing and Analysis, pages 1-12, 2014. Google Scholar
  70. Xin Zhang, Mayur Naik, and Hongseok Yang. Finding optimum abstractions in parametric dataflow analysis. ACM SIGPLAN Notices, 48(6):365-376, 2013. Google Scholar
  71. Yufeng Zhang, Zhenbang Chen, Ji Wang, Wei Dong, and Zhiming Liu. Regular property guided dynamic symbolic execution. In 2015 IEEE/ACM 37th IEEE International Conference on Software Engineering, volume 1, pages 643-653. IEEE, 2015. Google Scholar
  72. Zhiqiang Zuo, John Thorpe, Yifei Wang, Qiuhong Pan, Shenming Lu, Kai Wang, Guoqing Harry Xu, Linzhang Wang, and Xuandong Li. Grapple: A graph system for static finite-state property checking of large-scale systems code. In EuroSys, pages 1-17, 2019. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact