ikos
Public release 3.4
IKOS (ядро вывода для открытых статических анализаторов) является статическим анализатором для C/C ++ на основе теории абстрактной интерпретации.
Ikos начинал как библиотека C ++, предназначенную для облегчения разработки звуковых статических анализаторов на основе абстрактной интерпретации. Специализация статического анализатора для приложения или семейства применений имеет решающее значение для достижения как точности, так и масштабируемости. Разработка такого анализатора является трудным и требует значительного опыта в абстрактной интерпретации.
IKOS обеспечивает общую и эффективную реализацию современных структур данных и алгоритмов абстрактной интерпретации, таких как графики управления, итераторы Fixpoint, числовые абстрактные домены и т. Д. IKOS не зависит от конкретного языка программирования.
IKOS также предоставляет статический анализатор C и C ++ на основе LLVM. Он реализует масштабируемые анализы для обнаружения и доказывания отсутствия ошибок времени выполнения в программах C и C ++.
IKOS был выпущен в соответствии с соглашением NASA с открытым исходным кодом версии 1.3, см. License.pdf
Смотрите релизы.
См. Устранение неполадок.md
Чтобы установить IKOS на Linux или MacOS , мы рекомендуем использовать HomeBrew .
Во -первых, установите Homebrew , следуя этим инструкциям.
Затем просто беги:
$ brew install nasa-sw-vnv/core/ikos
Для Windows рассмотрите возможность использования подсистемы Windows для Linux.
Предположим, мы хотим проанализировать следующую программу C в файле с именем 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 : }Чтобы проанализировать эту программу с Ikos, просто запустите:
$ ikos loop.c
Вы увидите следующий вывод. Ikos сообщает о двух случаях переполнения буфера в строке 8 и 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]);
^
Команда ikos принимает исходный файл ( .c , .cpp ) или файл бит -кода LLVM ( .bc ) в качестве входных данных, анализирует его, чтобы найти ошибки времени выполнения (также называемые неопределенными поведениями), создает результат базы данных output.db в текущем рабочем каталоге и печатает отчет.
В отчете каждая строка имеет один из следующих статусов:
По умолчанию IKOS показывает предупреждения и ошибки непосредственно в вашем терминале, как это делал компилятор.
Если отчет о анализе слишком большой, вы должны использовать:
ikos-report output.db для изучения отчета в вашем терминалеikos-view output.db для изучения отчета в веб-интерфейсеДополнительная информация:
Ниже приведены инструкции по созданию IKOS из Source. Это только для продвинутых пользователей, которые хотят либо упаковать IKOS для операционной системы, либо экспериментировать с кодовой базой. В противном случае, пожалуйста, следуйте инструкциям выше.
Чтобы построить и запустить анализатор, вам понадобятся следующие зависимости:
Большинство из них могут быть установлены с помощью вашего диспетчера пакетов.
ПРИМЕЧАНИЕ. Если вы создаете LLVM из Source, вам необходимо включить информацию типа времени выполнения (RTTI).
Теперь, когда у вас есть все зависимости от вашей системы, вы можете создавать и установить IKOS.
Когда вы откроете распределение IKOS, вы увидите следующую структуру каталога:
.
├── CMakeLists.txt
├── LICENSE.pdf
├── README.md
├── RELEASE_NOTES.md
├── TROUBLESHOOTING.md
├── analyzer
├── ar
├── cmake
├── core
├── doc
├── frontend
├── script
└── test
Ikos использует систему сборки Cmake. Вам нужно будет указать каталог установки, который будет содержать все двоичные файлы, библиотеки и заголовки после установки. Если вы не указаете этот каталог, Cmake установит все, что install в корневом каталоге распределения. На следующих шагах мы установим IKOS Under /path/to/ikos-install-directory .
Вот шаги по созданию и установке IKOS:
$ mkdir build
$ cd build
$ cmake -DCMAKE_INSTALL_PREFIX=/path/to/ikos-install-directory ..
$ make
$ make install
Затем добавьте Ikos на свой путь (подумайте о добавлении этого в свой .bashrc):
$ PATH="/path/to/ikos-install-directory/bin:$PATH"
Чтобы построить и запустить тесты, просто введите:
$ make check
Смотрите Antormors.md
Sung Kook Kim, Arnaud J. Venet, Aditya V. Thakur. Детерминированная параллельная вычисление Fixpoint. В принципах языков программирования (Popl 2020) , Новый Орлеан, Луизиана (PDF).
Гийом Брат, Хорхе Навас, Ния Ши и Арно Венет. IKOS: структура для статического анализа, основанная на абстрактной интерпретации. В материалах Международной конференции по разработке программного обеспечения и формальным методам (SEFM 2014) , Гренобль, Франция (PDF).
Арно Венет. Домена датчика: масштабируемый анализ инвариантов линейного неравенства. В материалах проверки компьютерной помощи (CAV 2012) , Беркли, Калифорния, США 2012. Лекции. Заметки в области компьютерных наук, стр. 139-154, том 7358, Springer 2012 (PDF).
См. DOC/CODING_STANDARDS.MD
Смотрите doc/uperview.md
