Interpretación abstracta

En todos los capítulos anteriores hemos usado el término «correcto» de manera informal: un análisis es correcto si las propiedades que infiere se cumplen en todas las ejecuciones reales del programa. La interpretación abstracta proporciona el fundamento matemático de qué significa exactamente eso, relacionando la especificación del análisis con la semántica formal del lenguaje. Y sirve además para otra cosa igual de útil: para entender si un diseño de análisis es lo más preciso posible dado su retículo, y dónde exactamente se pierde precisión. Las ideas fundamentales son de Cousot y Cousot, de los años setenta.

21.1 La semántica colectora

Empezamos definiendo la semántica formal del mismo subconjunto de TIP que usamos para el análisis de signos: sin llamadas a función, sin punteros y sin registros. En lugar de los estilos tradicionales —semántica operacional, denotacional o axiomática— elegimos un enfoque basado en restricciones que se alinea bien con las formulaciones de los capítulos anteriores, y la definimos sobre el CFG. Lo que importa es que la semántica capture el significado de los programas en ejecuciones ordinarias, sin aproximación alguna.

Un estado concreto es una aplicación parcial de variables en enteros:

Para cada nodo v del CFG tenemos una variable de restricción que toma valores en conjuntos de estados concretos, {[v]} ⊆ ConcreteState. La idea es que {[v]} denote el conjunto de estados concretos posibles inmediatamente después de la instrucción de v, en alguna ejecución. Se llama semántica colectora (collecting semantics) porque «colecciona» los estados posibles.

Las funciones auxiliares son las contrapartidas concretas de las del análisis de signos. La evaluación de expresiones, ceval : ConcreteState × Exp → ℘(ℤ):

ceval(rho, X)          = { rho(X) }
ceval(rho, I)          = { I }
ceval(rho, input)      = Z
ceval(rho, E1 + E2)    = { z1 + z2 : z1 en ceval(rho,E1), z2 en ceval(rho,E2) }
ceval(rho, E1 / E2)    = { z1 / z2 : z1 en ceval(rho,E1), z2 en ceval(rho,E2) }

Nótese que la división por cero produce simplemente el conjunto vacío de valores: no hay error, hay ausencia de resultado. Es la contrapartida concreta del ⊥ absorbente del capítulo «6».

ceval se sobrecarga a conjuntos de estados por unión. La función csucc : ConcreteState × Node → ℘(Node) da los sucesores posibles de un nodo relativos a un estado: para un nodo condicional con condición E, contiene el sucesor verdadero si ceval(ρ, E) contiene algún z ≠ 0, y el falso si contiene el 0. Y CJOIN reúne los estados de los predecesores que efectivamente pueden llegar a v.

Con esa maquinaria, la semántica de un programa P es el menor punto fijo de la función de restricción semántica, y el resultado del análisis el de la función de restricción del análisis:

Un ejemplo. Para

var x;
x = 0;
while (input) {
    x = x + 2;
}

la solución que nos interesa aplica {[x = 0]} al único estado donde x vale cero, y {[x = x + 2]} al conjunto de todos los estados donde x es un entero par positivo.

21.2 Abstracción y concretización

Para aclarar la conexión entre información concreta y abstracta, considérense tres funciones de abstracción que indican cómo se describe con mayor precisión cada elemento de los retículos semánticos mediante un elemento de los retículos del análisis:

alpha_a : P(Z)                  -> Sign
alpha_b : P(ConcreteState)      -> State
alpha_c : (P(ConcreteState))^n  -> State^n

definidas por:

alpha_a(D) = bottom  si D es vacio
           = +       si D es no vacio y solo contiene enteros positivos
           = -       si D es no vacio y solo contiene enteros negativos
           = 0       si D es no vacio y solo contiene el entero 0
           = T       en otro caso

alpha_b(R) = sigma   donde sigma(X) = alpha_a({ rho(X) : rho en R })

alpha_c(R1, ..., Rn) = (alpha_b(R1), ..., alpha_b(Rn))

Es natural exigir que las funciones de abstracción sean monótonas: un conjunto mayor de valores concretos no debería representarse por un elemento abstracto menor.

Dualmente se definen funciones de concretización, que expresan el significado de los elementos del retículo del análisis en términos concretos:

gamma_a(s) = vacio            si s = bottom
           = {1, 2, 3, ...}   si s = +
           = {-1, -2, -3,...} si s = -
           = {0}              si s = 0
           = Z                si s = T

gamma_b(sigma) = { rho : rho(X) en gamma_a(sigma(X)) para toda X en Var }

gamma_c(sigma_1, ..., sigma_n) = (gamma_b(sigma_1), ..., gamma_b(sigma_n))

También ellas son naturalmente monótonas.

21.3 Conexiones de Galois

Las funciones de abstracción y concretización que surgen de forma natural al diseñar análisis están estrechamente conectadas.

21.4 Corrección

Con esto ya podemos decir qué significa exactamente que un análisis sea correcto.

21.5 Optimalidad

La corrección no dice nada sobre la precisión: el análisis que responde ⊤ siempre es correcto. La pregunta interesante es cuál es la mejor función de transferencia abstracta posible dado el retículo.

Dos ejemplos, ambos instructivos.

El producto abstracto del análisis de signos es óptimo. En efecto, s₁ *̂ s₂ = αa(γa(s₁) · γa(s₂)), donde · se sobrecarga a conjuntos. Lo mismo vale para todos los operadores abstractos del capítulo «6». Y en el análisis de intervalos, la definición general op̂([l₁,h₁],[l₂,h₂]) = [min …, max …] es óptima por construcción; como se señaló en el capítulo «8», no es directamente implementable, así que en la práctica se prefiere una alternativa no óptima pero correcta.

Y sin embargo eval no es óptima. Éste es el punto fino del capítulo. Aunque todos los operadores abstractos sean óptimos, la función eval construida inductivamente a partir de ellos no lo es. Contraejemplo: sea σ con σ(x) = ⊤ y considérese la expresión x - x. Entonces

porque en toda ejecución concreta x - x vale cero. Definir una función inductiva y composicionalmente a partir de abstracciones óptimas no la hace óptima. La causa es que la composición pierde la correlación entre las dos ocurrencias de x, y es exactamente el fenómeno de los atributos independientes del capítulo «9».

21.6 Completitud

Como es habitual en lógica, el dual de la corrección es la completitud. Si la corrección para P es α({[P]}) ⊑ ⟦P⟧, es natural definir que el análisis es completo para P si

Un análisis es completo si lo es para todos los programas. Si es correcto y completo para P, entonces α({[P]}) = ⟦P⟧: el resultado del análisis es exactamente la mejor descripción posible de la semántica en ese retículo.

Ni siquiera con eval óptima se consigue la completitud. Contraejemplo:

x = input;
y = x;
z = x - y;

Sea σ el estado abstracto tras y = x, con σ(x) = σ(y) = ⊤. Cualquier abstracción correcta de z = x - y dará z ↦ ⊤, pero la respuesta 0 sería más precisa y seguiría siendo correcta. El análisis no conoce la correlación entre x e y. Se podría, en principio, añadir una regla ad hoc que reconociera este patrón concreto; la solución sensata es el análisis relacional del capítulo «9».

21.7 Semánticas colectoras alternativas

La semántica colectora de la «sección 21.1 · La semántica colectora» colecciona conjuntos de estados por punto de programa, lo que la hace adecuada para razonar sobre el análisis de signos, el de intervalos y los demás análisis hacia adelante que estiman valores. No sirve, en cambio, para razonar sobre variables vivas o definiciones alcanzables, porque esos análisis no hablan de valores sino de relaciones entre puntos del programa.

Para ellos se usa una semántica de trazas (trace semantics), que colecciona secuencias de estados en lugar de conjuntos, y de la que la semántica colectora de estados es a su vez una abstracción. Se obtiene así una jerarquía de semánticas, cada una abstracción de la anterior:

   semantica de trazas          (secuencias de estados)
            |  alpha
            v
   semantica colectora          (conjuntos de estados por punto)
            |  alpha
            v
   analisis de intervalos       (un intervalo por variable y punto)
            |  alpha
            v
   analisis de signos           (un signo por variable y punto)

Y ésa es una de las aportaciones conceptuales más valiosas de la interpretación abstracta: la relación entre un análisis y otro es del mismo tipo que la relación entre un análisis y la semántica. Todo es abstracción de algo, y las conexiones de Galois se componen.

21.8 Widening y narrowing, revisitados

El capítulo «8» presentó el widening como un truco para forzar la terminación. Con el aparato de este capítulo se ve como lo que es: una aproximación del punto fijo en el sentido preciso siguiente.

Un operador de widening ∇ define una sucesión x₀ = ⊥, xi+1 = xᵢ ∇ f(xᵢ) que converge en un número finito de pasos a un post-punto-fijo de f, es decir, a un x con f(x) ⊑ x; y por el teorema de Tarski todo post-punto-fijo está por encima de lfp(f). La corrección se sigue, pues, del mismo teorema que se usó en el capítulo «8», ahora en su contexto natural.

El narrowing es la operación dual: partiendo de un post-punto-fijo, la sucesión decreciente fi(x) sigue estando por encima de lfp(f), y un operador Δ garantiza que la sucesión termine.

Lo que este capítulo añade es la libertad de diseño: ∇ no tiene por qué venir del dominio abstracto. Se puede diseñar un ∇ distinto para cada punto de widening, o hacerlo depender del historial de la iteración, o combinarlo con Δ alternadamente. La única condición es la de la «sección 8.5 · El operador de widening», y cualquier operador que la cumpla da un análisis correcto.

21.9 En el análisis de binarios

21.10 Lecturas

Las referencias originales de la interpretación abstracta son Cousot y Cousot (1976, 1977, 1979). El diseño sistemático de conexiones de Galois y las operaciones inducidas —cómo derivar la función de transferencia abstracta a partir de la concreta y de la conexión, en lugar de construirla a mano— son la versión general del resultado de optimalidad de la «sección 21.5 · Optimalidad», y la lectura recomendada para quien quiera construir dominios abstractos de forma metódica.