A scalable static analysis framework for reliable program development exploiting incrementality and modularity

Resumen

Automatic static analysis tools allow inferring properties about software without executing it and without the need for human interaction. When these tools are based on formal methods, the properties are guaranteed to hold and come with a mathematical proof. The usage of these tools during the coding, testing, and maintenance phases of the software development cycle helps reduce efforts in terms of time and cost, as they contribute to the early detection of bugs, automatic optimizations, or automatic documentation. The increasing importance of the reliability of evolving software is evidenced by the current number of tools and on-line platforms for continuous integration and deployment. In this setting, when changes happen fast, analysis tools are only useful if they are precise and, at the same time, scalable enough to provide results before the next change happens. In this thesis we study scalable analyses in the context of abstract interpretation. Since a way to improve scalability is to perform coarser abstractions, we first inspect what effect this may have in effectively proving the absence of bugs. Second, we present a framework for scalable static analyses which is generic, that is, independent of the data abstraction of the program. We present several algorithms for incrementally reanalyzing whole programs in a context-sensitive manner, reusing as much as possible previous analysis results. A key novel aspect of the approach is to take advantage of the modular structure of programs, typically as defined by the programmer, while keeping a fine-grained relation between the analysis result and the source program. Additionally, we present a mechanism for the programmer to help the analyzer in terms of precision and performance by means of assertions. We show that these assertions together with incremental analysis are specially useful when analyzing generic code. All these algorithms have been implemented and evaluated for different abstract domains within the CiaoPP framework. Lastly, we present an application of the analysis framework to perform on-the-fly assertion checking, providing continuous and almost instantaneous feedback to the programmer as the code is written. Here the incrementality and modular nature of the presented algorithms, and the locality of the changes, are key to achieving fast response times. ----------RESUMEN---------- Las herramientas automáticas de análisis estático permiten inferir propiedades del software sin ejecutarlo y sin necesidad de intervención humana. Si dichas herramientas se basan en métodos formales, éstas proporcionan garantías matemáticas de que las propiedades se cumplen. El uso de estas herramientas durante las fases de codificación, prueba y mantenimiento del ciclo de desarrollo del software ayuda a reducir esfuerzo en términos de tiempo y coste, ya que contribuye a la detección temprana de errores, a la optimización automática y a la documentación automática. La creciente importancia de la fiabilidad de un software en constante evolución se ha puesto de manifiesto por el número de herramientas y plataformas disponibles on-line para la integración y despliegue continuos de software. En este contexto, en el que los cambios ocurren rápido, las herramientas de análisis son útiles sólo si son precisas y lo suficientemente escalables como para proporcionar resultados más rápidamente de lo que ocurren los cambios. En esta tesis estudiamos análisis escalables en el ámbito de la interpretación abstracta. Dado que una forma de mejorar la escalabilidad es generalizar las abstracciones, primero estudiamos qué efecto tienen estas generalizaciones en la eficacia del dominio para demostrar la ausencia de errores. Segundo, presentamos un marco para el análisis estático que es genérico, es decir, independiente de la abstracción de los datos del programa. Presentamos diferentes algorithmos para reanalizar incrementalmente programas enteros, de forma sensible al contexto, reutilizando lo máximo posible un resultado anterior. Un aspecto novedoso y clave de nuestro enfoque es aprovechar la estructura modular de los programas, típicamente definida por la persona programadora, pero manteniendo una relación precisa entre el programa original y el resultado del análisis. Adicionalmente, presentamos un mecanismo para que la programadora pueda ayudar al analizador en términos de precisión y rendimiento mediante aserciones. Mostramos que estas aserciones junto con un análisis incremental son especialmente útiles para analizar código genérico. Todos los algoritmos han sido implementados y evaluados para diferentes dominios abstractos dentro de la herramienta CiaoPP. Por último, presentamos una aplicación de este marco de análisis para realizar comprobación de aserciones en tiempo de compilación al vuelo, de forma que se proporciona una retroalimentación continua a la programadora mientras escribe el código. Aquí, la naturaleza incremental y modular de los algoritmos, además de la localización de los cambios, son clave para lograr tiempos de respuesta rápidos.