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 vinculadas y asignadas dinámicamente en programas informáticos (generalmente imperativos ). Por lo general, se usa 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 clasificación clasifique correctamente una lista. Para los programas C, puede buscar lugares donde un bloque de memoria no se libere correctamente.
Aplicaciones
El análisis de forma se ha aplicado a una variedad de problemas:
- Seguridad de la memoria: encontrar pérdidas de memoria , eliminar referencias de punteros colgantes y descubrir casos en los que un bloque de memoria se libera más de una vez. [1] [2]
- Encontrar errores fuera de límites de matriz [ cita requerida ]
- Comprobación de las propiedades de estado de tipo (por ejemplo, asegurarse de que un archivo esté
open()
antes queread()
) [ cita requerida ] - Asegurarse de que un método para invertir una lista enlazada no introduzca ciclos en la lista [2]
- Verificar que un método de clasificación devuelve un resultado ordenado [ cita requerida ]
Ejemplo
El análisis de forma es una forma de análisis de puntero , aunque es más preciso que el análisis de puntero típico. El análisis de puntero intenta determinar el conjunto de objetos a los que puede apuntar un puntero (denominado conjunto de puntos a del puntero). Desafortunadamente, estos análisis son necesariamente aproximados (ya que un análisis estático perfectamente preciso podría resolver el problema de la detención ). El análisis de forma puede determinar conjuntos de puntos a más pequeños (más precisos).
Considere el siguiente programa simple de C ++.
Elemento * elementos [ 10 ]; for ( int i = 0 ; i < 10 ; ++ i ) { items [ i ] = new Item (...); // 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_items
función está libre de errores, está claro que el programa es seguro: nunca hace referencia a la memoria liberada y borra 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 conjuntos de puntos a, un análisis de puntero 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 puntero 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 determinada del programa. En el ejemplo anterior, todos los objetos construidos en la línea [1] tendrían el mismo nombre. Por lo tanto, cuando la delete
declaración se analiza por primera vez, el análisis determina que uno de los objetos nombrados [1] está siendo eliminado. La segunda vez que se analiza el enunciado (ya que está en un bucle) el análisis advierte de un posible error: al no poder distinguir los objetos del arreglo, puede ser que el segundo delete
esté borrando el mismo objeto que el primero delete
. Esta advertencia es falsa y el objetivo del análisis de forma es evitar tales advertencias.
Resumen y materialización
El análisis de formas supera los problemas del análisis de punteros mediante el uso de un sistema de nombres más flexible para los objetos. En lugar de darle a un objeto el mismo nombre en todo un programa, los objetos pueden cambiar de nombre dependiendo de 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 un objeto resumido está a punto de ser utilizado por el programa, puede materializarse , es decir, el objeto resumido se divide en dos objetos con nombres distintos, uno que representa un objeto único 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 utilizando objetos materializados únicos, mientras que los objetos que no se utilizan se resumen.
La matriz de objetos del ejemplo anterior se resume de forma separada en las líneas [1], [2] y [3]. En la línea [1], la matriz se ha construido solo en parte. Los elementos de la matriz 0..i-1 contienen objetos construidos. El elemento de matriz i está a punto de construirse y los siguientes elementos 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 iy un resumen para las ubicaciones restantes no inicializadas, de la siguiente manera:
0 .. i-1 | I | i + 1 .. 9 |
puntero al objeto construido (resumen) | no inicializado | sin inicializar (resumen) |
Una vez que termina el ciclo, en la línea [2], no hay necesidad de mantener nada materializado. El análisis de forma determina en este punto que todos los elementos de la matriz se han inicializado:
0 .. 9 |
puntero al objeto construido (resumen) |
En la línea [3], sin embargo, el elemento de matriz i
está en uso nuevamente. 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 i
se ha eliminado y los elementos restantes siguen siendo válidos (suponiendo que la delete
declaración no se haya ejecutado todavía).
0 .. i-1 | I | i + 1 .. 9 |
gratis (resumen) | puntero al objeto construido | puntero al objeto construido (resumen) |
Observe que en este caso, el análisis reconoce que el puntero en el índice i
aún no se ha eliminado. Por lo tanto, no advierte de una doble eliminación.
Ver también
Referencias
- ^ Rinetzky, Noam; Sagiv, Mooly (2001). "Análisis de forma interprocedimiento para programas recursivos" (PDF) . Construcción del compilador . Apuntes de conferencias en Ciencias de la Computación. 2027 . págs. 133-149 . doi : 10.1007 / 3-540-45306-7_10 . ISBN 978-3-540-41861-0.
- ^ a b Berdine, Josh; Calcagno, Cristiano; Cook, Byron; Distefano, Dino; o'Hearn, Peter W .; Wies, Thomas; Yang, Hongseok (2007). "Análisis de formas para estructuras de datos compuestos" (PDF) . Verificación asistida por computadora . Apuntes de conferencias en Ciencias de la Computación. 4590 . págs. 178-192. doi : 10.1007 / 978-3-540-73368-3_22 . ISBN 978-3-540-73367-6.
Bibliografía
- Neil D. Jones; Steven S. Muchnick (1982). "Un enfoque flexible para el análisis de flujo de datos entre procedimientos y programas con estructuras de datos recursivas". POPL '82 Actas del 9º Simposio ACM SIGPLAN-SIGACT sobre principios de lenguajes de programación . ACM: 66–74. doi : 10.1145 / 582153.582161 . ISBN 0897910656.
- Mooly Sagiv ; Thomas Reps ; Reinhard Wilhelm (mayo de 2002). "Análisis de formas paramétricas mediante lógica de 3 valores" (PDF) . Transacciones ACM sobre lenguajes y sistemas de programación . ACM. 24 (3): 217-298. CiteSeerX 10.1.1.147.2132 . doi : 10.1145 / 292540.292552 .
- Wilhelm, Reinhard; Sagiv, Mooly; Representantes, Thomas (2007). "Capítulo 12: Análisis de formas y aplicaciones". En Srikant, YN; Shankar, Priti (eds.). El manual de diseño del compilador: optimizaciones y generación de código de máquina, segunda edición . Prensa CRC. págs. 12–1–12–44. ISBN 978-1-4200-4382-2.