Символическое исполнение
В информатике входные символическое выполнение (также символическое вычисление или симбекс ) — это средство анализа программы для определения того, какие данные каждой части программы вызывают выполнение . Интерпретатор следует за программой, принимая символические значения для входных данных , а не получая фактические входные данные, как это было бы при обычном выполнении программы. Таким образом, он приходит к выражениям в терминах этих символов для выражений и переменных в программе, а также к ограничениям в терминах этих символов для возможных результатов каждого условного перехода. Наконец, возможные входные данные, которые запускают ветвь, могут быть определены путем решения ограничений.
В области символического моделирования та же концепция применяется к аппаратному обеспечению. Символьные вычисления применяют эту концепцию к анализу математических выражений.
Пример [ править ]
Рассмотрим приведенную ниже программу, которая считывает значение и завершается сбоем, если входное значение равно 6.
int f() {
...
y = read();
z = y * 2;
if (z == 12) {
fail();
} else {
printf("OK");
}
}
Во время нормального выполнения («конкретного» выполнения) программа считывает конкретное входное значение (например, 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()
{
FILE *fp = fopen("doc.txt");
...
if (condition) {
fputs("some data", fp);
} else {
fputs("some other data", fp);
}
...
data = 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, Хьюстон, Техас, США.