Improving Run-time Checking in Dynamic Programming Languages

Detectar comportamientos incorrectos en los programas es una parte importante en el ciclo de desarrollo de software. Es una tarea compleja y tediosa, especialmente en el contexto de los lenguajes dinámicos. Se han propuesto numerosas técnicas que ayudan en el proceso, entre las cuales nos hemos centrado en el uso de construcciones a nivel de lenguaje para describir el comportamiento esperado del programa, y en las herramientas necesarias para comparar el comportamiento real del programa en contraposición con el esperado, como, por ejemplo, analizadores/verificadores estáticos de código y entornos de verificación en tiempo de ejecución. En la práctica, sin embargo, el alto coste durante la ejecución hace que el uso de estas herramientas sea poco viable, especialmente para propiedades complejas. Esto reduce el interés en hacer comprobaciones en tiempo de ejecución desde el punto de vista de los programadores y programadoras, quienes esporádicamente permitirán comprobaciones de condiciones muy sencillas pero tenderán a desactivarlas para propiedades complejas. Algunos trabajos optan por limitar la expresividad del lenguaje de aserciones para reducir este coste. Con esta motivación, el objetivo de esta tésis es doble: - primero, pretendemos mejorar la expresividad del lenguaje de aserciones para reflejar todas las características relacionadas con el lenguaje de programación, incluyendo, por ejemplo, construcciones de orden superior, haciéndolo de forma que el/la programador/ a pueda escribir especificaciones sin necesidad de aprender o programar para ello; - al mismo tiempo, nuestra meta es comprobar de forma eficiente dichas especificaciones, reduciendo el coste asociado en tiempo de ejecución en la medida de lo posible y sin comprometer las garantías de seguridad que proporcionan dichas comprobaciones. Esta tésis presenta varias mejoras para la comprobación de especificaciones en tiempo de ejecución entre las que se encuentran: - un mecanismo discreto de memorización de resultados intermedios de comprobación, de forma que pueden ser reutilizados en el proceso de comprobación en lugar de recalcularlos; - un técnica que combina comprobación en tiempo de compilación y en tiempo de ejecución, que usa las propiedades de esta última como información adicional en tiempo de compilación, lo que implica que más propiedades se puedan comprobar estáticamente, aligerando el trabajo en tiempo de ejecución; - y otra técnica para mejorar la inferencia de estructuras durante el análisis estático de programas, que aprovecha las reglas de visibilidad de términos del entorno modular subyacente, lo que permite simplificar las comprobaciones de propiedades del programa consiguiendo un sobrecoste constante en casos relevantes. Finalmente, para atacar el problema de la expresividad limitada de los lenguajes de especificaciones, esta tésis se enfoca en el caso concreto de aportar especificaciones detalladas para rutinas de orden superior. Las técnicas y herramientas estudiadas en esta tésis se presentan, por concreción, en el entorno de comprobación en tiempo de ejecución Ciao. No obstante, los resultados son generales e independientes del sistema, y creemos que pueden trasladarse de forma sencilla a otros lenguajes de programación declarativos. Además, dados los avances en verificación en gran parte de los lenguajes de programación, incluyendo los imperativos, mediante la traducción a cláusulas de Horn y probando propiedades a este nivel, y el hecho de que este enfoque está totalmente soportado en el sistema Ciao, argumentamos que nuestros resultados se pueden adaptar fácilmente a un espectro mucho mas amplio de lenguajes. ----------ABSTRACT---------- Detecting incorrect program behaviors is an important part of the software development life cycle. It is also a complex and tedious one, in which dynamic languages bring special challenges. A number of techniques have been proposed to aid in the process, among which we center our attention on the use of language-level constructs to describe expected program behavior, and of associated tools to compare actual program behavior against expectations, such as static code analyzers/ verifiers and run-time verification frameworks. In practice, however, the run-time overhead associated with these tools often remains impractically high, specially for non-trivial properties, or complex data structure tests. This reduces the attractiveness of run-time checking to programmers, who may allow sporadic checking of very simple conditions, but will tend to turn off run-time checking for more complex properties in favor of faster execution. Some approaches even opt for limiting the expressiveness of the assertion language in order to reduce the overhead. Our research objective in this thesis is twofold: - first, we aim to enhance the expressiveness of the assertion language to reflect all the features of the related programming language, including, e.g., higher-order constructs, and to do so in a way that allows the programmer to write precise program specifications while not imposing a learning or programming burden on them; - at the same time, our goal is to efficiently check specifications, mitigating the associated run-time overhead as much as possible without compromising the safety guarantees that the checks provide. With respect to checking specifications efficiently this dissertation presents several improvements for run-time specification checking, including: - a mechanism for unobtrusive caching of intermediate run-time checking results so that they can be re-used in the checking process instead of being re-evaluated, contributing to undesirable (and unnecessary) run-time overhead; - a technique of combining compile- and run-time checking in a way that uses the properties from the program specification as an additional information source during static specification checking, which results in more properties checked statically and fewer of them turned into run-time checks; - and another technique for improving term shape inference during static program analysis, exploiting term visibility rules of the underlying module system, which allows to simplify property checks in a program in a way that constant run-time overhead is achievable in relevant cases. Finally, to address the limited expressiveness of the specification languages, this dissertation targets the concrete case of providing detailed specifications for higher-order program routines. The techniques and tools discussed in this thesis are presented for concreteness in the context of the Ciao run-time checking framework. Nevertheless, these results are general and system-independent, and we believe they can be straightforwardly transferred to the contexts of other declarative languages. In addition, given the recent advances in verification of a wide class of programming languages, including imperative ones, by translation into Horn clauses and proving properties at this level, and the fact that this approach is fully supported in the Ciao system, we argue that our results can easily be adapted to a much broader spectrum of languages