В этом посте мы попробуем применить технику символьного выполнения на примере символьной ВМ KLEE для решения простого ASCII-лабиринта. Как вы думаете, сколько верных решений мы сможем найти?
Сам лабиринт представляет собой программу на С, код которой вы можете взять здесь. После запуска игра ожидает ввода последовательности шагов (a — шаг влево, d — вправо, w — вверх и s — вниз). Выглядит это так:
Несмотря на кажущуюся простоту, лабиринт скрывает в себе один секрет и поэтому имеет более чем одно решение.
KLEE — символьный интерпретатор биткода LLVM, т.е. он может выполнять код, сгенерированный любым фронт-эндом. Суть символьного выполнения сводится к тому, что все входные значения запускаемой программы содержат не конкретные значения, а символьные ограничения на возможные значения. В процессе выполнения могут создаваться новые символьные переменные (например, когда их значения зависят от результата какой-либо операции с символьным операндом), а так же изменяться существующие (при ветвлении на пути выполнения программы). Во втором случае KLEE использует SMT решатель, чтобы определить, возможно ли в принципе выполнение программы по данному пути.
Если вас заинтересовала эта тема, можете посмотреть здесь и почитать это или даже это.
Идея поста проста — скормить программе-лабиринту символьную строку и посмотреть как KLEE найдет решения.
Лабиринт задается в виде двумерного массива символов.
Задача draw() — рисовать наш массив на экране.
Функция main() начинается с объявления переменных, хранящих позицию игрока, итератора и 28-байтного массива, который хранит действия. Затем, начальная позиция игрока устанавливается равной (1,1) и на этом месте рисуется крестик.
Читаем из stdin что там ввел игрок.
Далее, на каждой итерации цикла мы сохраняем старые координаты пользователя и двигаем его на новое место.
Если игрок дошел до конца — поздравляем его.
Если что-то не так — возвращаемся на место, где стояли.
Если врезались в стену — игрок проиграл.
Ну а если ничего не случилось — значит мы просто шагнули. Двигаем игрока, рисуем картинку, увеличиваем итератор и возвращаемся на начало.
Если вам вдруг захочется пройти игру самим, то, скорее всего, вы получите следующее решение: ssssddddwwaawwddddssssddwwww
Прежде всего, нам понадобится LLVM, транслятор C -> LLVM IR (llvm-gcc или clang) и, собственно, KLEE. В большинстве дистрибутивов Linux эти пакеты уже есть в репозиториях.
Чтобы транслировать mace.c в биткод LLVM нужно выполнить команду
Как и говорилось ранее, вместо llvm-gcc можно использовать clang.
В результате выполнения этой команды мы получил файл maze.bc, который представляет собой биткод программы-лабиринта. Его даже можно запустить на интерпретаторе LLVM:
Для тестирования кода с помощью KLEE, нам необходимо пометить какие-нибудь переменные символьными. В данном случае, это будет массив действий, объявленный в начале main(). Итак, заменяем строку
на
И не забудем добавить заголовочный файл KLEE
Теперь KLEE сможет пройти по любому возможному пути выполнения (да и коридору лабиринта). Причем, если эти пути могут привести к какой-либо ошибке (например, к переполнению буфера), KLEE сигнализирует нам об этом. Выполняем
и наблюдаем такую картину:
Как видно из последних 3х сообщений, KLEE нашла 321 разный путь. Правда, это не 321 верное решение.
Подробный отчет сохраняется в директорию klee-last
Каждый тест можно просмотреть с помощью утилиты ktest-tool
В данном случае, вы можете просто взять значение переменной program отсюда и воспроизвести тест, передав это значение программе-лабиринту.
Итак, мы и нашли все возможные пути следования в программе. Но не просматривать же каждый тест, чтобы найти все верные решения! Нам нужно заставить KLEE выделить тесты, которые действительно доходят до «You win!».
В интерфейсе KLEE присутствует функция klee_assert(), которая делает то же самое, что и аналогичная ей assert() в C — вычисляет значение булевого выражения и, если оно false — прерывает выполнение программы. Для нашего случая это то, что доктор прописал.
Добавим после строки
безусловный вызов klee_assert()
Теперь KLEE не перестанет генерировать тесты для всех возможных путей выполнения, однако тесты, приводящие к вызову klee_assert() будут иметь .err в своем имени:
Давайте посмотрим на один из них
Итак, предлагаемое KLEE решение — sddwddddssssddwwww
Эй, позвольте! Оно выглядит коротким! Давайте попробуем его на настоящем лабиринте:
Я так и знал!!! В лабиринте есть ненастоящие стены! И KLEE благополучно прошла сквозь них! Но погодите, если KLEE должна была найти все решения, то где наше самое первое? Почему KLEE не нашла его?
Чтож, обычно нам достаточно одного пути до ошибки, если мы ищем саму ошибку, а альтернативные пути до нее нам не требуются. Поэтому, в данном случае воспользуемся одной из 10000 опций командной строки.
Смотрим на результат:
Теперь мы получили 4 теста, которые и являются 4 возможными решениями нашего лабиринта:
Итак, решения данного лабиринта:
1. ssssddddwwaawwddddssssddwwww
2. ssssddddwwaawwddddsddw
3. sddwddddssssddwwww
4. sddwddddsddw
Лабиринт
Сам лабиринт представляет собой программу на С, код которой вы можете взять здесь. После запуска игра ожидает ввода последовательности шагов (a — шаг влево, d — вправо, w — вверх и s — вниз). Выглядит это так:
Player pos: 1x4 Iteration no. 2. Action: s. +-+---+---+ |X| |#| |X| --+ | | |X| | | | |X+-- | | | | | | +-----+---+
Несмотря на кажущуюся простоту, лабиринт скрывает в себе один секрет и поэтому имеет более чем одно решение.
KLEE
KLEE — символьный интерпретатор биткода LLVM, т.е. он может выполнять код, сгенерированный любым фронт-эндом. Суть символьного выполнения сводится к тому, что все входные значения запускаемой программы содержат не конкретные значения, а символьные ограничения на возможные значения. В процессе выполнения могут создаваться новые символьные переменные (например, когда их значения зависят от результата какой-либо операции с символьным операндом), а так же изменяться существующие (при ветвлении на пути выполнения программы). Во втором случае KLEE использует SMT решатель, чтобы определить, возможно ли в принципе выполнение программы по данному пути.
Если вас заинтересовала эта тема, можете посмотреть здесь и почитать это или даже это.
Идея поста проста — скормить программе-лабиринту символьную строку и посмотреть как KLEE найдет решения.
Разберем код
Лабиринт задается в виде двумерного массива символов.
#define H 7
#define W 11
char maze[H][W] = { "+-+---+---+",
"| | |#|",
"| | --+ | |",
"| | | | |",
"| +-- | | |",
"| | |",
"+-----+---+" };
Задача draw() — рисовать наш массив на экране.
void draw ()
{
int i, j;
for (i = 0; i < H; i++)
{
for (j = 0; j < W; j++)
printf ("%c", maze[i][j]);
printf ("\n");
}
printf ("\n");
}
Функция main() начинается с объявления переменных, хранящих позицию игрока, итератора и 28-байтного массива, который хранит действия. Затем, начальная позиция игрока устанавливается равной (1,1) и на этом месте рисуется крестик.
int
main (int argc, char *argv[])
{
int x, y; //Player position
int ox, oy; //Old player position
int i = 0; //Iteration number
#define ITERS 28
char program[ITERS];
x = 1;
y = 1;
maze[y][x]='X';
Читаем из stdin что там ввел игрок.
read(0,program,ITERS);
Далее, на каждой итерации цикла мы сохраняем старые координаты пользователя и двигаем его на новое место.
while(i < ITERS)
{
ox = x; //Save old player position
oy = y;
switch (program[i])
{
case 'w':
y--;
break;
case 's':
y++;
break;
case 'a':
x--;
break;
case 'd':
x++;
break;
default:
printf("Wrong command!(only w,s,a,d accepted!)\n");
printf("You loose!\n");
exit(-1);
}
Если игрок дошел до конца — поздравляем его.
if (maze[y][x] == '#')
{
printf ("You win!\n");
printf ("Your solution \n",program);
exit (1);
}
Если что-то не так — возвращаемся на место, где стояли.
if (maze[y][x] != ' ' &&
!((y == 2 && maze[y][x] == '|' && x > 0 && x < W)))
{
x = ox;
y = oy;
}
Если врезались в стену — игрок проиграл.
if (ox==x && oy==y){
printf("You loose\n");
exit(-2);
}
Ну а если ничего не случилось — значит мы просто шагнули. Двигаем игрока, рисуем картинку, увеличиваем итератор и возвращаемся на начало.
maze[y][x]='X';
draw (); //draw it
i++;
sleep(1); //me wait to human
}
Пройдем лабиринт вручную
Если вам вдруг захочется пройти игру самим, то, скорее всего, вы получите следующее решение: ssssddddwwaawwddddssssddwwww
А теперь с KLEE
Прежде всего, нам понадобится LLVM, транслятор C -> LLVM IR (llvm-gcc или clang) и, собственно, KLEE. В большинстве дистрибутивов Linux эти пакеты уже есть в репозиториях.
Чтобы транслировать mace.c в биткод LLVM нужно выполнить команду
$ llvm-gcc -c –emit-llvm maze.c -o maze.bc
Как и говорилось ранее, вместо llvm-gcc можно использовать clang.
В результате выполнения этой команды мы получил файл maze.bc, который представляет собой биткод программы-лабиринта. Его даже можно запустить на интерпретаторе LLVM:
$ lli maze.bc
Для тестирования кода с помощью KLEE, нам необходимо пометить какие-нибудь переменные символьными. В данном случае, это будет массив действий, объявленный в начале main(). Итак, заменяем строку
read(0,program,ITERS);
на
klee_make_symbolic(program,ITERS,"program");
И не забудем добавить заголовочный файл KLEE
#include <klee/klee.h>
Теперь KLEE сможет пройти по любому возможному пути выполнения (да и коридору лабиринта). Причем, если эти пути могут привести к какой-либо ошибке (например, к переполнению буфера), KLEE сигнализирует нам об этом. Выполняем
$ klee maze.bc
и наблюдаем такую картину:
Как видно из последних 3х сообщений, KLEE нашла 321 разный путь. Правда, это не 321 верное решение.
KLEE: done: total instructions = 112773 KLEE: done: completed paths = 321 KLEE: done: generated tests = 318
Подробный отчет сохраняется в директорию klee-last
$ ls klee-last/ assembly.ll test000078.ktest test000158.ktest info test000079.ktest test000159.ktest messages.txt test000080.ktest test000160.ktest run.istats test000081.ktest test000161.ktest run.stats test000082.ktest test000162.ktest test000001.ktest test000083.ktest test000163.ktest test000075.ktest test000155.ktest warnings.txt
Каждый тест можно просмотреть с помощью утилиты ktest-tool
$ ktest-tool klee-last/test000222.ktest ktest file : ‘klee-last/test000222.ktest’ args : ['maze_klee.o'] num objects: 1 object 0: name: ‘program’ object 0: size: 29 object 0: data: ‘ssssddddwwaawwddddssssddwwwd\x00′
В данном случае, вы можете просто взять значение переменной program отсюда и воспроизвести тест, передав это значение программе-лабиринту.
Итак, мы и нашли все возможные пути следования в программе. Но не просматривать же каждый тест, чтобы найти все верные решения! Нам нужно заставить KLEE выделить тесты, которые действительно доходят до «You win!».
В интерфейсе KLEE присутствует функция klee_assert(), которая делает то же самое, что и аналогичная ей assert() в C — вычисляет значение булевого выражения и, если оно false — прерывает выполнение программы. Для нашего случая это то, что доктор прописал.
Добавим после строки
printf ("You win!\n");
безусловный вызов klee_assert()
printf ("You win!\n");
klee_assert(0); //Signal The solution!!
Теперь KLEE не перестанет генерировать тесты для всех возможных путей выполнения, однако тесты, приводящие к вызову klee_assert() будут иметь .err в своем имени:
$ ls -1 klee-last/ |grep -A2 -B2 err test000096.ktest test000097.ktest test000098.assert.err test000098.ktest test000098.pc
Давайте посмотрим на один из них
$ ktest-tool klee-last/test000098.ktest ktest file : ‘klee-last/test000098.ktest’ args : ['maze_klee.o'] num objects: 1 object 0: name: ‘program’ object 0: size: 29 object 0: data: ‘sddwddddssssddwwww\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00′
Итак, предлагаемое KLEE решение — sddwddddssssddwwww
Эй, позвольте! Оно выглядит коротким! Давайте попробуем его на настоящем лабиринте:
Я так и знал!!! В лабиринте есть ненастоящие стены! И KLEE благополучно прошла сквозь них! Но погодите, если KLEE должна была найти все решения, то где наше самое первое? Почему KLEE не нашла его?
Чтож, обычно нам достаточно одного пути до ошибки, если мы ищем саму ошибку, а альтернативные пути до нее нам не требуются. Поэтому, в данном случае воспользуемся одной из 10000 опций командной строки.
$ klee –emit-all-errors maze_klee.o
Смотрим на результат:
Теперь мы получили 4 теста, которые и являются 4 возможными решениями нашего лабиринта:
$ ktest-tool klee-last/test000097.ktest ktest file : ‘klee-last/test000097.ktest’ args : ['maze_klee.o'] num objects: 1 object 0: name: ‘program’ object 0: size: 29 object 0: data: ‘sddwddddsddw\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00′ $ ktest-tool klee-last/test000136.ktest ktest file : ‘klee-last/test000136.ktest’ args : ['maze_klee.o'] num objects: 1 object 0: name: ‘program’ object 0: size: 29 object 0: data: ‘sddwddddssssddwwww\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00′ $ ktest-tool klee-last/test000239.ktest ktest file : ‘klee-last/test000239.ktest’ args : ['maze_klee.o'] num objects: 1 object 0: name: ‘program’ object 0: size: 29 object 0: data: ‘ssssddddwwaawwddddsddw\x00\x00\x00\x00\x00\x00\x00′ $ ktest-tool klee-last/test000268.ktest ktest file : ‘klee-last/test000268.ktest’ args : ['maze_klee.o'] num objects: 1 object 0: name: ‘program’ object 0: size: 29 object 0: data: ‘ssssddddwwaawwddddssssddwwww\x00′
Итак, решения данного лабиринта:
1. ssssddddwwaawwddddssssddwwww
2. ssssddddwwaawwddddsddw
3. sddwddddssssddwwww
4. sddwddddsddw
