A Flow-Insensitive-Complete Program Representation | SpringerLink
Skip to main content
Springer Nature Link
Log in

A Flow-Insensitive-Complete Program Representation

  • Conference paper
  • First Online:
Verification, Model Checking, and Abstract Interpretation (VMCAI 2022)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 13182))

Abstract

When designing a static analysis, choosing between a flow-insensitive or a flow-sensitive analysis often amounts to favor scalability over precision. It is well known than specific program representations can help to reconcile the two objectives at the same time. For example the SSA representation is used in modern compilers to perform a constant propagation analysis flow-insensitively without any loss of precision.

This paper proposes a provably correct program transformation that reconciles them for any analysis. We formalize the notion of Flow-Insensitive-Completeness with two collecting semantics and provide a program transformation that permits to analyze a program in a flow insensitive manner without sacrificing the precision we could obtain with a flow sensitive approach.

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
¥17,985 /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
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 10295
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 12869
Price includes VAT (Japan)
  • 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.

    The source code can be found at https://github.com/SemDyal/fic-transform.

References

  1. Alpern, B., Wegman, M.N., Zadeck, F.K.: Detecting equality of variables in programs. In: POPL (1988)

    Google Scholar 

  2. Andersen, L.O.: Program analysis and specialization for the C programming language. Ph.D. thesis. Datalogisk Institut (1994)

    Google Scholar 

  3. Bodík, R., Gupta, R., Sarkar, V.: ABCD: eliminating array bounds checks on demand. In: PLDI. ACM (2000)

    Google Scholar 

  4. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Conference of POPL’78, pp. 84–96. ACM Press (1978)

    Google Scholar 

  5. Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13(4), 451–490 (1991)

    Article  Google Scholar 

  6. Gulwani, S., Necula, G.C.: A polynomial-time algorithm for global value numbering. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 212–227. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27864-1_17

    Chapter  MATH  Google Scholar 

  7. Hardekopf, B., Lin, C.: Flow-sensitive pointer analysis for millions of lines of code. In: Proceedings of CGO’11. ACM Press (2011)

    Google Scholar 

  8. Henry, J., Monniaux, D., Moy, M.: PAGAI: a path sensitive static analyser. Electr. Notes Theor. Comput. Sci. 289, 15–25 (2012)

    Article  Google Scholar 

  9. Hubert, L., et al.: Sawja: static analysis workshop for java. In: Beckert, B., Marché, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 92–106. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-18070-5_7

    Chapter  Google Scholar 

  10. Kildall, G.A.: A unified approach to global program optimization. In: Proceedings of POPL’73, pp. 194–206. ACM Press (1973)

    Google Scholar 

  11. Liu, J., Rival, X.: Abstraction of optional numerical values. In: Feng, X., Park, S. (eds.) APLAS 2015. LNCS, vol. 9458, pp. 146–166. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-26529-2_9

    Chapter  Google Scholar 

  12. Logozzo, F., Fähndrich, M.: Pentagons: a weakly relational abstract domain for the efficient validation of array accesses. Sci. Comput. Program. 75(9), 796–807 (2010)

    Article  MathSciNet  Google Scholar 

  13. Maroneze, A.O.: Certified compilation and worst-case execution time estimation. Theses, Université Rennes 1 (2014). https://hal.archives-ouvertes.fr/tel-01064869

  14. Miné, A.: The octagon abstract domain. In: Proceedings of WCRE’01, p. 310. IEEE Computer Society (2001)

    Google Scholar 

  15. Mirliaz, S., Pichardie, D.: A flow-insensitive-complete program representation (2021). https://hal.archives-ouvertes.fr/hal-03384612. working paper or preprint

  16. Nazaré, H., Maffra, I., Santos, W., Barbosa, L., Gonnord, L., Quintão Pereira, F.M.: Validation of memory accesses through symbolic analyses. ACM SIGPLAN Not. 49(10), 791–809 (2014)

    Article  Google Scholar 

  17. Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (2004). https://books.google.fr/books?id=RLjt0xSj8DcC

  18. Oh, H., Heo, K., Lee, W., Lee, W., Yi, K.: Design and implementation of sparse global analyses for C-like languages. In: Proceedings of PLDI’12. ACM Press (2012)

    Google Scholar 

  19. Pereira, F., Rastello, F.: Static Single Information form (2018). http://ssabook.gforge.inria.fr/latest/book.pdf. Chapter 11 in the SSA-book

  20. Wegman, M.N., Zadeck, F.K.: Constant propagation with conditional branches. In: Proceedings of POPL’85, pp. 291–299. ACM Press (1985)

    Google Scholar 

Download references

Acknowledgments

This work was supported by a European Research Council (ERC) Consolidator Grant for the project VESTA, funded under the European Union’s Horizon 2020 Framework Programme (grant agreement 772568). ENS Rennes was the only recipient of this grant.

Author information

Authors and Affiliations

  1. Univ Rennes, Inria, CNRS, IRISA, Rennes, France

    Solène Mirliaz

  2. Facebook, Paris, France

    David Pichardie

Authors
  1. Solène Mirliaz
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David Pichardie
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Solène Mirliaz .

Editor information

Editors and Affiliations

  1. Helmholtz Center for Information Security, Saarbrücken, Germany

    Bernd Finkbeiner

  2. New York University, New York, NY, USA

    Thomas Wies

Rights and permissions

Reprints and permissions

Copyright information

© 2022 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Mirliaz, S., Pichardie, D. (2022). A Flow-Insensitive-Complete Program Representation. In: Finkbeiner, B., Wies, T. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2022. Lecture Notes in Computer Science(), vol 13182. Springer, Cham. https://doi.org/10.1007/978-3-030-94583-1_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-94583-1_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-94582-4

  • Online ISBN: 978-3-030-94583-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation