clam
1.0.0
CLAM es un analizador estático basado en la interpretación abstracta que calcula los invariantes inductivos para el código de bits LLVM basado en la biblioteca de cangrejo. Esta rama admite LLVM 14.
La documentación disponible se puede encontrar tanto en Wiki de almeja como en Wiki de cangrejo.
Puede obtener almeja de Docker Hub (construido nocturno) usando el comando:
docker pull seahorn/clam-llvm14:nightly
La almeja está escrita en C ++ y usa en gran medida 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
La infraestructura de prueba depende de varios paquetes de Python. Para ejecutar pruebas debe instalar lit y OutputCheck :
pip3 install lit
pip3 install OutputCheck
Los pasos básicos de compilación son:
1. mkdir build && cd build
2. cmake -DCMAKE_INSTALL_PREFIX=$DIR ../
3. cmake --build . --target crab && cmake ..
4. cmake --build . --target extra && cmake ..
5. cmake --build . --target install
El comando en la línea 2 intentará encontrar LLVM 14 de las rutas estándar. Si instaló LLVM 14 en una ruta no estándar, agregue opción -DLLVM_DIR=$LLVM-14_INSTALL_DIR/lib/cmake/llvm a la línea 2. El comando en la línea 3 descargará el cangrejo y lo compilará de fuentes. Clam utiliza dos componentes externos que se instalan a través del objetivo extra en la línea 4. Estos componentes son:
SEA-DSA es el análisis de almacenamiento utilizado para traducir las instrucciones de memoria LLVM. Los detalles se pueden encontrar aquí y aquí.
LLVM-Seahorn ofrece versiones especializadas de componentes LLVM para que sean más susceptibles de verificación. llvm-seahorn es opcional, pero es muy recomendable.
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 de Pplite, agregue -DCRAB_USE_APRON=ON -DCRAB_USE_PPLITE=ON opciones.
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 almejas con cajas y delantal:
1. mkdir build && cd build
2. cmake -DCMAKE_INSTALL_PREFIX=$DIR -DCRAB_USE_LDD=ON -DCRAB_USE_APRON=ON ../
3. cmake --build . --target crab && cmake ..
4. cmake --build . --target extra && cmake ..
5. cmake --build . --target ldd && cmake ..
6. cmake --build . --target apron && cmake ..
7. cmake --build . --target install
Por ejemplo, las líneas 5 y 6 descargarán, compilarán e instalarán las cajas y las bibliotecas del delantal, respectivamente. Si ya ha compilado e instalado estas bibliotecas en su máquina, omita los comandos en la línea 5 y 6 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_DIR Para ejecutar algunas pruebas de regresión:
cmake --build . --target test-simple
Clam proporciona un script de Python llamado clam.py (ubicado en $DIR/bin , donde $DIR es el directorio donde se instaló la almeja) para interactuar con los usuarios. El comando más simple es clam.py test.c Escriba clam.py --help para todas las opciones y lea nuestro wiki.
