SymC++: un depurador simbólico para C++

Abstract

En este proyecto se estudia y desarrolla una herramienta basada en depuración simbólica que permite conocer el funcionamiento de programas informáticos sin ser ejecutados en base a observar todas sus posibles ramas de ejecución (hasta un cierto nivel), así como los correspondientes pares entrada-salida. Dicha herramienta está ideada con la idea de ayudar a los estudiantes de iniciación a la programación, y en general a programadores inexpertos a la hora de razonar acerca de la corrección de sus programas. El núcleo de la herramienta está basado en la ejecución simbólica, una de las técnicas más potentes para hacer estudios estáticos del comportamiento de los programas. La ejecución simbólica consiste en el análisis de un programa usando valores simbólicos (o variables) en lugar de valores concretos. Esto permite comprender la ejecución del programa gracias a la observación de los comportamientos de sus diferentes caminos de ejecución, así como determinar las condiciones que deben ser verificadas por los datos de entrada para obtener un resultado particular, y la relación entre los valores ingresados y producidos en la ejecución de un programa. La herramienta desarrollada, denominada SymC++, recibe una serie de parámetros de entrada sobre la función a testear, partiendo de un código C++, obteniendo así información de las distintas ramas generadas. Dichos resultados se generan en formato XML lo cual facilita la portabilidad y escalabilidad del proyecto ofreciendo un depurador que se puede adaptar a diferentes interfaces de usuario.

This project studies and develops a tool based on symbolic debugging that allows reasoning about programs behavior statically, i.e., without being executed, by means of observing all possible branches of execution (up to a level) and their corresponding input-output behaviors. The tool is designed with the idea of helping students of introduction to programming, and, in general, inexperienced developers to reason about the correctness of their programs. The core of the tool is based on symbolic execution, one of the most powerful technologies for statically studying programs behavior. Symbolic execution consists in executing a program using symbolic values (or variables) instead of concrete values. This allows understanding the program execution by means of observing the behavior of the different execution branches and to determine the conditions that must be verified by the input data to obtain a particular result, and the relationship between the input and produced values in the execution of the program. The developed tool, called SymC++, receives a set of input parameters of the function to be tested (a C++ function), and obtains information about the generated execution branches. The results are output in XML format, which facilitates portability and scalability, hence providing a debugger that can be adapted to different user interfaces.