[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Log in

Sound and precise static analysis using a generalization of static single assignment and value numbering

  • General
  • Special Issue: SOAP 2023
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

CodePeer is a static analysis tool based on compiler optimization techniques such as static single assignment and value numbering. CodePeer infers and reports on implicit preconditions for each function of the program, based on limitations it identifies within the algorithm of the function. Presuming these inferred preconditions are satisfied, CodePeer then simulates the execution of each function, and identifies places where a program might still fail at run time, due to violating some run-time check or an error that leads to undefined behavior. CodePeer uses static single assignment and global value numbering to ensure that the determination of possible run-time values of each variable and expression encountered during the simulation of the execution of each function is both sound and precise. The approximations performed to ensure that the determination of possible values converges in the face of loops and recursion are systematic and based on the kinds of conservative analysis performed by compiler optimizers. The output of CodePeer includes for each function an enumeration of its global inputs and global outputs and inferred preconditions and postconditions. The output also includes, interspersed within a listing of the source of the function, an identification of the places where possible run-time failures or undefined behavior could occur. This output is designed to support code review, which gives the tool its CodePeer name.

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

Access this article

Subscribe and save

Springer+ Basic
£29.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

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Similar content being viewed by others

References

  1. AdaCore: GNATSAS CodePeer documentation (2024). https://www.adacore.com/static-analysis-suite/defects-and-vulnerability

  2. Boulanger, J.-L. (ed.): Static Analysis of Software: The Abstract Interpretation. John Wiley & Sons, Inc. (2012)

    Google Scholar 

  3. 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, 451–490 (1991). ISSN 0164-0925. https://doi.org/10.1145/115372.115320

    Article  Google Scholar 

  4. Briggs, P., Cooper, K.D., Simpson, L.T.: Value numbering. Softw. Pract. Exp. 27, 701–724 (1997). ISSN 0038-0644

    Article  Google Scholar 

  5. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238–252. ACM, Los Angeles (1977). http://doi.acm.org/10.1145/512950.512973

    Google Scholar 

  6. Taft, T., Duff, R.: 1.1.5 Classification of Errors. Ada Reference Manual (2022). http://www.ada-auth.org/standards/22rm/html/RM-1-1-5.html. Retrieved 4-Oct-23

  7. Kildall, G.A.: A unified approach to global program optimization. In: Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 194–206. ACM, Boston (1973). ISBN 9781450373494. https://doi.org/10.1145/512927.512945

    Chapter  Google Scholar 

  8. Allen, F.E., Cocke, J.: A program data flow analysis procedure. Commun. ACM 19, 137 (1976). ISSN 0001-0782. https://doi.org/10.1145/360018.360025

    Article  Google Scholar 

  9. Rival, X., Yi, K.: Introduction to Static Analysis an Abstract Interpretation Perspective. The MIT Press, Cambridge (2020)

    Google Scholar 

  10. Cocke, J., Kennedy, K.: An algorithm for reduction of operator strength. Commun. ACM 20, 850–856 (1977). ISSN 0001-0782. https://doi.org/10.1145/359863.359888

    Article  Google Scholar 

  11. Intermetrics: Computer Program Development Specification for Ada Integrated Environment. Ada Compiler Phases B5-AIE (1). COMP (1) (1982). https://apps.dtic.mil/sti/citations/ADA134032

  12. Bernstein, S.J., Duff, R.S.: Optimizing Ada on the fly. In: Proceedings of the 1999 Annual ACM SIGAda International Conference on Ada, pp. 169–179. Association for Computing Machinery, Redondo Beach (1999). ISBN 1581131275. https://doi.org/10.1145/319294.319321

    Chapter  Google Scholar 

  13. Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Global value numbers and redundant computations. In: Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 12–27. Association for Computing Machinery, San Diego (1988). ISBN 0897912527 https://doi.org/10.1145/73560.73562.

    Chapter  Google Scholar 

  14. Facebook: Pulse Infer Plugin 1.1.0. Facebook, Inc. (2023). https://fbinfer.com/docs/checker-pulse

  15. Lemerre, M.: SSA Translation Is an Abstract Interpretation in Proc. ACM Program. Lang., vol. 7 (2023)

    Google Scholar 

  16. Brat, G., Navas, J.A., Shi, N., Venet, A.: IKOS: a framework for static analysis based on abstract interpretation. In: Giannakopoulou, D., Salaün, G. (eds.) Proceedings, Software Engineering and Formal Methods - 12th International Conference, SEFM 2014, Grenoble, France, September 1-5, 2014, vol. 8702, pp. 271–277. Springer (2014). https://doi.org/10.1007/978-3-319-10431-7%5C_20

    Google Scholar 

  17. Lesbre, D., Lemerre, M.: Compiling with abstract interpretation. Proc. ACM Program. Lang. 8, 162 (2024). https://doi.org/10.1145/3656392

    Article  Google Scholar 

  18. Fähndrich, M., Logozzo, F.: Static contract checking with abstract interpretation. In: Beckert, B., Marché, C. (eds.) Formal Verification of Object-Oriented Software - International Conference, FoVeOOS 2010, Paris, France, June 28-30, 2010. Revised Selected Papers, vol. 6528, pp. 10–30. Springer (2010). https://doi.org/10.1007/978-3-642-18070-5%5C_2

    Chapter  Google Scholar 

Download references

Acknowledgements

The original design and implementation of CodePeer were developed by a team at SofCheck, Inc, starting in 2002. CodePeer was integrated with the GNAT Ada compiler front end, productized, and further developed at AdaCore, Inc, which acquired SofCheck in 2011. An in-depth description of CodePeer’s original design appeared as Chap. 5 in a book on Static Analysis of Software [2]. CodePeer is currently a part of a commercial static analysis suite of tools from AdaCore, Inc [1]. The design we describe represents the current state of the technology, which has undergone fifteen years of ongoing development since it was first released to customers in 2008.

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to S. Tucker Taft.

Additional information

Publisher’s Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Taft, S.T. Sound and precise static analysis using a generalization of static single assignment and value numbering. Int J Softw Tools Technol Transfer 26, 621–632 (2024). https://doi.org/10.1007/s10009-024-00762-1

Download citation

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-024-00762-1

Keywords

Navigation