Ejecución simbólica

La ejecución simbólica de todas las rutas de programa factibles no es escalable para programas grandes. El número de rutas factibles en un programa crece exponencialmente con el aumento del tamaño del programa e incluso puede ser infinito en el caso de programas con iteraciones de bucle ilimitadas. ^{[ 1 ]} Las soluciones al problema de la explosión de rutas generalmente utilizan heurísticas para la búsqueda de rutas para aumentar la cobertura de código, ^{[ 2 ]} reducen el tiempo de ejecución paralelizando rutas independientes, ^{[ 3 ]} o fusionando 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 analizar un programa paso a paso, lo cual supone una ventaja frente al análisis entrada por entrada, como hacen otros paradigmas de prueba (por ejemplo, el análisis dinámico de programas ). Sin embargo, si pocas entradas siguen la misma ruta a través del programa, el ahorro es mínimo en comparación con probar cada entrada por separado.

La ejecución simbólica es más difícil cuando se puede acceder a la misma ubicación de memoria mediante diferentes nombres ( alias ). Los alias no siempre se pueden 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 la otra. ^{[ 6 ]}

Dado que un array es una colección de muchos valores distintos, los ejecutores simbólicos deben tratar todo el array como un solo valor o tratar cada elemento del array como una ubicación separada. El problema de tratar cada elemento del array por separado es que una referencia como "A[i]" solo se puede especificar dinámicamente, cuando el valor de i tiene un valor concreto. ^{[ 6 ]}

Los programas interactúan con su entorno mediante llamadas al sistema , recepción de señales, etc. Pueden surgir problemas de consistencia cuando la ejecución alcanza 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 main () { FILE * fp = fopen ( "my_document.txt" , "w" ); char data [ 100 ]; bool cond = /* alguna condición aquí */ ; if ( cond ) { fputs ( "Algunos datos" , fp ); } else { fputs ( "Otros datos" , fp ); } fgets ( data , sizeof ( data ), fp ); }

Este programa abre un archivo y, según una condición, escribe diferentes tipos de datos en él. Posteriormente, lee 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 ahí tendría su propia copia del archivo. Por lo tanto, la instrucción en la línea 11 devolvería datos consistentes con el valor de "condición" en la línea 5. En la práctica, las operaciones de archivo se implementan como llamadas al 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:

Ejecutar llamadas al entorno directamente. La ventaja de este enfoque es su sencillez de implementación. La desventaja es que los efectos secundarios de dichas llamadas sobrescribirán todos los estados gestionados por el motor de ejecución simbólica. En el ejemplo anterior, la instrucción de la línea 11 devolvería "algunos datos, otros datos" o "otros datos, algunos datos" dependiendo del orden secuencial de los estados.

Modelado del entorno. En este caso, el motor instrumenta las llamadas al sistema con un modelo que simula sus efectos y que almacena todos los efectos secundarios en un almacenamiento por estado. La ventaja es que se obtienen resultados correctos al ejecutar simbólicamente programas que interactúan con el entorno. La desventaja es que se necesita implementar y mantener muchos modelos potencialmente complejos de llamadas al sistema. Herramientas como KLEE, ^{[ 7 ]} Cloud9 y Otter ^{[ 8 ]} adoptan este enfoque implementando modelos para operaciones del sistema de archivos, sockets, IPC , etc.

La bifurcación del estado completo del sistema. Las herramientas de ejecución simbólica basadas en máquinas virtuales resuelven el problema del entorno mediante la bifurcación del estado completo de la máquina virtual. Por ejemplo, en S2E ^{[ 9 ],} cada estado es una instantánea independiente de la máquina virtual que puede ejecutarse por separado. Este enfoque reduce la necesidad de escribir y mantener modelos complejos y permite ejecutar simbólicamente prácticamente cualquier binario de programa. Sin embargo, conlleva un mayor consumo de memoria (las instantáneas de la máquina virtual pueden ser grandes).