seahorn
v0.1.0 Release (SV-COMP'16)
Seahorn es un marco de análisis automatizado para idiomas basados en LLVM. Esta versión se compila contra LLVM 14.
Algunas de las características compatibles son
Seahorn se desarrolla principalmente como un marco para realizar investigaciones en verificación automatizada. Los marcos proporcionan muchos componentes que se pueden juntar de varias maneras. Sin embargo, no es una herramienta de análisis estático "listo para usar".
Muchas herramientas y ejemplos de análisis se proporcionan con el marco. Estamos constantemente buscando nuevas aplicaciones y brindamos soporte a los nuevos usuarios. Para obtener más información sobre lo que está sucediendo, consulte nuestro blog (con poca frecuencia).
Seahorn se distribuye bajo una licencia BSD modificada. Consulte License.txt para más detalles.
Seahorn proporciona un guión de Python llamado sea para interactuar con los usuarios. Dado un programa C anotado con afirmaciones, los usuarios solo necesitan escribir: sea pf file.c
El resultado de sea-pf unsat está en cuenta si todas las afirmaciones se mantienen, un sat si se violan alguna de las afirmaciones.
La opción pf le dice a Seahorn que traduzca file.c al código de bits LLVM, genere un conjunto de condiciones de verificación (VC) y finalmente resuelva. El principal solucionador de back-end es espaciador.
El comando pf proporciona, entre otras, las siguientes opciones:
--show-invars : Mostrar invariantes calculados si la respuesta era unsat .
--cex=FILE : almacena un contraejemplo en FILE si la respuesta fue sat .
-g : se compila con información de depuración para contraexplicaciones más rastreables.
--step=large : codificación de paso grande. Cada relación de transición corresponde a un fragmento sin bucle.
--step=small : codificación de paso pequeño. Cada relación de transición corresponde a un bloque básico.
--track=reg : modelo (entero) solo registros.
--track=ptr : Registros y punteros del modelo (pero no contenido de memoria)
--track=mem : Modelo de escalares, punteros y contenido de la memoria
--inline : Inline el programa antes de la verificación
--crab : inyectar invariantes en spacer generados por la herramienta basada en la interpretación de resumen de cangrejo. Lea aquí para obtener detalles sobre todas las opciones de cangrejo (prefijo --crab ). Puede ver qué invariantes son inferidos por el cangrejo al escribir la opción --log=crab .
--bmc : use el motor BMC.
sea pf es una tubería que ejecuta múltiples comandos. Las partes individuales de la tubería también se pueden ejecutar por separado:
sea fe file.c -o file.bc : Seahorn Frontend traduce un programa C en código de bits LLVM optimizado, incluida la transformación de semántica mixta.
sea horn file.bc -o file.smt2 : Seahorn genera las condiciones de verificación de file.bc y las genera en formato SMT -LIB V2. Los usuarios pueden elegir entre diferentes estilos de codificación con varios niveles de precisión al agregar:
--step={small,large,fsmall,flarge} Donde una small codificación de pasos pequeños, large es una codificación de granja de bloques, fsmall es una pequeña codificación de pasos que produce cláusulas de bocina plana (es decir, genera un sistema de transición con solo un predicado) y flarge : codificación de bloques que producen clas de bocina plana.
--track={reg,ptr,mem} donde reg solo modela escalares enteros, modelos ptr reg y direcciones de puntero, y mem Models ptr y contenido de memoria.
sea smt file.c -o file.smt2 : genera CHC en formato SMT -LIB2. Es un alias para sea fe seguido de sea horn . El comando sea pf es un alias para sea smt --prove .
sea clp file.c -o file.clp : genera CHC en formato CLP.
sea lfe file.c -o file.ll : ejecuta el front -end heredado
Para ver todos los comandos, escriba sea --help . Para ver opciones para cada comando individual CMD (por ejemplo, horn ), tipo sea CMD --help (por ejemplo, sea horn --help ).
Seahorn no usa cangrejo por defecto. Para habilitar el cangrejo, agregue la opción --crab al comando sea .
El intérprete de abstracto es por defecto intraprocedural y utiliza el dominio de zonas como dominio abstracto numérico. Estas opciones predeterminadas deberían ser suficientes para los usuarios normales. Para los desarrolladores, si desea usar otros dominios abstractos, necesita:
cmake -DCRAB_USE_LDD=ON -DCRAB_USE_ELINA=ONsea con la opción --crab-dom=DOM DOM puede ser:int para intervalosterm-int para intervalos con funciones no interpretadasboxes : para intervalos disyuntivosoct para octágonespk para polihedra Para usar el análisis interprocedural de cangrejo, debe ejecutar sea con la opción --crab-inter
Por defecto, el intérprete abstracto solo razona sobre las variables escalares (es decir, registros LLVM). Ejecute sea con las opciones --crab-track=mem --crab-singleton-aliases=true para la razón sobre el contenido de la memoria.
El cangrejo es principalmente insensible a la ruta, mientras que el espaciador, nuestro solucionador de cláusula de cuerno, es sensible al camino. Aunque los análisis insensibles a la ruta son más eficientes, la sensibilidad a la ruta generalmente se requiere para probar la propiedad del interés. Esto motiva nuestra decisión de ejecutar First Crab (IF Opción --crab ) y luego pasar a los invariantes generados a Spacer. Actualmente hay dos formas para que Spacer use los invariantes generados por CRAB. La opción sea --horn-use-invs=VAL le dice spacer cómo usar esos invariantes:
VAL es igual a bg , los invariantes solo se usan para ayudar spacer a demostrar que un lema es inductivo.VAL es igual a always , el comportamiento es similar a bg , pero además los invariantes también se usan para ayudar spacer a bloquear un contraejemplo. El valor predeterminado es bg . Por supuesto, si el cangrejo puede demostrar que el programa es seguro, entonces Spacer no incurre en ningún costo adicional.
Se supone que las propiedades son afirmaciones. Seahorn proporciona un comando de afirmación estática sassert , como se ilustra en el siguiente ejemplo
/* verification command: sea pf --horn-stats test.c */
#include "seahorn/seahorn.h"
extern int nd ();
int main ( void ) {
int k = 1 ;
int i = 1 ;
int j = 0 ;
int n = nd ();
while ( i < n ) {
j = 0 ;
while ( j < i ) {
k += ( i - j );
j ++ ;
}
i ++ ;
}
sassert ( k >= n );
} Internamente, Seahorn sigue la convención SV-Comp de codificación de ubicaciones de errores mediante una llamada a la función de error designada __VERIFIER_error() . Seahorn regresa unsat cuando __VERIFIER_error() es inalcanzable, y el programa se considera seguro. Seahorn Devuelve sat cuando __VERIFIER_error() es accesible y el programa no es seguro. El método sassert() se define en seahorn/seahorn.h . H.
Además de probar propiedades o producir contraejemplos, a veces es útil inspeccionar el código en análisis para tener una idea de su complejidad. Para esto, Seahorn proporciona un comando sea inspect . Por ejemplo, dado un programa C de ex.c :
sea inspect ex.c --sea-dsa=cs+t --mem-dot
La opción --sea-dsa=cs+t permite el nuevo análisis SEA-DSA sensible al tipo de contexto descrito en FMCAD19. Este comando genera un archivo FUN.mem.dot para cada función FUN en el programa de entrada. Para visualizar el gráfico de la función principal, use la interfaz Web Graphivz o los siguientes comandos:
$ dot -Tpdf main.mem.dot -o main.mem.pdfMás detalles sobre los gráficos de memoria se encuentran en el repositorio de SEADSA: aquí.
Use sea inspect --help para ver todas las opciones. Actualmente, las opciones disponibles son:
sea inspect --profiler imprime el número de funciones, bloques básicos, bucles, etc.sea inspect --mem-callgraph-dot Impresiones para dot el gráfico de llamadas construido por SEADSA.sea inspect --mem-callgraph-stats Impresiones a salida estándar algunas estatus estatales sobre la construcción del gráfico de llamadas realizado por SEADSA.sea inspect --mem-smc-stats imprime la cantidad de accesos de memoria que SEADSA puede demostrar que SEADSA puede demostrar que SEADSA.La forma más fácil de comenzar con Seahorn es a través de una distribución de Docker.
$ docker pull seahorn/seahorn-llvm10:nightly
$ docker run --rm -it seahorn/seahorn-llvm10:nightly Comience por explorar lo que puede hacer el comando sea :
$ sea --help
$ sea pf --help La etiqueta nightly se actualiza automáticamente diariamente y contiene la última versión de desarrollo. Mantenemos todas las demás etiquetas (que requieren actualización manual) con poca frecuencia. Verifique las fechas en DockerHub y registre un problema en GitHub si son demasiado obsoletos.
Ejemplos adicionales y opciones de configuración están en el blog. El blog se actualiza con poca frecuencia. En particular, las opciones cambian, las características se eliminan gradualmente, se agregan cosas nuevas. Si encuentra problemas en el blog, háganoslo saber. Al menos actualizaremos la publicación del blog para indicar que no se espera que funcione con la última versión del código.
También puede instalar manualmente por:
Siguiendo las instrucciones en el archivo Docker Dockerfile: docker/seahorn-builder.Dockerfile .
Si esto no funciona, ejecute:
$ wget https://apt.llvm.org/llvm.sh
$ chmod +x llvm.sh
$ sudo ./llvm.sh 14
$ apt download libpolly-14-dev && sudo dpkg --force-all -i libpolly-14-dev *Los primeros 3 comandos instalarán LLVM 14, el 4to instalará libpolly, que se omite erróneamente de LLVM 14 (pero se incluye en versiones posteriores)
A continuación, siga la instrucción en el archivo Docker anterior
La información a partir de este punto es solo para desarrolladores. Si desea contribuir a Seahorn, construya sus propias herramientas en función de ello o simplemente interesado en cómo funciona dentro, sigue leyendo.
Seahorn requiere LLVM, Z3 y Boost. Las versiones exactas de las bibliotecas siguen cambiando, pero CMake Craft se usa para verificar que la versión correcta esté disponible.
Para especificar una versión específica de cualquiera de las dependencias, use las variables CMake habituales <PackageName>_ROOT y/o <PackageName>_DIR (consulte Find_Package () para obtener detalles).
Seahorn se divide en múltiples componentes que viven en diferentes repositorios (bajo la organización Seahorn). El proceso de compilación verifica automáticamente todo según sea necesario. Para las instrucciones de compilación actuales, consulte los scripts CI.
Estos son los pasos genéricos. No los uses. Sigue leyendo para una mejor manera:
cd seahorn ; mkdir build ; cd build (el directorio de compilación también puede estar fuera del directorio de origen).cmake -DCMAKE_INSTALL_PREFIX=run ../ (¡es necesario instalar! )cmake --build . --target extra && cmake .. (componentes de clones que viven en otro lugar)cmake --build . --target crab && cmake .. (Biblioteca de cangrejo de clones)cmake --build . --target install (construir e instalar todo en run )cmake --build . --target test-all (Ejecutar pruebas)Nota : ¡El objetivo de instalación es necesario para que las pruebas funcionen!
Para una experiencia de desarrollo mejorada:
clanglld Linkercompile_commands.json En Linux, sugerimos la siguiente configuración cmake :
$ cd build
$ cmake -DCMAKE_INSTALL_PREFIX=run
-DCMAKE_BUILD_TYPE=RelWithDebInfo
-DCMAKE_CXX_COMPILER="clang++-14"
-DCMAKE_C_COMPILER="clang-14"
-DSEA_ENABLE_LLD=ON
-DCMAKE_EXPORT_COMPILE_COMMANDS=1
../
-DZ3_ROOT=<Z3_ROOT>
-DLLVM_DIR=<LLMV_CMAKE_DIR>
-GNinja
$ (cd .. && ln -sf build/compile_commands.json .)
donde <Z3_ROOT es un directorio que contiene distribución binaria Z3, y LLMV_CMAKE_DIR es un directorio que contiene LLVMConfig.cmake .
Otras opciones legales para CMAKE_BUILD_TYPE son Debug y Coverage . Tenga en cuenta que el CMAKE_BUILD_TYPE debe ser compatible con el utilizado para compilar LLVM . En particular, necesitará una construcción Debug de LLVM para compilar SeaHorn en el modo `debug **. Asegúrese de tener mucha paciencia, espacio en disco y tiempo si decide seguir esta ruta.
Alternativamente, el proyecto se puede configurar utilizando presets Cmake. Para hacer esto, simplemente ejecute el siguiente comando:
$ cmake --preset < BUILD_TYPE > - < PRESET_NAME > Para configurar cmake, donde <BUILD_TYPE> es uno de: Debug , RelWithDebInfo o Coverage y <PRESET_NAME> es el preajuste que le gustaría usar. Los presets que están actualmente disponibles son: jammy . Estos preajustes suponen que tiene Z3 instalado en /opt/z3-4.8.9 y Yices instalados en /opt/yices-2.6.1 .
Esto también permitirá que el proyecto se configure y compilará dentro del código VS utilizando la extensión de herramientas CMake.
Si desea utilizar diferentes configuraciones de compilación o si tiene Z3 o Yices instalados en cualquier otro directorio, deberá hacer su propio archivo CMakeUserPresets.json con sus propios preajustes.
No incluya -DSEA_ENABLE_LLD=ON . El compilador predeterminado es el rango, por lo que es posible que no necesite configurarlo explícitamente.
Seahorn proporciona varios componentes que se clonan e instalan automáticamente a través del objetivo extra . Estos componentes pueden ser utilizados por otros proyectos fuera de Seahorn.
Sea-DDSA: git clone https://github.com/seahorn/sea-dsa.git
sea-dsa es un nuevo análisis de montón basado en DSA. A diferencia de llvm-dsa , sea-dsa es sensible al contexto y, por lo tanto, una partición de grano más fino del montón se puede generar en presencia de llamadas de funciones.
Almeja: git clone https://github.com/seahorn/crab-llvm.git
clam proporciona invariantes inductivos utilizando técnicas de interpretación abstracta para el resto de los backends de Seahorn.
llvm-Seahorn: git clone https://github.com/seahorn/llvm-seahorn.git
llvm-seahorn proporciona versiones personalizadas a verificación de los pases InstCombine e IndVarSimplify LLVM, así como un pase LLVM para convertir valores indefinidos en llamadas no deterministas, entre otras cosas.
Seahorn no viene con su propia versión de Clang y espera encontrarla en el directorio de compilación ( run/bin ) o en el camino. Asegúrese de que la versión de Clang coincida con la versión de LLVM que se usó para compilar Seahorn (actualmente LLVM14). La forma más fácil de proporcionar la versión correcta de Clang es descargarla de LLVM.org, impactarla en algún lugar y crear un enlace simbólico a clang y clang++ en run/bin .
$ cd seahorn/build/run/bin
$ ln -s < CLANG_ROOT > /bin/clang clang
$ ln -s < CLANG_ROOT > /bin/clang++ clang++ donde <CLANG_ROOT> es la ubicación en la que se desempaquetó Clang.
La infraestructura de prueba depende de varios paquetes de Python. Estos tienen sus propias dependencias. Si no puede resolverlos, use Docker en su lugar.
$ pip install lit OutputCheck networkx pygraphviz Podemos usar gcov y lcov para generar información de cobertura de prueba para Seahorn. Para construir con la cobertura habilitada, necesitamos ejecutar la compilación en un directorio diferente y establecer CMAKE_BUILD_TYPE en Coverage durante la configuración de CMake.
Ejemplo de pasos para generar informe de cobertura para el objetivo test-opsem :
mkdir coverage; cd coverage Crear e ingresar el directorio de construcción de coberturacmake -DCMAKE_BUILD_TYPE=Coverage <other flags as you wish> ../cmake --build . --target test-opsem Ejecute las pruebas OPSEM, ahora se deben crear archivos .gcda y .gcno en los directorios CMakeFiles correspondienteslcov -c --directory lib/seahorn/CMakeFiles/seahorn.LIB.dir/ -o coverage.info recopilar datos de cobertura del módulo deseado, si clang se usa como compilador en lugar de gcc , cree un script bash llvm-gcov.sh : #! /bin/bash
exec llvm-cov gcov " $@ " $ chmod +x llvm-gcov.sh luego agregar --gcov-tool <path_to_wrapper_script>/llvm-gcov.sh al comando lcov -c ... 6. Extraiga datos de los directorios deseados y genere el informe HTML:
lcov --extract coverage.info " */lib/seahorn/* " -o lib.info
lcov --extract coverage.info " */include/seahorn/* " -o header.info
cat header.info lib.info > all.info
genhtml all.info --output-directory coverage_report Luego abra coverage_report/index.html en el navegador para ver el informe de cobertura
Consulte también scripts/coverage para los scripts utilizados por el CI. El informe de cobertura para compilaciones nocturnas está disponible en CodeCov
Base de datos de compilación para el proyecto Seahorn y todos sus subproyectos se genera utilizando -DCMAKE_EXPORT_COMPILE_COMMANDS=ON OPCIÓN PARA cmake .
Una manera fácil de obtener la indexación de código para funcionar con el soporte de la base de datos de compilación es vincular el archivo compilation_database.json en el directorio principal del proyecto y seguir instrucciones específicas para su editor.
lsp-ui con clangd que están disponibles en Spacemacs Develop Branch Para una guía detallada para un flujo de trabajo remoto con Clion Check Clion-Configuration.
Use nuestro bifurcado de mainframer. No se pierda la configuración de ejemplo.
