Содержание к диссертации
Введение
Глава 1. Способы формализации ограничений и модели программы для их проверки 10
1.1. Используемая терминология 13
1.2. Методы формализации и записи ограничений 24
1.3. Модели и представления программ для проверки ограничений 32
1.4. Алгоритмы статического анализа для проверки ограничений 35
1.5. Сравнительный обзор существующих статических анализаторов 40
Глава 2. Построение модели программы и её памяти 43
2.1. Модель программы 43
2.2. Операторы на ААСГ 49
2.3. Модель памяти 50
Глава 3. Формализация ограничений 71
3.1. Предикатная модель ограничений 71
3.2. Примеры формализации 75
3.3. Классификация ограничений 78
Глава 4. Алгоритмы статического анализа и их реализация в инфраструктуре Clang 87
4.1. Особенности реализованного подмножества правил 88
4.2. Этапы работы и особенности реализации анализатора 89
4.3. Разработанные алгоритмы анализа 98
4.4. Межмодульные алгоритмы 102
4.5. Результаты тестирования анализатора 103
Заключение 110
Список публикаций 112
Литература 113
- Методы формализации и записи ограничений
- Операторы на ААСГ
- Классификация ограничений
- Разработанные алгоритмы анализа
Методы формализации и записи ограничений
В настоящей главе приведён обзор существующих исследований, связанных со статическим анализом программ. В разделе 1.1 рассмотрены основные термины, используемые в тексте диссертационной работы. В разделе 1.2 приведен обзор классификаций и формальных нотаций для задания ограничений. В разделе 1.3 описаны модели и представления программ, с помощью которых производится их анализ и проверка. В разделе 1.4 обсуждаются существующие алгоритмы получения данных для проверки правил: алгоритмы поиска побочных эффектов, построения модели памяти, анализа псевдонимов. В разделе 1.4 приведён сравнительный анализ существующих средств поиска нефункциональных ошибок методами статического анализа: Coverity SA, Klocwork Insight, Parasoft C/C++ test, Svace.
Многие ограничения языков С и СИ—Ь содержатся в уже опубликованных стандартах программирования (JSF, MISRA) и сборниках правил кодирования (HICPP). Однако проблема создания анализатора состоит в том, что поскольку данные ограничения сформулированы на естественном языке, они интерпретируются неоднозначно и неточно. Это делает их реализацию субъективной, а проверку неполной или даже некорректной, приводит к огромному количеству ложных срабатываний на прикладных программах. Поэтому, в первую очередь, для создания эффективно работающего анализатора необходимо провести их формализацию. Стандартизированной или общепринятой модели и нотации для ограничений на данный момент не существует, поэтому в этой главе приводится обзор существующих методов их формальной записи и классификации.
В разделе 1.2 рассмотрены различные модели программ, используемые для определения и проверки ограничений. Наиболее распространенным с практической точки зрения является представление программы в виде абстрактного синтаксического дерева (АСД), а правила жестко запрограммированы непосредственно в анализаторе. Это позволяет добиться высокой производительности, однако ограничивает количество доступных для проверки правил. Кроме того, анализ только АСД, как правило, приводит к сравнительно низкой точности. Рассмотренное представление программы в виде необходимых фактов на языке Пролог позволяет задавать правила на этом же языке с использованием разработанной библиотеки, однако имеет невысокую скорость работы, а точность определяется способом извлечения фактов из программы, которая в теоретических работах обычно ограничена синтаксическим анализом. Другие представления правил, например, используемое при рефакторинге, сильно ограничивают множество правил, доступных для проверки, а также требуют создания интерпретатора. Таким образом, использование нового декларативного языка для формальной записи правил приводит к значительным накладным расходам на его интерпретацию, поскольку не задает механизма проверки. Кроме того, для освоения языка уровня Пролога и знакомства с библиотекой реализованных предикатов требуется сравнительно высокая квалификация и немалое количество времени.
Простого императивного языка без условных операторов и циклов недостаточно для задания правил, создание нового императивного языка не оправдано ввиду необходимости поддержки указанных сложных конструкций. Поэтому эффективным решением является использование различных представлений правил: для формализации и для практической реализации. Поскольку большая часть правил задается в терминах анализируемого языка программирования, разумно использовать модель программы для их определения. Поскольку правило - это фактически предикат, заданный на модели программы, то для определения правила можно использовать математическую логику предикатов, а для реализации в анализаторе - язык, на котором написан анализатор. При этом получается декларативная и императивная форма записи правила на базе общей модели программы.
Для применения анализатора в прикладных программных проектах необходимо выдавать предупреждения только в тех ситуациях, которые действительно могут приводить к ошибкам. Как уже было отмечено, для этого в большинстве случаев недостаточно синтаксического анализа или анализа типов, а требуется информация о потоке данных и потоке управления программы. Многие алгоритмы, используемые для вычисления необходимых анализатору данных, позаимствованы из области компиляторных технологий. К ним относятся алгоритмы синтаксического и семантического анализа, построения абстрактного синтаксического дерева, графов потока управления и вызовов, поиск инварианта в цикле и метод решения задачи потока данных. Однако при создании анализатора требуется решение ряда специфичных задач, например, вычисление конкретных побочных эффектов выражений, поэтому в разделе 1.3 приводится описание существующих алгоритмов для извлечения необходимой для проверки правил информации. К ним относятся алгоритмы поиска побочных эффектов, алгоритмы построения модели памяти, анализ границ значений переменных, а также анализ исключений в программе на СН—Ь
В разделе 1.4 проведен сравнительный обзор существующих статических анализаторов. Часть из них, осуществляя глубокий анализ исходного кода, требует огромного количества ресурсов, другие ограничиваются лишь синтаксическим анализом, что либо сокращает набор реализованных правил, либо значительно снижает качество результатов. Таким образом показано, что существующие инструменты не решают поставленных задач. 1.1. Используемая терминология
При описании алгоритмов и моделей будем предполагать, что программы заданы на языках С или СН—Ь Все рассматриваемые алгоритмы анализа являются статическими, т.е. не требующими запуска программы для своей работы. Используемые в тексте работы английские термины из области компиляторных технологий соответствуют терминологии, принятой в книге [19]. Будем использовать понятие «выражение» {expression) для обозначения выражений языков С и СИ—\- согласно пунктам 5.1 стандартов [20, 21], где оно определяется как последовательность операторов и операндов, задающих некоторое вычисление. Термин «оператор» {statement) мы будем понимать в контексте рассматриваемых языков программирования. Операторы определяются в указанных выше документах в главе 6 [20, 21] и задают действие, которое необходимо выполнить, например, операторы for, switch. Термин «операция» {operator) также в соответствии со стандартами используется для обозначения операций языка, например, бинарные операции сложения, умножения, унарная операция отрицания. Для обозначения некоторой атомарной операции на промежуточном представлении программы будем использовать термин «инструкция» {instruction).
Операторы на ААСГ
Во второй главе проводится описание модели программы, которая используется как для её формального представления, так и для задания правил. Многие правила требуют сохранения незначимой с точки зрения семантики языка информации об исходном тексте программы, например, данных о комментариях, отступах. Такие данные, как правило, не учитываются и тем более не сохраняются компилятором при построении абстрактного синтаксического дерева (АСД) с целью экономии ресурсов. Кроме того, АСД не предусматривает их хранение. С другой стороны, было показано, что некоторые правила требуют сведений о потоке управления, побочных эффектах и других параметров программы, которые сложно вычислять на уровне АСД. При этом иногда такая информация требуется одновременно, что приводит к необходимости использования наиболее абстрактного представления программы.
Поэтому предложено расширение АСД до абстрактного графа с аннотациями и метками. Определение Аннотированный абстрактный семантический граф (ААСГ) - это структура данных, представляющая собой абстрактный семантический граф, каждая вершина которого дополнена аннотацией, а каждое ребро поме чено. Определение Под аннотацией ААСГ будем понимать множество пар (имя, значение) атрибута.
Абстрактный семантический граф конструируется на основе АСД, дополняется атрибутами и ребрами, например, ребром из вершины, использующей переменную, к её объявлению. Пометки на ребрах выражают ассоциации между вершинами графа, например, родитель в АСД.
Таким образом, ААСГ = (V, , Л, С), где V - множество вершин, Е - множество ребер, = VxS b D- множество аннотаций, задаваемое как отображение декартова произведения вершины и строки из S, задающей имя атрибута, во множество допустимых значений атрибутов D, ж С = - множество меток узла. Для удобства получение значения х Є D атрибута с именем а Є S вершины v Є V будем записывать х = v.а.
В каждой вершине ААСГ задан тип, определяющий её семантику. Для унификации введем специальный атрибут т: V ь Т, где Т - конечное множество возможных типов. Тип узла обозначает, какой сущности в программе или её представлении соответствует рассматриваемая вершина графа. Поскольку ААСГ создан для хранения данных с разных этапов анализа программы, в нем содержатся вершины для представления лексем, вершин АСД, вершин графа потока управления, причем каждая из них имеет заданное множество типов: Г = Lex U AST U CFG Lex = {Lex.:-.Keyword, Lex::Identifier}... } AST = {AST ::IfStmt, AST; -.BinaryOperator,...} CFG = {CFG::BasicBlock, CFG:.Stmt, CFG:.erminator}
Например, для вершины, соответствующей условному оператору ifhen-else абстрактного синтаксического дерева v±t hen-eise .т = AST: :IfStmt. Для каждого типа определены множества обязательных и допустимых атрибутов. Рассмотрим в качестве примера абстрактный семантический граф, соответствующий участку программы, представленной на листинге 2.1.
Схематичное изображение ААСГ приведено на рисунке 2.1. В данном примере граф программы состоит из трех сильно связанных компонентов-подграфов, соответствующих результатам лексического анализа (Lex), синтаксического анализа (AST) и анализа потока управления (CFG). Для упрощения восприятия связи между компонентами представлены не полностью и обозначены жирными короткими пунктирными стрелками. Так, например, для всех вершин из AST часть исходящих ребер обеспечивает связь с соответствующими лексемами. На рисунке это продемонстрировано в вершине с г = A.ST::IfStmt, из которой выходят 3 ребра, соответствующих началу оператора - токену ключевого слова if, ключевому слову else и концу оператора - токену, имеющему тип «разделитель» (т = Lex;/Separator) и значение «точка с запятой». Также нетрудно заметить, что программа в представлении ААСГ, как и при компиляции, после лексического анализа представляет собой цепочку лексем и таблицу символов (не представлена на рис. 2.1). Основные отличия состоят в наличии обратных ребер и добавлении дополнительных атрибутов токенов. Также несложно догадаться, что в основе подграфа AST лежит абстрактное синтаксическое дерево (АСД), дополненное ребрами к родительским вершинам, для которых введено пунктирное обозначение и, например, ребрами с меткой «Use» из вершины, соответствующей определению переменной к её использованиям. Аналогично, в основе подграфа CFG лежат вершины базовых блоков (г = CFG ::BasicBlock), составляющих их операторов (г = CFG :: CFGStmt) и условий перехода (г = CFG :: Terminator). Поскольку в примере все базовые блоки состоят не более чем из одного оператора, отдельно отметим, что они упорядочены в двусвязный список, аналогично токенам. Статический граф вызовов моделируется с помощью ребер между вершинами объявлений функций и методов (г = AST::FuctionDeel).
Классификация ограничений
Приведенный пример показывает, как с помощью описанной модели памяти проводить достаточно точный анализ состояния памяти программы. Рассмотрено использование подобласти памяти для манипуляций с элементами класса, что является частичным, однако достаточным для поставленной задачи анализа, решением проблемы псевдонимов. Также, пример позволяет детально понять, как, применяя набор заданных формальных правил, производить анализ реальных программ, записанных в виде модели.
Предложенные модели программы и памяти позволяют анализировать все множество конструкций языков С и СН—Ь, а не только искусственно выделенное подмножество, обычно рассматриваемое в работах, посвященных статическому анализу программ. При этом осуществляется нечувствительный к потоку управления, контекстно-чувствительный анализ заданных свойств программы, необходимых для проверки ограничений. Модель специально адаптирована для работы со стандартными представлениями сущностей языка в компиляторах, что позволяет её использовать не только для рассматриваемых языков, но и включить поддержку, например, С или Java. Доказана детерминированность и завершаемость анализа на основе предложенной модели, в процессе чего показано, что для большинства операторов требуется всего один проход, а для вложенных циклов - не более, чем количество изменяемых переменных в теле цикла. В главе 4, посвященной реализации предложенной модели в статическом анализаторе на основе компилятора Clang, будет показано, как осуществляется взаимодействие между анализом различных модулей компиляции, требуемое для достижения контекстной чувствительности. Глава З Формализация ограничений
В данной главе предлагается подход к формализации ограничений языков С и СИ—Ь, основанный на логике предикатов. Поскольку для эффективной реализации в анализаторе требуется императивное задание правил, предлагается использовать одновременно обе формализации: в форме предиката для достижения однозначности трактовки, поскольку формулировка на естественном языке допускает неточность интерпретации; в виде реализации на СИ—Ь для эффективной проверки в анализаторе. Оба представления правила объединяет единая модель программы, описанная в предыдущем разделе, что позволяет упростить переход от декларативного представления к императивному. В части 1 предложена предикатная модель правил, включающая примеры определения правил из сборников MISRA, JSF, НІСРР. В части 2 приведены основные свойства предложенной модели, такие, как непротиворечивость, избыточность. В части 3 рассмотрена классификация всего множества правил из сборников, основанная на необходимом уровне анализа программы, требуемом для их проверки, которая легко выводится из формальной записи правил и используется для определения оптимальной последовательности их проверки в анализаторе.
Обобщив рассмотренные в главе 1 формализации ограничений С и СН—Ь, можно сформулировать определение
Определение Ограничение (правило) - это предикат, заданный на модели программы. При такой формулировке определения правил использование Пролога кажется наиболее подходящим для их формальной записи. Как было отмечено ранее, при этом возникает три основные проблемы: требуется формализация на Прологе большого количества сущностей языка программирования, использованных при задании правила. С помощью предложенной в предыдущем разделе формализации программы и ее памяти эта проблема существенно упрощается, т.к. на основе хорошо известных из теории формальных грамматик и анализа программ терминов и выводов задается большая часть необходимых понятий. Кроме того, с помощью определенных на модели программы функциональных символов упрощается запись выводов, сформулированных в терминах модели программы. необходимо знание языка Пролог. Поскольку утверждения Пролога реализуются на основе предикатов математической логики дизъюнктов Хорна, что является подмножеством логики предикатов первого порядка, а также все люди, владеющие Прологом, знакомы с записью формул с помощью аппарата математической логики, но не наоборот, то разумно и удобно использование математической нотации при формулировке правил. за счет декларативной природы языка Пролог во многих случаях представление того же правила на императивном языке оказывается намного эффективнее как по времени, так и по требованиям к ресурсам. В результате для достижения сопоставимой с промышленными аналогами производительности анализатора, при условии сохранения формальной записи, предлагается задавать правила с помощью терминов математической логики для публикации в сборниках и использования людьми, а также на императивном СН—Ь для реализации в анализаторе. Поскольку обе записи используют единую модель программы и ее памяти, переход от одной нотации к другой не представляет серьезной проблемы. Кроме того, одним из дальнейших направлений данной работы является автоматизация данного преобразования. За счет специфики формулировки правил и общего набора базовых предикатов для многих правил такая автоматизация вполне достижима.
Рассмотренная в предыдущем разделе модель программы представляет её в виде графа, что позволяет сконцентрировать всю информацию в его вершинах, а также ввести обращение к пометкам на ребрах по аналогии с атрибутами вершин для унификации. Таким образом, в основе алфавита модели правил лежат вершины ААСГ. Для проверки значений атрибутов будем использовать привычные символы =, Ф" вместо соответствующих предикатных символов = ( 1, 2),7 ( 1 2)- Более того, для удобства и простоты записи предлагается применение, где это допустимо, отношений для множеств (є, , С, С,...) Тогда, например, запись реализует правило MISRA2004-20_4-3, запрещающее использование перечисленных функций, что может быть полезно для (1) чистых СИ—Ь программ, использующих для выделения памяти new, delete, а также (2) для микроконтроллеров, не поддерживающих динамическую память. Формально говоря, для построения модели правил на основе логики первого порядка необходимо задать интерпретацию, т.е. несущее множество Т и семантическую функцию
Разработанные алгоритмы анализа
Подсистема сбора информации отвечает за построение модели программы, которое уже несколько раз было разобрано в других подразделах. Наибольший интерес вызывают модель памяти и распространение информации о побочных эффектах.
При построении модели памяти производится последовательное применение сформулированных в соответствующей главе правил, фактически реализующее обход графа потока управления функции. Для каждого оператора вызывается соответствующее правило его интерпретации, изменяющее состояние окружения (переменных) и значения областей памяти. Наибольший интерес представляет анализ ветвлений и циклов, который был разобран с теоретической точки зрения. На практике условия ветвлений сериализуются в систему уравнений и неравенств с целью проверки инвариантности с помощью внешнего решателя. Такие данные вычисляются только в вершинах ветвлений и задействуют минимальное количество переменных, участвующих в формировании условий перехода. Поэтому решение получающихся небольших систем не является слишком ресурсоемким.
Анализ циклов при построении модели памяти осуществляется итеративно до достижения стационарности окружения и памяти. Каждая новая итерация выбирает измененную в цикле область памяти, значение которой устанавливается в Т. Поскольку количество измененных в цикле переменных с учетом иерархии областей памяти (для структур и массивов) невелико, процесс быстро завершается, однако с непредсказуемым качеством результата. Решение системы неравенств и анализ инвариантов цикла позволяют получать более точные результаты, однако не укладываются в ограничения по времени.
Анализ границ значений переменных используется всего в нескольких пра вилах, поэтому реализуется с помощью внешнего решателя систем неравенств. Фактически, его реализация заключается в введении еще одного домена значений областей памяти целочисленного типа. Значения с плавающей запятой оценивать не требуется, т.к. они не используются в правилах. Таким образом, Мет дополняется отображением \ff: А ь- VRD, где VRD - домен хранения границ значений, могущий быть реализован различными способами - от интервалов до планарных многогранников.
Для сохранения информации между запусками анализатора для различных модулей компиляции использована реляционная база данных SQLite [83]. В подсистеме сбора информации разработан механизм сериализации и десери-ализации необходимых данных о типах, переменных и их областях памяти, аннотаций функций, позволяющий (1) не анализировать несколько раз функции в заголовочных файлах, (2) сохранять информацию о побочных эффектах и исключениях на уровне функций, (3) сохранять условные предупреждения, требующих данные о функции, в еще не анализированном модуле компиляции. Кроме этого, сохранение предупреждений в базе данных позволяет вести историю для каждого проекта, быстро выявляя возникающие ошибки и улучшая качество анализа, а также собирать различную полезную для разработки статистику.
Реализованы методы сериализации данных различных типов, интерфейс взаимодействия с базой данных, а также некоторые оптимизации, как, например, загрузка базы данных в память на время работы анализатора. Путь к файлу с базой данных (БД) передается в качестве аргумента командной строки перехватчиком, встраивающимся в систему сборки. 4.2.6. Интеграция с системой сборки
Разработанный анализатор поддерживает различные системы сборки проектов для автоматического запуска и анализа только той части исходных текстов, которая компилируется в результирующую программу. Такой механизм позволяет перехватывать опции запуска, переменные окружения и предопределенные значения макросов компилятора, запускаемого при сборке проекта, затем изменять их в соответствии с требованиями Clang, настраивать соответствующее окружение анализатора, а также передавать другие аргументы, поддерживаемые только анализатором, например, путь к файлам с базой данных, конфигурацией и настраиваемым параметрам правил.
Механизм перехвата основан на переопределении переменной окружения LD_PRELOAD. Этот способ позднее был успешно применен для реализации перехвата сборки в статическом анализаторе Svace [11] и инструменте количественного анализа исходного кода Caldara. Это позволяет принудительно загружать у всех дочерних процессов специально разработанную динамическую библиотеку, которая размещается в памяти и производится динамическое связывание. Библиотека содержит реализацию функций группы exec (execve, execv, execl, execvp, execlp), которые анализируют командную строку и запускают скрипты исправления параметров, путей, окружения, а затем анализатор, если обнаруживают там пути к компилятору или компоновщику. Возможен также перехват функций установки переменных окружения, доступа к файлам, позволяющие более точно настраивать окружение анализатора в случае использования, например, средств кросс-компиляции, типа scratchbox [84] или gbs [85].
Такая система позволяет с небольшими доработками использовать практически любой компилятор и любую систему сборки. Для удобства используется программа-оболочка, обрабатывающая входные параметры и запускающая ко манды сборки. Предложенный подход не влияет на процесс сборки программы, позволяя генерировать вспомогательные файлы, запускать сторонние приложения для автоматической генерации кода. При этом все файлы, участвующие в сборке результирующей программы или библиотеки, будут проверены анализатором.