Статический анализ программ для проверки настраиваемых ограничений языков программирования C и C++

• Автор: Игнатьев, Валерий Николаевич
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2015
• Место защиты: Москва
• Количество страниц: 121 с. : ил.

Содержание
Введение
Глава 1. Способы формализации ограничений и модели программы для их проверки
1.1. Используемая терминология
1.2. Методы формализации и записи ограничений
1.3. Модели и представления программ для проверки ограничений .
1.4. Алгоритмы статического анализа для проверки ограничений
1.5. Сравнительный обзор существующих статических анализаторов .
Глава 2. Построение модели программы и её памяти
2.1. Модель программы
2.2. Операторы на ААСГ
2.3. Модель памяти
Глава 3. Формализация ограничений
3.1. Предикатная модель ограничений
3.2. Примеры формализации
3.3. Классификация ограничений
Глава 4. Алгоритмы статического анализа и их реализация в инфраструктуре Clang
4.1. Особенности реализованного подмножества правил
4.2. Этапы работы и особенности реализации анализатора
4.3. Разработанные алгоритмы анализа
4.4. Межмодульные алгоритмы
4.5. Результаты тестирования анализатора

Заключение
Список публикаций
Литература

Введение
Актуальность работы
Языки программирования С и С++, несмотря на свой возраст, остаются незаменимыми и занимают первое и четвертое место в рейтинге распространённости «ТЮВЕ» [6]. Однако бесконтрольное использование их возможностей обычными программистами часто приводит к серьезным ошибкам. Решением проблемы употребления «опасных» конструкций является введение ограничений на язык с помощью уточнения или изменения его семантики. Это достигается внедрением правил программирования, которые могут быть ориентированы на поиск различных проблем: форматирования кода, безопасности, производительности, переносимости. Минимальные наборы правил состоят из конвенций форматирования кода и именования сущностей в программе. В самых ответственных проектах используются отраслевые стандарты кодирования, например, ЛБИ [7] для ПО самолета, МШИА [8-10] для встраиваемых автомобильных систем. Так как обычно используется значительное количество правил на большом объеме исходного кода, требуется автоматизация проверки программ на соответствие им, а формулировка большинства правил в терминах языка программирования требует применения статического анализа исходного текста.
Основной проблемой при этом является отсутствие универсального статического анализатора, сочетающего достаточно качественную проверку ограничений с малым временем работы, сравнимым со временем компиляции. Под проверкой ограничений (правил) здесь и далее будем понимать проверку кода программ на соответствие этим ограничениям (правилам). Так, практически мгновенно работающие анализаторы ограничиваются только лишь проверкой стилистических правил и не способны выявить остальные ошибки. Анализаторы, осуществляющие глубокий, учитывающий контекст и поток управления анализ, требуют огромное количество ресурсов и времени, вплоть до нескольких су-
крытого компилятора Clang [49]. Он осуществляет потоко-чуветвительную развертку программы. При этом получается «граф развертки», в узлах которого хранятся состояния программы, состоящие из отображений выражений языка в их символьные значения, «адресов» (locations) памяти в соответствующие символьные значения и зависимостей этих значений. Выражения языка при этом хранятся в виде поддеревьев АСД, сохраняя большую часть языково-зависимой информации. Правила, в зависимости от требуемых для анализа данных, вызываются при обходе предопределенных узлов АСД или графа развертки, а также имеют доступ к любым другим узлам для анализа контекста. Реализованные на данный момент правила Clang Static Analyzer не используют в полном объеме преимущества потоковой чувствительности, поскольку большинство ограничений не требуют такой информации. Однако построение лишних структур данных существенно увеличивает общее время анализа, поэтому вместо разработки универсальной инфраструктуры проверки правил, предоставляющей широкие возможности, эффективная реализация требует выбора только минимального числа данных, необходимых большинству правил и реализации эффективных алгоритмов для их вычисления.
1.4. Алгоритмы статического анализа для проверки ограничений
В настоящее время промышленные стандарты кодирования GNU [50] и Google [51], а также многие правила из перечисленных ранее стандартов (MISRA, JSF, HICPP) сформулированы нестрого, что допускает использование для их проверки инструментов, ограничивающихся синтаксическим анализом. В классических книгах по эффективному программированию на С-Н- [52-54] рассмотрены истинные причины возникновения некоторых правил из приведенных сборников. На основе указанных причин можно интерпретировать неформаль-