Статический анализ и символическое исполнение в реализации
Чем отличается реализация статического анализа от символьного исполнения?
2 ответа
Мне очень нравится этот слайд из выступления Джулиана Коэна "Современный автоматический анализ программ". Одним словом, людям нравится делить программный анализ на две широкие категории статического и динамического анализа. Но на самом деле существует широкий спектр методов анализа программ, от статического до динамического, от ручного до полностью автоматического. Символьное выполнение - интересная техника, которая находится где-то посередине между статическим и динамическим анализом и обычно применяется как полностью автоматический подход.
Статический анализ - это любое автономное вычисление, которое проверяет код и выдает мнение о качестве кода. Вы можете применить это к исходному коду, к коду виртуальной машины для наборов команд виртуальной машины Java/C#/... и даже к двоичному объектному коду. Не существует "одного" статического анализа (хотя классическое управление компилятором и поток данных часто играют важную роль в качестве основы для SA); этот термин в совокупности применяется ко всем типам механизмов, которые могут использоваться в автономном режиме.
Символьное выполнение - это особый вид автономных вычислений, который вычисляет некоторую аппроксимацию того, что на самом деле делает программа, путем построения формул, представляющих состояние программы в различных точках. Это называется "символическим", потому что аппроксимация обычно представляет собой какую-то формулу, включающую программные переменные и ограничения на их значения.
Статический анализ может использовать символьное выполнение и проверять полученную формулу. Или он может использовать другую технику (регулярные выражения, классический анализ потока компилятора,...) или некоторую комбинацию. Но статический анализ не должен использовать символическое исполнение.
Символическое выполнение может использоваться только для показа ожидаемого символического результата вычисления. Это не статический анализ по вышеприведенному определению, потому что нет никакого мнения о том, насколько хорош этот результат. Или формула может быть подвергнута анализу, после чего она становится частью статического анализа. С практической точки зрения можно использовать другие методы анализа программы для поддержки символьного выполнения ("эта формула для переменной распространяется на то, что читает переменную x?" - это вопрос, который обычно хорошо решается анализом потока).
Вы можете настаивать на том, что статический анализ - это любое автономное вычисление над вашим исходным кодом, когда символическое выполнение - это просто особый случай. Я не нахожу это определение полезным, потому что оно недостаточно хорошо различает варианты использования.