ikos
Public release 3.4
IKOS (noyau d'inférence pour les analyseurs statiques ouverts) est un analyseur statique pour C / C ++ basé sur la théorie de l'interprétation abstraite.
IKOS a commencé comme une bibliothèque C ++ conçue pour faciliter le développement d'analyseurs statiques sonores basés sur une interprétation abstraite. La spécialisation d'un analyseur statique pour une application ou une famille d'applications est essentielle pour atteindre à la fois la précision et l'évolutivité. Le développement d'un tel analyseur est ardu et nécessite une expertise significative dans l'interprétation abstraite.
IKOS fournit une implémentation générique et efficace des structures et des algorithmes de données d'interprétation de pointe, tels que les graphiques de flux de contrôle, les itérateurs de FixPoint, les domaines abstraits numériques, etc. IKOS est indépendant d'un langage de programmation particulier.
IKOS fournit également un analyseur statique C et C ++ basé sur LLVM. Il met en œuvre des analyses évolutives pour détecter et prouver l'absence d'erreurs d'exécution dans les programmes C et C ++.
IKOS a été publié dans le cadre de l'accord open source de la NASA version 1.3, voir Licence.pdf
Voir les versions.
Voir le dépannage.md
Pour installer IKOS sur Linux ou MacOS , nous vous recommandons d'utiliser Homebrew .
Tout d'abord, installez Homebrew en suivant ces instructions.
Ensuite, exécutez simplement:
$ brew install nasa-sw-vnv/core/ikos
Pour Windows, envisagez d'utiliser le sous-système Windows pour Linux.
Supposons que nous voulons analyser le programme C suivant dans un fichier, appelé loop.c :
1 : #include <stdio.h>
2 : int a [ 10 ];
3 : int main ( int argc , char * argv []) {
4 : size_t i = 0 ;
5 : for (; i < 10 ; i ++ ) {
6 : a [ i ] = i ;
7 : }
8 : a [ i ] = i ;
9 : printf ( "%i" , a [ i ]);
10 : }Pour analyser ce programme avec IKOS, exécutez simplement:
$ ikos loop.c
Vous verrez la sortie suivante. IKOS rapporte deux occurrences de débordement de tampon aux lignes 8 et 9.
[*] Compiling loop.c
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
[*] Running liveness analysis
[*] Running widening hint analysis
[*] Running interprocedural value analysis
[*] Analyzing entry point 'main'
[*] Checking properties for entry point 'main'
# Time stats:
clang : 0.037 sec
ikos-analyzer: 0.023 sec
ikos-pp : 0.007 sec
# Summary:
Total number of checks : 7
Total number of unreachable checks : 0
Total number of safe checks : 5
Total number of definite unsafe checks: 2
Total number of warnings : 0
The program is definitely UNSAFE
# Results
loop.c: In function 'main':
loop.c:8:10: error: buffer overflow, trying to access index 10 of global variable 'a' of 10 elements
a[i] = i;
^
loop.c: In function 'main':
loop.c:9:18: error: buffer overflow, trying to access index 10 of global variable 'a' of 10 elements
printf("%i", a[i]);
^
La commande ikos prend un fichier source ( .c , .cpp ) ou un fichier bitcode LLVM ( .bc ) en tant qu'entrée, l'analyse pour trouver des erreurs d'exécution (également appelées comportements indéfinis), crée une base de données de résultats output.db dans le répertoire de travail actuel et imprime un rapport.
Dans le rapport, chaque ligne a l'un des statuts suivants:
Par défaut, IKOS montre des avertissements et des erreurs directement dans votre terminal, comme le ferait un compilateur.
Si le rapport d'analyse est trop grand, vous devez utiliser:
ikos-report output.db pour examiner le rapport dans votre terminalikos-view output.db pour examiner le rapport dans une interface WebInformations supplémentaires:
Vous trouverez ci-dessous des instructions pour construire des IKOS à partir de la source. Ce n'est que pour les utilisateurs avancés qui souhaitent l'emballage d'iKOS pour un système d'exploitation ou d'expérimenter la base de code. Sinon, veuillez suivre les instructions ci-dessus.
Pour construire et exécuter l'analyseur, vous aurez besoin des dépendances suivantes:
La plupart d'entre eux peuvent être installés à l'aide de votre gestionnaire de packages.
Remarque: Si vous construisez LLVM à partir de la source, vous devez activer les informations de type d'exécution (RTTI).
Maintenant que vous avez toutes les dépendances sur votre système, vous pouvez créer et installer IKOS.
Lorsque vous ouvrez la distribution IKOS, vous verrez la structure du répertoire suivant:
.
├── CMakeLists.txt
├── LICENSE.pdf
├── README.md
├── RELEASE_NOTES.md
├── TROUBLESHOOTING.md
├── analyzer
├── ar
├── cmake
├── core
├── doc
├── frontend
├── script
└── test
IKOS utilise le système de construction CMake. Vous devrez spécifier un répertoire d'installation qui contiendra tous les binaires, bibliothèques et en-têtes après l'installation. Si vous ne spécifiez pas ce répertoire, CMake installera tout sous install dans le répertoire racine de la distribution. Dans les étapes suivantes, nous installerons IKOS Under /path/to/ikos-install-directory .
Voici les étapes pour construire et installer IKOS:
$ mkdir build
$ cd build
$ cmake -DCMAKE_INSTALL_PREFIX=/path/to/ikos-install-directory ..
$ make
$ make install
Ensuite, ajoutez des ikos sur votre chemin (pensez à l'ajouter dans votre .bashrc):
$ PATH="/path/to/ikos-install-directory/bin:$PATH"
Pour construire et exécuter les tests, tapez simplement:
$ make check
Voir contributeurs.md
Sung Kook Kim, Arnaud J. Venet, Aditya V. Thakur. Calcul de correction parallèle déterministe. Dans les principes des langages de programmation (POPL 2020) , la Nouvelle-Orléans, Louisiane (PDF).
Guillaume Brat, Jorge Navas, Nija Shi et Arnaud Venet. IKOS: un cadre d'analyse statique basé sur l'interprétation abstraite. Dans les actes de la Conférence internationale sur l'ingénierie logicielle et les méthodes formelles (SEFM 2014) , Grenoble, France (PDF).
Arnaud Venet. Le domaine de jauge: analyse évolutive des invariants d'inégalité linéaire. Dans Actes de vérification assistée par ordinateur (CAV 2012) , Berkeley, Californie, États-Unis 2012. Notes de cours en informatique, pages 139-154, volume 7358, Springer 2012 (PDF).
Voir doc / coding_standards.md
Voir Doc / Overview.md
