En informática , el análisis de asignación definida es un análisis del 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.
Motivación
En los programas C y C ++ , una fuente de errores particularmente difíciles de diagnosticar es el comportamiento no determinista que resulta de leer variables no inicializadas ; este comportamiento puede variar entre plataformas, compilaciones e incluso de ejecución a ejecución.
Hay dos formas habituales de solucionar este problema. Una es asegurarse de que todas las ubicaciones estén escritas 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 aceptará solo programas que satisfagan esta restricción, mientras rechaza algunos programas correctos, y el análisis de asignación definido 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 en tiempo de compilación si el análisis falla. Ambos lenguajes requieren una forma específica de análisis que se detalla meticulosamente. 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 explícitas innecesarias. En C #, este análisis fue formalizado por Fruja, y es tan preciso como 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 migración de programas en C. [5]
La segunda forma de resolver el problema es inicializar automáticamente todas las ubicaciones a un valor fijo y predecible en el punto en el que se definen, pero esto introduce nuevas asignaciones que pueden impedir el rendimiento. En este caso, el análisis de asignación definida permite una optimización del compilador donde las asignaciones redundantes (asignaciones seguidas solo por otras asignaciones sin posibles lecturas intermedias) pueden eliminarse. En este caso, no se rechaza ningún programa, pero los programas para los que el análisis no reconoce una asignación definida pueden contener una inicialización redundante. El Common Language Infrastructure se basa en este enfoque. [6]
Terminología
Se puede decir que una variable o ubicación está en uno de tres estados en cualquier punto del programa:
- Asignado definitivamente : Se sabe con certeza que la variable se asignará.
- Definitivamente sin asignar : 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 para determinar cuál.
El analisis
Lo siguiente se basa en la formalización de Fruja del análisis de asignación definida intraprocedimiento (método único) de C #, que es responsable de garantizar que todas las variables locales se asignen antes de su uso. [4] Simultáneamente realiza análisis de asignaciones definidas y propagación constante de valores booleanos. Definimos cinco funciones estáticas:
Nombre | Dominio | Descripción |
---|---|---|
antes de | Todas las declaraciones y expresiones | Variables definitivamente asignadas antes de la evaluación de la declaración o expresión dada. |
después | Todas las declaraciones y expresiones | Variables definitivamente asignadas después de la evaluación de la declaración o expresión dada, asumiendo que se completa normalmente. |
vars | Todas las declaraciones y expresiones | Todas las variables disponibles en el ámbito de la declaración o expresión dada. |
cierto | Todas las expresiones booleanas | Variables definitivamente asignadas después de la evaluación de la expresión dada, asumiendo que la expresión se evalúa como verdadera . |
falso | Todas las expresiones booleanas | Variables definitivamente asignadas después de la evaluación de la expresión dada, asumiendo que la expresión se evalúa como falsa . |
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. Suponga por el momento que no hay declaraciones goto , break , continue , return o manejo de excepciones . A continuación se muestran algunos ejemplos de estas ecuaciones:
- Cualquier expresión o enunciado 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 antes ( v ) = antes ( e ), y después ( e ) = después ( v ) U {loc}.
- Sea e la expresión verdadera . Entonces verdadero ( e ) = antes ( e ) y falso ( e ) = vars ( e ). En otras palabras, si e se evalúa como falso , todas las variables se asignan (de forma vacía ) definitivamente, porque e no se evalúa como falso.
- Dado que los argumentos del método se evalúan de izquierda a derecha, antes ( arg i + 1 ) = después ( arg i ). Una vez que se completa un método, se asignan definitivamente los parámetros de salida .
- Sea s el enunciado condicional si ( e ) s 1 else s 2 . Entonces antes ( e ) = antes ( s ), antes (s 1 ) = verdadero ( e ), antes ( s 2 ) = falso ( e ), y después ( s ) = después ( s 1 ) se cruzan después ( s 2 ) .
- Sea s el enunciado del ciclo while mientras que ( e ) es 1 . Entonces antes ( e ) = antes ( s ), antes ( s 1 ) = verdadero ( e ) y después ( s ) = falso ( e ).
- Y así.
Al comienzo del método, no se asignan definitivamente variables locales. El verificador itera repetidamente sobre el árbol de sintaxis abstracta y usa 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 usa 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 manejo de excepciones. Cualquier declaración que pueda ser el objetivo de uno de estos saltos debe intersecar su conjunto anterior con el conjunto de variables definitivamente asignadas en la fuente del salto. Cuando se introducen, el flujo de datos resultante puede tener varios puntos fijos, como en este ejemplo:
int i = 1 ; L : goto L ;
Dado que se puede llegar a la etiqueta L desde dos ubicaciones, la ecuación de flujo de control para goto dicta que antes (2) = después (1) se intersecan antes (3). Pero antes (3) = antes (2), entonces antes (2) = después (1) se cruzan antes (2). Esto tiene dos puntos fijos para antes (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 punto fijo máximo único (punto fijo de mayor tamaño) que proporciona la mayor información posible sobre las variables definitivamente asignadas. Dicho punto fijo máximo (o máximo) puede calcularse mediante técnicas estándar; ver 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:
int i ; si ( j < 0 ) volver ; más i = j ; imprimir ( i );
La ecuación de flujo de datos para if dice que después de (2) = después ( retorno ) se cruzan después de ( i = j ). Para que esto funcione correctamente, definimos after ( e ) = vars ( e ) para todos los saltos de flujo de control; esto es vacuosamente válido en el mismo sentido que la ecuación falso ( verdadero ) = 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.
Referencias
- ^ J. Gosling; B. Alegría; G. Steele; G. Bracha. "La especificación del lenguaje Java, tercera edición" . págs. Capítulo 16 (págs. 527–552) . Consultado el 2 de diciembre de 2008 .
- ^ "Estándar ECMA-334, Especificación del lenguaje C #" . ECMA Internacional . págs. Sección 12.3 (págs. 122-133) . Consultado el 2 de diciembre de 2008 .
- ^ Stärk, Robert F .; E. Borger; Joachim Schmid (2001). Java y la máquina virtual Java: definición, verificación, validación . Secaucus, Nueva Jersey, EE.UU .: Springer-Verlag New York, Inc. págs. Sección 8.3. ISBN 3-540-42088-6.
- ^ a b Fruja, Nicu G. (octubre de 2004). "La exactitud del análisis de asignación definida en C #" . Revista de tecnología de objetos . 3 (9): 29–52. CiteSeerX 10.1.1.165.6696 . doi : 10.5381 / jot.2004.3.9.a2 . Consultado el 2 de diciembre de 2008 .
De hecho, demostramos más que lo correcto: mostramos que la solución del análisis es una solución perfecta (y no solo una aproximación segura).
- ^ "Ciclón: asignación definitiva" . Manual del usuario de Cyclone . Consultado el 16 de diciembre de 2008 .
- ^ "Estándar ECMA-335, Common Language Infrastructure (CLI)" . ECMA Internacional . págs. Sección 1.8.1.1 (Partición III, pág. 19) . Consultado el 2 de diciembre de 2008 .