Мутационное тестирование ядра ОС

Опыт с Mull был не совсем успешным (не только из-за незрелости самого инструмента!) и желание попробовать MT всё еще оставалось. После всех экспериментов я переключился на другой проект и там Mull не получилось бы использовать: в качестве основного компилятора используется GCC и тесты написаны не на Google Test, а на своём собственном фреймворке. Поэтому всё пришлось делать с нуля, в том числе и выбор инструмента.

Читая о проекте формальной верификации в Astra Linux я узнал про инструмент Frama-C. Это статический анализатор для кода на C. Отличие его от других статических анализаторов в том, что можно писать для него расширения и он поддерживает язык разметки ACSL, который используют для описания предикатов. Я рассуждал так: если это статический анализатор с возможностью расширения, то теоретически для него можно написать расширение, которое может добавлять мутации в код. Оказалось, что так рассуждал не только я и такое расширение уже есть.

Что надо автоматизировать для MT:

  1. запустить тесты по дефолту и собрать результаты
  2. сделать препроцессинг исходного файла (см. раздел 5.1 в документации)
  3. сделать мутацию для исходного файла
  4. пересобрать проект
  5. запустить тесты и собрать результаты
  6. сравнить оригинальные результаты и предыд результаты
  7. сохранить мутацию и результат прогона
  8. перейти в п.2

Как выглядит мутация исходного кода с Frama-C:

int max(int i, int j) { return (i < j) ? j : i; }

int main() {
  max(1, 0);
  return 0;
}

$ frama-c sample.c -mut -mut-code -mut-spec -mut-summary-file SUMMARY
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing sample.c (with preprocessing)
$

$ ls -1 mutant_*
mutant_0.c
mutant_1.c
mutant_2.c
mutant_3.c
mutant_4.c
mutant_5.c
$

В файл SUMMARY находятся список названий файлов с мутациями и сама мутация:

$ cat summary.csv
mutant_0.c,sample.c:2: `<` --> `!=`
mutant_1.c,sample.c:2: `<` --> `==`
mutant_2.c,sample.c:2: `<` --> `>=`
mutant_3.c,sample.c:2: `<` --> `>`
mutant_4.c,sample.c:2: `<` --> `<=`
mutant_5.c,sample.c:2: `i < j` --> `! (i < j)`

$ frama-c FILE -mut [-mut-code] [-mut-spec] [-mut-summary-file SUMMARY]

* Replacement of a binary operator
* Condition reversal
* Loop invariant deletion
* Postcondition deletion
* Conjunction pruning
* Replacement of numerical values

Кратко о том, как это выглядело: выполняется обычная сборка проекта (make os) и проверка того, что тесты успешно проходят (make -C os qemutests/run). Во время сборки скрипт находит строку для компиляции нашего файла в выводе gcc, это нужно, чтобы Frama-C нашла все необходимые заголовочные файлы. Потом скрипт c помощью Frama-C и плагина для мутаций генерирует для целевого файла N-файлов с одной мутацией в каждом. Далее подменяем в дереве исходников целевой файл на файл с мутацией и запускаем пересборку с последующим запуском тестов. После обработки каждого исходного файла проекта я отдельным скриптом генерировал простенький HTML-отчет.

Всего было сделано ~3200 мутаций для исходных файлов в разных подсистемах ядра (mm, task, thread, vmm, io) и результаты выполнения тестов на мутированном коде можно поделить на несколько категорий:

  1. ОС не смогла успешно загрузиться в эмуляторе QEMU и генерировала исключение
  2. ОС зависала во время загрузки в QEMU
  3. ОС загружалась и тесты проходили успешно

Случаи 1 и 2 нас не сильно интересуют. Логи для результаты тестов из 3-й категории я просматривал вручную и нашел строки, которые у нас покрыты тестами, но при мутации в этой строке тесты проходят успешно. То есть это именно то, ради чего все и затевалось. Нашлось как минимум 35 мутаций с которыми тесты проходили успешно, при том, что строки, в которые вносились мутации были покрыты этими тестами.

Всё тестирование для перечисленных ниже файлов заняло примерно 1.5 недели, в основном из-за того, что если ОС зависает, то выполнение тестов прерывается по таймауту, который составляет примерно 3 мин. Если тесты проходят успешно, итерация с одной мутацией занимает ~10 сек.

Из проблем с Frama-C:

  • Frama-C требует название входной функции (аргумент -main), и не понятно что делать в случае мутаций множества файлов. Если добавить пустую функцию main(), то Frama-C не ругается.
  • Портился вывод в CSV формат и пришлось сделать патч для расширения Frama-C-Mutation
  • Исходный код проекта потребовал небольших изменений, потому что Frama-C отказывалась выдавала ошибки. Предполагаю, что Frama-C не настолько крутой парсер конструкций C, как например в промышленных компиляторах типа clang или gcc.

Дальше решили проверить библиотеку для ядра ОС и тут возникли проблемы. Frama-C смогла распарсить не весь код на Си. Для некоторых ошибок можно было быстро поправить или закомментировать строчки, но с некоторыми ошибками разобраться не получилось.

В статье про тестирование RCU написано, что они использовали инструмент из Is Mutation an Appropriate Tool for Testing Experiments?, потому что он простой (несколько сот строк на Prolog и Shell). (“8.4% of resulting mutants did not compile”). Я написал автору статьи Alex Groce и он посоветовал использовать: cmutate или universalmutator, описанный в другой статье.

Подход universalmutator мне показался слишком простым: инструмент использует использует регулярные выражения для внесения мутаций и после каждой мутации сохраняет исходный файл с изменением. Остальную часть работы нужно делать самому. Строить синтаксическое дерево ей не требуется, и из-за этого мутации вносятся без учёта семантики языка. Большого выбора не было и я решил её попробовать. При запуске в ручном режиме на первом же файле после запуска тестов выжили четыре мутанта. Поэтому я написал скрипты для автоматизации работы и запустил уже для всех исходных файлов.

Резюме: очевидно, что польза от MT есть. Для внедрения в регулярное тестирование нужно сделать такое тестирование полностью автоматическим.

Теги: softwaretestingopensourcefeed

Новые

Все посты →