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.
Similar content being viewed by others
References
AdaCore: GNATSAS CodePeer documentation (2024). https://www.adacore.com/static-analysis-suite/defects-and-vulnerability
Boulanger, J.-L. (ed.): Static Analysis of Software: The Abstract Interpretation. John Wiley & Sons, Inc. (2012)
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
Briggs, P., Cooper, K.D., Simpson, L.T.: Value numbering. Softw. Pract. Exp. 27, 701–724 (1997). ISSN 0038-0644
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
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
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
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
Rival, X., Yi, K.: Introduction to Static Analysis an Abstract Interpretation Perspective. The MIT Press, Cambridge (2020)
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
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
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
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.
Facebook: Pulse Infer Plugin 1.1.0. Facebook, Inc. (2023). https://fbinfer.com/docs/checker-pulse
Lemerre, M.: SSA Translation Is an Abstract Interpretation in Proc. ACM Program. Lang., vol. 7 (2023)
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
Lesbre, D., Lemerre, M.: Compiling with abstract interpretation. Proc. ACM Program. Lang. 8, 162 (2024). https://doi.org/10.1145/3656392
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
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
Corresponding author
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.
About this article
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
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10009-024-00762-1