En informática , el análisis de asignación definitiva es un análisis de flujo de datos utilizado por los compiladores para garantizar de forma conservadora que una variable o ubicación siempre se asigne antes de su uso.
En los programas C y C++ , una fuente de errores particularmente difíciles de diagnosticar es el comportamiento no determinista que resulta de la lectura de variables no inicializadas ; este comportamiento puede variar entre plataformas, compilaciones e incluso de una ejecución a otra.
Existen dos formas comunes de resolver este problema. Una es asegurarse de que todas las ubicaciones se escriban antes de leerlas. El teorema de Rice establece que este problema no se puede resolver en general para todos los programas; sin embargo, es posible crear un análisis conservador (impreciso) que acepte solo programas que satisfagan esta restricción, al tiempo que rechaza algunos programas correctos, y el análisis de asignación definitiva es un análisis de este tipo. Las especificaciones del lenguaje de programación Java [1] y C# [2] requieren que el compilador informe un error de tiempo de compilación si el análisis falla. Ambos lenguajes requieren una forma específica del análisis que se explica en detalle meticuloso. En Java, este análisis fue formalizado por Stärk et al., [3] y algunos programas correctos son rechazados y deben modificarse para introducir asignaciones innecesarias explícitas. En C#, este análisis fue formalizado por Fruja, y es preciso y sólido, en el sentido de que todas las variables asignadas a lo largo de todas las rutas de flujo de control se considerarán asignadas definitivamente. [4] El lenguaje Cyclone también requiere que los programas pasen un análisis de asignación definido, pero sólo en variables con tipos de puntero, para facilitar la portabilidad de programas C. [5]
La segunda forma de resolver el problema es inicializar automáticamente todas las ubicaciones con un valor fijo y predecible en el punto en el que se definen, pero esto introduce nuevas asignaciones que pueden dificultar el rendimiento. En este caso, el análisis de asignaciones definidas permite una optimización del compilador en la que se pueden eliminar las asignaciones redundantes (asignaciones seguidas únicamente por otras asignaciones sin posibles lecturas intermedias). En este caso, no se rechaza ningún programa, pero los programas para los que el análisis no reconoce la asignación definida pueden contener una inicialización redundante. La Infraestructura del Lenguaje Común se basa en este enfoque. [6]
Se puede decir que una variable o ubicación está en uno de tres estados en cualquier punto dado del programa:
Lo siguiente se basa en la formalización de Fruja del análisis de asignación definida intraprocedimental (método único) de C#, que es responsable de garantizar que todas las variables locales se asignen antes de que se utilicen. [4] Realiza simultáneamente el análisis de asignación definida y la propagación constante de valores booleanos. Definimos cinco funciones estáticas:
Proporcionamos ecuaciones de flujo de datos que definen los valores de estas funciones en varias expresiones y declaraciones, en términos de los valores de las funciones en sus subexpresiones sintácticas. Supongamos por el momento que no hay declaraciones goto , break , continue , return o de manejo de excepciones . A continuación se muestran algunos ejemplos de estas ecuaciones:
Al comienzo del método, no se asignan variables locales de forma definitiva. El verificador itera repetidamente sobre el árbol de sintaxis abstracta y utiliza las ecuaciones de flujo de datos para migrar información entre los conjuntos hasta que se pueda alcanzar un punto fijo . Luego, el verificador examina el conjunto anterior de cada expresión que utiliza una variable local para asegurarse de que contiene esa variable.
El algoritmo se complica por la introducción de saltos de flujo de control como goto , break , continue , return y el manejo de excepciones. Cualquier instrucción que pueda ser el destino de uno de estos saltos debe intersecar su conjunto anterior con el conjunto de variables asignadas definitivamente en la fuente del salto. Cuando se introducen estos, el flujo de datos resultante puede tener múltiples puntos fijos, como en este ejemplo:
int i = 1 ; Yo : ir a L ; Como la etiqueta L se puede alcanzar desde dos ubicaciones, la ecuación de flujo de control para goto dicta que antes de (2) = después de (1) se intersecan antes de (3). Pero antes de (3) = antes de (2), por lo que antes de (2) = después de (1) se intersecan antes de (2). Esto tiene dos puntos fijos para antes de (2), {i} y el conjunto vacío. Sin embargo, se puede demostrar que debido a la forma monótona de las ecuaciones de flujo de datos, existe un único punto fijo máximo (punto fijo de mayor tamaño) que proporciona la mayor información posible sobre las variables asignadas definitivamente. Dicho punto fijo máximo (o máximo) se puede calcular mediante técnicas estándar; consulte análisis de flujo de datos .
Un problema adicional es que un salto de flujo de control puede hacer que ciertos flujos de control sean inviables; por ejemplo, en este fragmento de código, la variable i se asigna definitivamente antes de ser utilizada:
entero yo ; si ( j < 0 ) retorna ; de lo contrario i = j ; imprimir ( i );La ecuación de flujo de datos para if dice que after (2) = after( return ) intersecta after( i = j ). Para que esto funcione correctamente, definimos after ( e ) = vars ( e ) para todos los saltos de flujo de control; esto es vacuamente válido en el mismo sentido en que la ecuación false ( true ) = vars ( e ) es válida, porque no es posible que el control alcance un punto inmediatamente después de un salto de flujo de control.
En realidad, demostramos más que la corrección: demostramos que la solución del análisis es una solución perfecta (y no solo una aproximación segura).