Статический анализатор Svace как коллекция анализаторов разных уровней сложности

В статье описывается статический анализатор Svace, разрабатываемый в ИСП РАН.
Текущая версия анализатора осуществляет поиск ошибок в программах, написанных на языках Cи, Cи++, Java и Cи#. Svace осуществляет поиск дефектов различных типов, включая ошибки разыменования нулевого указателя, переполнение буфера, использование неинициализированных переменных, утечки памяти, двойные блокировки, наличие недостижимого кода, несогласованность конструкторов и деструкторов, ошибки деления на ноль, возвращение адреса локальных переменных, использование объектов после удаления. Целью анализа является поиск как можно большего количества дефектов при приемлемом количестве ложных срабатываний и времени анализа.
Дефекты в программе имеют разную природу и для их поиска необходимо правильно выбрать алгоритм анализа. Хороший инструмент будет включать в себя как простые детекторы, использующие синтаксический анализ, так и сложные детекторы, позволяющие найти нетривиальные межпроцедурные ошибки. Построение инструмента на основе нескольких анализаторов позволяет использовать преимущества этих видов анализаторов и находить больший диапазон ошибочных ситуаций.
Инструмент Svace состоит из набора анализаторов реализующих анализы разных типов: анализ на основе абстрактного синтаксического дерева, консервативный анализ потока данных для одной функции, потоко- чувствительный и межпроцедурный неконсервативный анализ с возможностью использовать чувствительность к путям.
Межпроцедурный анализ осуществляется на основе аннотаций. При таком подходе после анализа функции создаётся её аннотация, описывающая интересующие эффекты вызова функции. Аннотация используется при обработке вызова функции для эмуляции вызова, что позволяет избежать повторного анализа функции. На основе анализа отдельных функций реализован анализ пар конструкторов и деструкторов Си++, позволяющий находить несогласованность при их написании. Все описываемые анализы иллюстрируются примерами ошибок, найденными анализатором на проектах с открытым исходным кодом.