Теперь я запутался в символическом выполнении (SE) и анализе достижимости (RA). Насколько я знаю, SE использует символы для выполнения некоторого кода для достижения каждой ветки с условиями ветвления. И RA можно использовать для определения достижимости каждой ветки, верно? Когда используется RA, мы можем извлечь условие перехода для каждого перехода. Если да, то в чем между ними разница? Могут ли они быть быстрыми? Это все статический анализ?
Спасибо, Ева
Символическое выполнение выполняется без выполнения программы. Следовательно, это статический анализ.
Хороший символьный анализ вычисляет условия пути для каждой точки программы. Лучший сможет рассуждать о формуле пути, чтобы продемонстрировать, что она достижима (точка программы достижима) или нет (точка программы мертва).
По сравнению со скоростью выполнения скомпилированного кода символьное выполнение имеет тенденцию быть довольно медленным.
Анализ достижимости в основном используется, чтобы увидеть, может ли модель достичь состояния или нет. Тем не менее, символическое выполнение — это метод статического анализа (иногда также динамический, как это делает KLEE), чтобы найти все пути в программе/исходном коде.
Символьное выполнение не статично и выполняет программу символически. Из соображений производительности инструменты символьного выполнения, такие как klee, не решают условие перехода при обнаружении перехода. Он использует дешевый анализ, чтобы увидеть, будет ли он достижим. Он попытается сгенерировать тестовый пример при достижении выхода из программы. Если собранные ограничения от начальной точки (основной функции) до выхода выполнимы, то будет задан тестовый пример, иначе выход недоступен. SE использует анализ достижимости для создания тестового примера для покрытия кода.
