Abstract
Static analyses are mostly designed to show the absence of bugs: if the analysis reports no alarms then the program won’t exhibit any unwanted behaviours. To this aim they manipulate over-approximations of program semantics and, inevitably, they often report some false alarms. Recently, O’Hearn proposed Incorrectness Logic, that is based on under-approximations, as a formal method to find bugs that only reports true alarms. In this paper we aim to answer one important question raised by O’Hearn, namely which role can Abstract Interpretation play for the development of under-approximate tools for bug catching. In principle, Abstract Interpretation based static analyses can be defined for computing over-approximations as well as under-approximations, but in practice, most techniques exploited the former while few attempts developed the latter. To show why it is difficult to design effective under-approximation abstract domains, we first propose the new definitions of non emptying functions and highly surjective function family and then we formally prove the limits of under-approximation analysis by showing the non existence of abstract domains able to approximate such functions in a non trivial way. Our results outline the limits of under-approximation Abstract Interpretation and clarify, for the first time, why over- and under- approximation analyzers exhibited such a different development.
Research supported by MIUR PRIN Project 201784YSZ5 ASPRA–Analysis of Program Analyses.
Chapter PDF
Similar content being viewed by others
References
Boulanger, J.L. (ed.): Static Analysis of Software: The Abstract Interpretation. Wiley (2011)
Bourdoncle, F.: Abstract debugging of higher-order imperative languages. SIGPLAN Not. 28(6), 46–55 (Jun 1993). https://doi.org/10.1145/173262.155095
Calcagno, C., Distefano, D., Dubreil, J., Gabi, D., Hooimeijer, P., Luca, M., O’Hearn, P.W., Papakonstantinou, I., Purbrick, J., Rodriguez, D.: Moving fast with software verification. In: Proc. NFM’15. LNCS, vol. 9058, pp. 3–11. Springer (2015). https://doi.org/10.1007/978-3-319-17524-9_1
Cousot, P.: Principles of Abstract Interpretation. MIT Press (2021)
Cousot, P., Cousot, R.: Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and per analysis of functional languages). In: Proceedings of 1994 IEEE International Conference on Computer Languages (ICCL’94). pp. 95–112 (1994). https://doi.org/10.1109/ICCL.1994.288389
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. p. 238–252. POPL ’77, Association for Computing Machinery, New York, NY, USA (1977). https://doi.org/10.1145/512950.512973
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. p. 269–282. POPL ’79, Association for Computing Machinery, New York, NY, USA (1979). https://doi.org/10.1145/567752.567778
Cousot, P., Cousot, R., Fähndrich, M., Logozzo, F.: Automatic inference of necessary preconditions. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013. Proceedings. Lecture Notes in Computer Science, vol. 7737, pp. 128–148. Springer (2013). https://doi.org/10.1007/978-3-642-35873-9_10
Cousot, P., Cousot, R., Logozzo, F.: Precondition inference from intermittent assertions and application to contracts on collections. In: Jhala, R., Schmidt, D.A. (eds.) Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings. Lecture Notes in Computer Science, vol. 6538, pp. 150–168. Springer (2011). https://doi.org/10.1007/978-3-642-18275-4_12
Distefano, D., Fähndrich, M., Logozzo, F., O’Hearn, P.W.: Scaling static analyses at Facebook. Commun. ACM 62(8), 62–70 (2019). https://doi.org/10.1145/3338112
Filé, G., Ranzato, F.: Improving abstract interpretations by systematic lifting to the powerset. In: Proceedings of the 1994 International Symposium on Logic Programming. p. 655–669. ILPS ’94, MIT Press, Cambridge, MA, USA (1994)
Floyd, R.W.: Assigning meanings to programs. Proceedings of Symposium on Applied Mathematics 19, 19–32 (1967)
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (Oct 1969). https://doi.org/10.1145/363235.363259
Lev-Ami, T., Sagiv, M., Reps, T., Gulwani, S.: Backward analysis for inferring quantified preconditions. Tr-2007-12-01, Tel Aviv University (2007)
Miné, A.: Backward under-approximations in numeric abstract domains to automatically infer sufficient program conditions. Sci. Comput. Program. 93, 154–182 (Nov 2014). https://doi.org/10.1016/j.scico.2013.09.014
Miné, A.: Tutorial on static inference of numeric invariants by abstract interpretation. Found. Trends Program. Lang. 4(3–4), 120–372 (Dec 2017). https://doi.org/10.1561/2500000034
Nielson, F., Nielson, H., Hankin, C.: Principles of Program Analysis. Springer (2010). https://doi.org/10.1007/978-3-662-03811-6
O’Hearn, P.W.: Continuous reasoning: Scaling the impact of formal methods. In: Proc. LICS’18. p. 13–25. ACM (2018). https://doi.org/10.1145/3209108.3209109
O’Hearn, P.W.: Incorrectness logic. Proc. ACM Program. Lang. 4(POPL) (Dec 2019). https://doi.org/10.1145/3371078
Raad, A., Berdine, J., Dang, H.H., Dreyer, D., O’Hearn, P.W., Villard, J.: Local reasoning about the presence of bugs: Incorrectness separation logic. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12225, pp. 225–252. Springer (2020). https://doi.org/10.1007/978-3-030-53291-8_14
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings. pp. 55–74. IEEE Computer Society (2002). https://doi.org/10.1109/LICS.2002.1029817
Rival, X., Yi, K.: Introduction to Static Analysis – An Abstract Interpretation Perspective. MIT Press (2020)
Sadowski, C., Aftandilian, E., Eagle, A., Miller-Cushon, L., Jaspan, C.: Lessons from building static analysis tools at Google. Commun. ACM 61(4), 58–66 (Mar 2018). https://doi.org/10.1145/3188720
Schmidt, D.A.: A calculus of logical relations for over- and underapproximating static analyses. Sci. Comput. Program. 64(1), 29–53 (2007). https://doi.org/10.1016/j.scico.2006.03.008
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2022 The Author(s)
About this paper
Cite this paper
Ascari, F., Bruni, R., Gori, R. (2022). Limits and difficulties in the design of under-approximation abstract domains. In: Bouyer, P., Schröder, L. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2022. Lecture Notes in Computer Science, vol 13242. Springer, Cham. https://doi.org/10.1007/978-3-030-99253-8_2
Download citation
DOI: https://doi.org/10.1007/978-3-030-99253-8_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-99252-1
Online ISBN: 978-3-030-99253-8
eBook Packages: Computer ScienceComputer Science (R0)