27.04.2017: CPAchecker-BAM-BnB и BLAST 2.7.3 на SV-COMP'2017
На международных соревнованиях инструментов статической верификации (SV-COMP 2017), проходивших в рамках международной конференции TACAS, Уппсала, Швеция, были представлены доклады по инструментам CPAchecker-BAM-BnB и BLAST 2.7.3.
Инструмент CPAchecker-BAM-BnB является улучшением инструмента CPAchecker в части использования техники кэширования абстрактных блоков и улучшения модели памяти. Инструмент занял пятое место в категории Software Systems.
В докладе была представлена новая модель памяти BnB. Модель памяти, использующаяся по умолчанию, разбивала всю память на регионы по типам переменных. Так, считалось, что указатели разных типов не могут указывать на одну и ту же область памяти. А для того, чтобы различить указатели одного типа, которые потенциально способны указывать на одинаковую ячейку памяти, в процессе анализа строилась формула, которая затем разрешалась с помощью внешнего компонента - решателя. Большое количество использующихся в программе указателей требовало большого количества ресурсов.
Новая модель памяти позволяет разбивать память на большее число непересекающихся регионов, что приводит к снижению нагрузки на решатель. Так, указатели, являющиеся полями структур, от которых не брался адрес не могут быть алиасами никаких других указателей, поэтому они могут быть выделены в отдельные регионы. Таким образом, построенные в процессе анализа формулы становятся проще, и снижается нагрузка на решатель.
Полученные результаты являются неоднозначными. С одной стороны, упрощение формул приводит к тому, что некоторые верификационные задачи могут быть решены быстрее, но с другой стороны, для некоторых задач вердикт стал выноситься заметно медленее, так как анализ стал менее консервативным: некоторые указатели перестали быть алиасами.
Во втором докладе были представлены рекомендации по использованию инструментов статической верификации для применения к драйверам ядра ОС Linux. Во-первых, для визуализации результатов верификации было предложено внести важные детали в формат доказательств и трасс ошибок, предоставляемых инструментами. Так инструменты, предоставляющие данную информацию, смогут использовать единобразный механизм визуализации.
Второе предложение касалось подготовки наборов верификационных задач для соревнований. На данный момент во многих наборах, в особенности в драйверах ОС Linux, используются функции без определения, что является источником неопреденного поведения программы. Для определения поведения данных функций было предложено рассмотреть понятие памяти "по-требованию", в которой содержимое памяти определяется при обращении к ней и считается, что ее использование является безопасным. В тоже время мы не накладываем ограничений на взаимосвязи объектов в этой памяти, поэтому не теряем достижимых путей.
