Помощь студентам в учебе
Гибридный языково-независимый статический анализ как элемент комплексной технологии программирования
|
Введение 7
Глава 1. Обзор литературы 14
1.1 Анализаторы кода 14
1.2 Представление структуры программного кода 17
1.3 Языки спецификации поведения 20
1.4 Методы верификации 21
1.5 Методы интеграции 24
Глава 2. Архитектура программного решения 26
Глава 3. Особенности чтения исходных текстов 27
3.1 Формальная модель программы 27
3.2 Семантики языков программирования 29
3.3 Организация языково-независимого чтения 30
3.4 Метод чтения нескольких файлов и объединения их семантики34
3.5 Система типов данных 37
3.5.1 Принципы хранения данных 38
3.5.2 Структура типов 41
3.6 Организация чтения и записи сериализированных данных . . 42
Глава 4. Виртуальная машина и промежуточное представление Midair 44
4.1 Язык Midair 44
4.2 Гипервизор и виртуальные машины 45
4.3 Трансляция подпрограмм из обобщенных деревьев в
промежуточное представление 46
4.3.1 Метод обобщения 50
4.3.2 Метод инстанцирования 52
4.4 Модифицирование и упрощение команд в результате анализа .53
4.5 Поддержка различных языков программирования в одном
контексте 54
Глава 5. Структура и функции гибридного решателя 56
5.1 Аналитическое представление программы 56
5.2 Моделирование памяти 57
5.2.1 Версионирование переменных 58
5.2.2 Разбиение на регионы 60
5.2.3 Анализ псевдонимов 62
5.2.4 Инкрементальные и кумулятивные модели 65
5.2.5 Свойства и их перенос 66
5.3 Метод трансформации программ в SMT-представление ....68
5.4 Обнаружение ошибок при помощи SMT-решателя 72
5.5 Обнаружение ошибок с помощью вычислителя 73
5.6 Ошибки типов 75
Глава 6. Интеграции с языковыми инструментами 77
6.1 Контракты в языке РуСи 77
6.2 Проверка комментариев Doxygen 78
6.3 Анализ групп связности 79
6.4 Анализ зависимостей 80
6.5 Анализ языка 81
6.6 Композиционный анализ 82
6.7 Интерфейс клиент-серверного взаимодействия 83
6.8 Интерактивное управление 83
6.9 Интеграция различных архитектур и компиляторов 84
6.10 Моделирование поддержки различных операционных систем .88
6.11 Сканирующий запуск компиляции 89
6.12 Эмуляция окружения на основе аргументов компиляторов . .90
Глава 7. Обеспечение качества решения 92
7.1 Тестирование в различных режимах и средах 93
Глава 8. Апробация решения 95
8.1 Апробация в синтетических тестах 95
8.2 Апробация на промышленных проектах 96
8.3 Тестирование межъязыкового анализа 97
8.4 Тестирование технологического решения по интеграции ...99
8.5 Апробация в научном сообществе 101
Заключение 103
Словарь терминов 105
Список литературы 109
Приложение А. Схема работы анализатора 128
Приложение Б. Поддерживаемые дополнения 129
Приложение В. Обнаруживаемые классы ошибок 130
Приложение Г. Схема работы модуля чтения 131
Приложение Д. Универсальный языковой базис 132
Приложение Е. Принцип работы подсистемы виртуальных машин134
Приложение Ж. Команды языка Midair 135
Приложение З. Типы и их размеры 138
Приложение И. Отображение конструкций C++ в языковой базис .139
Приложение К. Отображение конструкций РуСи в языковой базис143
Приложение Л. Отображение конструкций ACSL в языковой базис145
Приложение М. Перенос тегов между регионами памяти 147
Приложение Н. Уникальные конструкции языков 148
Приложение О. Основные группы юнит-тестов 149
Приложение П. Организация системного тестирования 150
Стр.
Приложение Р. Организация тестирования в различных средах . .151
Приложение С. Результат тестирования на бенчмарке Toyota ITC .152
Глава 1. Обзор литературы 14
1.1 Анализаторы кода 14
1.2 Представление структуры программного кода 17
1.3 Языки спецификации поведения 20
1.4 Методы верификации 21
1.5 Методы интеграции 24
Глава 2. Архитектура программного решения 26
Глава 3. Особенности чтения исходных текстов 27
3.1 Формальная модель программы 27
3.2 Семантики языков программирования 29
3.3 Организация языково-независимого чтения 30
3.4 Метод чтения нескольких файлов и объединения их семантики34
3.5 Система типов данных 37
3.5.1 Принципы хранения данных 38
3.5.2 Структура типов 41
3.6 Организация чтения и записи сериализированных данных . . 42
Глава 4. Виртуальная машина и промежуточное представление Midair 44
4.1 Язык Midair 44
4.2 Гипервизор и виртуальные машины 45
4.3 Трансляция подпрограмм из обобщенных деревьев в
промежуточное представление 46
4.3.1 Метод обобщения 50
4.3.2 Метод инстанцирования 52
4.4 Модифицирование и упрощение команд в результате анализа .53
4.5 Поддержка различных языков программирования в одном
контексте 54
Глава 5. Структура и функции гибридного решателя 56
5.1 Аналитическое представление программы 56
5.2 Моделирование памяти 57
5.2.1 Версионирование переменных 58
5.2.2 Разбиение на регионы 60
5.2.3 Анализ псевдонимов 62
5.2.4 Инкрементальные и кумулятивные модели 65
5.2.5 Свойства и их перенос 66
5.3 Метод трансформации программ в SMT-представление ....68
5.4 Обнаружение ошибок при помощи SMT-решателя 72
5.5 Обнаружение ошибок с помощью вычислителя 73
5.6 Ошибки типов 75
Глава 6. Интеграции с языковыми инструментами 77
6.1 Контракты в языке РуСи 77
6.2 Проверка комментариев Doxygen 78
6.3 Анализ групп связности 79
6.4 Анализ зависимостей 80
6.5 Анализ языка 81
6.6 Композиционный анализ 82
6.7 Интерфейс клиент-серверного взаимодействия 83
6.8 Интерактивное управление 83
6.9 Интеграция различных архитектур и компиляторов 84
6.10 Моделирование поддержки различных операционных систем .88
6.11 Сканирующий запуск компиляции 89
6.12 Эмуляция окружения на основе аргументов компиляторов . .90
Глава 7. Обеспечение качества решения 92
7.1 Тестирование в различных режимах и средах 93
Глава 8. Апробация решения 95
8.1 Апробация в синтетических тестах 95
8.2 Апробация на промышленных проектах 96
8.3 Тестирование межъязыкового анализа 97
8.4 Тестирование технологического решения по интеграции ...99
8.5 Апробация в научном сообществе 101
Заключение 103
Словарь терминов 105
Список литературы 109
Приложение А. Схема работы анализатора 128
Приложение Б. Поддерживаемые дополнения 129
Приложение В. Обнаруживаемые классы ошибок 130
Приложение Г. Схема работы модуля чтения 131
Приложение Д. Универсальный языковой базис 132
Приложение Е. Принцип работы подсистемы виртуальных машин134
Приложение Ж. Команды языка Midair 135
Приложение З. Типы и их размеры 138
Приложение И. Отображение конструкций C++ в языковой базис .139
Приложение К. Отображение конструкций РуСи в языковой базис143
Приложение Л. Отображение конструкций ACSL в языковой базис145
Приложение М. Перенос тегов между регионами памяти 147
Приложение Н. Уникальные конструкции языков 148
Приложение О. Основные группы юнит-тестов 149
Приложение П. Организация системного тестирования 150
Стр.
Приложение Р. Организация тестирования в различных средах . .151
Приложение С. Результат тестирования на бенчмарке Toyota ITC .152
Стремительное развитие микроэлектроники в 20 веке привело к распространению кремниевых микросхем в различных сферах человеческой деятельности. Долгое время увеличение производительности процессоров происходило через увеличение числа транзисторов по закону Мура [1], но индустрия постепенно стала подходить к физическим пределам плотности их размещения, что потребовало новых подходов к производству транзисторов [2]. Индустрия ответила концепцией параллельных вычислений, появились спекулятивное исполнение, внеочередное исполнение и другие технологии, повышающие производительность. Появились специализированные микросхемы, которые добились большей производительности благодаря специализации вычислений. Первыми такими микросхемами стали видео-ускорители. В дальнейшем стали развиваться программируемые микросхемы (FPGA) [3; 4], сетевые процессоры, нейросетевые процессоры, акселераторы глубокого обучения [5], сопроцессоры.
Такие методы решения проблемы производительности привели к значительному увеличению сложности разработки программного обеспечения. Программное обеспечение теперь одновременно разрабатывается для компьютеров, внешних устройств, сопроцессоров, FPGA, требует обучения сопутствующих нейронных сетей. В начале века на рынке процессоров господствовала архитектура x86, и разработчики предпочитали писать программы только под нее. Остальные архитектуры не были массовыми. В настоящее время самой популярной архитектурой можно считать ARM [6] в связи с выпуском большого количества устройств на базе Android [7] (на базе Linux), для стационарных компьютеров — x86_64 (amd64) [8], для маршрутизаторов — MIPS. Переход компании Apple на архитектуру Apple Silicon [9] — процессоров M1 на базе ARM — существенно изменил отношение рынка к процессорам ARM, и теперь сложно представить современную программу для массового потребителя без поддержки данной архитектуры.
Эта тенденция прямо влияет на анализ программ с целью выявления ошибок и несоответствия спецификации. Ранние программы для ЭВМ можно было формально доказать с первой до последней строки в связи с их небольшим размером, но современные программы состоят из множества модулей, в том числе внешних, написанных на разных языках, для множества операционных систем и для различающегося аппаратного обеспечения. В качестве примера можно привести современные системы быстрого оптического распознавания: низкоуровневое программное обеспечение для камеры и другой периферии написано на С или ассемблере (архитектура может быть различной), прошивка микроконтроллера, использующего камеру, написана на C/C++ (чаще всего для архитектуры ARM), передача потока осуществляется на сервер на базе архитектуры AMD64, нейронная сеть тренируется на нейросетевом процессоре, используются FPGA для увеличения производительности, вывод осуществляется при помощи графического ускорителя. Проверить алгоритмы таких программ очень сложно.
Разнообразие конфигураций порождает проблемы совместимости и масштабируемости. Возникает вопрос: как производить качественный статический анализ программ на разных языках, для разных процессоров, операционных систем?
После значительного числа инцидентов [10;11], связанных с ошибками в программах, исследователи разработали методы защиты от ошибок. Их можно разбить на несколько групп:
- Установка требований к программному коду, ограничение используемых конструкций. Организации могут запретить использовать арифметику указателей в C [12], являющуюся значительным источником ошибок. Однако данный метод является организационным, т.к. он не предотвращает возможность допустить ошибку, а скорее делает её затруднительной.
- Защитные языки программирования. Их идея сводится к снижению возможности допустить ошибку — в основном, за счет удачного синтаксиса и проверок в компиляторе [13]. Интересным способом достижения корректности является использование сертифицированных компиляторов, таких как CompCert [14].
- Анализ программ — это проверка программного кода. Он может осуществляться как статически, т.е. без запуска программы и с учетом всех возможных путей исполнения, так и динамически, т.е. с запуском программы и с учетом только действующих путей исполнения. Статические проверки кода могут проводиться через проверку модели, т.е. сравнение реальной программы с эталоном, заданным либо полностью формальной моделью, либо через аннотации. Другой вариант — через символьное исполнение программы, которое не исключает возможность последующей проверки модели.
- Методы предотвращения ошибок на уровне среды исполнения. Один из наиболее очевидных способов — запрет обращения к определенной памяти через проверку допустимости действия во время исполнения, явный запрет разыменования нулевых указателей и т.п.
Комбинирование указанных методов является эффективным способом достижения безопасности программ [15], что подтверждается их использованием в авионике [16] и других сферах, где качество кода критически важно.
Несмотря на разнообразие подходов, в настоящий момент в сфере разработки безопасного программного обеспечения наблюдается некоторая стагнация. Крупные организации все чаще предлагают разработчикам пере-ходить на новые «безопасные» языки программирования, такие как Rust [17], Go [18], а также интерпретируемые языки с JIT [19]: C# [20], Kotlin [21]. Обсуждается даже добавление модулей на языке Rust в Linux [22]. Несмотря на все достоинства безопасных языков, перенос кодовой базы на них является крайне амбициозной задачей. Вероятен сценарий, когда новые ошибки будут добавлены просто вследствие переписывания достаточно хорошо протестированной (но ни в коем случае не безошибочной) кодовой базы на новый язык.
Другая проблема заключается в том, что расширение количества поддерживаемых программным проектом языковых семантик неизбежно влечет необходимость контроля за всеми реализаций как по отдельности, так и в совокупности, что не может не снизить качество программы. При этом статический анализ зачастую достаточно прогрессивен технически, чтобы поддерживать разные языки, но межъязыковое взаимодействие остается нерешенной проблемой. Многоязыковые анализаторы обычно имеют возможность переходить границы языков в рамках одной технологии (JVM [23], .NET [24], биткоды LLVM [25]), но не далее.
Немаловажным является и опыт разработчиков. Переход с одного языка на другой оправдан, если это в небольшой степени влияет на накопленный программистами опыт, не «обнуляет» его. Например, переход с Java на Kotlin не влияет на опыт, если программа пишется в стиле Java, но Kotlin добавляет функциональные вставки, корутины и другие возможности, использование которых рекомендуется разработчиками языка. При этом «бесшовность» перехода в таком случае является весьма относительной с точки зрения опыта программистов.
Таким образом, переход на безопасные языки программирования является устойчивой тенденцией, при этом процесс происходит медленно: разработчикам и их инструментам необходимо поддерживать взаимодействующие кодовые базы на разных языках.
К настоящему моменту статические анализаторы кода сформировались в отдельные программные продукты, которые обеспечивают две основные сервисные модели: локальную проверку кода и работу на сервере в рамках Continuous Integration.Фактическое отсутствие других моделей существенно ограничивает взаимодействие анализаторов с внешними программами. Если сделать анализатор менее зависимым от модели использования, то из анализа можно извлечь больше полезных сведений: дополнительные статические инварианты, данные для генерации юнит-тестов, сведения для поддержки межъязыковых контрактов, пути исполнения программ и т.п.
В работе [26] автор рассматривает возможность применения статических анализаторов в рамках нетрадиционных сервисных моделей. Это требует корректировки принципа работы самого анализатора.
Подобные модели требуются для комплексной среды программирования [27;28], разрабатываемой на кафедре системного программирования Санкт-Петербургского государственного университета под руководством заведующего кафедрой, профессора Андрея Николаевича Терехова. Проект ставит перед собой амбициозную задачу разработки комплексной технологии программирования, подразумевающей полный цикл: языки программирования, компиляторы [29], статические и динамические анализаторы, методы оптимизации программ, виртуальные машины для исполнения [30], кодизайн аппаратного обеспечения [31], тестирование. Важное свойство проекта — взаимодействие с другими языками программирования.
Перед статическими анализаторами в комплексных средах стоит множество вызовов. Во-первых, велика зависимость инструментов анализа от систем чтения кода и их внутренних структур данных. Во-вторых, у анализаторов зачастую отсутствует точная информация о целевой платформе. В-третьих, анализаторы часто не приспособлены к анализу на стадии проектирования, не подразумевают интерактивности и неклассических моделей использования. В-четвертых, реализация независимых инструментов в таких условиях неминуемо становится сложной.
Таким образом, комплексные среды разработки предполагают, что анализаторы имеют гибридность (поддержку различных методов анализа от контроля синтаксических деревьев до проверки модели, абстрактной интерпретации), языковую независимость (работоспособность на про-граммах, написанных на разных языках программирования, возможность их анализа в одном контексте), поддержку различных программно-аппаратных платформ с адаптацией (маскировкой) под наборы компиляции для уточнения данных о целевой платформе, простоту интеграции во весь цикл разработки от проектирования до тестирования и итогового приема, широкую функциональность (обнаружение дефектов, проверки инвариантов, определение языка проекта, описание существующих в коде переменных, функций и их назначения, навигация по коду, выявление параметров сложности кода, определение зависимостей, помощь в сертификации). Анализаторам необходимо не только соответствовать всем этим требованиям, но и обеспечивать идентичный опыт разработки на различных технологиях. По отдельности эти задачи решаются, но комплексный подход к созданию данной «экосистемы» по существу не рассматривался и является актуальной задачей программной инженерии.
Для создания подходящего под эти требования статического анализатора необходимо техническое решение, обладающее широким спектром возможностей. Equid [32] разрабатывается автором с 2015 г. Проект развился из обычного анализатора шаблонов в анализатор путей исполнения для поиска состояний гонки [33], а затем был развит до полнофункционального анализатора [34]. Проект был успешно применен в различных коммерческих проектах и доказал свою эффективность в решении промышленных задач.
Целью данной работы является разработка методологии проведения статического анализа для комплексной технологии программирования на базе языков C, C++, РуСи с учетом требований о возможности взаимодействия различных частей программного комплекса, полноценной поддержке различных языков программирования и их применения в одном контексте.
Для достижения поставленной цели необходимо решить следующие задачи:
1. Разработать метод трансляции абстрактного синтаксического дерева в обобщенное синтаксическое дерево на основе унифицированного языкового базиса (Гл.3).
2. Подготовить алгоритм трансляции обобщенных синтаксических деревьев в промежуточное представление, обеспечивающее анализ программ на разных языках программирования. (Гл. 4).
3. Исследовать методы композиции семантик различных языков программирования и предложить вариант, позволяющий объединить в одном анализе программы на C, C++, РуСи и других потенциальных языках (п. 4.5).
4. Организовать взаимодействие между методами проверки модели, абстрактной интерпретации и символьного исполнения для проведения качественного и быстрого анализа в условиях многоязыковой среды (Гл.5)
5. Исследовать архитектуры и способы обеспечения взаимодействия статического анализатора с другими частями комплекса, реализовать библиотеки для обеспечения их бесшовного взаимодействия (Гл.6).
6. Подготовить архитектурное решение для программного продукта, поддерживающее разработанные методы во всей полноте (Гл.2).
7. Реализовать разработанные методы и интегрировать их в систему статического анализа.
Научная новизна. Новизной обладает методология обеспечения анализа «в целом», состоящая из следующих частей:
1. Методы трансляции программ в обобщенные синтаксические деревья (Гл.3) и промежуточное представление (п. 4.3).
2. Язык промежуточного представления Midair, а также соответствующий фреймворк для анализа, состоящий из виртуальных машин и гипервизоров (Гл. 4).
3. Эффективные алгоритмы гибридного решателя, подходящие для межъязыкового анализа (Гл.5).
4. Архитектура и методы обеспечения взаимодействия с компонентами комплексной технологии программирования (Гл.6).
Теоретическая и практическая значимость. Теоретический результат работы — разработанная методология проведения статического анализа, складывающаяся из сочетания алгоритмов, архитектурных и технических решений, а также опыта решений проблем, и позволяющая проводить анализ программ из разных языковых контекстов.
Практическая значимость определяется фактом разработки средства анализа кода для языков C, C++, РуСи, используемого в промышленных компаниях.
Методология и методы исследования. В работе используются базвые методы информатики и программной инженерии. Статический анализ основывается на методах проверки модели, символьного исполнения и абстрактной интерпретации. Разработанное языково-независимое представление строится на теории компиляторов. Активно используются методы теории для задачи выполнимости формул в теориях (SMT).
Личный вклад. Автор самостоятельно разработал статический анализатор и основные библиотеки для взаимодействия с ним, подготовил и описал методологический базис. Автор консультировал разработчиков дополнения поддержки статического анализа для интегрированного средства разработки комплексной технологии программирования, лично внедрил поддержку анализа в компилятор РуСи, а также вносил правки в другие элементы комплексной технологии программирования.
Такие методы решения проблемы производительности привели к значительному увеличению сложности разработки программного обеспечения. Программное обеспечение теперь одновременно разрабатывается для компьютеров, внешних устройств, сопроцессоров, FPGA, требует обучения сопутствующих нейронных сетей. В начале века на рынке процессоров господствовала архитектура x86, и разработчики предпочитали писать программы только под нее. Остальные архитектуры не были массовыми. В настоящее время самой популярной архитектурой можно считать ARM [6] в связи с выпуском большого количества устройств на базе Android [7] (на базе Linux), для стационарных компьютеров — x86_64 (amd64) [8], для маршрутизаторов — MIPS. Переход компании Apple на архитектуру Apple Silicon [9] — процессоров M1 на базе ARM — существенно изменил отношение рынка к процессорам ARM, и теперь сложно представить современную программу для массового потребителя без поддержки данной архитектуры.
Эта тенденция прямо влияет на анализ программ с целью выявления ошибок и несоответствия спецификации. Ранние программы для ЭВМ можно было формально доказать с первой до последней строки в связи с их небольшим размером, но современные программы состоят из множества модулей, в том числе внешних, написанных на разных языках, для множества операционных систем и для различающегося аппаратного обеспечения. В качестве примера можно привести современные системы быстрого оптического распознавания: низкоуровневое программное обеспечение для камеры и другой периферии написано на С или ассемблере (архитектура может быть различной), прошивка микроконтроллера, использующего камеру, написана на C/C++ (чаще всего для архитектуры ARM), передача потока осуществляется на сервер на базе архитектуры AMD64, нейронная сеть тренируется на нейросетевом процессоре, используются FPGA для увеличения производительности, вывод осуществляется при помощи графического ускорителя. Проверить алгоритмы таких программ очень сложно.
Разнообразие конфигураций порождает проблемы совместимости и масштабируемости. Возникает вопрос: как производить качественный статический анализ программ на разных языках, для разных процессоров, операционных систем?
После значительного числа инцидентов [10;11], связанных с ошибками в программах, исследователи разработали методы защиты от ошибок. Их можно разбить на несколько групп:
- Установка требований к программному коду, ограничение используемых конструкций. Организации могут запретить использовать арифметику указателей в C [12], являющуюся значительным источником ошибок. Однако данный метод является организационным, т.к. он не предотвращает возможность допустить ошибку, а скорее делает её затруднительной.
- Защитные языки программирования. Их идея сводится к снижению возможности допустить ошибку — в основном, за счет удачного синтаксиса и проверок в компиляторе [13]. Интересным способом достижения корректности является использование сертифицированных компиляторов, таких как CompCert [14].
- Анализ программ — это проверка программного кода. Он может осуществляться как статически, т.е. без запуска программы и с учетом всех возможных путей исполнения, так и динамически, т.е. с запуском программы и с учетом только действующих путей исполнения. Статические проверки кода могут проводиться через проверку модели, т.е. сравнение реальной программы с эталоном, заданным либо полностью формальной моделью, либо через аннотации. Другой вариант — через символьное исполнение программы, которое не исключает возможность последующей проверки модели.
- Методы предотвращения ошибок на уровне среды исполнения. Один из наиболее очевидных способов — запрет обращения к определенной памяти через проверку допустимости действия во время исполнения, явный запрет разыменования нулевых указателей и т.п.
Комбинирование указанных методов является эффективным способом достижения безопасности программ [15], что подтверждается их использованием в авионике [16] и других сферах, где качество кода критически важно.
Несмотря на разнообразие подходов, в настоящий момент в сфере разработки безопасного программного обеспечения наблюдается некоторая стагнация. Крупные организации все чаще предлагают разработчикам пере-ходить на новые «безопасные» языки программирования, такие как Rust [17], Go [18], а также интерпретируемые языки с JIT [19]: C# [20], Kotlin [21]. Обсуждается даже добавление модулей на языке Rust в Linux [22]. Несмотря на все достоинства безопасных языков, перенос кодовой базы на них является крайне амбициозной задачей. Вероятен сценарий, когда новые ошибки будут добавлены просто вследствие переписывания достаточно хорошо протестированной (но ни в коем случае не безошибочной) кодовой базы на новый язык.
Другая проблема заключается в том, что расширение количества поддерживаемых программным проектом языковых семантик неизбежно влечет необходимость контроля за всеми реализаций как по отдельности, так и в совокупности, что не может не снизить качество программы. При этом статический анализ зачастую достаточно прогрессивен технически, чтобы поддерживать разные языки, но межъязыковое взаимодействие остается нерешенной проблемой. Многоязыковые анализаторы обычно имеют возможность переходить границы языков в рамках одной технологии (JVM [23], .NET [24], биткоды LLVM [25]), но не далее.
Немаловажным является и опыт разработчиков. Переход с одного языка на другой оправдан, если это в небольшой степени влияет на накопленный программистами опыт, не «обнуляет» его. Например, переход с Java на Kotlin не влияет на опыт, если программа пишется в стиле Java, но Kotlin добавляет функциональные вставки, корутины и другие возможности, использование которых рекомендуется разработчиками языка. При этом «бесшовность» перехода в таком случае является весьма относительной с точки зрения опыта программистов.
Таким образом, переход на безопасные языки программирования является устойчивой тенденцией, при этом процесс происходит медленно: разработчикам и их инструментам необходимо поддерживать взаимодействующие кодовые базы на разных языках.
К настоящему моменту статические анализаторы кода сформировались в отдельные программные продукты, которые обеспечивают две основные сервисные модели: локальную проверку кода и работу на сервере в рамках Continuous Integration.Фактическое отсутствие других моделей существенно ограничивает взаимодействие анализаторов с внешними программами. Если сделать анализатор менее зависимым от модели использования, то из анализа можно извлечь больше полезных сведений: дополнительные статические инварианты, данные для генерации юнит-тестов, сведения для поддержки межъязыковых контрактов, пути исполнения программ и т.п.
В работе [26] автор рассматривает возможность применения статических анализаторов в рамках нетрадиционных сервисных моделей. Это требует корректировки принципа работы самого анализатора.
Подобные модели требуются для комплексной среды программирования [27;28], разрабатываемой на кафедре системного программирования Санкт-Петербургского государственного университета под руководством заведующего кафедрой, профессора Андрея Николаевича Терехова. Проект ставит перед собой амбициозную задачу разработки комплексной технологии программирования, подразумевающей полный цикл: языки программирования, компиляторы [29], статические и динамические анализаторы, методы оптимизации программ, виртуальные машины для исполнения [30], кодизайн аппаратного обеспечения [31], тестирование. Важное свойство проекта — взаимодействие с другими языками программирования.
Перед статическими анализаторами в комплексных средах стоит множество вызовов. Во-первых, велика зависимость инструментов анализа от систем чтения кода и их внутренних структур данных. Во-вторых, у анализаторов зачастую отсутствует точная информация о целевой платформе. В-третьих, анализаторы часто не приспособлены к анализу на стадии проектирования, не подразумевают интерактивности и неклассических моделей использования. В-четвертых, реализация независимых инструментов в таких условиях неминуемо становится сложной.
Таким образом, комплексные среды разработки предполагают, что анализаторы имеют гибридность (поддержку различных методов анализа от контроля синтаксических деревьев до проверки модели, абстрактной интерпретации), языковую независимость (работоспособность на про-граммах, написанных на разных языках программирования, возможность их анализа в одном контексте), поддержку различных программно-аппаратных платформ с адаптацией (маскировкой) под наборы компиляции для уточнения данных о целевой платформе, простоту интеграции во весь цикл разработки от проектирования до тестирования и итогового приема, широкую функциональность (обнаружение дефектов, проверки инвариантов, определение языка проекта, описание существующих в коде переменных, функций и их назначения, навигация по коду, выявление параметров сложности кода, определение зависимостей, помощь в сертификации). Анализаторам необходимо не только соответствовать всем этим требованиям, но и обеспечивать идентичный опыт разработки на различных технологиях. По отдельности эти задачи решаются, но комплексный подход к созданию данной «экосистемы» по существу не рассматривался и является актуальной задачей программной инженерии.
Для создания подходящего под эти требования статического анализатора необходимо техническое решение, обладающее широким спектром возможностей. Equid [32] разрабатывается автором с 2015 г. Проект развился из обычного анализатора шаблонов в анализатор путей исполнения для поиска состояний гонки [33], а затем был развит до полнофункционального анализатора [34]. Проект был успешно применен в различных коммерческих проектах и доказал свою эффективность в решении промышленных задач.
Целью данной работы является разработка методологии проведения статического анализа для комплексной технологии программирования на базе языков C, C++, РуСи с учетом требований о возможности взаимодействия различных частей программного комплекса, полноценной поддержке различных языков программирования и их применения в одном контексте.
Для достижения поставленной цели необходимо решить следующие задачи:
1. Разработать метод трансляции абстрактного синтаксического дерева в обобщенное синтаксическое дерево на основе унифицированного языкового базиса (Гл.3).
2. Подготовить алгоритм трансляции обобщенных синтаксических деревьев в промежуточное представление, обеспечивающее анализ программ на разных языках программирования. (Гл. 4).
3. Исследовать методы композиции семантик различных языков программирования и предложить вариант, позволяющий объединить в одном анализе программы на C, C++, РуСи и других потенциальных языках (п. 4.5).
4. Организовать взаимодействие между методами проверки модели, абстрактной интерпретации и символьного исполнения для проведения качественного и быстрого анализа в условиях многоязыковой среды (Гл.5)
5. Исследовать архитектуры и способы обеспечения взаимодействия статического анализатора с другими частями комплекса, реализовать библиотеки для обеспечения их бесшовного взаимодействия (Гл.6).
6. Подготовить архитектурное решение для программного продукта, поддерживающее разработанные методы во всей полноте (Гл.2).
7. Реализовать разработанные методы и интегрировать их в систему статического анализа.
Научная новизна. Новизной обладает методология обеспечения анализа «в целом», состоящая из следующих частей:
1. Методы трансляции программ в обобщенные синтаксические деревья (Гл.3) и промежуточное представление (п. 4.3).
2. Язык промежуточного представления Midair, а также соответствующий фреймворк для анализа, состоящий из виртуальных машин и гипервизоров (Гл. 4).
3. Эффективные алгоритмы гибридного решателя, подходящие для межъязыкового анализа (Гл.5).
4. Архитектура и методы обеспечения взаимодействия с компонентами комплексной технологии программирования (Гл.6).
Теоретическая и практическая значимость. Теоретический результат работы — разработанная методология проведения статического анализа, складывающаяся из сочетания алгоритмов, архитектурных и технических решений, а также опыта решений проблем, и позволяющая проводить анализ программ из разных языковых контекстов.
Практическая значимость определяется фактом разработки средства анализа кода для языков C, C++, РуСи, используемого в промышленных компаниях.
Методология и методы исследования. В работе используются базвые методы информатики и программной инженерии. Статический анализ основывается на методах проверки модели, символьного исполнения и абстрактной интерпретации. Разработанное языково-независимое представление строится на теории компиляторов. Активно используются методы теории для задачи выполнимости формул в теориях (SMT).
Личный вклад. Автор самостоятельно разработал статический анализатор и основные библиотеки для взаимодействия с ним, подготовил и описал методологический базис. Автор консультировал разработчиков дополнения поддержки статического анализа для интегрированного средства разработки комплексной технологии программирования, лично внедрил поддержку анализа в компилятор РуСи, а также вносил правки в другие элементы комплексной технологии программирования.
Основные выносимые на защиту результаты работы заключаются в следующем:
1. В рамках исследования была разработана методология проведения статического анализа для комплексной технологии программирования на базе C, C++, РуСи с учетом требования по анализу программ на этих языках в одном контексте. Это требовало создания языково-независимых методов чтения исходных текстов, промежуточного представления Midair, фреймворка виртуальных машин и гибридного решателя, поддерживающих анализ многоязычных программ на разных уровнях.
2. Сформирована методическая основа для обеспечения взаимодействия различных частей программного комплекса.
3. Автором была спроектирована архитектура анализатора, воплощающая разработанную методологию.
4. Спроектированная система была практически реализована на языках C/C++ с частичным использованием ANTLR, LLVM/Clang, CVC4/Z3 и других открытых индустриальных модулей.
5. Была произведена апробация системы, которая выявила высокое качество алгоритмов обнаружения ошибок, показала возможность применения межъязыкового анализа, а также подтвердила способности проекта по интеграции с внешними средствами комплексной среды программирования.
Рекомендуется использовать наработки данного исследования в системах статического анализа, предназначенных для комплексных сред программирования, где необходимо эффективно и единообразно анализировать программы на разных языках программирования.
В дальнейшем планируется испытать анализатор на большем числе открытых проектов, поучаствовать в различных соревнованиях по качеству анализа. В систему будут добавлены детекторы других языков программирования, увеличена точность анализа за счет применения решателей дизъюнктов Хорна. С большой долей вероятности проект будет открыт для использования внешними участниками.
В заключение автор выражает благодарность Терехову А. Н. за научное руководство, поддержку и помощь при работе над выпускной квалификационной работой. Также автор благодарит коммерческие организации, в которых он работал, за помощь в подготовке тестового материала и за поддержку на ранних этапах развития проекта. Значительный вклад в проект внесли анонимные рецензенты поданных автором на различные конференции статей, отзывы участников конференций. Отдельное спасибо супруге Светлане и дочери Софье за помощь в подготовке исследования.
1. В рамках исследования была разработана методология проведения статического анализа для комплексной технологии программирования на базе C, C++, РуСи с учетом требования по анализу программ на этих языках в одном контексте. Это требовало создания языково-независимых методов чтения исходных текстов, промежуточного представления Midair, фреймворка виртуальных машин и гибридного решателя, поддерживающих анализ многоязычных программ на разных уровнях.
2. Сформирована методическая основа для обеспечения взаимодействия различных частей программного комплекса.
3. Автором была спроектирована архитектура анализатора, воплощающая разработанную методологию.
4. Спроектированная система была практически реализована на языках C/C++ с частичным использованием ANTLR, LLVM/Clang, CVC4/Z3 и других открытых индустриальных модулей.
5. Была произведена апробация системы, которая выявила высокое качество алгоритмов обнаружения ошибок, показала возможность применения межъязыкового анализа, а также подтвердила способности проекта по интеграции с внешними средствами комплексной среды программирования.
Рекомендуется использовать наработки данного исследования в системах статического анализа, предназначенных для комплексных сред программирования, где необходимо эффективно и единообразно анализировать программы на разных языках программирования.
В дальнейшем планируется испытать анализатор на большем числе открытых проектов, поучаствовать в различных соревнованиях по качеству анализа. В систему будут добавлены детекторы других языков программирования, увеличена точность анализа за счет применения решателей дизъюнктов Хорна. С большой долей вероятности проект будет открыт для использования внешними участниками.
В заключение автор выражает благодарность Терехову А. Н. за научное руководство, поддержку и помощь при работе над выпускной квалификационной работой. Также автор благодарит коммерческие организации, в которых он работал, за помощь в подготовке тестового материала и за поддержку на ранних этапах развития проекта. Значительный вклад в проект внесли анонимные рецензенты поданных автором на различные конференции статей, отзывы участников конференций. Отдельное спасибо супруге Светлане и дочери Софье за помощь в подготовке исследования.