crab
1.0.0
El cangrejo es una biblioteca C ++ para construir análisis estáticos basados en la interpretación abstracta. El cangrejo proporciona un rico conjunto de dominios abstractos, solucionadores fixpoint basados en Kleene, así como diferentes análisis, como DataFlow, interprocedural y hacia atrás. El diseño del cangrejo es bastante modular, por lo que es fácil completar nuevos dominios y solucionadores abstractos o crear nuevos análisis.
Los dominios abstractos de cangrejo pueden razonar sobre el contenido de la memoria, matrices de tipo C y propiedades numéricas. El cangrejo utiliza implementaciones eficientes de dominios numéricos populares, como zonas y octágones y dominios novedosos para razonar, por ejemplo, sobre términos simbólicos (también conocido como funciones nointerpretadas). El cangrejo también implementa dominios no relacionales populares, como el intervalo o las congruencias que utilizan mapas de entorno eficientes, y permite la combinación de dominios arbitrarios a través de construcciones de productos reducidas estándar. El Crab también proporciona dominios no convexos, como intervalos disyuntivos especializados llamados cajas basadas en diagramas de decisión lineales y una estrategia de partición de valor más general que eleva un dominio arbitrario a una sobreproximación de su finalización de disyunción. Además de estos dominios, todos desarrollados por autores de cangrejos, la biblioteca de cangrejos integra bibliotecas de dominio abstractos populares como delantal, Elina y Pplite.
El cangrejo proporciona el solucionador FixPoint intercalado de última generación que utiliza el orden topológico débil de Bourdoncle para seleccionar el conjunto de puntos de ampliación. Para mitigar las pérdidas de precisión durante el ensanchamiento, el cangrejo implementa algunas técnicas populares, como la ampliación con umbrales y la ampliación de lookhead.
El cangrejo proporciona dos implementaciones diferentes de análisis interprocedurales: un análisis interprocedural de arriba hacia abajo con memoización con soporte para llamadas recursivas y un análisis híbrido de arriba hacia arriba + de arriba hacia abajo. Por último, pero no menos importante, el cangrejo también implementa un análisis hacia atrás más experimental que puede usarse para calcular las condiciones previas necesarias y/o reducir el número de falsas alarmas.
El cangrejo no analiza directamente un lenguaje de programación convencional, sino que analiza su propia representación intermedia basada en CFG llamada Crabir. Crabir es un código de tres direcciones y está fuertemente escrito. En Crabir, el flujo de control se define mediante instrucciones de GOTO no deterministas. Además de las operaciones booleanas y aritméticas estándar, Crabir proporciona declaraciones especiales de asumir y afirmar. El primero se puede usar para refinar el flujo de control y el segundo proporciona un mecanishm simple para verificar las propiedades definidas por el usuario. A pesar de su diseño simple, Crabir es lo suficientemente rico como para representar idiomas como LLVM.
El cangrejo está activamente en desarrollo. Si encuentra un error, abra un problema de GitHub. Las solicitudes de extracción con nuevas funciones son muy bienvenidas. La documentación disponible se puede encontrar en nuestro wiki. Si usa esta biblioteca, cita este documento.
| Windows | Ubuntu | OS X | Cobertura |
|---|---|---|---|
| TBD |  | TBD |
Una versión (nocturna) preconstruida de cangrejo que ejecuta todas las pruebas se puede obtener usando Docker:
docker pull seahorn/crab:bionic
docker run -v ` pwd ` :/host -it seahorn/crab:bionicEl cangrejo está escrito en C ++ y se basa en la biblioteca BOOST. Los principales requisitos son:
-DCRAB_USE_APRON=ON o -DCRAB_USE_ELINA=ON )-DCRAB_USE_PPLITE=ON )En Linux, puede instalar requisitos escribiendo los comandos:
sudo apt-get install libboost-all-dev libboost-program-options-dev
sudo apt-get install libgmp-dev
sudo apt-get install libmpfr-dev
sudo apt-get install libflint-dev
Para instalar cangrejo, escriba:
1. mkdir build && cd build
2. cmake -DCMAKE_INSTALL_PREFIX=$INSTALL_DIR ../
3. cmake --build . --target install
El directorio tests contiene muchos ejemplos de cómo construir programas escritos en crabir y calcular invariantes utilizando diferentes análisis y dominios abstractos. Para compilar estas pruebas, agregue la opción -DCRAB_ENABLE_TESTS=ON la línea 2.
Y luego, por ejemplo, para ejecutar test1 :
build/test-bin/test1
Las cajas/delantal/los dominios Elina/Pplite requieren bibliotecas de terceros. Para evitar la carga para los usuarios que no están interesados en esos dominios, la instalación de las bibliotecas es opcional.
Si desea usar el dominio de cuadros, agregue -DCRAB_USE_LDD=ON OPCIÓN.
Si desea usar los dominios de la biblioteca delantal, agregue -DCRAB_USE_APRON=ON OPCIÓN.
Si desea usar los dominios de la biblioteca Elina, agregue -DCRAB_USE_ELINA=ON OPCIÓN.
Si desea usar los dominios de la biblioteca Pplite, agregue -DCRAB_USE_PPLITE=ON OPCIÓN.
IMPORTANTE: Apron y Elina actualmente no son compatibles, por lo que no puede habilitar -DCRAB_USE_APRON=ON y -DCRAB_USE_ELINA=ON al mismo tiempo.
Por ejemplo, para instalar cangrejo con cajas y delantal, escriba:
1. mkdir build && cd build
2. cmake -DCMAKE_INSTALL_PREFIX=$INSTALL_DIR -DCRAB_USE_LDD=ON -DCRAB_USE_APRON=ON ../
3. cmake --build . --target ldd && cmake ..
4. cmake --build . --target apron && cmake ..
5. cmake --build . --target install
Las líneas 3 y 4 descargarán, compilarán e instalarán las cajas y los dominios del delantal, respectivamente. Reemplace apron en la línea 4 con elina o pplite si desea usar Elina o Pplite en su lugar. Si ya ha compilado e instalado estas bibliotecas en su máquina, omita los comandos en la línea 3 y 4 y agregue las siguientes opciones en la línea 2.
-DAPRON_ROOT=$APRON_INSTALL_DIR-DELINA_ROOT=$ELINA_INSTALL_DIR-DCUDD_ROOT=$CUDD_INSTALL_DIR -DLDD_ROOT=$LDD_INSTALL_DIR-DPPLITE_ROOT=$PPLITE_INSTALL_DIR -DFLINT_ROOT=$FLINT_INSTALL_DIRPara incluir el cangrejo en su aplicación C ++, debe:
Incluya los archivos de encabezado C ++ ubicados en $INSTALL_DIR/crab/include , y
Enlace su aplicación con las bibliotecas de cangrejo instaladas en $INSTALL_DIR/crab/lib .
Si se compila con cuadros/delantal/Elina/Pplite, también debe incluir $INSTALL_DIR/EXT/include y enlazar con $INSTALL_DIR/EXT/lib donde EXT=apron|elina|ldd|pplite .
Si su proyecto usa cmake , solo necesita agregar CMakeLists.txt de su proyecto.txt:
add_subdirectory(crab)
include_directories(${CRAB_INCLUDE_DIRS})
Y luego vincule su ejecutable con ${CRAB_LIBS}
Si su proyecto usa make , lea esta muestra MakeFile.
