Análisis de asignación definitiva

En informática , el análisis de asignación definitiva es un análisis de flujo de datos que utilizan los compiladores para garantizar de forma conservadora que una variable o ubicación siempre se asigne antes de ser utilizada.

En los programas escritos en 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.

Hay dos maneras comunes de resolver este problema. Una es asegurar 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 los programas que satisfagan esta restricción, rechazando algunos programas correctos, y el análisis de asignación definitiva es un ejemplo de dicho análisis. Las especificaciones de los lenguajes de programación Java ^{[ 1 ]} y C# ^{[ 2 ]} requieren que el compilador reporte un error en tiempo de compilación si el análisis falla. Ambos lenguajes requieren una forma específica del análisis que se detalla minuciosamente. 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 definitivamente asignadas. ^{[ 4 ]} El lenguaje Cyclone también requiere que los programas pasen un análisis de asignación definido, pero solo en variables con tipos de puntero, para facilitar la portabilidad de programas C. ^{[ 5 ]}

La segunda forma de resolver el problema consiste en inicializar automáticamente todas las ubicaciones con un valor fijo y predecible en el momento de su definición, pero esto introduce nuevas asignaciones que pueden afectar al rendimiento. En este caso, el análisis de asignación definida permite una optimización del compilador que elimina las asignaciones redundantes ( asignaciones seguidas únicamente por otras sin lecturas intermedias posibles ) . De este modo, no se rechaza ningún programa, pero aquellos en los que el análisis no reconoce la asignación definida pueden contener inicializaciones redundantes. La Infraestructura de Lenguaje Común (CLI) se basa en este enfoque. ^{[ 6 ]}

Se puede decir que una variable o ubicación se encuentra en uno de tres estados en cualquier momento del programa:

• Asignado definitivamente : Se sabe con certeza que la variable está asignada.
• Definitivamente no asignada : Se sabe con certeza que la variable no está asignada.
• Desconocido : La variable puede estar asignada o no asignada; el análisis no es lo suficientemente preciso como para determinar cuál es el caso.

Lo siguiente se basa en la formalización de Fruja del análisis de asignación definida intraprocedimental (método único) de C#, que se encarga de asegurar que todas las variables locales se asignen antes de ser utilizadas. ^{[ 4 ]} Realiza simultáneamente análisis de asignación definida y 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 diversas expresiones y sentencias, en función de los valores de las funciones en sus subexpresiones sintácticas. Supongamos por el momento que no hay sentencias goto , break , continue , return ni de manejo de excepciones . A continuación, se muestran algunos ejemplos de estas ecuaciones:

• Cualquier expresión o instrucción e que no afecte al conjunto de variables definitivamente asignadas: después ( e ) = antes ( e )
• Sea e la expresión de asignación loc = v . Entonces before ( v ) = before ( e ), y after ( e ) = after ( v ) U {loc}.
• Sea e la expresión verdadera . Entonces verdadero ( e ) = antes ( e ) y falso ( e ) = variables ( e ). En otras palabras, si e se evalúa como falso , todas las variables se asignan ( vacuamente ) definitivamente, porque e no se evalúa como falso.
• Dado que los argumentos de los métodos se evalúan de izquierda a derecha, before( arg _{i  +  1} ) = after( arg _i ). Una vez que un método finaliza, los parámetros de salida se asignan definitivamente.
• Sea s la declaración condicional if ( e ) s ₁ else s ₂ . Entonces before ( e ) = before ( s ), before (s ₁ ) = true ( e ), before ( s ₂ ) = false ( e ), y after( s ) = after( s ₁ ) intersect after( s ₂ ).
• Sea s la instrucción del bucle while while ( e ) s ₁ . Entonces before( e ) = before( s ), before( s ₁ ) = true( e ), y after( s ) = false( e ).
• Etcétera.

Al inicio del método, no se asigna ninguna variable local de forma definitiva. El verificador itera repetidamente sobre el árbol de sintaxis abstracta y utiliza las ecuaciones de flujo de datos para transferir información entre los conjuntos hasta alcanzar un punto fijo . A continuación, el verificador examina el conjunto previo de cada expresión que utiliza una variable local para asegurarse de que la contiene.

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 before con el conjunto de variables definitivamente asignadas en el origen del salto. Cuando se introducen estos saltos, el flujo de datos resultante puede tener múltiples puntos fijos, como en este ejemplo:

int i = 1 ;L :ir a L ;

Dado que la etiqueta L puede alcanzarse desde dos ubicaciones, la ecuación de flujo de control para goto dicta que before (2) = after (1) intersecta before (3). Pero before (3) = before (2), por lo que before (2) = after (1) intersecta before (2). Esto tiene dos puntos fijos para before (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 cantidad de información posible sobre las variables definitivamente asignadas. Dicho punto fijo máximo puede calcularse mediante técnicas estándar; véase análisis de flujo de datos .

Un problema adicional es que un salto en el 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:

int i ;si ( j < 0 ) regresar ; 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 que la ecuación false ( true ) = vars ( e ) es válida, porque no es posible que el control llegue a un punto inmediatamente después de un salto de flujo de control.