Checking Array Bounds by Abstract Interpretation and Symbolic Expressions
| Autor: | Fausto Spoto, Étienne Payet |
|---|---|
| Přispěvatelé: | Department of Computer Science [Verona] (UNIVR | DI), University of Verona (UNIVR), Laboratoire d'Informatique et de Mathématiques (LIM), Université de La Réunion (UR), Didier Galmiche, Stephan Schulz, Roberto Sebastiani |
| Jazyk: | angličtina |
| Rok vydání: | 2018 |
| Předmět: |
Correctness
Scale (ratio) C dynamic memory allocation Computer science Static Analysis Array 020207 software engineering 0102 computer and information sciences 02 engineering and technology Static analysis Static Analysis Array Linear Constraints Abstract interpretation 01 natural sciences Polyhedron 010201 computation theory & mathematics Linear Constraints Scalability 0202 electrical engineering electronic engineering information engineering Code (cryptography) [INFO]Computer Science [cs] Algorithm |
| Zdroj: | Lecture Notes in Computer Sciences 9th International Joint Conference on Automated Reasoning (IJCAR'18) 9th International Joint Conference on Automated Reasoning (IJCAR'18), Jul 2018, Oxford, United Kingdom. pp.706-722, ⟨10.1007/978-3-319-94205-6_46⟩ Automated Reasoning ISBN: 9783319942049 IJCAR |
| Popis: | International audience; 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 instrumen-tation. Its proof of correctness, its implementation inside the commercial Julia analyzer and experiments on third-party code complete the work. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|