Análisis de forma (análisis de programa)

En el análisis de programas , el análisis de forma es una técnica de análisis de código estático que descubre y verifica las propiedades de las estructuras de datos enlazadas y asignadas dinámicamente en programas informáticos (generalmente imperativos ). Se suele utilizar 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 programas Java , se puede utilizar para asegurar que un método de ordenación ordene correctamente una lista. En programas C , puede buscar lugares donde un bloque de memoria no se libera correctamente.

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

• Seguridad de la memoria: detección de fugas de memoria , desreferencias de punteros colgantes y detección de casos en los que un bloque de memoria se libera más de una vez. ^{[ 1 ] [ 2 ]}
• Detección de errores de índices fuera de los límites de la matriz
• Comprobar las propiedades del estado del tipo (por ejemplo, asegurarse de que un archivo sea open()antes de que sea read())
• Asegurar que un método para invertir una lista enlazada no introduzca ciclos en la lista ^{[ 2 ]}

El análisis de formas es una forma de análisis de punteros , aunque 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 un puntero puede apuntar (denominado conjunto de punteros). Desafortunadamente, estos análisis son necesariamente aproximados (ya que un análisis estático perfectamente preciso podría resolver el problema de la parada ). El análisis de formas puede determinar conjuntos de punteros más pequeños (y, por lo tanto, más precisos).

Considere el siguiente programa simple en C++ .

Artículo * artículos [ 10 ];for ( int i = 0 ; i < 10 ; ++ i ) { items [ i ] = new Item (...); // línea [1] }procesar_elementos ( elementos ); // línea [2]for ( int i = 0 ; i < 10 ; ++ i ) { delete items [ i ]; // línea [3] }

Este programa crea un array de objetos, los procesa de forma arbitraria y luego los elimina. Suponiendo que la process_itemsfunción no contenga errores, es evidente que el programa es seguro: nunca accede a memoria liberada y elimina todos los objetos que ha creado.

Desafortunadamente, la mayoría de los análisis de punteros tienen dificultades para analizar este programa con precisión. Para determinar los conjuntos a los que apunta, un análisis de punteros debe poder nombrar los objetos del 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 consiste en dar a todos los objetos asignados en una línea determinada del programa el mismo nombre. 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 instrucción por primera vez, el análisis determina que se está eliminando uno de los objetos llamados [1]. La segunda vez que se analiza la instrucción (ya que está en un bucle), el análisis advierte de un posible error: como no puede distinguir los objetos en el array, puede que la segunda instrucción deleteesté eliminando el mismo objeto que la primera delete. Esta advertencia es espuria, y el objetivo del análisis de forma es evitar este tipo de advertencias.

El análisis de formas supera los problemas del análisis de punteros mediante un sistema de nombres más flexible para los objetos. En lugar de asignar el mismo nombre a un objeto a lo largo de todo el programa, los objetos pueden cambiar de nombre según las acciones del programa. En ocasiones, varios objetos distintos con nombres diferentes pueden resumirse o fusionarse para que tengan el mismo nombre. Luego, cuando un objeto resumido está a punto de ser utilizado por el programa, se puede materializar ; es decir, el objeto resumido se divide en dos objetos con nombres distintos, uno que representa un solo 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 el programa está utilizando se representan mediante objetos materializados únicos, mientras que los objetos que no se utilizan se resumen.

El conjunto de objetos del ejemplo anterior se resume de distintas maneras en las líneas [1], [2] y [3]. En la línea [1], el conjunto se ha construido solo parcialmente. Los elementos del conjunto 0..i-1 contienen objetos construidos. El elemento i está a punto de construirse, y los elementos siguientes no están inicializados. El análisis de forma puede aproximar 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, como se muestra a continuación:

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 del array han sido inicializados:

En la línea [3], sin embargo, el elemento de la matriz ivuelve a estar en uso. 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 haya ejecutado).

Nótese 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.

• Análisis de alias
• Análisis de escape

• Neil D. Jones; Steven S. Muchnick (1982). «Un enfoque flexible para el análisis del flujo de datos interprocedimental y programas con estructuras de datos recursivas». Actas del 9.º simposio ACM SIGPLAN-SIGACT sobre Principios de los lenguajes de programación - POPL '82 . ACM. págs. 66-74 . doi : 10.1145/582153.582161 . ISBN  0897910656. S2CID 13266723 . 

• Mooly Sagiv ; Thomas Reps ; Reinhard Wilhelm (mayo de 2002). "Análisis de forma paramétrica mediante lógica trivalente" (PDF) . ACM Transactions on Programming Languages ​​and Systems . 24 (3). ACM: 217–298 . CiteSeerX 10.1.1.147.2132 . doi : 10.1145/292540.292552 . S2CID 101653 .  

• Wilhelm, Reinhard; Sagiv, Mooly; Reps, Thomas (2007). «Capítulo 12: Análisis de formas y aplicaciones». En Srikant, YN; Shankar, Priti (eds.). The Compiler Design Handbook: Optimizations and Machine Code Generation, Segunda edición . CRC Press. pp.  12–1–12–44. ISBN 978-1-4200-4382-2.