Goanna. Обнаружитель дефектов на основе modelchecking

Goanna позволяет обнаруживать следующие типы дефектов в программах на С/С++:

• ошибки выхода за границу массива


• арифметические ошибки


• ошибки копирования


• ошибки непредсказуемого поведения (неинициализированные переменные)


• ошибки работы с памятью


• ошибки с указателями на функции


• ошибки неправильного использования указателей


• ошибки неспецифицированного порядка выполнения.

Для обнаружения дефектов используется верификатор NuSMV. Подробнее использование верификатора описано в статье Goanna: Syntactic Software Model Checking

Разработчики проверяли средство на свободно-распространяемых проектах, в том числе на Firefox.Плотность обнаружения дефектов составила 0.3-2 дефекта на 1000 строк исходного кода.

Для получения более объективной картины ниже приведены результаты средства на простых тестах (менее 20 строк кода, 1 функция):

• Выход за границу массива -- находятся случаи, когда реально выходят за границу массива и не находятся случаи, когда выходят за границу размерности (например, a[1][-1] в массиве размера 2x2)


• Разыменование указателя, выведенного за границу объекта -- не обнаруживается вообще


• Переполнения буфера для memcpy не обнаруживается


• Сравнение и вычитание указателей на различные объекты не обнаруживается


• Использование неинициализированной переменной (памяти)




• через указатель не находит


• в виде параметров функции находит


• не находится при копировании неинициализированной памяти с помощью memcpy




• Разыменование неинициализированного указателя -- находится


• Разыменование нулевого указателя -- находится в простых случаях, при использовании результата malloc, но не находится для статического указателя (инициализируется нулем)

Необходимо отметить, что ошибки выхода за границу массива достаточно хорошо обнаруживаются средством в рамках одной функции, но не находятся при межпроцедурном варианте теста.

В средстве реализовано обнаружение множества дефектов, то есть после нахождения одного дефекта анализ продолжается. Например, в коде

#include
int main(void)
{
int *p = NULL;
int *q = NULL;
*p = 0;
*q = 0;
return 0;
}

Обнаруживаются ошибки для обоих указателей, хотя после разыменования p программа упадет.

Средство порадовало отсутствием ложных обнаружений, хотя понятно, что для тестирования использовались простые программы, в которых у качественного анализатора не должно быть ложных обнаружений. Если посмотреть возможности обнаружения дефектов, то они весьма средние. Например, крайне сложные и важные для языка C ошибки выхода за границу объекта не обнаруживаются вообще.
Для тестирования использовалась версия goanna-cmdline-linux-2.1.tgz с интерфейсом командной строки.

Применение на практике mcheck

Читая описания шаблонов спецификации темпоральных свойств, встретил такую формулу

<>p -> (!p U (s & !p & X(!p U t))) 

Эта формула описывает требование, что событию p предшествуют события s,t.

На первый взгляд, кажется, что подформулу !p & X(!p U t) можно заменить на более короткую формулу !p U t. Эквивалентность этих двух формул можно легко проверить с помощью mcheck. Для этого необходимо создать файл eq.txt, содержащий пару формул с префиксом '?' и разделителем ':':

? !p & X(!p U t)
: !p U t

После запуска верификатора выясняется, что формулы не эквивалентные, и имеется контр-пример:

$ java -jar mch.jar eq.txt 
Comparing: LTL : !p & X (!p U t)

     with: LTL : !p U t


Not equivalent.

second allows: T t {T T T T}*

Анализируя контр-пример, становится понятно, что вторая формула допускает состояние с меткой t в следующем (втором) состоянии после начального, тогда как первая - не допускает!