En informática , la ejecución simbólica (también evaluación simbólica o symbex ) es un medio de analizar un programa para determinar qué entradas hacen que se ejecute cada parte de un programa . Un intérprete sigue el programa, asumiendo valores simbólicos para las entradas en lugar de obtener entradas reales como lo haría la ejecución normal del programa. De este modo, llega a expresiones en términos de esos símbolos para expresiones y variables en el programa, y restricciones en términos de esos símbolos para los posibles resultados de cada rama condicional. Finalmente, las posibles entradas que activan una rama se pueden determinar resolviendo las restricciones.
El campo de la simulación simbólica aplica el mismo concepto al hardware. La computación simbólica aplica el concepto al análisis de expresiones matemáticas.
Considere el programa a continuación, que lee un valor y falla si la entrada es 6.
entero f () { ... y = leer (); z = y * 2 ; si ( z == 12 ) { fallar (); } demás { printf ( "OK" ); }}Durante una ejecución normal (ejecución "concreta"), el programa leería un valor de entrada concreto (por ejemplo, 5) y lo asignaría a y. Luego, la ejecución continuaría con la multiplicación y la rama condicional, que se evaluaría como falso e imprimiría OK.
Durante la ejecución simbólica, el programa lee un valor simbólico (por ejemplo, λ) y lo asigna a y. El programa luego procedería con la multiplicación y asignaría λ * 2a z. Al llegar a la ifdeclaración, evaluaría λ * 2 == 12. En este punto del programa, λpodría tomar cualquier valor y, por lo tanto, la ejecución simbólica puede continuar a lo largo de ambas ramas, "bifurcando" dos caminos. A cada camino se le asigna una copia del estado del programa en la instrucción de bifurcación, así como una restricción de ruta. En este ejemplo, la restricción de ruta es λ * 2 == 12para la iframa y λ * 2 != 12para la elserama. Ambos caminos se pueden ejecutar simbólicamente de forma independiente. Cuando las rutas terminan (por ejemplo, como resultado de la ejecución fail()o simplemente de la salida), la ejecución simbólica calcula un valor concreto para λal resolver las restricciones de ruta acumuladas en cada ruta. Estos valores concretos se pueden considerar como casos de prueba concretos que pueden, por ejemplo, ayudar a los desarrolladores a reproducir errores. En este ejemplo, el solucionador de restricciones determinaría que, para llegar a la fail()declaración, λnecesitaría ser igual a 6.
La ejecución simbólica de todas las rutas de programa factibles no es escalable para programas grandes. La cantidad de rutas factibles en un programa crece exponencialmente con el aumento del tamaño del programa e incluso puede ser infinita en el caso de programas con iteraciones de bucle ilimitadas. [1] Las soluciones al problema de explosión de rutas generalmente utilizan heurísticas para la búsqueda de rutas para aumentar la cobertura del código, [2] reducen el tiempo de ejecución mediante la paralelización de rutas independientes, [3] o mediante la fusión de rutas similares. [4] Un ejemplo de fusión es el veritesting , que "emplea la ejecución simbólica estática para amplificar el efecto de la ejecución simbólica dinámica". [5]
La ejecución simbólica se utiliza para razonar sobre un programa ruta por ruta, lo que es una ventaja sobre el razonamiento sobre un programa entrada por entrada como lo utilizan otros paradigmas de prueba (por ejemplo, el análisis dinámico de programas ). Sin embargo, si pocas entradas toman la misma ruta a través del programa, hay poco ahorro en comparación con probar cada una de las entradas por separado.
La ejecución simbólica es más difícil cuando se puede acceder a la misma ubicación de memoria a través de diferentes nombres ( aliasing ). El aliasing no siempre se puede reconocer de forma estática, por lo que el motor de ejecución simbólica no puede reconocer que un cambio en el valor de una variable también cambia el de la otra. [6]
Dado que una matriz es una colección de muchos valores distintos, los ejecutores simbólicos deben tratar la matriz completa como un valor o tratar cada elemento de la matriz como una ubicación separada. El problema de tratar cada elemento de la matriz por separado es que una referencia como "A[i]" solo se puede especificar de forma dinámica, cuando el valor de i tiene un valor concreto. [6]
Los programas interactúan con su entorno realizando llamadas al sistema , recibiendo señales, etc. Pueden surgir problemas de coherencia cuando la ejecución llega a componentes que no están bajo el control de la herramienta de ejecución simbólica (por ejemplo, el núcleo o las bibliotecas). Considere el siguiente ejemplo:
int principal () { ARCHIVO * fp = fopen ( "doc.txt" ); ... si ( condición ) { fputs ( "algunos datos" , fp ); } demás { fputs ( "algunos otros datos" , fp ); } ... datos = fgets (..., fp ); }Este programa abre un archivo y, en función de una condición, escribe distintos tipos de datos en el archivo. Luego, vuelve a leer los datos escritos. En teoría, la ejecución simbólica bifurcaría dos rutas en la línea 5 y cada ruta a partir de allí tendría su propia copia del archivo. Por lo tanto, la instrucción en la línea 11 devolvería datos que son consistentes con el valor de "condición" en la línea 5. En la práctica, las operaciones de archivo se implementan como llamadas del sistema en el núcleo y están fuera del control de la herramienta de ejecución simbólica. Los principales enfoques para abordar este desafío son:
Ejecución directa de llamadas al entorno. La ventaja de este enfoque es que es fácil de implementar. La desventaja es que los efectos secundarios de dichas llamadas afectarán todos los estados administrados por el motor de ejecución simbólica. En el ejemplo anterior, la instrucción en la línea 11 devolvería "algunos datosalgunos otros datos" o "algunos otros datosalgunosdatos" según el orden secuencial de los estados.
Modelado del entorno. En este caso, el motor instrumenta las llamadas del sistema con un modelo que simula sus efectos y que guarda todos los efectos secundarios en un almacenamiento por estado. La ventaja es que se obtendrían resultados correctos al ejecutar simbólicamente programas que interactúan con el entorno. La desventaja es que es necesario implementar y mantener muchos modelos potencialmente complejos de llamadas del sistema. Herramientas como KLEE, [7] Cloud9 y Otter [8] adoptan este enfoque implementando modelos para operaciones del sistema de archivos, sockets, IPC , etc.
Bifurcación del estado completo del sistema. Las herramientas de ejecución simbólica basadas en máquinas virtuales resuelven el problema del entorno bifurcando el estado completo de la máquina virtual. Por ejemplo, en S2E [9] cada estado es una instantánea de la máquina virtual independiente que se puede ejecutar por separado. Este enfoque alivia la necesidad de escribir y mantener modelos complejos y permite ejecutar simbólicamente prácticamente cualquier binario de programa. Sin embargo, tiene mayores gastos generales de uso de memoria (las instantáneas de la máquina virtual pueden ser grandes).
El concepto de ejecución simbólica se introdujo académicamente en la década de 1970 con descripciones de: el sistema Select, [12] el sistema EFFIGY, [13] el sistema DISSECT, [14] y el sistema de Clarke. [15]