Skip to main content
SpringerLink
Log in

Existential Label Flow Inference Via CFL Reachability

  • Conference paper
Static Analysis (SAS 2006)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 4134))

Included in the following conference series:

Abstract

In programming languages, existential quantification is useful for describing relationships among members of a structured type. For example, we may have a list in which there exists some mutual exclusion lock l in each list element such that l protects the data stored in that element. With this information, a static analysis can reason about the relationship between locks and locations in the list even when the precise identity of the lock and/or location is unknown. To facilitate the construction of such static analyses, this paper presents a context-sensitive label flow analysis algorithm with support for existential quantification. Label flow analysis is a core part of many static analysis systems. Following Rehof et al, we use context-free language (CFL) reachability to develop an efficient O(n 3) label flow inference algorithm. We prove the algorithm sound by reducing its derivations to those in a system based on polymorphically-constrained types, in the style of Mossin. We have implemented a variant of our analysis as part of a data race detection tool for C programs.

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. Das, M.: Unification-based Pointer Analysis with Directional Assignments. In: The 2000 Conference on Programming Language Design and Implementation, Vancouver, BC, Canada, pp. 35–46 (2000)

    Google Scholar 

  2. Mitchell, J.C., Plotkin, G.D.: Abstract types have existential type. ACM Transactions on Programming Languages and Systems 10, 470–502 (1988)

    Article  Google Scholar 

  3. Xi, H., Pfenning, F.: Dependent Types in Practical Programming. In: The 26th Annual Symposium on Principles of Programming Languages, San Antonio, Texas, pp. 214–227 (1999)

    Google Scholar 

  4. Pratikakis, P., Foster, J.S., Hicks, M.: Context-Sensitive Correlation Analysis for Race Detection. In: The 2006 Conference on Programming Language Design and Implementation, Ottawa, Canada (to appear, 2006)

    Google Scholar 

  5. Flanagan, C., Abadi, M.: Types for Safe Locking. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 91–108. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  6. Minamide, Y., Morrisett, G., Harper, R.: Typed closure conversion. In: The 23rd Annual Symposium on Principles of Programming Languages, St. Petersburg Beach, Florida, pp. 271–283 (1996)

    Google Scholar 

  7. Fähndrich, M., Rehof, J., Das, M.: Scalable Context-Sensitive Flow Analysis using Instantiation Constraints. In: The 2000 Conference on Programming Language Design and Implementation, Vancouver, BC, Canada, pp. 253–263 (2000)

    Google Scholar 

  8. Das, M., Liblit, B., Fähndrich, M., Rehof, J.: Estimating the Impact of Scalable Pointer Analysis on Optimization. In: Cousot, P. (ed.) Static Analysis, Eighth International Symposium, Paris, France, pp. 260–278 (2001)

    Google Scholar 

  9. Myers, A.C.: Practical Mostly-Static Information Flow Control. In: The 26th Annual Symposium on Principles of Programming Languages, San Antonio, Texas, pp. 228–241 (1999)

    Google Scholar 

  10. Foster, J.S., Johnson, R., Kodumal, J., Aiken, A.: Flow-insensitive type qualifiers. ACM Transactions on Programming Languages and Systems (to appear)

    Google Scholar 

  11. Kodumal, J., Aiken, A.: The Set Constraint/CFL Reachability Connection in Practice. In: The 2004 Conference on Programming Language Design and Implementation, Washington, DC, pp. 207–218 (2004)

    Google Scholar 

  12. Johnson, R., Wagner, D.: Finding User/Kernel Bugs With Type Inference. In: The 13th Usenix Security Symposium, San Diego, CA (2004)

    Google Scholar 

  13. Mossin, C.: Flow Analysis of Typed Higher-Order Programs. PhD thesis, DIKU, Department of Computer Science, University of Copenhagen (1996)

    Google Scholar 

  14. Rehof, J., Fähndrich, M.: Type-Based Flow Analysis: From Polymorphic Subtyping to CFL-Reachability. In: The 28th Annual Symposium on Principles of Programming Languages, London, United Kingdom, pp. 54–66 (2001)

    Google Scholar 

  15. Fähndrich, M., Rehof, J., Das, M.: From Polymorphic Subtyping to CFL Reachability: Context-Sensitive Flow Analysis Using Instantiation Constraints. Technical Report MS-TR-99-84, Microsoft Research (2000)

    Google Scholar 

  16. Flanagan, C., Felleisen, M.: Componential Set-Based Analysis. In: The 1997 Conference on Programming Language Design and Implementation, Las Vegas, Nevada, pp. 235–248 (1997)

    Google Scholar 

  17. Fähndrich, M., Aiken, A.: Making Set-Constraint Based Program Analyses Scale. In: First Workshop on Set Constraints at CP 1996, Available as CSD-TR-96-917, University of California at Berkeley (1996)

    Google Scholar 

  18. Fähndrich, M.: BANE: A Library for Scalable Constraint-Based Program Analysis. PhD thesis, University of California, Berkeley (1999)

    Google Scholar 

  19. von Behren, R., Condit, J., Zhou, F., Necula, G.C., Brewer, E.: Capriccio: Scalable threads for internet services. In: ACM Symposium on Operating Systems Principles (2003)

    Google Scholar 

  20. Pratikakis, P., Hicks, M., Foster, J.S.: Existential Label Flow Inference via CFL Reachability. Technical Report CS-TR-4700, University of Maryland, Computer Science Department (2005)

    Google Scholar 

  21. Henglein, F.: Type Inference with Polymorphic Recursion. ACM Transactions on Programming Languages and Systems 15, 253–289 (1993)

    Article  Google Scholar 

  22. Botlan, D.L., Rémy, D.: MLF—Raising ML to the Power of System F. In: The Eighth International Conference on Functional Programming, Uppsala, Sweden, pp. 27–38 (2003)

    Google Scholar 

  23. Läufer, K., Odersky, M.: Polymorphic type inference and abstract data types. ACM Transactions on Programming Languages and Systems 16, 1411–1430 (1994)

    Article  Google Scholar 

  24. Rémy, D.: Programming objects with MLART: An extension to ML with abstract and record types. In: The International Symposium on Theoretical Aspects of Computer Science, Sendai, Japan, pp. 321–346 (1994)

    Google Scholar 

  25. Simonet, V.: An Extension of HM(X) with Bounded Existential and Universal Data Types. In: The Eighth International Conference on Functional Programming, Uppsala, Sweden, pp. 39–50 (2003)

    Google Scholar 

  26. Mitchell, J.C.: Type inference with simple subtypes. Journal of Functional Programming 1, 245–285 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  27. Reps, T., Horwitz, S., Sagiv, M.: Precise Interprocedural Dataflow Analysis via Graph Reachability. In: The 22nd Annual Symposium on Principles of Programming Languages, San Francisco, California, pp. 49–61 (1995)

    Google Scholar 

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

    Google Scholar 

  29. Wells, J.B.: Typability and type checking in System F are equivalent and undecidable. Ann. Pure Appl. Logic 98, 111–156 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  30. Odersky, M., Sulzmann, M., Wehr, M.: Type inference with constrained types. Theory and Practice of Object Systems 5, 35–55 (1999)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Maryland, College Park

    Polyvios Pratikakis, Jeffrey S. Foster & Michael Hicks

Authors
  1. Polyvios Pratikakis
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jeffrey S. Foster
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Michael Hicks
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Seoul National University, P.O. Box, Korea

    Kwangkeun Yi

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Pratikakis, P., Foster, J.S., Hicks, M. (2006). Existential Label Flow Inference Via CFL Reachability. In: Yi, K. (eds) Static Analysis. SAS 2006. Lecture Notes in Computer Science, vol 4134. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11823230_7

Download citation

  • DOI: https://doi.org/10.1007/11823230_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-37756-6

  • Online ISBN: 978-3-540-37758-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation