Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Mutual Refinements of Context-Free Language Reachability

  • Conference paper
  • First Online:
Static Analysis (SAS 2023)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 14284))

Included in the following conference series:

Abstract

Context-free language reachability is an important program analysis framework, but the exact analysis problems can be intractable or undecidable, where CFL-reachability approximates such problems. For the same problem, there could be many over-approximations based on different CFLs \(C_1,\ldots ,C_n\). Suppose the reachability result of each \(C_i\) produces a set \(P_i\) of reachable vertex pairs. Is it possible to achieve better precision than the straightforward intersection \(\bigcap _{i=1}^n P_i\)?

This paper gives an affirmative answer: although CFLs are not closed under intersections, in CFL-reachability we can “intersect” graphs. Specifically, we propose mutual refinement to combine different CFL-reachability-based over-approximations. Our key insight is that the standard CFL-reachability algorithm can be slightly modified to trace the edges that contribute to the reachability results of \(C_1\), and \(C_2\)-reachability only need to consider contributing edges of \(C_1\), which can, in turn, trace the edges that contribute to \(C_2\)-reachability, etc. We prove that there exists a unique optimal refinement result (fix-point). Experimental results show that mutual refinement can achieve better precision than the straightforward intersection with reasonable extra cost.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 69.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 89.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

Similar content being viewed by others

Notes

  1. 1.

    \(\textsc {collect}\) can be implemented using either breadth-first-search or depth-first-search.

  2. 2.

    https://github.com/proganalysis/type-inference.

  3. 3.

    The implementation is available on GitHub (https://github.com/sdingcn/mutual-refinement) and Zenodo (https://doi.org/10.5281/zenodo.8191389). Certain low-level data structure optimizations were used.

  4. 4.

    https://github.com/yuanboli233/interdyck_graph_reduce.

References

  1. Chatterjee, K., Choudhary, B., Pavlogiannis, A.: Optimal dyck reachability for data-dependence and alias analysis. Proc. ACM Program. Lang. 2(POPL), 30:1–30:30 (2018)

    Google Scholar 

  2. Chaudhuri, S.: Subcubic algorithms for recursive state machines. In: Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, 7–12 January 2008, pp. 159–169. ACM (2008)

    Google Scholar 

  3. Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms. MIT Press, Cambridge (2022)

    Google Scholar 

  4. Cousot, P.: Asychronous iterative methods for solving a fixed point system of monotone equations in a complete lattice (1977)

    Google Scholar 

  5. Fähndrich, M., Foster, J.S., Su, Z., Aiken, A.: Partial online cycle elimination in inclusion constraint graphs. In: Proceedings of the ACM SIGPLAN 1998 Conference on Programming Language Design and Implementation (PLDI), Montreal, Canada, 17–19 June 1998, pp. 85–96. ACM (1998)

    Google Scholar 

  6. Fink, S.J., Yahav, E., Dor, N., Ramalingam, G., Geay, E.: Effective typestate verification in the presence of aliasing. ACM Trans. Softw. Eng. Methodol. 17(2), 9:1–9:34 (2008)

    Google Scholar 

  7. Fleming, P.J., Wallace, J.J.: How not to lie with statistics: the correct way to summarize benchmark results. Commun. ACM 29(3), 218–221 (1986)

    Article  Google Scholar 

  8. Harrison, M.A.: Introduction to Formal Language Theory. Addison-Wesley Longman Publishing Co., Inc. (1978)

    Google Scholar 

  9. Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to automata theory, languages, and computation. ACM SIGACT News 32(1), 60–65 (2001)

    Article  Google Scholar 

  10. Huang, W., Dong, Y., Milanova, A., Dolby, J.: Scalable and precise taint analysis for android. In: Proceedings of the 2015 International Symposium on Software Testing and Analysis, ISSTA 2015, pp. 106–117. ACM (2015)

    Google Scholar 

  11. Kahlon, V.: Boundedness vs. unboundedness of lock chains: characterizing decidability of pairwise CFL-reachability for threads communicating via locks. In: Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, 11–14 August 2009, Los Angeles, CA, USA, pp. 27–36. IEEE Computer Society (2009)

    Google Scholar 

  12. Kildall, G.A.: A unified approach to global program optimization. In: Conference Record of the ACM Symposium on Principles of Programming Languages, Boston, Massachusetts, USA, October 1973, pp. 194–206. ACM Press (1973)

    Google Scholar 

  13. Kjelstrøm, A.H., Pavlogiannis, A.: The decidability and complexity of interleaved bidirected dyck reachability. Proc. ACM Program. Lang. 6(POPL), 1–26 (2022)

    Google Scholar 

  14. Kleene, S.C.: Introduction to metamathematics (1952)

    Google Scholar 

  15. Kodumal, J., Aiken, A.: The set constraint/CFL reachability connection in practice. In: Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation 2004, Washington, DC, USA, 9–11 June 2004, pp. 207–218. ACM (2004)

    Google Scholar 

  16. Lattner, C., Adve, V.S.: LLVM: a compilation framework for lifelong program analysis & transformation. In: 2nd IEEE/ACM International Symposium on Code Generation and Optimization (CGO 2004), 20–24 March 2004, San Jose, CA, USA, pp. 75–88. IEEE Computer Society (2004)

    Google Scholar 

  17. Lei, Y., Sui, Y., Ding, S., Zhang, Q.: Taming transitive redundancy for context-free language reachability. Proc. ACM Program. Lang. 6(OOPSLA2), 1556–1582 (2022)

    Article  Google Scholar 

  18. Li, Y., Zhang, Q., Reps, T.W.: Fast graph simplification for interleaved dyck-reachability. In: Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, pp. 780–793. ACM (2020)

    Google Scholar 

  19. Lu, Y., Shang, L., Xie, X., Xue, J.: An incremental points-to analysis with CFL-reachability. In: Jhala, R., De Bosschere, K. (eds.) CC 2013. LNCS, vol. 7791, pp. 61–81. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37051-9_4

    Chapter  Google Scholar 

  20. Melski, D., Reps, T.W.: Interconvertibility of a class of set constraints and context-free-language reachability. Theor. Comput. Sci. 248(1–2), 29–98 (2000)

    Article  MathSciNet  Google Scholar 

  21. Milanova, A.: Flowcfl: generalized type-based reachability analysis: graph reduction and equivalence of CFL-based and type-based reachability. Proc. ACM Program. Lang. 4(OOPSLA), 178:1–178:29 (2020)

    Google Scholar 

  22. Pratikakis, P., Foster, J.S., Hicks, M.: Existential label flow inference via CFL reachability. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 88–106. Springer, Heidelberg (2006). https://doi.org/10.1007/11823230_7

    Chapter  Google Scholar 

  23. Rehof, J., Fähndrich, M.: Type-base flow analysis: from polymorphic subtyping to CFL-reachability. In: Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, UK, 17–19 January 2001, pp. 54–66. ACM (2001)

    Google Scholar 

  24. Reps, T.: Undecidability of context-sensitive data-dependence analysis. ACM Trans. Program. Lang. Syst. (TOPLAS) 22(1), 162–186 (2000)

    Article  Google Scholar 

  25. Reps, T.W.: Program analysis via graph reachability. Inf. Softw. Technol. 40(11–12), 701–726 (1998)

    Article  Google Scholar 

  26. Reps, T.W., Horwitz, S., Sagiv, S.: Precise interprocedural dataflow analysis via graph reachability. In: Conference Record of POPL 1995: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, 23–25 January 1995, pp. 49–61. ACM Press (1995)

    Google Scholar 

  27. Späth, J., Ali, K., Bodden, E.: Context-, flow-, and field-sensitive data-flow analysis using synchronized pushdown systems. Proc. ACM Program. Lang. 3(POPL), 48:1–48:29 (2019)

    Google Scholar 

  28. SPEC: SPEC CPU 2017 (2017). https://www.spec.org/cpu2017/. Accessed 6 Nov 2022

  29. Sridharan, M., Bodík, R.: Refinement-based context-sensitive points-to analysis for java. In: Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation, Ottawa, Ontario, Canada, 11–14 June 2006, pp. 387–400. ACM (2006)

    Google Scholar 

  30. Su, Y., Ye, D., Xue, J.: Parallel pointer analysis with CFL-reachability. In: 43rd International Conference on Parallel Processing, ICPP 2014, Minneapolis, MN, USA, 9–12 September 2014, pp. 451–460. IEEE Computer Society (2014)

    Google Scholar 

  31. Sui, Y., Xue, J.: SVF: interprocedural static value-flow analysis in LLVM. In: Proceedings of the 25th International Conference on Compiler Construction, pp. 265–266. ACM (2016)

    Google Scholar 

  32. Tan, T., Li, Y., Ma, X., Xu, C., Smaragdakis, Y.: Making pointer analysis more precise by unleashing the power of selective context sensitivity. Proc. ACM Program. Lang. 5(OOPSLA), 1–27 (2021)

    Google Scholar 

  33. Xiao, X., Zhang, Q., Zhou, J., Zhang, C.: Persistent pointer information. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, Edinburgh, United Kingdom - 09–11 June 2014, pp. 463–474. ACM (2014)

    Google Scholar 

  34. Yan, D., Xu, G., Rountev, A.: Demand-driven context-sensitive alias analysis for java. In: Proceedings of the 20th International Symposium on Software Testing and Analysis, ISSTA 2011, Toronto, ON, Canada, 17–21 July 2011, pp. 155–165. ACM (2011)

    Google Scholar 

  35. Yannakakis, M.: Graph-theoretic methods in database theory. In: Proceedings of the Ninth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, PODS 1990, pp. 230–242. ACM Press (1990)

    Google Scholar 

  36. Zhang, Q., Lyu, M.R., Yuan, H., Su, Z.: Fast algorithms for Dyck-CFL-reachability with applications to alias analysis. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013, Seattle, WA, USA, 16–19 June 2013, pp. 435–446. ACM (2013)

    Google Scholar 

  37. Zhang, Q., Su, Z.: Context-sensitive data-dependence analysis via linear conjunctive language reachability. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pp. 344–358. ACM (2017)

    Google Scholar 

Download references

Acknowledgement

We thank the anonymous reviewers for their feedback on earlier drafts of this paper. This work was supported, in part, by the United States National Science Foundation (NSF) under grants No. 1917924, No. 2114627, and No. 2237440; and by the Defense Advanced Research Projects Agency (DARPA) under grant N66001-21-C-4024. Any opinions, findings, conclusions, or recommendations expressed in this publication are those of the authors and do not necessarily reflect the views of the above sponsoring entities.

Author information

Authors and Affiliations

  1. Georgia Institute of Technology, Atlanta, GA, 30332, USA

    Shuo Ding & Qirun Zhang

Authors
  1. Shuo Ding
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Qirun Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Shuo Ding .

Editor information

Editors and Affiliations

  1. U. Politécnica de Madrid (UPM) and IMDEA Software Institute, Pozuelo de Alarcón, Madrid, Spain

    Manuel V. Hermenegildo

  2. U. Politécnica de Madrid (UPM) and IMDEA Software Institute, Pozuelo de Alarcon, Spain

    José F. Morales

Rights and permissions

Reprints and permissions

Copyright information

© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Ding, S., Zhang, Q. (2023). Mutual Refinements of Context-Free Language Reachability. In: Hermenegildo, M.V., Morales, J.F. (eds) Static Analysis. SAS 2023. Lecture Notes in Computer Science, vol 14284. Springer, Cham. https://doi.org/10.1007/978-3-031-44245-2_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-44245-2_12

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-44244-5

  • Online ISBN: 978-3-031-44245-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation