Interpretación abstracta

En informática, la interpretación abstracta es una teoría de aproximación sólida de la semántica de los programas informáticos, basada en funciones monótonas sobre conjuntos ordenados, especialmente redes. Puede verse como una ejecución parcial de un programa de computadora que obtiene información sobre su semántica (por ejemplo, flujo de control, flujo de datos) sin realizar todos los cálculos.

Su principal aplicación concreta es el análisis estático formal, la extracción automática de información sobre las posibles ejecuciones de programas informáticos; tales análisis tienen dos usos principales:

• dentro de los compiladores, para analizar programas y decidir si ciertas optimizaciones o transformaciones son aplicables;
• para la depuración o incluso la certificación de programas contra clases de errores.

La interpretación abstracta fue formalizada por la pareja de científicos informáticos franceses Patrick Cousot y Radhia Cousot a fines de la década de 1970.

Intuición

Esta sección ilustra la interpretación abstracta por medio de ejemplos no informáticos del mundo real.

Considere a las personas en una sala de conferencias. Asuma un identificador único para cada persona en la habitación, como un número de seguro social en los Estados Unidos. Para probar que alguien no está presente, todo lo que hay que hacer es ver si su número de seguro social no está en la lista. Dado que dos personas diferentes no pueden tener el mismo número, es posible probar o refutar la presencia de un participante simplemente consultando su número.

Sin embargo, es posible que solo se hayan registrado los nombres de los asistentes. Si el nombre de una persona no se encuentra en la lista, podemos concluir con seguridad que esa persona no estaba presente; pero si lo es, no podemos concluir definitivamente sin más indagaciones, debido a la posibilidad de homónimos (por ejemplo, dos personas llamadas John Smith). Tenga en cuenta que esta información imprecisa seguirá siendo adecuada para la mayoría de los propósitos, porque los homónimos son raros en la práctica. Sin embargo, con todo rigor, no podemos decir con certeza que alguien estuviera presente en la habitación; todo lo que podemos decir es que él o ella posiblemente estuvo aquí. Si la persona que buscamos es un delincuente, emitiremos una alarma; pero por supuesto existe la posibilidad de emitir una falsa alarma. Fenómenos similares ocurrirán en el análisis de programas.

Si solo estamos interesados ​​en alguna información específica, digamos, "¿había una persona de edad n en la habitación?", no es necesario mantener una lista de todos los nombres y fechas de nacimiento. Podemos limitarnos con seguridad y sin pérdida de precisión a mantener una lista de las edades de los participantes. Si esto ya es demasiado para manejar, podríamos mantener solo la edad de la persona más joven, m y la de mayor edad, M. Si la pregunta es sobre una edad estrictamente inferior a m o estrictamente superior a M, entonces podemos responder con seguridad que dicho participante no estuvo presente. De lo contrario, es posible que solo podamos decir que no sabemos.

En el caso de la computación, la información concreta y precisa en general no es computable dentro de un tiempo y una memoria finitos (ver el teorema de Rice y el problema de la detención). La abstracción se utiliza para permitir respuestas generalizadas a las preguntas (por ejemplo, responder "quizás" a una pregunta de sí/no, lo que significa "sí o no", cuando nosotros (un algoritmo de interpretación abstracta) no podemos calcular la respuesta precisa con certeza); esto simplifica los problemas, haciéndolos susceptibles a soluciones automáticas. Un requisito crucial es agregar suficiente vaguedad para que los problemas sean manejables y al mismo tiempo conservar la precisión suficiente para responder las preguntas importantes (como "¿podría fallar el programa?").

Interpretación abstracta de programas informáticos

Dado un lenguaje de programación o especificación, la interpretación abstracta consiste en dar varias semánticas unidas por relaciones de abstracción. Una semántica es una caracterización matemática de un posible comportamiento del programa. La semántica más precisa, que describe muy de cerca la ejecución real del programa, se denomina semántica concreta.. Por ejemplo, la semántica concreta de un lenguaje de programación imperativo puede asociar a cada programa el conjunto de rastros de ejecución que puede producir, siendo un rastro de ejecución una secuencia de posibles estados consecutivos de la ejecución del programa; un estado generalmente consta del valor del contador del programa y las ubicaciones de la memoria (globales, pila y montón). Luego se derivan semánticas más abstractas; por ejemplo, uno puede considerar solo el conjunto de estados alcanzables en las ejecuciones (lo que equivale a considerar los últimos estados en trazas finitas).

El objetivo del análisis estático es derivar una interpretación semántica computable en algún punto. Por ejemplo, se puede optar por representar el estado de un programa que manipula variables enteras olvidando los valores reales de las variables y manteniendo únicamente sus signos (+, − o 0). Para algunas operaciones elementales, como la multiplicación, tal abstracción no pierde precisión: para obtener el signo de un producto, basta con conocer el signo de los operandos. Para algunas otras operaciones, la abstracción puede perder precisión: por ejemplo, es imposible conocer el signo de una suma cuyos operandos son respectivamente positivos y negativos.

A veces es necesaria una pérdida de precisión para que la semántica sea decidible (ver el teorema de Rice y el problema de la detención). En general, se debe llegar a un compromiso entre la precisión del análisis y su decidibilidad (computabilidad) o manejabilidad (costo computacional).

En la práctica, las abstracciones que se definen se adaptan tanto a las propiedades del programa que se desea analizar como al conjunto de programas de destino. El primer análisis automatizado a gran escala de programas informáticos con interpretación abstracta estuvo motivado por el accidente que supuso la destrucción del primer vuelo del cohete Ariane 5 en 1996.

Formalización

Sea L un conjunto ordenado, llamado conjunto concreto y sea L ′ otro conjunto ordenado, llamado conjunto abstracto. Estos dos conjuntos están relacionados entre sí mediante la definición de funciones totales que asignan elementos de uno a otro.

Una función α se llama función de abstracción si mapea un elemento x en el conjunto concreto L a un elemento α(x) en el conjunto abstracto L ′. Es decir, el elemento α(x) en L ′ es la abstracción de x en L.

Una función γ se llama función de concretización si mapea un elemento x ′ en el conjunto abstracto L ′ a un elemento γ(x ′) en el conjunto concreto L. Es decir, el elemento γ(x ′) en L es una concreción de x ′ en L ′.

Sean L ₁, L ₂, L ′ ₁ y L ′ ₂ conjuntos ordenados. La semántica concreta f es una función monótona de L ₁ a L ₂. Se dice que una función f ′ de L ′ ₁ a L ′ ₂ es una abstracción válida de f si para todo x ′ en L ′ ₁, (f ∘ γ)(x ′) ≤ (γ ∘ f ′)(x ′).

La semántica del programa generalmente se describe utilizando puntos fijos en presencia de bucles o procedimientos recursivos. Supongamos que L es un retículo completo y sea f una función monótona de L en L. Entonces, cualquier x ′ tal que f (x ′) ≤ x ′ es una abstracción del menor punto fijo de f, que existe, según el teorema de Knaster-Tarski.

La dificultad ahora es obtener tal x ′. Si L ′ es de altura finita, o al menos verifica la condición de cadena ascendente (todas las secuencias ascendentes son finalmente estacionarias), entonces tal x ′ puede obtenerse como el límite estacionario de la secuencia ascendente x ′ _n definida por inducción como sigue: x ′ ₀ =⊥ (el elemento mínimo de L ′) y x ′ _{n +1} = f ′(x ′ _n).

En otros casos, aún es posible obtener tal x ′ a través de un operador de ampliación ∇: para todo x e y, x ∇ y debe ser mayor o igual que x e y, y para cualquier secuencia y ′ _n, la secuencia definida por x ′ ₀ =⊥ y x ′ _{n +1} = x ′ _n ∇ y ′ _n es finalmente estacionaria. Entonces podemos tomar y ′ _n = f ′(x ′_n).

En algunos casos, es posible definir abstracciones usando conexiones de Galois (α, γ) donde α es de L a L ′ y γ es de L ′ a L. Esto supone la existencia de mejores abstracciones, lo que no es necesariamente el caso. Por ejemplo, si abstraemos conjuntos de pares (x, y) de números reales encerrando poliedros convexos, no existe una abstracción óptima para el disco definido por x + y ≤ 1.

Ejemplos de dominios abstractos

Dominios abstractos numéricos

Se puede asignar a cada variable x disponible en un punto de programa dado un intervalo [ L _x, H _x ]. Un estado que asigne el valor v (x) a la variable x será una concreción de estos intervalos si para todo x, v (x) está en [ L _x, H _x ]. De los intervalos [ L _x, H _x ] y [ L _y, H _y ] para las variables x e y, uno puede obtener fácilmente intervalos para x + y ([ L _x + L _y, H _x + H _y ]) y para x − y ([ L _x − H _y, H _x − L _y ]); tenga en cuenta que estas son abstracciones exactas, ya que el conjunto de resultados posibles para, digamos, x + y, es precisamente el intervalo ([ L _x + L _y, H _x + H_y ]). Se pueden derivar fórmulas más complejas para la multiplicación, la división, etc., lo que da como resultado la llamada aritmética de intervalos.

Consideremos ahora el siguiente programa muy simple:

y = x;
z = x - y;

Con tipos aritméticos razonables, el resultado dezdebe ser cero. Pero si hacemos aritmética de intervalos a partir deXen [0, 1], se obtienezen [−1, +1]. Si bien cada una de las operaciones tomadas individualmente se abstrajo exactamente, su composición no lo es.

El problema es evidente: no llevamos la cuenta de la relación de igualdad entreXyy; en realidad, este dominio de intervalos no tiene en cuenta ninguna relación entre variables y, por lo tanto, es un dominio no relacional. Los dominios no relacionales tienden a ser rápidos y simples de implementar, pero imprecisos.

Algunos ejemplos de dominios abstractos numéricos relacionales son:

• relaciones de congruencia en números enteros
• poliedros convexos (ver imagen de la izquierda) – con algunos costos computacionales altos
• matrices ligadas a diferencias
• "octágonos"
• igualdades lineales

y combinaciones de los mismos (como el producto reducido, véase la imagen de la derecha).

Cuando uno elige un dominio abstracto, normalmente tiene que lograr un equilibrio entre mantener relaciones detalladas y altos costos computacionales.

Dominios abstractos de palabras de máquina

Mientras que los lenguajes de alto nivel, como Python o Haskell, usan números enteros ilimitados de forma predeterminada, los lenguajes de programación de nivel inferior, como C o el lenguaje ensamblador, generalmente operan en palabras de máquina de tamaño finito, que se modelan de manera más adecuada utilizando el módulo de números enteros (donde n es el ancho de bit de una palabra de máquina). Hay varios dominios abstractos adecuados para varios análisis de tales variables.

El dominio de campo de bits trata cada bit de una palabra de máquina por separado, es decir, una palabra de ancho n se trata como una matriz de n valores abstractos. Los valores abstractos se toman del conjunto y las funciones de abstracción y concretización vienen dadas por:

Las operaciones bit a bit en estos valores abstractos son idénticas a las operaciones lógicas correspondientes en algunas lógicas de tres valores:

NO UN)A¬A01⊥⊥10	Y (A, B)A ∧ BB0⊥1A0000⊥0⊥⊥10⊥1	O(A, B)A ∨ BB0⊥1A00⊥1⊥⊥⊥11111