A unified lattice model and framework for purity analyses

ABSTRACT

Analyzing methods in object-oriented programs whether they are side-effect free and also deterministic, i.e., mathematically pure, has been the target of extensive research. Identifying such methods helps to find code smells and security related issues, and also helps analyses detecting concurrency bugs. Pure methods are also used by formal verification approaches as the foundations for specifications and proving the pureness is necessary to ensure correct specifications. However, so far no common terminology exists which describes the purity of methods. Furthermore, some terms (e.g., pure or side-effect free) are also used inconsistently. Further, all current approaches only report selected purity information making them only suitable for a smaller subset of the potential use cases. In this paper, we present a fine-grained unified lattice model which puts the purity levels found in the literature into relation and which adds a new level that generalizes existing definitions. We have also implemented a scalable, modularized purity analysis which produces significantly more precise results for real-world programs than the best-performing related work. The analysis shows that all defined levels are found in real-world projects.

References

1. Dotty documentation overview – Effect capabilities, 2018. Retrieved 2018-04-21.
2. B. Alpern, S. Augart, S. M. Blackburn, M. Butrico, A. Cocchi, P. Cheng, J. Dolby, S. Fink, D. Grove, M. Hind, K. S. McKinley, M. Mergen, J. E. B. Moss, T. Ngo, V. Sarkar, and M. Trapp. The jikes research virtual machine project: Building an open-source research community. IBM Systems Journal, 44(2):399–417, 2005.
3. D. F. Bacon and P. F. Sweeney. Fast static analysis of C++ virtual function calls. ACM Sigplan Notices, 31(10):324–341, 1996.
4. A. Banerjee and D. A. Naumann. Secure information flow and pointer confinement in a Java-like language. In CSFW, volume 2, page 253, 2002.
5. M. Barnett, D. A. Naumann, W. Schulte, and Q. Sun. 99.44% pure: Useful abstractions in specifications. In ECOOP workshop on Formal Techniques for Java-like Programs (FTfJP), 2004.
6. M. Barnett, D. A. Naumann, W. Schulte, and Q. Sun. Allowing state changes in specifications. ETRICS, 3995:321–336, 2006.
7. W. C. Benton and C. N. Fischer. Mostly-functional behavior in Java programs. In International Workshop on Verification, Model Checking, and Abstract Interpretation, pages 29–43. Springer, 2009.
8. C. Boyapati, S. Khurshid, and D. Marinov. Korat: Automated testing based on Java predicates. In ACM SIGSOFT Software Engineering Notes, volume 27, pages 123–133. ACM, 2002.
9. B. Cahoon and K. S. McKinley. Data flow analysis for software prefetching linked data structures in Java. In Parallel Architectures and Compilation Techniques, 2001. Proceedings. 2001 International Conference on, pages 280–291. IEEE, 2001.
10. J.-D. Choi, M. Gupta, M. Serrano, V. C. Sreedhar, and S. Midkiff. Escape analysis for Java. Acm Sigplan Notices, 34(10):1–19, 1999.
11. L. R. Clausen. A Java bytecode optimizer using side-effect analysis. Concurrency and Computation: Practice and Experience, 9(11):1031–1045, 1997.
12. D. R. Cok. Reasoning with specifications containing method calls and model fields. Journal of Object Technology, 4(8):77–103, 2005.
13. V. Dallmeier. Static vs. dynamic purity analysis. Dept. Comput. Sci., Saarland Univ., Saarbrucken, Germany, Tech. Rep. SU-CS-2013-012, 2007.
14. V. Dallmeier, C. Lindig, A. Wasylkowski, and A. Zeller. Mining object behavior with ADABU. In Proceedings of the 2006 international workshop on Dynamic systems analysis, pages 17–24. ACM, 2006.
15. Á. Darvas and K. R. M. Leino. Practical reasoning about invocations and implementations of pure methods. In FASE, volume 4422, pages 336–351. Springer, 2007.
16. Á. Darvas and P. Müller. Reasoning about method calls in interface specifications. Journal of Object Technology, 5(5):59–85, 2006.
17. J. Dietrich, H. Schole, L. Sui, and E. Tempero. XCorpus–an executable corpus of Java programs. The Journal of Object Technology, 16(4), 2017.
18. J. J. Dolado, M. Harman, M. C. Otero, and L. Hu. An empirical investigation of the influence of a type of side effects on program comprehension. IEEE Transactions on Software Engineering, 29(7):665–670, 2003.
19. M. Eichberg, F. Kübler, D. Helm, M. Reif, G. Salvaneschi, and M. Mezini. Lattice based modularization of static analyses. SOAP 2018, 2018.
20. M. Finifter, A. Mettler, N. Sastry, and D. Wagner. Verifiable functional purity in Java. In Proceedings of the 15th ACM conference on Computer and communications security, pages 161–174. ACM, 2008.
21. C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. PLDI 2002: Extended static checking for Java. ACM Sigplan Notices, 48(4S):22–33, 2013.
22. D. Gay and B. Steensgaard. Fast escape analysis and stack allocation for objectbased programs. In International Conference on Compiler Construction, pages 82–93. Springer, 2000.
23. S. Genaim and F. Spoto. Constancy analysis. Formal Techniques for Java-like Programs (FTfJP), page 100, 2008.
24. M. Hind and A. Pioli. Which pointer analysis should I use? In ACM SIGSOFT Software Engineering Notes, volume 25, pages 113–123. ACM, 2000.
25. W. Huang and A. Milanova. ReImInfer: Method purity inference for Java. In Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering, page 38. ACM, 2012.
26. W. Huang, A. Milanova, W. Dietl, and M. D. Ernst. ReIm & ReImInfer: Checking and inference of reference immutability and method purity. In ACM SIGPLAN Notices, volume 47, pages 879–896. ACM, 2012.
27. R. Ierusalimschy and N. Rodriguez. Side-effect free functions in object-oriented languages. Computer languages, 21(3):129–146, 1995.
28. A. Le, O. Lhoták, and L. J. Hendren. Using inter-procedural side-effect information in JIT optimizations. In CC, pages 287–304. Springer, 2005.
29. G. T. Leavens and Y. Cheon. Design by contract with JML, 2006.
30. J. M. Lucassen and D. K. Gifford. Polymorphic effect systems. In Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 47–57. ACM, 1988.
31. D. Marinov, A. Andoni, D. Daniliuc, S. Khurshid, and M. Rinard. An evaluation of exhaustive testing for data structures. Technical report, Technical Report MIT-LCS-TR-921, MIT CSAIL, Cambridge, MA, 2003.
32. D. A. Naumann. Observational purity and encapsulation. In FASE, volume 3442, pages 190–204. Springer, 2005.
33. D. Pearce. JPure: a modular purity system for Java. In Compiler construction, pages 104–123. Springer, 2011.
34. A. Potanin, J. Östlund, Y. Zibin, and M. D. Ernst. Immutability. In Aliasing in Object-Oriented Programming. Types, Analysis and Verification, pages 233–269. Springer, 2013.
35. A. Rountev. Precise identification of side-effect-free methods in Java. In Software Maintenance, 2004. Proceedings. 20th IEEE International Conference on, pages 82–91. IEEE, 2004.
36. A. Sabelfeld and A. C. Myers. Language-based information-flow security. IEEE Journal on selected areas in communications, 21(1):5–19, 2003.
37. A. Stewart, R. Cardell-Oliver, and R. Davies. Fine-grained classification of sideeffect free methods in real-world Java code and applications to software security. In Proceedings of the Australasian Computer Science Week Multiconference, page 37. ACM, 2016.
38. A. Sălcianu and M. Rinard. A combined pointer and purity analysis for Java programs. 2004.
39. A. Sălcianu and M. C. Rinard. Purity and side effect analysis for Java programs. In VMCAI, volume 5, pages 199–215. Springer, 2005.
40. E. Tempero, C. Anslow, J. Dietrich, T. Han, J. Li, M. Lumpe, H. Melton, and J. Noble. The Qualitas corpus: A curated collection of Java code for empirical studies. In Software Engineering Conference (APSEC), 2010 17th Asia Pacific, pages 336–345. IEEE, 2010.
41. O. Tkachuk and M. B. Dwyer. Adapting side effects analysis for modular program model checking, volume 28. ACM, 2003.
42. H. Xu, C. J. Pickett, and C. Verbrugge. Dynamic purity analysis for Java programs. In Proceedings of the 7th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, pages 75–82. ACM, 2007.
43. J. Zhao, I. Rogers, C. Kirkham, and I. Watson. Pure method analysis within Jikes RVM. Proc. ICOOOLPS, 2008.

Index Terms

• Software and its engineering

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Automated static analysis

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program analysis