Interpretación abstracta

Enfoque del análisis de programas estáticos

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 retículos . Puede considerarse como una ejecución parcial de un programa informático 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 son aplicables ciertas optimizaciones o transformaciones ;
• 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 finales de la década de 1970. ^{[1] [2]}

Intuición

Esta sección ilustra la interpretación abstracta mediante ejemplos del mundo real, no informáticos.

Pensemos en las personas que se encuentran en una sala de conferencias. Supongamos que cada persona tiene un identificador único, como un número de seguridad social en los Estados Unidos. Para demostrar que alguien no está presente, todo lo que hay que hacer es comprobar si su número de seguridad social no está en la lista. Como dos personas diferentes no pueden tener el mismo número, es posible demostrar o refutar la presencia de un participante simplemente buscando su número.

Sin embargo, es posible que sólo se hayan registrado los nombres de los asistentes. Si no se encuentra el nombre de una persona en la lista, podemos concluir con seguridad que esa persona no estaba presente; pero si está, no podemos concluir definitivamente sin más indagaciones, debido a la posibilidad de que haya 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 poco frecuentes en la práctica. Sin embargo, con todo rigor, no podemos decir con certeza que alguien estaba presente en la sala; todo lo que podemos decir es que posiblemente estaba aquí. Si la persona que estamos buscando es un criminal, 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 sólo nos interesa alguna información específica, por ejemplo, "¿había una persona mayor de edad en la sala?", no es necesario llevar una lista de todos los nombres y fechas de nacimiento. Podemos limitarnos con seguridad y sin pérdida de precisión a llevar una lista de las edades de los participantes. Si esto ya es demasiado para manejar, podemos llevar sólo la edad de la persona más joven y de la más mayor, . Si la pregunta es sobre una edad estrictamente inferior o estrictamente superior a , entonces podemos responder con seguridad que no había ningún participante de ese tipo presente. De lo contrario, sólo podemos decir que no lo sabemos. ${\displaystyle n}$ ${\displaystyle m}$ ${\displaystyle M}$ ${\displaystyle m}$ ${\displaystyle M}$

En el caso de la informática, la información concreta y precisa no es, en general, computable en un tiempo y una memoria finitos (véase 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 "tal vez" a una pregunta de sí/no, es decir, "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 de soluciones automáticas. Un requisito crucial es agregar suficiente vaguedad para que los problemas sean manejables y al mismo tiempo se conserve 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 de especificación, la interpretación abstracta consiste en dar varias semánticas vinculadas 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 llama semántica concreta . Por ejemplo, la semántica concreta de un lenguaje de programación imperativo puede asociar a cada programa el conjunto de trazas de ejecución que puede producir – una traza de ejecución es una secuencia de posibles estados consecutivos de la ejecución del programa; un estado consiste típicamente en el valor del contador del programa y las ubicaciones de 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 momento. Por ejemplo, se puede optar por representar el estado de un programa que manipula variables enteras olvidando los valores reales de las variables y solo conservando sus signos (+, − o 0). Para algunas operaciones elementales, como la multiplicación , una abstracción de este tipo no pierde precisión: para obtener el signo de un producto, es suficiente 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 positivo y negativo.

A veces es necesaria una pérdida de precisión para que la semántica sea decidible (véase el teorema de Rice y el problema de la detención ). En general, hay que 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 fue motivado por el accidente que provocó la destrucción del primer vuelo del cohete Ariane 5 en 1996. ^[3]

Formalización

Ejemplo: abstracción de conjuntos de números enteros (rojo) a conjuntos de signos (verde)

Sea un conjunto ordenado , llamado conjunto concreto , y sea 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. ${\displaystyle L}$ ${\displaystyle L'}$

Una función se denomina función de abstracción si asigna un elemento del conjunto concreto a un elemento del conjunto abstracto . Es decir, el elemento in es la abstracción de in . ${\displaystyle \alpha }$ ${\displaystyle x}$ ${\displaystyle L}$ ${\displaystyle \alpha (x)}$ ${\displaystyle L'}$ ${\displaystyle \alpha (x)}$ ${\displaystyle L'}$ ${\displaystyle x}$ ${\displaystyle L}$

Una función se denomina función de concretización si asigna un elemento del conjunto abstracto a un elemento del conjunto concreto . Es decir, el elemento in es una concretización de in . ${\displaystyle \gamma }$ ${\displaystyle x'}$ ${\displaystyle L'}$ ${\displaystyle \gamma (x')}$ ${\displaystyle L}$ ${\displaystyle \gamma (x')}$ ${\displaystyle L}$ ${\displaystyle x'}$ ${\displaystyle L'}$

Sean , , , y conjuntos ordenados. La semántica concreta es una función monótona de a . Se dice que una función de a es una abstracción válida de si, para todo en , tenemos . ${\displaystyle L_{1}}$ ${\displaystyle L_{2}}$ ${\displaystyle L'_{1}}$ ${\displaystyle L'_{2}}$ ${\displaystyle f}$ ${\displaystyle L_{1}}$ ${\displaystyle L_{2}}$ ${\displaystyle f'}$ ${\displaystyle L'_{1}}$ ${\displaystyle L'_{2}}$ ${\displaystyle f}$ ${\displaystyle x'}$ ${\displaystyle L'_{1}}$ ${\displaystyle (f\circ \gamma )(x')\leq (\gamma \circ f')(x')}$

La semántica de los programas se describe generalmente utilizando puntos fijos en presencia de bucles o procedimientos recursivos. Supongamos que es una red completa y sea una función monótona de en . Entonces, cualquier tal que sea una abstracción del menor punto fijo de , que existe, de acuerdo con el teorema de Knaster-Tarski . ${\displaystyle L}$ ${\displaystyle f}$ ${\displaystyle L}$ ${\displaystyle L}$ ${\displaystyle x'}$ ${\displaystyle f(x')\leq x'}$ ${\displaystyle f}$

La dificultad ahora es obtener tal . Si es de altura finita, o al menos verifica la condición de cadena ascendente (todas las secuencias ascendentes son en última instancia estacionarias), entonces tal puede obtenerse como el límite estacionario de la secuencia ascendente definida por inducción de la siguiente manera: (el menor elemento de ) y . ${\displaystyle x'}$ ${\displaystyle L'}$ ${\displaystyle x'}$ ${\displaystyle x'_{n}}$ ${\displaystyle x'_{0}=\bot }$ ${\displaystyle L'}$ ${\displaystyle x'_{n+1}=f'(x'_{n})}$

En otros casos, todavía es posible obtenerlo mediante un operador de ampliación (de pares) , ^[4] definido como un operador binario que satisface las siguientes condiciones: ${\displaystyle x'}$ ${\displaystyle \nabla \colon L\times L\to L}$

1. Para todos y , tenemos y , y ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle x\leq x\mathbin {\nabla } y}$ ${\displaystyle y\leq x\mathbin {\nabla } y}$
2. Para cualquier secuencia ascendente , la secuencia definida por y es en última instancia estacionaria. Podemos entonces tomar . ${\displaystyle (y'_{n})_{n\geq 0}}$ ${\displaystyle x'_{0}:=\bot }$ ${\displaystyle x'_{n+1}:=x'_{n}\mathbin {\nabla } y'_{n}}$ ${\displaystyle y'_{n}=f'(x'_{n})}$

En algunos casos, es posible definir abstracciones utilizando conexiones de Galois donde es de a y es de a . Esto supone la existencia de mejores abstracciones, lo que no es necesariamente el caso. Por ejemplo, si abstraemos conjuntos de pares de números reales encerrando poliedros convexos , no existe una abstracción óptima para el disco definido por . ${\displaystyle (\alpha ,\gamma )}$ ${\displaystyle \alpha }$ ${\displaystyle L}$ ${\displaystyle L'}$ ${\displaystyle \gamma }$ ${\displaystyle L'}$ ${\displaystyle L}$ ${\displaystyle (x,y)}$ ${\displaystyle x^{2}+y^{2}\leq 1}$

Ejemplos de dominios abstractos

Dominios abstractos numéricos

Se puede asignar a cada variable disponible en un punto dado del programa un intervalo . Un estado que asigne el valor a la variable será una concretización de estos intervalos si, para todo , tenemos . A partir de los intervalos y para las variables y , respectivamente, se pueden obtener fácilmente intervalos para (a saber, ) y para (a saber, ); tenga en cuenta que se trata de abstracciones exactas , ya que el conjunto de resultados posibles para, digamos, , es precisamente el intervalo . Se pueden derivar fórmulas más complejas para la multiplicación, división, etc., lo que produce la denominada aritmética de intervalos . ^[5] ${\displaystyle x}$ ${\displaystyle [L_{x},H_{x}]}$ ${\displaystyle v(x)}$ ${\displaystyle x}$ ${\displaystyle x}$ ${\displaystyle v(x)\in [L_{x},H_{x}]}$ ${\displaystyle [L_{x},H_{x}]}$ ${\displaystyle [L_{y},H_{y}]}$ ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle x+y}$ ${\displaystyle [L_{x}+L_{y},H_{x}+H_{y}]}$ ${\displaystyle x-y}$ ${\displaystyle [L_{x}-H_{y},H_{x}-L_{y}]}$ ${\displaystyle x+y}$ ${\displaystyle [L_{x}+L_{y},H_{x}+H_{y}]}$

Consideremos ahora el siguiente programa muy simple:

y = x;z = x - y;

Con tipos aritméticos razonables, el resultado paraeldebería ser cero. Pero si hacemos aritmética de intervalos a partir deincógnitaen [0, 1], se obtieneelen [−1, +1]. Si bien cada una de las operaciones tomadas individualmente fue abstraída con exactitud, su composición no lo es.

El problema es evidente: no hicimos un seguimiento de la relación de igualdad entreincógnitayy; 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 sencillos de implementar, pero imprecisos.

Algunos ejemplos de dominios abstractos numéricos relacionales son:

• relaciones de congruencia en números enteros ^{[6] [7]}
• Poliedros convexos ^[8] (cf. imagen de la izquierda) – con unos costes computacionales elevados
• matrices con límites diferenciales ^[9]
• "octágonos" ^{[10] [11] [12]}
• igualdades lineales ^[13]

y combinaciones de los mismos (como el producto reducido, ^[2] cf. imagen de la derecha).

Cuando uno elige un dominio abstracto, generalmente 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 utilizan números enteros ilimitados de forma predeterminada, los lenguajes de programación de nivel inferior como C o el lenguaje ensamblador suelen operar con palabras de máquina de tamaño finito , que se modelan de forma más adecuada utilizando el módulo de números enteros ${\textstyle 2^{n}}$ (donde n es el ancho de bits de una palabra de máquina). Existen varios dominios abstractos adecuados para diversos análisis de dichas variables.

El dominio de campo de bits trata cada bit en 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 se dan por: ^{[14] [15]} , , , , , , . Las operaciones bit a bit sobre estos valores abstractos son idénticas a las operaciones lógicas correspondientes en algunas lógicas de tres valores : ^[16] ${\textstyle \{0,1,\bot \}}$ ${\displaystyle \gamma (0)=\{0\}}$ ${\displaystyle \gamma (1)=\{1\}}$ ${\displaystyle \gamma (\bot )=\{0,1\}}$ ${\displaystyle \alpha (\{0\})=0}$ ${\displaystyle \alpha (\{1\})=1}$ ${\displaystyle \alpha (\{0,1\})=\bot }$ ${\displaystyle \alpha (\{\})=\bot }$

Otros dominios incluyen el dominio de intervalos con signo y el dominio de intervalos sin signo . Los tres dominios admiten operadores abstractos hacia adelante y hacia atrás para operaciones comunes como la suma, los desplazamientos , la operación xor y la multiplicación. Estos dominios se pueden combinar utilizando el producto reducido. ^[17]

Véase también

• Comprobación de modelos
• Simulación simbólica
• Ejecución simbólica
• Lista de herramientas para el análisis de código estático : contiene herramientas basadas en interpretación abstracta (sólidas) y ad hoc (no sólidas)
• Análisis de programas estáticos : descripción general de los métodos de análisis, que incluyen, entre otros, la interpretación abstracta
• Intérprete (informática)

Referencias

1. Cousot, Patrick; Cousot, Radhia (1977). "Interpretación abstracta: un modelo reticular unificado para el análisis estático de programas mediante la construcción o aproximación de puntos fijos" (PDF) . Acta de la conferencia del cuarto simposio de la ACM sobre principios de lenguajes de programación, Los Ángeles, California, EE. UU., enero de 1977. ACM Press. págs. 238–252. doi :10.1145/512950.512973. S2CID  207614632.
2. Cousot, Patrick; Cousot, Radhia (1979). "Diseño sistemático de marcos de análisis de programas" (PDF) . Acta de la conferencia del sexto simposio anual de la ACM sobre principios de lenguajes de programación, San Antonio, Texas, EE. UU ., enero de 1979. ACM Press. págs. 269–282. doi :10.1145/567752.567778. S2CID  1547466.
3. Faure, Christèle. «Historia de PolySpace Technologies» . Consultado el 3 de octubre de 2010 .
4. Cousot, P.; Cousot, R. (agosto de 1992). "Comparación de la conexión de Galois y los enfoques de ampliación/reducción de la interpretación abstracta" (PDF) . En Bruynooghe, Maurice; Wirsing, Martin (eds.). Actas del 4.º Simposio Internacional sobre Implementación de Lenguajes de Programación y Programación Lógica (PLILP) . Apuntes de clase en Ciencias de la Computación. Vol. 631. Springer. págs. 269–296. ISBN. 978-0-387-55844-8.
5. Cousot, Patrick; Cousot, Radhia (1976). "Determinación estática de propiedades dinámicas de programas" (PDF) . Actas del Segundo Simposio Internacional sobre Programación . Dunod, París, Francia. pp. 106–130.
6. Granger, Philippe (1989). "Análisis estático de congruencias aritméticas". Revista internacional de matemáticas informáticas . 30 (3–4): 165–190. doi :10.1080/00207168908803778.
7. Philippe Granger (1991). "Análisis estático de igualdades de congruencia lineal entre variables de un programa". En Abramsky, S.; Maibaum, TSE (eds.). Proc. Int. J. Conf. on Theory and Practice of Software Development (TAPSOFT) . Apuntes de clase en informática. Vol. 493. Springer. págs. 169–192.
8. Cousot, Patrick; Halbwachs, Nicolas (enero de 1978). "Descubrimiento automático de restricciones lineales entre variables de un programa" (PDF) . Conf. Rec. 5.º Simposio ACM sobre principios de lenguajes de programación (POPL) . págs. 84–97.
9. Miné, Antoine (2001). "Un nuevo dominio numérico abstracto basado en matrices de límites diferenciales". En Danvy, Olivier; Filinski, Andrzej (eds.). Programas como objetos de datos, segundo simposio, (PADO) . Apuntes de clase en informática. Vol. 2053. Springer. págs. 155–172. arXiv : cs/0703073 .
10. Miné, Antoine (diciembre de 2004). Dominios abstractos numéricos débilmente relacionales (PDF) (tesis doctoral). Laboratoire d'Informatique de l'École Normale Supérieure.
11. Antoine Miné (2006). "El dominio abstracto del octágono". Símbolo de orden superior. Comput . 19 (1): 31–100. arXiv : cs/0703084 . doi :10.1007/s10990-006-8609-1.
12. Clarisó, Robert; Cortadella, Jordi (2007). "El dominio abstracto del octaedro". Ciencia de la programación informática . 64 : 115–139. doi :10.1016/j.scico.2006.03.009. hdl : 10609/109823 .
13. Michael Karr (1976). "Relaciones afines entre variables de un programa". Acta Informatica . 6 (2): 133–151. doi :10.1007/BF00268497. S2CID  376574.
14. Miné, Antoine (junio de 2012). "Dominios abstractos para operaciones de máquina de nivel de bit con números enteros y coma flotante". WING'12 - 4.º Taller internacional sobre generación de invariantes . Manchester, Reino Unido: 16.
15. Regehr, John; Duongsaa, Usit (junio de 2006). "Derivación de funciones de transferencia abstractas para analizar software integrado". Actas de la conferencia ACM SIGPLAN/SIGBED de 2006 sobre lenguaje, compiladores y herramientas de soporte para sistemas integrados . LCTES '06. Nueva York, NY, EE. UU.: Association for Computing Machinery. págs. 34–43. doi :10.1145/1134650.1134657. ISBN 978-1-59593-362-1.S2CID13221224  .​
16. Reps, T.; Loginov, A.; Sagiv, M. (julio de 2002). "Minimización semántica de fórmulas proposicionales de 3 valores". Actas del 17.º Simposio anual IEEE sobre lógica en informática . págs. 40-51. doi :10.1109/LICS.2002.1029816. ISBN . 0-7695-1483-9.S2CID8451238  .​
17. Yoon, Yongho; Lee, Woosuk; Yi, Kwangkeun (6 de junio de 2023). "Síntesis de programas inductivos mediante interpretación abstracta iterativa hacia adelante y hacia atrás". Actas de la ACM sobre lenguajes de programación . 7 (PLDI): 174:1657–174:1681. arXiv : 2304.10768 . doi : 10.1145/3591288 .

Enlaces externos

• Una página web sobre interpretación abstracta mantenida por Patrick Cousot
• Artículo de Roberto Bagnara que muestra cómo es posible implementar un analizador estático basado en interpretación abstracta para un lenguaje de programación tipo C
• Simposios de análisis estático, actas que aparecen en la serie LNCS de Springer
• Conferencia sobre verificación, verificación de modelos e interpretación abstracta (VMCAI), afiliada a la conferencia POPL , actas que aparecen en la serie LNCS de Springer

Notas de la conferencia

• Interpretación abstracta. Patrick Cousot. MIT.
• Notas de la conferencia de David Schmidt sobre interpretación abstracta
• Notas de la conferencia de Møller y Schwarzbach sobre análisis de programas estáticos
• Apuntes de Agostino Cortesi sobre Análisis y verificación de programas
• Diapositivas de Grégoire Sutre que repasan cada paso de la interpretación abstracta con numerosos ejemplos y que también presentan las conexiones de Galois