stringtranslate.com

Análisis de formas (análisis de programas)

En el análisis de programas , el análisis de formas es una técnica de análisis de código estático que descubre y verifica las propiedades de estructuras de datos enlazadas y asignadas dinámicamente en programas informáticos (normalmente imperativos ). Normalmente se utiliza en tiempo de compilación para encontrar errores de software o para verificar las propiedades de corrección de alto nivel de los programas. En los programas Java , se puede utilizar para garantizar que un método de ordenación ordena correctamente una lista. En los programas C, puede buscar lugares en los que un bloque de memoria no se libera correctamente.

Aplicaciones

El análisis de formas se ha aplicado a una variedad de problemas:

Ejemplo

El análisis de formas es una forma de análisis de punteros , aunque es más preciso que el análisis de punteros típico. El análisis de punteros intenta determinar el conjunto de objetos a los que puede apuntar un puntero (llamado el conjunto de puntos a los que apunta el puntero). Desafortunadamente, estos análisis son necesariamente aproximados (ya que un análisis estático perfectamente preciso podría resolver el problema de detención ). El análisis de formas puede determinar conjuntos de puntos a los que apuntar más pequeños (más precisos).

Considere el siguiente programa C++ simple.

Elemento * elementos [ 10 ]; para ( int i = 0 ; i < 10 ; ++ i ) { elementos [ i ] = new Elemento (...); // línea [1] } process_items ( elementos ); // línea [2] para ( int i = 0 ; i < 10 ; ++ i ) { eliminar elementos [ i ]; // línea [3] }                            

Este programa crea una matriz de objetos, los procesa de alguna manera arbitraria y luego los elimina. Suponiendo que la process_itemsfunción no tiene errores, está claro que el programa es seguro: nunca hace referencia a la memoria liberada y elimina todos los objetos que ha construido.

Desafortunadamente, la mayoría de los análisis de punteros tienen dificultades para analizar este programa con precisión. Para determinar los conjuntos de puntos a los que apunta, un análisis de punteros debe poder nombrar los objetos de un programa. En general, los programas pueden asignar un número ilimitado de objetos; pero para terminar, un análisis de punteros solo puede usar un conjunto finito de nombres. Una aproximación típica es dar el mismo nombre a todos los objetos asignados en una línea dada del programa. En el ejemplo anterior, todos los objetos construidos en la línea [1] tendrían el mismo nombre. Por lo tanto, cuando deletese analiza la declaración por primera vez, el análisis determina que se está eliminando uno de los objetos nombrados [1]. La segunda vez que se analiza la declaración (ya que está en un bucle), el análisis advierte de un posible error: dado que no puede distinguir los objetos en la matriz, puede ser que el segundo deleteesté eliminando el mismo objeto que el primero delete. Esta advertencia es falsa y el objetivo del análisis de formas es evitar tales advertencias.

Resumen y materialización

El análisis de formas supera los problemas del análisis de punteros al utilizar un sistema de nombres más flexible para los objetos. En lugar de darle a un objeto el mismo nombre en todo el programa, los objetos pueden cambiar de nombre según las acciones del programa. A veces, se pueden resumir o fusionar varios objetos distintos con nombres diferentes para que tengan el mismo nombre. Luego, cuando el programa va a utilizar un objeto resumido, se puede materializar , es decir, el objeto resumido se divide en dos objetos con nombres distintos, uno que representa un único objeto y el otro que representa los objetos resumidos restantes. La heurística básica del análisis de formas es que los objetos que utiliza el programa se representan mediante objetos materializados únicos, mientras que los objetos que no se utilizan se resumen.

La matriz de objetos del ejemplo anterior se resume de forma independiente en las líneas [1], [2] y [3]. En la línea [1], la matriz se ha construido solo parcialmente. Los elementos de la matriz 0..i-1 contienen objetos construidos. El elemento de la matriz i está a punto de construirse y los siguientes elementos no están inicializados. El análisis de forma puede aproximarse a esta situación utilizando un resumen para el primer conjunto de elementos, una ubicación de memoria materializada para el elemento i y un resumen para las ubicaciones restantes no inicializadas, de la siguiente manera:

Una vez finalizado el bucle, en la línea [2], no es necesario mantener nada materializado. El análisis de forma determina en este punto que todos los elementos de la matriz se han inicializado:

Sin embargo, en la línea [3], el elemento de la matriz ise vuelve a utilizar. Por lo tanto, el análisis divide la matriz en tres segmentos como en la línea [1]. Esta vez, sin embargo, el primer segmento anterior ise ha eliminado y los elementos restantes siguen siendo válidos (suponiendo que la deleteinstrucción aún no se ha ejecutado).

Tenga en cuenta que, en este caso, el análisis reconoce que el puntero en el índice iaún no se ha eliminado. Por lo tanto, no advierte de una doble eliminación.

Véase también

Referencias

  1. ^ Rinetzky, Noam; Sagiv, Mooly (2001). "Análisis de forma interprocedimental para programas recursivos" (PDF) . Construcción de compiladores. Apuntes de clase en informática. Vol. 2027. págs. 133–149. doi :10.1007/3-540-45306-7_10. ISBN 978-3-540-41861-0.
  2. ^ ab Berdine, Josh; Calcagno, Cristiano; Cook, Byron; Distefano, Dino; o'Hearn, Peter W.; Wies, Thomas; Yang, Hongseok (2007). "Análisis de forma para estructuras de datos compuestas" (PDF) . Verificación asistida por computadora . Apuntes de clase en informática. Vol. 4590. págs. 178–192. doi :10.1007/978-3-540-73368-3_22. ISBN 978-3-540-73367-6.

Bibliografía