Skip to main content
SpringerLink
Log in

Verifying Pointer and String Analyses with Region Type Systems

  • Conference paper
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2010)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 6355))

Abstract

Pointer analysis statically approximates the heap pointer structure during a program execution in order to track heap objects or to establish alias relations between references, and usually contributes to other analyses or code optimizations. In recent years, a number of algorithms have been presented that provide an efficient, scalable, and yet precise pointer analysis. However, it is unclear how the results of these algorithms compare to each other semantically.

In this paper, we present a general region type system for a Java-like language and give a formal soundness proof. The system is subsequently specialized to obtain a platform for embedding the results of various existing context-sensitive pointer analysis algorithms, thereby equipping the computed relations with a common interpretation and verification. We illustrate our system by outlining an extension to a string value analysis that builds on pointer information.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Emami, M., Ghiya, R., Hendren, L.J.: Context-sensitive interprocedural points-to analysis in the presence of function pointers. In: 1994 Conference on Programming Language Design and Implementation (PLDI 1994), pp. 242–256. ACM, New York (1994)

    Google Scholar 

  2. Andersen, L.O.: Program Analysis and Specialization for the C Programming Language. PhD thesis, DIKU, University of Copenhagen (1994)

    Google Scholar 

  3. Steensgaard, B.: Points-to analysis in almost linear time. In: 23rd Symposium on Principles of Programming Languages (POPL 1996), pp. 32–41. ACM, New York (1996)

    Google Scholar 

  4. Berndl, M., Lhoták, O., Qian, F., Hendren, L., Umanee, N.: Points-to analysis using BDDs. In: 2003 Conference on Programming Language Design and Implementation (PLDI 2003). ACM, New York (2003)

    Google Scholar 

  5. Bravenboer, M., Smaragdakis, Y.: Strictly declarative specification of sophisticated points-to analyses. In: 24th Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2009), pp. 243–262. ACM, New York (2009)

    Google Scholar 

  6. Igarashi, A., Pierce, B., Wadler, P.: Featherweight Java: A minimal core calculus for Java and GJ. In: 1999 Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 1999). ACM, New York (1999)

    Google Scholar 

  7. Ryder, B.G.: Dimensions of precision in reference analysis of object-oriented programming languages. In: Hedin, G. (ed.) CC 2003. LNCS, vol. 2622, pp. 126–137. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  8. Christensen, A.S., Møller, A., Schwartzbach, M.I.: Precise analysis of string expressions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  9. Crégut, P., Alvarado, C.: Improving the Security of Downloadable Java Applications With Static Analysis. Electronic Notes in Theoretical Computer Science 141(1), 129–144 (2005)

    Article  Google Scholar 

  10. Shivers, O.: Control-Flow Analysis of Higher-Order Languages, or Taming Lambda. PhD thesis, Carnegie Mellon University, Pittsburgh, PA, USA, Technical Report CMU-CS-91-145 (1991)

    Google Scholar 

  11. Banerjee, A., Jensen, T.: Modular control-flow analysis with rank 2 intersection types. Mathematical Structures in Computer Science 13(1), 87–124 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  12. Hardekopf, B., Lin, C.: Semi-sparse flow-sensitive pointer analysis. SIGPLAN Not. 44(1), 226–238 (2009)

    Article  MATH  Google Scholar 

  13. Lucassen, J.M., Gifford, D.K.: Polymorphic effect systems. In: 15th Symposium on Principles of Programming Languages (POPL 1988), pp. 47–57. ACM, New York (1988)

    Google Scholar 

  14. Benton, N., Kennedy, A., Beringer, L., Hofmann, M.: Relational semantics for effect-based program transformations with dynamic allocation. In: Principles and Practice of Decl. Prog. (PPDP 2007). ACM, New York (2007)

    Google Scholar 

  15. Tofte, M., Talpin, J.P.: Region-based memory management. Information and Computation 132(2), 109–176 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  16. Crary, K., Walker, D., Morrisett, G.: Typed memory management in a calculus of capabilities. In: 26th Symposium on Principles of Programming Languages (POPL 1999), pp. 262–275. ACM, New York (1999)

    Google Scholar 

  17. Foster, J.S., Terauchi, T., Aiken, A.: Flow-sensitive type qualifiers. In: 2002 Conference on Programming Language Design and Implementation (PLDI 2002), pp. 1–12. ACM, New York (2002)

    Google Scholar 

  18. Lhoták, O.: Program Analysis using Binary Decision Diagrams. PhD thesis, McGill University (January 2006)

    Google Scholar 

  19. Lenherr, T.: Taxonomy and Applications of Alias Analysis. Master’s thesis, ETH Zürich (2008)

    Google Scholar 

  20. Hofmann, M., Jost, S.: Type-based amortised heap-space analysis. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 22–37. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  21. Beringer, L., Grabowski, R., Hofmann, M.: Verifying Pointer and String Analyses with Region Type Systems: Soundness proofs and other material (2010), http://www.tcs.ifi.lmu.de/~grabow/regions

  22. Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)

    MATH  Google Scholar 

  23. Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Muchnick, S.S., Jones, N.D. (eds.) Program Flow Analysis: Theory and Applications. Prentice Hall International, Englewood Cliffs (1981)

    Google Scholar 

  24. Milanova, A., Rountev, A., Ryder, B.G.: Parameterized object sensitivity for points-to analysis for Java. ACM Trans. Softw. Eng. Methodol. 14(1), 1–41 (2005)

    Article  Google Scholar 

  25. Whaley, J., Lam, M.S.: Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. SIGPLAN Not. 39(6), 131–144 (2004)

    Article  Google Scholar 

  26. Nystrom, E.M., Kim, H.S., Hwu, W.W.: Importance of heap specialization in pointer analysis. In: 5th Workshop on Program Analysis for Software Tools and Engineering (PASTE 2004). ACM, New York (2004)

    Google Scholar 

  27. Tripp, O., Pistoia, M., Fink, S.J., Sridharan, M., Weisman, O.: Taj: effective taint analysis of web applications. In: 2009 Conference on Programming Language Design and Implementation (PLDI 2009), pp. 87–97. ACM, New York (2009)

    Chapter  Google Scholar 

  28. Beringer, L., Hofmann, M., Pavlova, M.: Certification Using the Mobius Base Logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol. 5382, pp. 25–51. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  29. Barthe, G., Pichardie, D., Rezk, T.: A certified lightweight non-interference Java bytecode verifier. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 125–140. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  30. Diwan, A., McKinley, K.S., Moss, J.E.B.: Type-based alias analysis. In: 1998 Conference on Programming Language Design and Implementation (PLDI 1998), pp. 106–117. ACM, New York (1998)

    Google Scholar 

  31. Loncaric, S.: A survey of shape analysis techniques. Pattern Recognition 31, 983–1001 (1998)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Princeton University, 35 Olden Street, Princeton, 08540, New Jersey, USA

    Lennart Beringer

  2. Institut für Informatik, Ludwig-Maximilians-Universität, Oettingenstrasse 67, D-80538, München, Germany

    Robert Grabowski & Martin Hofmann

Authors
  1. Lennart Beringer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Robert Grabowski
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Martin Hofmann
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Carnegie Mellon University, USA

    Edmund M. Clarke

  2. School of Computer Science, University of Manchester, Kilburn Building, Oxford Road, M13 9PL, Manchester, UK

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Beringer, L., Grabowski, R., Hofmann, M. (2010). Verifying Pointer and String Analyses with Region Type Systems. In: Clarke, E.M., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2010. Lecture Notes in Computer Science(), vol 6355. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17511-4_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-17511-4_6

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-17510-7

  • Online ISBN: 978-3-642-17511-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation