Alex Aiken Stanford University aiken@cs.stanford.edu
Suhabe Bugrara Stanford University suhabe@cs.stanford.edu
Isil Dillig Stanford University isil@cs.stanford.edu
Thomas Dillig Stanford University tdillig@cs.stanford.edu
Brian Hackett Stanford University bhackett@cs.stanford.edu
Peter Hawkins Stanford University hawkinsp@cs.stanford.edu
Мы представляем обзор системы анализа программ Saturn[1], включающий в себя обоснование трёх главных технических решений: использование анализа единичной функции или анализа на основе обобщений, использование ограничений и использование языка логического программирования для описания алгоритмов программы анализа. Мы утверждаем, что комбинация обобщений и ограничений позволяет Saturn достигать как высокой масштабируемости, так и высокой точности, а использование языка логического программирования с механизмом ограничений позволяет использовать краткие высокоуровневые выражения для анализа программ.
Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages
General Terms Design, Experimentation, Languages
Keywords program analysis, verification, boolean satisfiability
Saturn --- система статического анализа программ. Saturn стремится как к масштабируемости, так и к точности, чтобы, в конечном счёте, иметь возможность верифицировать отсутствие определённых типов ошибок в реальных системах. Saturn основан на трёх основных идеях:
-
Saturn основан на обобщениях: каждая функция f анализируется отдельно, вычисляя обобщение f. В местах вызова f используется только обобщение f. Обобщение может быть прикреплено также к типам, глобальным переменным и массивам.
-
Saturn также основан на ограничениях: анализ выражен как система ограничений, описывающих как состояние в одной точке программы относится к состоянию в соседних точках программы. Базовый язык ограничений в Saturn основан на булевой выполнимости, где каждый бит доступен процедуре или циклу, представленными как отдельная булева переменная.
-
Анализ программы в Saturn выражен в языке логического программирования с поддержкой управления ограничениями и доступа к обобщениям.
В сочетании эти идеи дают возможность Saturn кратко выражать алгоритм точного анализа, в то же время обеспечивая возможность масштабирования для очень больших программ. Использование ограничений и программ на логическом языке программирования позволяет уменьшить анализы, что делает их проще для понимания и верификации чем анализы, написанные на более низких уровнях абстракции. Побитовый чувствительный к маршруту анализ обеспечивает точность, в то время как анализ одной функции за раз и обобщения обеспечивают масштабируемость --- Saturn повседневно используется для анализа всего ядра Linux (с более чем 6 млн. строк кода) и других больших проектов с открытыми исходными кодами.
На данный момент проект Saturn преследует две взаимосвязанные цели. Первая --- понять как программисты на практике структурируют большие системы. Это нужно для изучения и описания программ такими, какими они существуют в природе. Выбор и описание полезных структур в больших системах требует помощи автоматики (т.е. программного анализа) для классификации и систематизирования гигантского количества сырых данных (т.е. программ). Вторая цель --- создать инструменты, которые смогут доказывать полезные свойства программ, либо находя ошибки, либо доказывая их отсутствие. Анализы, разработанные для Saturn нашли тысячи неизвестных ранее ошибок в широко используемых программных системах [21, 20, 8, 6]. Мы также выяснили, что выявление шаблонов, которые программисты используют для структурирования кода чтобы понимать его --- всегда важный шаг в проектировании удобного инструмента для поиска ошибок или верификации.
На Рис. 1 можно увидеть блок-схему инструментария Saturn. Фронтэнд для C (на данный момент CIL[15]) представляет абстрактные синтаксические деревья программы как отношения, сохраняя их в нескольких синтаксических базах данных. Далее для каждой функции в синтаксической базе данных вызывается программа анализа, написанная на Calypso --- языке программирования Saturn. Программу исполняет интерпретатор Calypso, создающий ограничения и запрашивающий решатели ограничений, выдающие итоговую информацию и создающие отчёты об ошибках. Эти отчёты могут быть просмотрены как обычный тест, так и как основанный на XML пользовательский интерфейс, в зависимости от анализа.
Этот документ даёт краткий обзор основных компонент Saturn: использование обобщений (Раздел 2), ограничений (Раздел 3), язык логического программирования (Раздел 4) и то как они взаимодействуют друг с другом.
Одна из определяющих характеристик Saturn --- обобщённость: единица анализа --- функция, и единственный способ для функции f сослаться на результаты анализа функции g --- через обобщение g. Хотя анализ основанный на обобщениях был известен долгое время (начиная с ранних работ по пересечениям типов[14]), он противоречит многим недавним попыткам автоматизированного анализа программ, в том числе другим проектам, в которых задействованы члены нашей собственной группы. Поэтому стоит привести аргументы за и против обобщённого анализа.
Рис. 1. Структура инструментария Saturn.
На чисто семантическом уровне есть два привлекательных аспекта обобщённого анализа. Во-первых это, естественно, поддержка контекстной чувствительности, т.к. любой полиморфизм в общем случае легко обойти когда обобщение обрабатывается в разных местах вызова. Во-вторых также естественно, что в Saturn можно создавать композицию обобщённых анализов, которые применимы как к незамкнутым, так и к замкнутым программам. (Незамкнутая программа содержит свободные идентификаторы, такие как библиотеки, оторванные от программы; замкнутая программа полна и может исполняться). Под композицией мы понимаем что анализ функции не делает предположений о возможной среде исполнения, в которой функция вызывается, и таким образом вызывающие функции не должны присутствовать для вычисления полезной информации о функции, которая является объектом анализа отдельной библиотеки. Другой способ --- анализ всей программы, в котором создаётся представление всей программы и анализируется целиком. Некоторые анализы всей программы (например анализ мономорфных форм классов для объектно-ориентированных языков[16]) не могут быть восприняты для композиции анализа, потому что анализ предполагает знание специфичного контекста, в котором используется каждая функция в программе. Стоит отметить, тем не менее, что множество других систем анализа всей программы (большинство из них основаны на решении систем ограничений[10]) в принципе могут быть довольно просто адаптированы для композиционного анализа, но этого пока не сделано. По факту для создания композиционного анализа необходимо написать больше кода, чем для анализа всей программы. Как минимум необходимо спроектировать и потом реализовать полиморфные обобщения для каждой функции, и часто анализ требует дополнительных усилий для представления всех возможных окружений, в которых функция может использоваться. Хотя композиционный анализ, вероятно, наиболее естественен для Saturn, возможно также проводить и анализ всей программы (включая основанный на запросах межпроцедурный анализ), и на практике, по крайней мере пока, множество завершённых анализов Saturn выполнены с элементами обоих стилей.
На наш взгляд реальная польза обобщённого анализа заключается в ряде технических преимуществ. Ограничивающий фактор для большинства систем анализа --- не время, а объём: для больших программ сложно спроектировать представление, которое располагается полностью в главной памяти. Чем тратить усилия на поиск способов сжатия представления программы для уменьшения занимаемого объёма, лучше поступить также как поступают базы данных и научные приложения, сталкивающиеся с большими объёмами данных: использовать внешние алгоритмы, которые производят вычисления небольшими кусочками между диском и главной памятью. Анализ, основанный на обобщениях хорошо ложится на эту парадигму, имея в качестве единицы анализа отдельную функцию. В каждый момент времени только одна функция f находится в памяти вместе с информацией о её обобщении, обобщениями других функций, глобальными переменными и относящимися к f типами. Остальные функции и их обобщения хранятся на диске. Т.к. часть обрабатываемой программы, которая анализируется в момент времени всегда мала, то и память, задействованная для этого мала и неизменна (по крайней мере в хорошо спроектированном анализе). Это делает возможным написание анализов, которые могут обрабатывать очень большие программы. Так как стоимость анализа функции пропорциональна её размеру и размеру обобщений, от которых она зависит (т.е. обобщениям вызываемых ей функций), такой дизайн основывается на двух допущениях:
-
Размер обобщения функции ограничен константой --- обобщения не растут с ростом программы. Соблюдение этого свойства, или ограничение масштабируемости --- обязанность разработчика анализа. мы обсудим эти требования в Разделе 3.
-
Размер функции ограничен константой. Понятно, что разработчик анализа не может отвечать за размер функции, но на практике можно убедиться, что это ограничение хорошо сопоставимо с реальными программами. Например, недавняя версия ядра Linux с драйверами устройств содержит более 6 миллионов строк кода. На сколько мы знаем, ещё не было успешных попыток проанализировать всё ядро только в оперативной памяти, хотя подмножества из миллионов строк были проанализированы[11]. С точки зрения обобщённого анализа, ситуация не такая сложная. Средняя функция в ядре состоит всего из 29 строк кода, а медианный размер функции --- всего 16. Есть очень большие функции, но это редкость: наибольшая функция составляет 2249 строк, 6 функций составляют более 1000 строк, и всего 91 функция (меньше чем 0.1% от всех функций) состоит по крайней мере из 500 строк.
Осознанным компромиссом в Saturn является то, что он был спроектирован больше для масштабируемости, чем для скорости. Анализ одной функции содержит дорогие операции (например чтение и запись на диск), а анализируемая функция обычно маленькая, что предполагает возникновение проблемы слишком большого количества системных вызовов по отношению к полезной работе. Тем не менее другое достоинство анализа функций по отдельности том, что этот процесс легко параллелизуется, ограничиваясь только анализом зависимостей между функциями. Мы используем кластер из 40-100 ядер для запуска анализов Saturn в параллельном режиме, и обычно достигаем 80-90% эффективности. В результате Saturn по производительности, по крайней мере на достаточно большом кластере, может сравниться с другими известными системами; большинство анализов Saturn выполняются за несколько часов для программ, сопоставимых по размеру с Linux.
Стандартной методологией анализа программ является представление анализа как задачи удовлетворения ограничений: проход (или проходы) по программе создают ограничения, собирающие условия, при которых выполняется интересующее нас свойство, а отдельный решатель ограничений или система принятия решений говорит, могут ли быть удовлетворены те ограничения. Существует много теорий ограничений, которые применимы к анализу программ, но, как можно заметить из названия, в Saturn больше всего применяется выполнимость булевых форм (SAT).
Saturn делает обобщения не только для функций, но и для циклов; концептуально каждый цикл представляется в виде функции с хвостовой рекурсией. Такое представление позволяет ввести полезный инвариант, а именно что каждая функция/цикл не содержит итераций --- каждая точка в теле функции/цикла исполняется только один раз за вызов. Т.к. каждое выражение программы имеет доступ к фиксированным, заранее известным областям памяти, то каждую такую область можно статически проименовать.
Рассмотрим использование ограничений и взаимодействие с обобщениями функций на примере анализа перекрытий[8]. Представим перекрытия косвенно используя контролируемый граф указателей. В графе указателей узлами являются метки (названия участков памяти, которые мы не будем здесь определять) а дуги (l1, l2) означают, что указатели из участка l1 могут указывать на участок l2. Информацию о пересечениях легко получить из графа указателей; например, дуги (x, l) и (y ,l) показывают, что x и y могут пересекаться, т.к. они оба указывают на область l. Контролируемый граф указателей расширяет граф указателей ассоциируя каждую дугу с контролёром, ограничением говорящим под каким условием действителен указатель. Контролёры способствуют точности анализа указателей; например, если x и y могут указывать на l, но при наличии контролёра такое невозможно, они не пересекаются. Мы используем формулу над булевыми переменными b для контролёров:
g ∈ Guard ::= true | false | b | g0 ∧ g1 | g0 ∨ g1 | ¬g
ρ ∈ PTGraph = (Label × Label) → Guard⊥
Анализ перекрытий в Saturn внурипроцедурный и маршруто-чувствительный. Относительно простой способ достичь чувствительности к маршруту --- использовать разные булевы переменные для разделения информации об указателях между ветками. Даже без информации об условиях ветки (т.е. игнорируя фактический предикат условия), информация о маршруте может отслеживать корреляции между побочными эффектами. Например, информации о маршруте достаточно для статического определения того, что условный swap не может образовать перекрытие между a и b
a = x; b = y; // *x != *y
if (...) { t = a; a = b;
b = t; }
f(a,b);
Легко видеть, что a и b никогда не пересекутся при вызове f. Для примера приведём упрощённую версию правила для анализа условных операторов.
[[if ? c0 c1]] ρ (l, l ) =
let ρ0 = [[c0 ]]ρ in
let ρ1 = [[c1 ]]ρ in
let b be a fresh boolean variable in
(b ∧ ρ0 (l, l )) ∨ (¬b ∧ ρ1 (l, l ))
Это правило иллюстрирует как информация об условиях встраивается в контролёров: контролёры для двух ветвей разъединены, но всё ещё разделяются b для в итоговом графе указателей для выражения. Если поведение двух ветвей одинаково по отношению к l, то ρ0(l, l') ≡ ρ1 (l, l') и мы можем упростить результирующий контролёр без потери информации удалив ссылку на b.
Хотя это правило работает только с информацией о маршрутах, большинство анализов в Saturn используют более сложные анализы, которые выдают битовую модель самого условия ветки[21], которая критична для взаимодействия разных веток внутри процедуры. Например, в следующем наброске кода, который характерен для многих низкоуровневых программ, взаимосвязь между ветками, если она есть, может быть определена только рассматривая эффект операторов для каждого бита:
if (x & MASK1) ...
...
if (x & MASK2) ...
Рис. 2. Ветви к количеству путей в Linux.
Рис. 3. Функции/циклы с заданным количеством путей в Linux.
Возвращаясь к обсуждению общей архитектуры Saturn, существует важное взаимодействие между подходом к анализу на обобщениях и использованию ограничений. Чувствительность к маршруту на битовом уровне сложно масштабировать для больших программ; системы граничных проверок моделей, использующие подобный подход, ограничены программами в сотни строк кода[3, 4]. Как обсуждалось выше, требования ограничений для обобщений каждого цикла и функции делает закономерным предположение, что каждый цикл/функция являются маленьким безцикловым участком кода, что позволяет Saturn использовать что-нибудь дорогое и точное, например полное маршруточувствительное моделирование каждого бита в теле функции. Рисунки 2 и 3 определяют сложность маршруточувствительного внутрипроцедурного анализа в ОС Linux. На рис. 2 построено количество путей в процедуре (или цикле) как функция от количества ветвей. Заметьте, что ось y логарифмическая. На этом рисунке изображена только уплотнённая часть информации; несколько процедур не показаны, одна с 300 ветвями и 10^45 путями, и одна с примерно 1500 ветвями и более чем 100000 путями. Тем не менее, информация, изображённая на рис. 2 довольно удручающая: не только некоторые процедуры имеют множество ветвей, но и ветви располагаются в порядке, который почти всегда оказывается наихудшем экспоненциальным по количеству путей. Что рис. 2 не показывает, так это то, что почти все точки графика сконцентрированы возле источника. На рис. 3 изображено количество функций/циклов на каждое значение x в которых приходится от 10^x до 10^(x+1) путей. Заметьте, что обе оси имеют логарифмическое масштабирование. Как видно, подавляющее большинство функций содержит очень мало путей. В самом деле, медианное количество путей в функции или цикле в Linux - 3, и 95% функций/циклов имеют менее 100 путей. На графиках не показано, что чаще всего возможно произвести слияние информации без потерь, при котором пути соединяются как описано выше. Таким образом только для 1% самых больших функций/циклов (с 10^10 путями и более) сложно построить полную модель менее чем за минуту.
Такой уровень точности как полная чувствительность к маршруту несомненно не нужен для некоторых приложений, но он доказал своё удобство во всех приложениях, которые мы исследовали. Границей между точным внутрипроцедурным анализом и масштабируемым межпроцедурным анализом является обобщение функции. Выбор достаточного уровня абстракции в функции/цикла, который содержит в себе все особенности приложения, оставаясь масштабируемым и компактным --- задача разработчика анализа. В Saturn дизайн анализа --- это дизайн обобщений.
Возвращаясь к анализу указателей, итоговым результатом внутрипроцедурного анализа будет пара контролируемых графов указателей: предполагаемый контролируемый граф указателей на входе в функцию и итоговый контролируемый граф указателей на выходе из функции. Подводя итог вышесказанному, для обобщения, каким бы оно ни было, очень важно иметь ограниченный размер для обеспечения конечности анализа. Между тем, контролёры представляют проблему, т.к. если они появляются в обобщении, то они могут пропагировать из вызываемой функции в вызывающую особенности вызова, а размеры контролёров могут быть не ограничены. На текущий момент мы решили протестировать все контролёры в стартовых и итоговых графах на удовлетворительность и сделать все подходящие контролёры истинными, переводя контролируемый граф указателей в неконтролируемый внутри обобщений. Эта аппроксимация звучит так, будто она может только переоценить условия, при которых одна область указывает на другую. Таким образом, маршруто-чувствительная информация об указателях в текущей реализации анализа перекрытий является внутрипроцедурной. Учитывая, что количество областей, доступ к которым осуществляется напрямую ациклической функцией, фиксировано программой, а количество узлов в графе указателей из обобщения функции ограничено количество областей, становится ясно, что отбраковка маршруто-чувствительных контролёров в обобщении функции гарантирует, что обобщения будут иметь фиксированный размер.
Однако выясняется, что такой подход к обобщениям недостаточно масштабируем, и что анализ перекрытий множества программ, особенно больших, потребляет огромное количество памяти, что также проявлялось с предыдущим, потоко-чувствительным контекстно-чувствительным анализом указателей. Мы выяснили, что дороговизна анализа почти полностью вытекает из-за пересчёта отношений перекрытий среди типов, определённых пользователем и глобальных переменных, которые, будучи однажды введённым одной строкой, пропагируются по всей программе. Решение, которое мы адаптировали для анализа перекрытий, а также в других приложениях, заключается в том, что у нас есть тип и глобальные обобщения, которые являются потоко-нечувствительными фактами, ассоциированными с пользовательскими данными и глобальными переменными. Записи отношений указателей, которые находятся исключительно внутри пользовательских типов, только с этим же типом (например, одна ячейка указывает на другую ячейку того же типа) резко уменьшает количество информации, включаемой в обобщения. Предыдущая работа по потоко-чувствительному контекстно-чувствительному анализу указателей свелась к десяткам тысяч строк кода[13]. Использование разных уровней точности (потоковую и маршрутную чувствительность внутри функций, межпроцедурную потоковую чувствительность, потоковую нечувствительность для данных о структурах данных и глобальных переменных), позволяет нам масштабировать наш контекстно-, потоково-, и, частично, маршрутно-чувствительный анализ для всего ядра Linux. Процент ложных пересечений, определяемых Saturn --- примерно 26% (примерно одно из четырёх отношений указывания не подтверждается во время исполнения) [8]; на сколько мы знаем, это одновременно наиболее точный и наиболее масштабируемый анализ перекрытий из существующих.
Все программы анализа имеют язык, на котором пользователь может создавать анализ. В Saturn мы хотели избежать решений, которые приведут нас к точным формализмам или прекращению экспериментов с разными подходами к разным задачам анализа, поэтому выразительность была важнее чем алгоритмическая эффективность. По этой причине мы предпочли использовать язык логического программирования для написания анализов. Calypso, язык программирования Saturn'а --- логический язык программирования общего назначения с расширениями для поддержки ограничений и обобщений функций.
Использование логического программирования для анализа потока данных восходит к Ульману[19], а позже Репс открыл использование логических программ для выражения алгоритмов анализов, основанных на управлении запросами[17]. В Microsoft Research в поздние 1990-е для поиска тысяч ошибок в промышленном коде использовался язык логического программирования, делающий запросы к абстрактному синтаксическому дереву для поиска во многом синтаксических (но потенциально сложных) ошибочных практик кодирования[5]. Два недавних проекта использовали логическое программирование как запись масштабного анализа программ[12, 9], и мы во многом позаимствовали их опыт.
Обосновать использование логического программирования в анализе программ лучше всего на примере. Рассмотрим задачу разыменования выражения для потоко-чувствительного анализа указателей. Определённые разыменования могут иметь множество разных целей в зависимости от точки своего исполнения. В опубликованной статье можно найти правила вывода такие как:
pointsto(P, X, Y) eval(P, E, X)
-------------------------------
eval(P, ∗E, Y)
где pointsto(P,X,Y) говорит, что в точке программы P X может указывать на Y, а eval(P, E, X) говорит, что в точке программы P выражение E может вычислить X. Запись правила вывода (или небольшая его вариация) является обычной для существующих анализаторов программ.
В Saturn правила записываются следующим образом. Нам понадобится один или более предикат exp deref(ED,E), который показывает, что ED --- это разыменование D; оно просто даёт имя выражения *E из записи сверху. Далее мы можем написать операцию разыменования в Пролого-подобном синтаксисе:
eval(P,ED,Y) :- exp deref(ED,E), eval(P,E,X),
pointsto(P,X,Y)
Логическое программирование --- естественная реализация правил вывода; логическое программирование почти стирает грань между формальным описанием алгоритма анализа программы и его реализацией.
Реализация Calypso основана на восходящей интерпретации для программ логики первого порядка без побочных эффектов с уникальным набором особенностей. Большинство программ представляют смесь из восходящего и основанного на запросах вычисления, так для того чтобы разрешить поведение, основанное на запросах с восходящей интерпретацией, мы используем вариант magic-set преобразования[2]. Чтобы помочь создателям анализов быстро локализовывать ошибки в их коде, Saturn предоставляет строгую статическую типизацию, режим проверки и динамическую проверку детерминизма, которые тесно связаны с тем, что представлено в Mercury[18].
Calypso отличается от предыдущих попыток в первую очередь поддержкой ограничений и анализа, основанного на обобщениях. Несколько решателей ограничений могут быть встроены в Saturn и использоваться отдельными анализами. Каждый решатель ограничений имеет свой собственный интерфейс, множество простых предикатов для создания, управления и запроса ограничений. Например, предикат #and(G0,G1,G) может быть использован анализом для создания булевой формулы G методом взятия конъюнкции формул G0 и G1. Запрос предиката #sat(G) вызывает решатель SAT и проверяет удовлетворимость G. Расширяя наш пример сверху, если мы изменим предикат eval на eval(P,E,X,G), где G является контролёром, под которым E вычисляется в X в точке P, мы можем проверить, пересекаются ли выражения E0 и E1 в точке P, то есть есть некий X такой, что E0 и E1 могут одновременно вычисляться в X --- следующим Clypso кодом:
may alias(P,E0,E1) :-
eval(P,E0,X,G0), eval(P,E1,X,G1),
#and(G0,G1,G), #sat(G).
Повторим, этот код близко соответствует правилу вывода, которое должно использоваться для формальной спецификации анализа. Заметим, что Calypso сам по себе реализован с использованием обычного интерпретатора, а решатель ограничений используется только во время запроса к предикатам, таким как #and и #sat. Главная причина того, что ограничения отделены от ядра языка в том, чтобы сделать возможными эксперименты с разными системами решателяей и создавать приложения, которые используют множественные и смешанные[7] системы ограничений. Так как наиболее часто используется SAT, мы также использовали целочисленные решатели ограничений для некоторых анализов, и эксперементировали с другими решателями. Дизайн ограничений можно увидеть в [12], где простой формализм ограничений встраивается в логику языка программирования.
В дополнение к использованию ограничения решателей, анализы Calypso должны уметь генерировать и запрашивать общую информацию для выполнения межпроцедурного анализа. Анализу, основанному на обобщениях выдан статус первого класса через использование сессий. Сессия - устойчивый набор отношений, предоставляющих факты о программных объектах, такие как абстрактное синтаксическое дерево функции, или обобщение функции или типа. Анализ состоит из логики программы, которая выполняется отдельно в контексте каждой сессии в базе данных (обычно база данных функций и тел циклов), и может свободно запрашивать факты из каждой сессии и вычислять новые факты, добавляя их в любую сессию. Обычно анализ выполняется для каждой функции или тела цикла в программе, генерируя обобщение сессии для этой функции или цикла и запрашивая обобщения сессий каждой всего, что эта функция или цикл вызывает. Межпроцедурный планировщик содержит модель зависимостей между сессиями, и поэтому, если анализ обновляет сессию, все анализы, которые запрашивали эту сессию перезапускаются до следующей неподвижной точки.
Хранение модели зависимостей и возможность заново проанализировать функции позволяет нам освободить планировщик от необходимости анализировать функции в фиксированном порядке (хотя анализ может выбрать приоритет между восходящим и нисходящим обходом графа вызовов для минимизации повторного анализа). Это позволяет параллельным вычислениям использовать центральный планировщик/сервер, и любой анализ Calypso может быть сконвертирован из одноядерного анализа в распределённый с помощью нескольких аргументов командной строки (и нескольких дополнительных машин!), сохраняя создателю анализа значительные усилия в низкоуровневых деталях проектирования и написания распределённого анализа.
В общем сессии и язык Calypso скрывают низкоуровневое управление тем когда информация выделяется или очищается или сбрасывается на диск, как индексируется информация для быстрого поиска, как расположить и мемоизировать результаты разных анализов, вычислений и т. д. Хотя составители анализов теряют некоторый контроль над этим, их внимание больше уделяется дизайну анализа, чем реализации низкоуровневых деталей. По нашему опыту это делает и написание анализов, и разработку анализов легче, чем на низкоуровневом языке.
Мы провели обзор Saturn --- системы анализа программ, фокусирующейся на включении комбинации раздельного анализа функций и очень точного, основанного на ограничениях, внутрипроцедурного анализа тел функций. Мы выяснили, что анализируя функции раздельно и обобщая результаты мы имеем двойной выигрыш, позволяющий нам использовать более насыщенные вычислениями техники для анализа индивидуальных функций, одновременно с этим делая относительно простым масштабирование анализов Saturn для самых больших программ, доступных нам.
[1] A. Aiken, S. Bugrara, I. Dillig, T. Dillig, B. Hackett, and P. Hawkins. The Saturn program analysis system. http://saturn.stanford. edu, 2006.
[2] F. Bancilhon, D. Maier, Y. Sagiv, and J.D. Ullman. Magic sets and other strange ways to implement logic programs (extended abstract). In PODS ’86: Proceedings of the fifth ACM SIGACT- SIGMOD symposium on Principles of database systems, pages 1–15, New York, NY, USA, 1986. ACM Press.
[3] E. Clarke, A. Biere, R. Raimi, and Y. Zhu. Bounded model checking using satisfiability solving. In Formal Methods in System Design, July 2001.
[4]E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 2988 of Lecture Notes in Computer Science, pages 168–176. Springer, 2004.
[5] R. Crew. ASTLOG: A language for examining abstract syntax trees. In Proceedings of the USENIX Conference on Domain-Specific Languages, October 1997.
[6]I. Dillig, T. Dillig, and A. Aiken. Static error detection using semantic inconsistency inference. In Proceedings of the Conference on Programming Language Design and Implementation, page to appear, June 2007.
[7] M. F ̈ahndrich and A. Aiken. Program analysis using mixed term and set constraints. In Proceedings of the 4th International Symposium on Static Analysis, pages 114–126. Springer-Verlag, 1997.
[8]B. Hackett and A. Aiken. How is aliasing used in systems software? In Proceedings of the International Symposium on Foundations of Software Engineering, pages 69–80, September 2006.
[9]B. Hackett, M. Das, D. Wang, and Z. Yang. Modular checking for buffer overflows in the large. In Proceeding of the 28th International Conference on Software Engineering, pages 232–241, 2006.
[10] J. Kodumal and A. Aiken. The set constraint/CFL reachability connection in practice. In Proc. of the Conf. on Programming Language Design and Implementation, pages 207–218, 2004.
[11]J. Kodumal and A. Aiken. Banshee: A scalable constraint-based analysis toolkit. In Proceedings of the 12th International Static Analysis Symposium, pages 218–234. London, United Kingdom, September 2005.
[12]M. Lam, J. Whaley, B. Livshits, M. Martin, D. Avots, M. Carbin, and C. Unkel. Context-sensitive program analysis as database queries. In Proceedings of the Conference on Principles of Database Systems, pages 1–12, 2005.
[13] V.B. Livshits and M.S. Lam. Tracking pointers with path and context sensitivity for bug detection in C programs. In Proceedings of the European Software Engineering Conference, pages 317–326, 2003.
[14] R. Milner. A theory of type polymorphism in programming languages. Journal of Computer and System Sciences, 1998.
[15] G.C. Necula, S. McPeak, S.P. Rahul, and W. Weimer. CIL: Intermediate language and tools for analysis and transformation of C programs. In Proceedings of the 11th International Conference on Compiler Construction, March 2002.
[16] J. Palsberg and M.I. Schwartzbach. Object-oriented type inference. In Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, pages 146–161, 1991.
[17] T. Reps. Demand interprocedural program analysis using logic databases. In Applications of Logic Databases, pages 163–196, 1994.
[18] Z. Somogyi, F. Henderson, and T. Conway. The execution algorithm of Mercury, an efficient purely declarative logic programming language. JLP, 29(1–3):17–64, 1996.
[19] J.D. Ullman. Principles of Database and Knowledge-Base Systems. Computer Science Press, 1989.
[20] Y. Xie and A. Aiken. Context- and path-sensitive memory leak detection. In Proceedings of the International Symposium on Foundations of Software Engineering, pages 115–125, September 2005.
[21] Y. Xie and A. Aiken. Scalable error detection using boolean satisfiability. In Proceedings of the Symposium on Principles of Programming Languages, pages 351–363, January 2005.