KLEE visualization project

Abstract

En este proyecto se ha trabajado con una herramienta de ejecución simbólica llamada KLEE basada en LLVM IR. Esta herramienta se usa para el análisis de programas y generar pruebas de alta cobertura con el fin de depurarlos y encontrar errores. Esta herramienta genera archivos KTEST y KQUERY que son útiles para la comprensión del programa, pero en ninguno de ellos está la posibilidad de visualizar gráficamente la evolución de la memoria dinámica del programa analizado. Esto supone que la interpretación de los resultados obtenidos con KLEE sea una tarea compleja que requiere un conocimiento avanzado del formato de los archivos KTES y KQUERY. El objetivo principal de este proyecto consiste en extender la herramienta KLEE para generar gráficos que muestren la evolución de la memoria dinámica de un programa C/C++. Así pues, se generan una gran multitud de gráficos que muestran la evolución de los objetos de la memoria del programa hasta el alcanzar el grafico final. También, se muestra una animación de dicha evolución. Esto se consigue transformando esos archivos .DOT en .PNG para crear la animación, que es almacenada en un archivo .GIF. Para alcanzar dicho objetivo, se ha trabajado sobre las distintas clases que esta herramienta posee, añadiendo en cada una de ellas funcionalidades que permiten la obtención de resultados gráficos para facilitar la interpretación de los resultados. Con la nueva extensión de KLEE que se ha desarrollado en este trabajo, se consigue ayudar a los programadores a entender un programa y depurarlo, sobre todo en el ámbito relacionado con la evolución de la memoria dinámica durante del mismo, ya que con los archivos gráfico .DOT generados con la extensión de la herramienta, la compresión de los archivos creados por KLEE previamente es mucho más sencilla.

In this project work has been done with a symbolic execution tool called KLEE based on LLVM IR. This tool is used to analyze programs and generate high coverage tests in order to debug them and find bugs. This tool generates KTEST and KQUERY files that are useful for the understanding of the program, but none of them allows to visualize graphically the evolution of the dynamic memory of the analyzed program. This makes the interpretation of the results obtained with KLEE a complex task that requires an advanced knowledge of the KTES and KQUERY file format. The main objective of this project is to extend the KLEE tool to generate graphs showing the evolution of the dynamic memory of a C/C++ program. Thus, a large number of graphs are generated showing the evolution of the program's memory objects until the final graph is reached. Also, an animation of this evolution is shown. This is achieved by transforming these .DOT files into .PNG files to create the animation, which is stored in a .GIF file. To achieve this objective, work has been done on the different classes that this tool has, adding in each one of them functionalities that allow obtaining graphical results to facilitate the interpretation of the results. With the new KLEE extension that has been developed in this work, it is possible to help programmers to understand a program and debug it, especially in the area related to the evolution of the dynamic memory during the program, since with the .DOT graphic files generated with the extension of the tool, the compression of the files previously created by KLEE is much simpler.