Прочитал статью Технологии, используемые в анализаторе кода PVS-Studio для поиска ошибок и потенциальных уязвимостей и для меня было новостью, что в качестве одной из технологий используются статические аннотации для самых популярных библиотек. То есть они взяли самые популярные библиотеки (WinAPI, glibc, STL, Qt, OpenSSL и другие), проаннотировали каждую фунцию для описания инвариантов и при статическом анализе проверяют выполнение инвариантов из аннотаций. Очень похоже на подход Frama-C + ACSL для верификации исходного кода. Ещё мне в статье показалось странным, что они сравнивают свой статический анализатор с использованием регулярных выражений. Я конечно знаю про подход продавцов ПО "возьми самого слабого и сравнивайся с ним, чтобы в глазах покупателя выглядеть наиболее выгодно", но уж и сравнивать статический анализатор с наколенными инструментами, то с наиболее близким аналогом будет
coccinelle для семантических патчей, semgrep или coccigrep, но точно не regexp, который не учитывает контекст.Нашёл слайды от одного из создателей Coverity, они интересны тем, что там описывается и техническая и продуктовая составляющие сервиса. Очень познавательно.
В области статического анализа кода серьезная конкуренция, есть и коммерческие продукты и opensource аналоги, которые могут составить конкуренцию коммерческим продуктам. Может сложится впечатление, что все вместе они покрывают множество проблем, которые вообще возможно найти с помощью стат. анализа. Но это не так и приведу два примера для иллюстрации этого утверждения.
По стандарту POSIX функция
mmap() возвращает MAP_FAILED или -1 в случае ошибки выделения памяти. Популярной ошибкой среди разработчиков является проверка возвращаемого значения на 0, что не соответствует стандарту. Из-за этого возможно появление проблем. Эвристику на такую ошибку нашёл Hanno Böck, потом написал простейший скрипт и нашёл проблемы в проектах Geeqie, GDB, KDE/kwayland, Mesa, QEMU и др. В скрипте как раз используется стандартный grep, а для coccinelle семантический патч выглядел бы примерно так:identifier p; statement S; @@
p = mmap(...);
- if (!p) S
+ if (p != MAP_FAILED) S
Я оформил тикет для
clang-analyzer и возможно в ближайшее время проверка на такой тип ошибок появится в LLVM.Вторая одна эвристика выявляет проблемы с сортировкой. Yury Gribov написал подгружаемую с помощью
LD_PRELOAD библиотеку, которая проверяет выполнение условия для функций сортировки в `qsort()`: "When the same objects (consisting of width bytes, irrespective of their current positions in the array) are passed more than once to the comparison function, the results shall be consistent with one another. That is, they shall define a total ordering on the array.". Для сложных структур данных легко нарушить требование. Список проектов, в которых были найдены ошибки, внушителен: gcc, PostGIS, dpkg, graphicsmagick и другие.