Каковы различия между символическим выполнением и решателями SAT?
-
29-09-2020 - |
Вопрос
Насколько я понимаю, символическое выполнение имеет дело только с конкретными путями и плохими шаблонами, в то время как решатели SAT или теории выполнимости по модулю в целом обеспечивают гораздо более надежный анализ программы.
Может ли кто-нибудь подтвердить приведенное выше утверждение и (вкратце) объяснить различия между этими двумя формальными методологиями проверки?
Решение
ТЛ;ДР: Они различаются по основному вводу и выводу.Решатели SAT и SMT не знают, что такое программы;это инструменты, которые отвечают «да» или «нет» на вопросы о математических формулах.Символическое выполнение, с другой стороны, является методом анализа программ.Символическое выполнение обычно зависит от решателей SAT и SMT, но не наоборот.
Решатели SAT и SMT не имеют прямого отношения к программам.Вместо этого решатель SAT или SMT принимает на вход математически описанную «формулу» и примерно отвечает, истинна она или ложна.(Часто допускается третий вариант, неизвестный, для случаев, когда решатель не может найти ответ.)
Например, возможные входные данные для решателя SAT: (a and not b) or (not a and c)
.То есть это математическая формула, где a
, b
, и c
вот логические константы (0 или 1).Решающая программа SAT должна решить, может ли формула быть верной, выбирая значения a
, b
, и c
.Решатели SMT похожи, но a
, b
, и c
будут заменены более сложными формулами, использующими целые числа, строки, функции и т. д., например x + 3 = y^2
.
Символическое исполнение — это необычный способ запуска программы, но не тот, для которого она предназначена.Вместо этого программа запускается с использованием так называемых «символических» значений, которые представляют собой своего рода заполнители.Для примера того, что это значит, предположим, что у меня есть функция типа f(x) = if x > 0 then 1 else 0
.Обычно я запускаю программу, вводя, скажем, 3
, и получить f(3) = 1
, с 3
больше, чем 0
.При символическом выполнении я запускаю программу, вводя переменную-заполнитель: input
, и я оцениваю программу, чтобы получить два случая:или input > 0 and answer = 1
или input <= 0 and answer = 0
.Это может показаться бесполезным, но в конечном итоге это мощный способ анализа программ.
Связь между двумя заключается в том, что символическое выполнение часто полагается на решатели SMT во время выполнения, чтобы выяснить, действительно ли возможен определенный путь или его следует отбросить.Например, решатель SMT можно использовать, чтобы определить, input <= 0 and answer = 0
возможно (ответ – да, например, если input = 0
).Таким образом, SMT является своего рода «движущей силой», делающей возможным символическое исполнение.