seahorn
v0.1.0 Release (SV-COMP'16)
Seahorn est un cadre d'analyse automatisé pour les langues basées sur LLVM. Cette version compile contre LLVM 14.
Certaines des fonctionnalités prises en charge sont
Seahorn est développé principalement comme un cadre pour mener des recherches en vérification automatisée. Les cadres fournit de nombreux composants qui peuvent être assemblés de différentes manières. Cependant, ce n'est pas un outil d'analyse statique "prêt à l'emploi".
De nombreux outils et exemples d'analyse sont fournis avec le cadre. Nous recherchons constamment de nouvelles applications et fournissons un support aux nouveaux utilisateurs. Pour plus d'informations sur ce qui se passe, consultez notre blog (rarement mis à jour).
Seahorn est distribué sous une licence BSD modifiée. Voir Licence.txt pour plus de détails.
Seahorn fournit un script Python appelé sea pour interagir avec les utilisateurs. Étant donné un programme C annoté avec des affirmations, les utilisateurs ont juste besoin de taper: sea pf file.c
Le résultat de sea-pf unsat si l'on tient toutes les affirmations, une sat si l'une des affirmations est violée.
L'option pf indique à Seahorn de traduire file.c en Bitcode LLVM, générer un ensemble de conditions de vérification (VC) et enfin, les résoudre. Le solveur principal principal est l'espaceur.
La commande pf fournit, entre autres, les options suivantes:
--show-invars : affichez des invariants calculés si la réponse était unsat .
--cex=FILE : stocke un contre-exemple dans FILE si la réponse était sat .
-g : compile avec des informations de débogage pour des contre-exemples plus traçables.
--step=large : encodage en grande étape. Chaque relation de transition correspond à des fragments sans boucle.
--step=small : Encodage en petit pas. Chaque relation de transition correspond à un bloc de base.
--track=reg : modèle (entier) enregistre uniquement.
--track=ptr : Registres et pointeurs du modèle (mais pas de contenu de mémoire)
--track=mem : modéliser les scalaires, les pointeurs et le contenu de la mémoire
--inline : Inligne le programme avant vérification
--crab : Injecter les invariants dans spacer généré par l'outil basé sur l'interprétation du crabe. Lisez ici pour plus de détails sur toutes les options de crabe (Prefix --crab ). Vous pouvez voir quelles invariants sont déduits par crabe en tapant l'option --log=crab .
--bmc : Utilisez le moteur BMC.
sea pf est un pipeline qui exécute plusieurs commandes. Les parties individuelles du pipeline peuvent également être exécutées séparément:
sea fe file.c -o file.bc : Seahorn Frontend traduit un programme C en code binaire LLVM optimisé, y compris la transformation en sémantique mixte.
sea horn file.bc -o file.smt2 : Seahorn génère les conditions de vérification à partir de file.bc et les produit au format SMT-lib V2. Les utilisateurs peuvent choisir entre différents styles de codage avec plusieurs niveaux de précision en ajoutant:
--step={small,large,fsmall,flarge} où small est un petit pas encoding, large est en codage de bloc, fsmall est un petit pas, produisant des clauses à corne plate (c'est-à-dire qu'elle génère un système de transition avec un seul prédicat), et flarge recours à la corne de blocs produisant des clauses de corne plate.
--track={reg,ptr,mem} où reg ne modélise que les scalaires entiers, les modèles ptr reg et les adresses de pointeur, et les modèles mem ptr et le contenu de la mémoire.
sea smt file.c -o file.smt2 : génère CHC au format SMT-lib2. Est un alias pour sea fe suivi d' sea horn . Le Command sea pf est un alias pour sea smt --prove .
sea clp file.c -o file.clp : génère CHC au format CLP.
sea lfe file.c -o file.ll : exécute le front-end hérité
Pour voir toutes les commandes, tapez sea --help . Pour voir les options pour chaque commande individuelle CMD (par exemple, horn ), Type sea CMD --help (par exemple, sea horn --help ).
Seahorn n'utilise pas de crabe par défaut. Pour activer le crabe, ajoutez l'option --crab à la commande sea .
L'interprète abstrait est par défaut intra-procédural et il utilise le domaine des zones comme domaine abstrait numérique. Ces options par défaut devraient être suffisantes pour les utilisateurs normaux. Pour les développeurs, si vous souhaitez utiliser d'autres domaines abstraits, vous devez:
cmake -DCRAB_USE_LDD=ON -DCRAB_USE_ELINA=ONsea avec l'option --crab-dom=DOM où DOM peut être:int pour les intervallesterm-int pour les intervalles avec des fonctions non interprétéesboxes : pour des intervalles disjonctifsoct pour les octagonespk pour Polyhedra Pour utiliser l'analyse interprocédurale du crabe, vous devez exécuter sea avec l'option --crab-inter
Par défaut, l'interprète abstrait uniquement sur les variables scalaires (c'est-à-dire les registres LLVM). Exécutez sea avec les options --crab-track=mem --crab-singleton-aliases=true raison sur le contenu de la mémoire.
Le crabe est principalement insensible au chemin tandis que l'espaceur, notre solveur de clause Horn, est sensible au chemin. Bien que les analyses insensibles au chemin soient plus efficaces, la sensibilité au chemin est généralement nécessaire pour prouver la propriété d'intérêt. Cela motive notre décision de courir le premier crabe (IF Option --crab ), puis de passer les invariants générés à l'espaceur. Il existe actuellement deux façons pour l'espacer d'utiliser les invariants générés par le crabe. L'option sea --horn-use-invs=VAL raconte spacer comment utiliser ces invariants:
VAL est égal à bg , les invariants ne sont utilisés que pour aider spacer à prouver qu'un lemme est inductif.VAL est égal à always , le comportement est similaire à bg mais que les invariants sont également utilisés pour aider spacer à bloquer un contre-exemple. La valeur par défaut est bg . Bien sûr, si le crabe peut prouver que le programme est sûr, l'espaceur n'engage à aucun coût supplémentaire.
Les propriétés sont supposées être des affirmations. Seahorn fournit un sassert de commande d'affirmation statique, comme illustré dans l'exemple suivant
/* 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 );
} En interne, Seahorn suit la convention SV-COMP des emplacements d'erreur de codage par un appel à la fonction d'erreur désignée __VERIFIER_error() . Seahorn renvoie unsat que __VERIFIER_error() est inaccessible, et le programme est considéré comme sûr. Seahorn revient sat lorsque __VERIFIER_error() est accessible et que le programme est dangereux. La méthode sassert() est définie dans seahorn/seahorn.h .
En plus de prouver les propriétés ou de produire des contre-exemples, il est parfois utile d'inspecter le code d'analyse pour avoir une idée de sa complexité. Pour cela, Seahorn fournit une sea inspect de commande. Par exemple, étant donné un programme C ex.c Type:
sea inspect ex.c --sea-dsa=cs+t --mem-dot
L'option --sea-dsa=cs+t permet une nouvelle analyse de SEA-DSA SEA-SA-SEA-SENSITIVE décrite dans FMCAD19. Cette commande génère un fichier FUN.mem.dot pour chaque fonction FUN dans le programme d'entrée. Pour visualiser le graphique de la fonction principale, utilisez l'interface Web GraphIvz ou les commandes suivantes:
$ dot -Tpdf main.mem.dot -o main.mem.pdfPlus de détails sur les graphiques de mémoire se trouvent dans le référentiel SEADSA: ici.
Utilisez sea inspect --help pour voir toutes les options. Actuellement, les options disponibles sont:
sea inspect --profiler imprime le nombre de fonctions, de blocs de base, de boucles, etc.sea inspect --mem-callgraph-dot dot GRAPHE D'APPEL CONTABTÉ PAR SEADSA.sea inspect --mem-callgraph-stats IMPRESSE À STADER STANDARDS STATSTIQUES SUR LA CONSTRUCTION GRAPHE CALL FAIT PAR SEADSA.sea inspect --mem-smc-stats imprime le nombre d'accès à la mémoire qui peuvent être prouvés en sécurité par Seadsa.La façon la plus simple de commencer avec Seahorn est via une distribution Docker.
$ docker pull seahorn/seahorn-llvm10:nightly
$ docker run --rm -it seahorn/seahorn-llvm10:nightly Commencez par explorer ce que la commande sea peut faire:
$ sea --help
$ sea pf --help La balise nightly est automatiquement actualisée quotidiennement et contient la dernière version de développement. Nous maintenons toutes les autres balises (qui nécessitent une mise à jour manuelle) rarement. Vérifiez les dates sur DockerHub et enregistrez un problème sur GitHub s'ils sont trop périmés.
Des exemples supplémentaires et des options de configuration sont sur le blog. Le blog est rarement mis à jour. En particulier, les options changent, les fonctionnalités sont supprimées, de nouvelles choses sont ajoutées. Si vous trouvez des problèmes dans le blog, faites-le nous savoir. Nous mettons au moins à jour le billet de blog pour indiquer qu'il ne devrait pas fonctionner avec la dernière version du code.
Vous pouvez également installer manuellement par:
Suivant les instructions dans le fichier docker dockerfile: docker/seahorn-builder.Dockerfile .
Si cela ne fonctionne pas, exécutez:
$ 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 *Les 3 premières commandes installeront LLVM 14, la 4e installera libpolly qui est omise à tort de LLVM 14 (mais incluse dans les versions suivantes)
Ensuite, suivez l'instruction dans le fichier docker ci-dessus
Les informations de ce moment sont uniquement pour les développeurs. Si vous souhaitez contribuer à Seahorn, construisez vos propres outils en fonction de celui-ci ou vous intéressez simplement à la façon dont cela fonctionne à l'intérieur, continuez à lire.
Seahorn nécessite LLVM, Z3 et Boost. Les versions exactes des bibliothèques continuent de changer, mais CMake Craft est utilisé pour vérifier que la bonne version est disponible.
Pour spécifier une version spécifique de l'une des dépendances, utilisez le <PackageName>_ROOT et / ou <PackageName>_DIR habituel (voir Find_package () pour plus de détails) CMake Variables.
Seahorn est brisé en plusieurs composants qui vivent dans différents référentiels (sous l'organisation Seahorn). Le processus de construction vérifie automatiquement tout si nécessaire. Pour les instructions de construction actuelles, vérifiez les scripts CI.
Ce sont les étapes génériques. Ne les utilisez pas . Lisez la suite pour une meilleure façon:
cd seahorn ; mkdir build ; cd build (Le répertoire de construction peut également être en dehors du répertoire source.)cmake -DCMAKE_INSTALL_PREFIX=run ../ (l'installation est requise! )cmake --build . --target extra && cmake .. (composants clones qui vivent ailleurs)cmake --build . --target crab && cmake .. (bibliothèque de crabe de clones)cmake --build . --target install (construire et tout installer sous run )cmake --build . --target test-all (Exécuter les tests)Remarque : l'installation de la cible est requise pour que les tests fonctionnent!
Pour une expérience de développement améliorée:
clanglld Linkercompile_commands.json Sur Linux, nous suggérons la configuration cmake suivante:
$ 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 .)
Où <Z3_ROOT est un répertoire contenant une distribution binaire Z3, et LLMV_CMAKE_DIR est le répertoire contenant LLVMConfig.cmake .
Les autres options juridiques pour CMAKE_BUILD_TYPE sont Debug et Coverage . Notez que le CMAKE_BUILD_TYPE doit être compatible avec celui utilisé pour compiler LLVM . En particulier, vous aurez besoin d'une construction Debug de LLVM pour compiler SeaHorn en mode «débogage **. Assurez-vous que vous avez beaucoup de patience, d'espace disque et de temps si vous décidez de suivre cette voie.
Alternativement, le projet peut être configuré à l'aide des préréglages CMake. Pour ce faire, exécutez simplement la commande suivante:
$ cmake --preset < BUILD_TYPE > - < PRESET_NAME > Pour configurer CMake, où <BUILD_TYPE> est l'un des: Debug , RelWithDebInfo ou Coverage et <PRESET_NAME> est le préréglage que vous souhaitez utiliser. Les préréglages actuellement disponibles sont: jammy . Ces préréglages supposent que Z3 a installé Z3 dans /opt/z3-4.8.9 et Yices installés dans /opt/yices-2.6.1 .
Cela permettra également au projet d'être configuré et compilé dans VS Code à l'aide de l'extension CMake Tools.
Si vous souhaitez utiliser différents paramètres de compilation ou si vous avez installé Z3 ou Yices dans tout autre répertoire, vous devrez créer votre propre fichier CMakeUserPresets.json avec vos propres préréglages.
N'incluez pas -DSEA_ENABLE_LLD=ON . Le compilateur par défaut est Clang, vous n'aurez peut-être pas besoin de le définir explicitement.
Seahorn fournit plusieurs composants qui sont automatiquement clonés et installés via la cible extra . Ces composants peuvent être utilisés par d'autres projets à l'extérieur de Seahorn.
Sea-DSA: git clone https://github.com/seahorn/sea-dsa.git
sea-dsa est une nouvelle analyse de tas basée sur la DSA. Contrairement à llvm-dsa , sea-dsa est sensible au contexte et, par conséquent, une partition plus fine du tas peut être générée en présence d'appels de fonction.
Clam: git clone https://github.com/seahorn/crab-llvm.git
clam fournit des invariants inductifs en utilisant des techniques d'interprétation abstraites au reste des backends de Seahorn.
llvm-seahorn: git clone https://github.com/seahorn/llvm-seahorn.git
llvm-seahorn fournit des versions personnalisées à la vérification d' InstCombine et IndVarSimplify LLVM Pass ainsi qu'une passe LLVM pour convertir les valeurs indéfinies en appels non déterministes, entre autres.
Seahorn ne vient pas avec sa propre version de Clang et s'attend à la trouver dans le répertoire de construction ( run/bin ) ou dans le chemin. Assurez-vous que la version de Clang correspond à la version de LLVM qui a été utilisée pour compiler Seahorn (actuellement LLVM14). Le moyen le plus simple de fournir la bonne version de Clang est de le télécharger à partir de LLVM.org, de le défaut quelque part et de créer un lien symbolique vers clang et clang++ dans run/bin .
$ cd seahorn/build/run/bin
$ ln -s < CLANG_ROOT > /bin/clang clang
$ ln -s < CLANG_ROOT > /bin/clang++ clang++ où <CLANG_ROOT> est l'emplacement auquel Clang a été déballé.
Le test de l'infrastructure dépend de plusieurs packages Python. Ceux-ci ont leurs propres dépendances. Si vous ne pouvez pas les comprendre, utilisez Docker à la place.
$ pip install lit OutputCheck networkx pygraphviz Nous pouvons utiliser gcov et lcov pour générer des informations de couverture de test pour Seahorn. Pour construire avec la couverture activée, nous devons exécuter la construction dans un autre répertoire et définir CMAKE_BUILD_TYPE sur Coverage pendant la configuration Cmake.
Exemples d'étapes pour générer un rapport de couverture pour la cible test-opsem :
mkdir coverage; cd coverage Créez et entrez le répertoire de construction de couverturecmake -DCMAKE_BUILD_TYPE=Coverage <other flags as you wish> ../cmake --build . --target test-opsem RUN OPSEM Tests, maintenant les fichiers .gcda et .gcno doivent être créés dans les répertoires CMakeFiles correspondantslcov -c --directory lib/seahorn/CMakeFiles/seahorn.LIB.dir/ -o coverage.info Collecte les données de couverture du module souhaité, si clang est utilisé comme compilateur au lieu de gcc , créez un script bash llvm-gcov.sh : #! /bin/bash
exec llvm-cov gcov " $@ " $ chmod +x llvm-gcov.sh puis appelez --gcov-tool <path_to_wrapper_script>/llvm-gcov.sh à la commande lcov -c ... 6. Extraire les données des répertoires souhaités et générer un rapport 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 puis ouvrez coverage_report/index.html dans le navigateur pour afficher le rapport de couverture
Voir également scripts/coverage pour les scripts utilisés par l'IC. Rapport de couverture pour Nightly Builds est disponible sur Codecov
La base de données de compilation pour le projet Seahorn et tous ses sous-projets sont générés à l'aide de -DCMAKE_EXPORT_COMPILE_COMMANDS=ON l'option pour cmake .
Un moyen facile d'obtenir l'indexation de code pour travailler avec la prise en charge de la base de données de compilation consiste à relier le fichier compilation_database.json dans le répertoire principal du projet et à suivre les instructions spécifiques à votre éditeur.
lsp-ui avec clangd qui sont disponibles dans Spacemacs Développez la branche Pour un guide détaillé pour un flux de travail distant avec Clion Check Clion-Configuration.
Utilisez notre fourche de mainframer. Ne manquez pas l'exemple de configuration.
