Символическое исполнение
В информатике символическое выполнение (также символическое вычисление или симбекс ) — это средство анализа программы для определения того, какие входные данные каждой части программы вызывают выполнение . Интерпретатор следует за программой, принимая символические значения для входных данных, а не получая фактические входные данные, как это было бы при обычном выполнении программы. Таким образом, он приходит к выражениям в терминах этих символов для выражений и переменных в программе, а также к ограничениям в терминах этих символов для возможных результатов каждого условного перехода. Наконец, возможные входные данные, которые запускают ветвь, могут быть определены путем решения ограничений.
В области символического моделирования та же концепция применяется к аппаратному обеспечению. Символьные вычисления применяют эту концепцию к анализу математических выражений.
Пример [ править ]
Рассмотрим приведенную ниже программу, которая считывает значение и завершается сбоем, если входное значение равно 6.
int f () {
...
y = read ();
г = у * 2 ;
если ( z == 12 ) {
не удалось ();
} Еще {
printf ( «ОК» );
}
}
Во время нормального выполнения («конкретного» выполнения) программа считывает конкретное входное значение (например, 5) и присваивает его y. Затем выполнение продолжится с умножением и условной ветвью, которая будет оцениваться как ложь и печатать. OK.
Во время символьного выполнения программа считывает символическое значение (например, λ) и присваивает его y. Затем программа продолжит умножение и присвоит λ * 2 к z. Достигнув if заявление, оно будет оценивать λ * 2 == 12. На этом этапе программы λможет принимать любое значение, и поэтому символическое выполнение может происходить по обеим ветвям, «разветвляясь» на два пути. Каждому пути присваивается копия состояния программы в инструкции ветвления, а также ограничение пути. В этом примере ограничение пути λ * 2 == 12 для if филиал и λ * 2 != 12 для elseветвь. Оба пути могут быть символически выполнены независимо. Когда пути завершаются (например, в результате выполнения fail() или просто выход), символическое выполнение вычисляет конкретное значение для λпутем решения накопленных ограничений пути на каждом пути. Эти конкретные значения можно рассматривать как конкретные тестовые примеры, которые могут, например, помочь разработчикам воспроизводить ошибки. В этом примере решатель ограничений определит, что для достижения fail() заявление, λ должно быть равно 6.
Ограничения [ править ]
Взрыв пути [ править ]
Символическое выполнение всех возможных путей программы не масштабируется для больших программ. Число возможных путей в программе растет экспоненциально с увеличением размера программы и может даже быть бесконечным в случае программ с неограниченными итерациями цикла. [1] Решения проблемы взрыва пути обычно используют эвристику для поиска пути для увеличения покрытия кода, [2] сократить время выполнения за счет распараллеливания независимых путей, [3] или путем объединения похожих путей. [4] Одним из примеров слияния является veritesting , который «использует статическое символьное выполнение для усиления эффекта динамического символьного выполнения». [5]
- эффективность Программно зависимая
Символическое выполнение используется для последовательного рассмотрения программы, что является преимуществом перед рассуждениями о последовательном вводе программы, как это используют другие парадигмы тестирования (например, динамический анализ программы ). Однако если несколько входных данных проходят по одному и тому же пути через программу, экономия по сравнению с тестированием каждого из входных данных по отдельности невелика.
Псевдонимы памяти [ править ]
Символическое выполнение сложнее, когда к одной и той же ячейке памяти можно получить доступ через разные имена ( псевдонимы ). Псевдонимы не всегда могут быть распознаны статически, поэтому механизм символьного выполнения не может распознать, что изменение значения одной переменной также приводит к изменению другой. [6]
Массивы [ править ]
Поскольку массив представляет собой коллекцию множества различных значений, символьные исполнители должны либо рассматривать весь массив как одно значение, либо рассматривать каждый элемент массива как отдельное местоположение. Проблема с обработкой каждого элемента массива отдельно заключается в том, что такую ссылку, как «A[i]», можно указать динамически только тогда, когда значение i имеет конкретное значение. [6]
Взаимодействие с окружающей средой [ править ]
Программы взаимодействуют со своей средой, выполняя системные вызовы , получая сигналы и т. д. Проблемы согласованности могут возникнуть, когда выполнение достигает компонентов, которые не находятся под контролем инструмента символьного выполнения (например, ядра или библиотек). Рассмотрим следующий пример:
int main ()
{
ФАЙЛ * fp = fopen ( «doc.txt» );
...
if ( условие ) {
fputs ( «некоторые данные» , fp );
} else {
fputs ( «некоторые другие данные» , fp );
}
...
данные = fgets (..., fp );
}
Эта программа открывает файл и при определенных условиях записывает в него различные данные. Затем он позже считывает записанные данные. Теоретически символическое выполнение должно было бы разветвиться на два пути в строке 5, и каждый путь далее будет иметь свою собственную копию файла. Таким образом, оператор в строке 11 будет возвращать данные, соответствующие значению «условия» в строке 5. На практике файловые операции реализуются как системные вызовы в ядре и находятся вне контроля инструмента символьного выполнения. Основными подходами к решению этой проблемы являются:
Выполнение вызовов среды напрямую. Преимущество этого подхода в том, что он прост в реализации. Недостаток заключается в том, что побочные эффекты таких вызовов уничтожат все состояния, управляемые механизмом символического выполнения. В приведенном выше примере инструкция в строке 11 вернет «некоторые данные, другие данные» или «некоторые другие данные», в зависимости от последовательного порядка состояний.
Моделирование окружающей среды. В этом случае механизм инструментирует системные вызовы с помощью модели, которая имитирует их эффекты и сохраняет все побочные эффекты в хранилище для каждого состояния. Преимущество состоит в том, что можно получить правильные результаты при символическом выполнении программ, взаимодействующих с окружающей средой. Недостаток заключается в том, что необходимо реализовать и поддерживать множество потенциально сложных моделей системных вызовов. Такие инструменты, как KLEE, [7] Cloud9 и Выдра [8] используйте этот подход, реализуя модели для операций файловой системы, сокетов, IPC и т. д.
Формирование всего состояния системы. Инструменты символьного выполнения на основе виртуальных машин решают проблему среды, разделяя все состояние виртуальной машины. Например, в S2E [9] каждое состояние представляет собой независимый снимок виртуальной машины, который может выполняться отдельно. Такой подход устраняет необходимость в написании и поддержке сложных моделей и позволяет символически выполнять практически любую двоичную программу. Однако при этом возникают более высокие затраты на использование памяти (снимки виртуальной машины могут быть большими).
Инструменты [ править ]
Более ранние версии инструментов [ править ]
История [ править ]
Концепция символической казни была введена в академических кругах в 1970-х годах с описаниями: системы Select, [12] система ЭФФИГИ, [13] система ДИССЕКТ, [14] и система Кларка. [15]
См. также [ править ]
- Абстрактная интерпретация
- Символическое моделирование
- Символьное вычисление
- Конколическое тестирование
- Граф потока управления
- Динамическая перекомпиляция
Ссылки [ править ]
- ^ Ананд, Сасват; Патрис Годфруа; Николай Тильманн (2008). «Композиционно-символическое исполнение, ориентированное на спрос». Инструменты и алгоритмы построения и анализа систем . Конспекты лекций по информатике. Том. 4963. стр. 367–381. дои : 10.1007/978-3-540-78800-3_28 . ISBN 978-3-540-78799-0 .
- ^ Ма, Кин-Кенг; Ху Йит Пханг; Джеффри С. Фостер; Майкл Хикс (2011). «Направленная символическая казнь» . Материалы 18-й Международной конференции по статистическому анализу . Спрингер. стр. 95–111. ISBN 9783642237010 . Проверено 3 апреля 2013 г.
- ^ Стаатс, Мэтт; Корина Пасареану (2010). «Параллельное символическое выполнение для генерации структурных тестов». Материалы 19-го Международного симпозиума по тестированию и анализу программного обеспечения . стр. 183–194. дои : 10.1145/1831708.1831732 . ISBN 9781605588230 . S2CID 9898522 .
- ^ Кузнецов Владимир; Киндер, Йоханнес; Букур, Стефан; Кандеа, Джордж (01 января 2012 г.). «Эффективное государственное слияние при символическом исполнении». Материалы 33-й конференции ACM SIGPLAN по проектированию и реализации языков программирования . Нью-Йорк, штат Нью-Йорк, США: ACM. стр. 193–204. CiteSeerX 10.1.1.348.823 . дои : 10.1145/2254064.2254088 . ISBN 978-1-4503-1205-9 . S2CID 135107 .
- ^ «Улучшение символического исполнения с помощью веритестинга» .
- ^ Перейти обратно: а б ДеМилло, Рич; Оффатт, Джефф (1 сентября 1991 г.). «Автоматическая генерация тестовых данных на основе ограничений». Транзакции IEEE по разработке программного обеспечения . 17 (9): 900–910. дои : 10.1109/32.92910 .
- ^ Кадар, Кристиан; Данбар, Дэниел; Энглер, Доусон (1 января 2008 г.). «KLEE: автоматическое и автоматическое создание тестов с высоким покрытием для программ сложных систем» . Материалы 8-й конференции USENIX по проектированию и внедрению операционных систем . ОСДИ'08: 209–224.
- ^ Терпи, Джонатан; Рейснер, Эльнатан; Фостер, Джеффри; Хикс, Майкл. «MultiOtter: многопроцессное символическое выполнение» (PDF) .
- ^ Чипунов Виталий; Кузнецов Владимир; Кандеа, Джордж (01 февраля 2012 г.). «Платформа S2E: проектирование, реализация и приложения». АКМ Транс. Вычислить. Сист . 30 (1): 2:1–2:49. дои : 10.1145/2110356.2110358 . ISSN 0734-2071 . S2CID 16905399 .
- ^ Шарма, Асанхая (2014). «Использование неопределенного поведения для эффективного символического выполнения». ICSE Companion 2014: Материалы 36-й Международной конференции по программной инженерии . стр. 727–729. дои : 10.1145/2591062.2594450 . ISBN 9781450327688 . S2CID 10092664 .
- ^ Кадар, Кристиан; Ганеш, Виджай; Павловский, Питер М.; Дилл, Дэвид Л.; Энглер, Доусон Р. (2008). «EXE: автоматическое создание входных данных о смерти». АКМ Транс. Инф. Сист. Безопасность . 12 : 10:1–10:38. дои : 10.1145/1455518.1455522 . S2CID 10905673 .
- ^ Роберт С. Бойер, Бернард Эльспас и Карл Н. Левитт SELECT - формальная система тестирования и отладки программ путем символьного выполнения, Труды Международной конференции по надежному программному обеспечению, 1975, стр. 234–245, Лос-Анджелес, Калифорния.
- ^ Джеймс К. Кинг, Символическое выполнение и тестирование программ, Communications of ACM, том 19, номер 7, 1976, 385–394.
- ^ Уильям Э. Хауден, Эксперименты с системой символической оценки, Труды Национальной компьютерной конференции, 1976.
- ^ Лори А. Кларк, Система тестирования программ, ACM 76: Материалы ежегодной конференции, 1976, страницы 488-491, Хьюстон, Техас, США.