lart

Lart: herramienta de abstracción y refinamiento de LLVM

LART = LLVM Herramienta de abstracción y refinamiento. El objetivo de esta herramienta es proporcionar transformaciones LLVM a LLVM que implementen varias abstracciones del programa. En términos del conjunto de instrucciones, los programas resultantes son normales, programas concretos LLVM que pueden ejecutarse y analizarse. La información adicional sobre las abstracciones en efecto sobre un programa (fragmento) se inserta utilizando funciones intrínsecas LLVM especiales y nodos de metadatos LLVM. Lart proporciona una herramienta independiente que procesa archivos de código de bits en disco, así como un marco que puede integrarse en herramientas basadas en LLVM complejas. La principal motivación detrás de Lart es proporcionar un "preprocesador" para los controladores de modelos basados ​​en LLVM y otras herramientas de análisis, simplificando su trabajo al reducir el tamaño del problema sin comprometer la solidez de los análisis. Las abstracciones implementadas por Lart generalmente se pueden refinar en función de instrucciones específicas sobre qué "parte" de la abstracción es demasiado aproximada (una abstracción que es demasiado dura creará errores espurios visibles para los análisis posteriores pero no presente en el programa original).

Abstracciones para LLVM BitCode

El propósito de todo el ejercicio es abstraer la información del código de bits LLVM, haciendo que los análisis posteriores sean más eficientes (a expensas de cierta precisión). Con este fin, principalmente necesitamos poder codificar la elección no determinista en los programas LLVM, que se pueden hacer simplemente a través de una función de propósito especial (similar a las intrínsecs LLVM). La función se llama @lart.choice , toma un par de límites como argumentos y devuelve no deterministamente un valor que cae entre esos límites.

Esta extensión a la semántica de LLVM debe ser reconocida por la herramienta posterior. Esta es también la única desviación crucial del código de bits LLVM estándar. Muchas herramientas de análisis ya implementarán un mecanismo similar, internamente o incluso con una interfaz externa. La adaptación de herramientas sin soporte para @lart.choice para trabajar con Lart suele ser muy sencillo.

Hay otras funciones de uso especial proporcionadas por Lart, a saber, la familia @lart.meta.* , Pero en lo que respecta a estas instrucciones, la mayoría de las herramientas podrán ignorar de manera segura su existencia, al igual que con las llamadas existentes @llvm.dbg.* . Se esperaría que las transformaciones del programa retengan esas llamadas en caso de que se llame a Lart para refinar una abstracción (cada abstracción proporcionada por Lart viene con un procedimiento de refinamiento correspondiente, que a menudo necesitará encontrar las llamadas @lart.meta insertadas por la abstracción).

Mientras que la mayoría de los motores de abstracción tradicionales funcionan como intérpretes, las abstracciones también pueden "compilarse" en programas. En lugar de (re) interpretar instrucciones simbólicamente, las instrucciones simbólicas se pueden compilar. En el caso de la abstracción predicada, el código de bits resultante manipulará directamente y usará valoraciones de predicados en lugar de variables de concreto. Como se explicó anteriormente, la diferencia importante es que el código de bits necesita tomar decisiones no deterministas, ya que algunos predicados pueden tener valoraciones indeterminadas (son verdaderas y falsas). Algunas variables podrían incluso abstraer por completo, y todas las pruebas sobre tales variables producirán respuestas sí y no.

Construir

Use o repita la configuración de ./devcontainer/Dockerfile por el momento.

Entonces usa:

 ./scripts/build.sh

Ejecutar compilador

 ./build/bin/lartcc <domain> <compiler arguments> in.c

OPTAR

 opt -load build/lib/cc/liblart_module.so -lart < in.bc > out.bc

Prueba

 lit -v build/test

Nota: build/lartcc/lartcc tiene que tener permisiones exacutabple.