Abstract
Array access out of bounds is a typical programming error. From the ’70s, static analysis has been used to identify where such errors actually occur at runtime, through abstract interpretation into linear constraints. However, feasibility and scalability to modern object-oriented code has not been established yet. This article builds on previous work on linear constraints and shows that the result does not scale, when polyhedra implement the linear constraints, while the more abstract zones scale to the analysis of medium-size applications. Moreover, this article formalises the inclusion of symbolic expressions in the constraints and shows that this improves its precision. Expressions are automatically selected on-demand. The resulting analysis applies to code with dynamic memory allocation and arrays held in expressions. It is sound, also in the presence of arbitrary side-effects. It is fully defined in the abstract interpretation framework and does not use any code instrumentation. Its proof of correctness, its implementation inside the commercial Julia analyzer and experiments on third-party code complete the work.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
https://sv-comp.sosy-lab.org/2018/results/results-verified/META_MemSafety.table. See, in particular, the results for tools Map2Check, Symbiotic and Ultimate.
- 2.
- 3.
- 4.
- 5.
In Java bytecode, local variables are identified by number and their amount varies across program points. Source code variable names are not part of the bytecode.
- 6.
Line numbers, conveniently starting at 1, do not correspond to the actual line numbering of the examples, which are simplified and shortened w.r.t. their original code.
- 7.
We assume that public entries can be called with any values, as also done in [15].
References
Albert, E., Arenas, P., Genaim, S., Puebla, G.: Field-sensitive value analysis by field-insensitive analysis. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 370–386. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-05089-3_24
Albert, E., Arenas, P., Genaim, S., Puebla, G., Ramírez Deantes, D.V.: From object fields to local variables: a practical approach to field-sensitive analysis. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 100–116. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15769-1_7
Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1–2), 3–21 (2008)
Bagnara, R., Hill, P.M., Zaffanella, E.: Applications of polyhedral computations to the analysis and verification of hardware and software systems. Theoret. Comput. Sci. 410(46), 4672–4691 (2009)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principles of Programming Languages (POPL), pp. 238–252 (1977)
Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The Astrée analyzer. In: European Symposium on Programming (ESOP), pp. 21–30 (2005)
Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Rival, X.: Why does Astrée scale up? Formal Methods Syst. Des. 35(3), 229–264 (2009)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Principles of Programming Languages (POPL), Tucson, Arizona, USA, pp. 84–96, January 1978
Lindholm, T., Yellin, F., Bracha, G., Buckley, A.: The Java\(^{TM}\) Virtual Machine Specification. Financial Times/Prentice Hall, Upper Saddle River (2013)
Miné, A.: Weakly relational numerical abstract domains. Ph.D. thesis, École Polytechnique, Paris, France (2004)
Miné, A.: Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics. In: Languages, Compilers, and Tools for Embedded Systems (LCTES), Ottawa, Ontario, Canada, pp. 54–63 (2006)
Miné, A.: The octagon abstract domain. High.-Order Symbolic Comput. 19(1), 31–100 (2006)
Nikolic, D., Spoto, F.: Reachability analysis of program variables. Trans. Program. Lang. Syst. 35(4), 14:1–14:68 (2013)
Payet, É., Spoto, F.: Index Checking Experiments (2017). https://github.com/spoto/Index-Checker-Experiments.git
Santino, J.: Enforcing correct array indexes with a type system. In: Foundations of Software Engineering (FSE), pp. 1142–1144. ACM, Seattle (2016)
Secci, S., Spoto, F.: Pair-sharing analysis of object-oriented programs. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 320–335. Springer, Heidelberg (2005). https://doi.org/10.1007/11547662_22
Spoto, F.: The Julia static analyzer for Java. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 39–57. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-53413-7_3
Spoto, F., Jensen, T.P.: Class analyses as abstract interpretations of trace semantics. Trans. Program. Lang. Syst. 25(5), 578–630 (2003)
Spoto, F., Mesnard, F., Payet, É.: A termination analyzer for Java bytecode based on path-length. Trans. Program. Lang. Syst. 32(3), 8:1–8:70 (2010)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Payet, É., Spoto, F. (2018). Checking Array Bounds by Abstract Interpretation and Symbolic Expressions. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds) Automated Reasoning. IJCAR 2018. Lecture Notes in Computer Science(), vol 10900. Springer, Cham. https://doi.org/10.1007/978-3-319-94205-6_46
Download citation
DOI: https://doi.org/10.1007/978-3-319-94205-6_46
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-94204-9
Online ISBN: 978-3-319-94205-6
eBook Packages: Computer ScienceComputer Science (R0)