Инструменты статического анализа для LLVM IR

Я пытаюсь найти, имеются ли какие-либо инструменты статического анализа, которые выполняют анализ LLVM IR и сообщают о проблемах разработчику?Инструменты статического анализа для LLVM IR

Любое предложение приветствуется.

источник

2017-01-03 user2888308

LLVM сам по своей природе содержит множество различных статических анализов. Можете ли вы уточнить, какой анализ вы хотите запустить? – Oak

Многие языки имеют интерфейс для преобразования исходного кода в LLVM IR (например, C/C++, Fortran, Ruby и т. Д.). Я пытаюсь выяснить, можно ли выполнить статический анализ (любой вид, например, символическое выполнение, поток данных, поток управления и т. Д.) На LLVM IR и сообщить об ошибке разработчику, предоставляя информацию с точки зрения исходного кода (описание ошибки и источник код linenumber, где он произошел). – user2888308

Для всех, кого это интересует, я смог найти несколько исследовательских инструментов, которые выполняют анализ LLVM IR и сообщают разработчикам об ошибках/предупреждениях. Ниже приводится список:

KLEE (http://llvm.org/pubs/2008-12-OSDI-KLEE.html)- Запускается символическое исполнение на LLVM IR, полученные из исходного кода C и генерирует отчет, как описано здесь:. http://klee.github.io/tutorials/testing-regex/
KLOVER (http://www.cs.utah.edu/~ligd/publications/KLOVER-CAV11.pdf) - построен на вершине Кли для создания тестовые примеры для программ на С ++
LLBMC (http://llbmc.org/) - LLVM IR преобразуется в промежуточное логическое представление, которое преобразуется в формулу SMT-LIB. Формула SMT-lib затем решается с помощью решения SMT. Более подробную информацию можно найти здесь: http://llbmc.org/files/papers/ASE13.pdf
LAV (http://argo.matf.bg.ac.rs/?content=lav). Это инструмент поиска ошибок, построенный поверх инфраструктуры компилятора LLVM. LAV сочетает в себе символическое исполнение, SAT-кодирование потока управления программой и некоторые функции проверки ограниченной модели.

источник

2017-01-20 23:22:37 user2888308

Инструменты статического анализа для LLVM IR

ответ

Смежные вопросы