Esto está escrito en la entrada wiki de Ejecución simbólica , pero no puedo encontrar ninguna referencia para ello. ¿Alguien puede mostrarme un puntero? Gracias.
15
Esto está escrito en la entrada wiki de Ejecución simbólica , pero no puedo encontrar ninguna referencia para ello. ¿Alguien puede mostrarme un puntero? Gracias.
No conozco un artículo relacionado con la comparación entre ejecución simbólica e interpretación abstracta. Tampoco creo que se necesite uno. Leer las descripciones originales de estas dos técnicas debería ser suficiente.
(Por el contrario, si hubiera alguna conexión inesperada, entonces valdría la pena describirlo. Pero dudo mucho que sea así).
La idea principal de la ejecución simbólica es que, en un punto arbitrario de ejecución, puede expresar los valores de todas las variables como funciones de los valores iniciales. La idea principal de la interpretación abstracta es que puede explorar sistemáticamente todas las ejecuciones de un programa mediante una serie de aproximaciones excesivas. (Puedo escuchar a varios entusiastas de la IA quejándose por la aproximación previa).
Por lo tanto, al menos en la formulación original, la ejecución simbólica no estaba relacionada con la exploración de todas las ejecuciones posibles. Puedes ver esto incluso en el título: incluye la palabra 'prueba'. Pero aquí hay más de la Sección 8: "Para los programas con árboles de ejecución infinitos, la prueba simbólica no puede ser exhaustiva y no se puede establecer una prueba absoluta de corrección".
En contraste, la interpretación abstracta tiene como objetivo explorar todas las ejecuciones. Para hacerlo, utiliza varios ingredientes, uno de los cuales es muy similar a la idea principal de ejecución simbólica. Estos ingredientes son (1) estados abstractos, (2) unión y ampliación (por lo tanto, 'retícula' en el título).
Estados abstractosEl estado concreto de un programa en un momento determinado es básicamente una instantánea del contenido de la memoria (incluido el código del programa y el contador del programa). Esto tiene muchos detalles, lo cual es difícil de rastrear. Cuando analiza una propiedad en particular, es posible que desee ignorar grandes partes del estado concreto. O es posible que solo le importe si una variable en particular es negativa, cero o positiva, pero no le importa su valor exacto. En general, desea considerar una versión abstracta del estado concreto. Para que esto funcione, debe tener una propiedad de conmutatividad: si toma un estado concreto, ejecuta una declaración y luego abstrae el estado resultante, debe obtener el mismo resultado que si abstrae el estado inicial y luego ejecuta el mismo declaración pero sobre el estado abstracto. Este diagrama de conmutatividad aparece en ambos documentos. Esta es la idea común. Una vez más, la interpretación abstracta es más general, ya que no dicta cómo abstraer un estado, solo dice que debería haber una manera de hacerlo. En contraste, la ejecución simbólica dice que usa expresiones (simbólicas) que mencionan los valores iniciales.
Unirse y ensancharse. Si la ejecución del programa alcanza una determinada declaración de dos maneras diferentes, la ejecución simbólica no intenta fusionar los dos análisis. Es por eso que la cita anterior habla de árboles de ejecución, en lugar de dags. Pero, recuerde que la interpretación abstracta quiere cubrir todas las ejecuciones. Por lo tanto, pide una forma de fusionar los análisis de dos ejecuciones en el punto donde tienen el mismo contador de programa. (La unión podríaser muy tonto ({a} join {b} = {a, b}) de modo que equivale a lo que hace la ejecución simbólica). En general, unirse no es suficiente para garantizar que finalmente termine de analizar todas las ejecuciones. (En particular, la unión tonta mencionada anteriormente no funcionará). Considere un programa con un bucle: "n = input (); para i en el rango (n): dostuff ()". ¿Cuántas veces deberías dar la vuelta y seguir uniéndote? Ninguna respuesta fija funciona. Por lo tanto, se necesita algo más, y se está ampliando , lo que puede verse como una heurística. Supongamos que recorrió el circuito 3 veces y aprendió que "i = 0 o i = 1 o i = 2". Luego dices: hmmm, ... ensanchémonos, y obtienes "i> = 0". Una vez más, la interpretación abstracta no dice cómo hacer el ensanchamiento, solo dice qué propiedades debe tener el ensanchamiento.
(Perdón por esta larga respuesta: realmente no tuve tiempo para acortarla).
Creo que esto se entiende en un sentido muy superficial. El primer paso de la interpretación abstracta es identificar una semántica de recolección concreta. En lugar de describir la evolución de un solo estado, la semántica de recopilación describe la evolución de conjuntos de estados. Dado que las razones de ejecución simbólica sobre las representaciones de conjuntos de estados, se puede argumentar que representa la semántica concreta del programa. No tengo conocimiento de que se esté elaborando una correspondencia más precisa.
Ver Patrick Cousot. Métodos iterativos de construcción y aproximación de puntos fijos de operadores monótonos sobre un fondo, analizar semántica de programas (Métodos iterativos para la construcción y aproximación de puntos fijos de operadores monótonos en redes, análisis estático de programas). Thèse ès Sciences Mathématiques, Université Joseph Fourier, Grenoble, Francia, 21 de marzo de 1978. https://cs.nyu.edu/~pcousot/publications.www/CousotTheseEsSciences1978.pdf (desafortunadamente en francés), página (3) -27 a (3) -29
fuente