В чем разница между реализацией статического анализа и символьным выполнением?
Статический анализ против символьного выполнения в реализации
Ответы (2)
Статический анализ — это любое автономное вычисление, которое проверяет код и дает заключения о его качестве. Вы можете применить это к исходному коду, к коду виртуальной машины для наборов инструкций виртуальной машины Java/C#/... и даже к двоичному объектному коду. Не существует «одного» статического анализа (хотя классическое управление компилятором и поток данных часто занимают видное место в качестве основного механизма для SA); этот термин в совокупности применяется ко всем типам механизмов, которые могут использоваться в автономном режиме.
Символьное выполнение — это особый вид офлайн-вычислений, который вычисляет некоторое приближение к тому, что на самом деле делает программа, путем построения формул, представляющих состояние программы в различных точках. Он называется «символическим», потому что аппроксимация обычно представляет собой какую-то формулу, включающую программные переменные и ограничения на их значения.
Статический анализ может использовать символьное выполнение и проверять результирующую формулу. Или он может использовать какой-то другой метод (регулярные выражения, классический анализ потока компилятора,...) или некоторую комбинацию. Но статический анализ не обязательно должен использовать символьное выполнение.
Символьное выполнение может использоваться только для демонстрации ожидаемого символьного результата вычисления. Это не статический анализ в соответствии с приведенным выше определением, потому что нет никакого мнения о том, насколько хорош этот результат. Или формула может быть подвергнута анализу, после чего она станет частью статического анализа. С практической точки зрения можно использовать другие методы анализа программы для поддержки символьного выполнения («эта формула для переменной распространяется на то, какое чтение переменной x?» — вопрос, на который обычно хорошо отвечает анализ потока).
Вы можете настаивать на том, что статический анализ — это любое автономное вычисление вашего исходного кода, и в этом случае символьное выполнение является лишь особым случаем. Я не нахожу это определение полезным, потому что оно недостаточно хорошо различает варианты использования.
person
Ira Baxter
schedule
21.09.2016
Благодарю. В общем, какая реализация менее трудоемка?
- person any; 22.09.2016
что занимает меньше времени? Речь идет не об усилиях по реализации. Вы выбираете технологию/архитектуру для достижения цели из множества вариантов, которые у вас есть. Но без конкретного заявления о цели у вас нет возможности ранжировать, какой из них более разумен. Если у вас нет конкретной цели и вы хотите сделать как можно меньше работы, вы просто ничего не делаете.
- person Ira Baxter; 22.09.2016
Теперь у вас может быть конкретная задача. Вы обнаружите, что независимо от того, какую из этих технологий вы хотели бы использовать, все они требуют значительного времени для создания с нуля. Если вы хотите достичь своей цели, вам следует приобрести нужные вам технологии таким образом, чтобы они были аккуратно интегрированы, чтобы вы могли сосредоточиться на их настройке для решения вашей конкретной проблемы. Мой опыт показывает, что в большинстве случаев вы не можете найти их вместе, и поэтому я решил решить эту проблему. См. semdesigns.com/Products/DMS/LifeAfterParsing.html.
- person Ira Baxter; 22.09.2016
Я сказал это, потому что мое время ограничено. Когда я читаю статьи о статическом анализе, например, языки моделирования. com/ и сравните ее с тем, что вы сказали в stackoverflow.com/questions/39490607/ Я обнаружил несколько сходств, например, оба они используют абстрактное синтаксическое дерево. Мне непонятно, в чем именно разница между ними с точки зрения реализации и используемых технологий (не цели).
- person any; 22.09.2016
Лучше всего использовать понимание и опыт, которые с трудом приобрели другие люди в сообществе. Абстрактные синтаксические деревья — хорошая идея, но делать это так, как это делает большинство людей, добавляет сложности, верьте или нет, вам нужны абстрактные синтаксические деревья, полученные из конкретных, если вы не хотите, чтобы абстрактная часть создавала more< /i> работать. См. stackoverflow.com/a/1916687/120163. Но деревья — это простая часть, безусловно; Life After Parsing расскажет вам, что вам нужно на практике, если вы хотите учесть тот факт, что ваше время ограничено. В противном случае вы изобретаете все заново, плохо.
- person Ira Baxter; 22.09.2016
Вы избегаете говорить о своей истинной цели. Эта цель поможет решить, какие вспомогательные технологии вы хотели бы использовать. Затем вам понадобятся реализации этих технологий; да, вы можете построить все сами, но если вы попытаетесь сделать это, вы никогда не успеете по-настоящему работать над поставленной целью. Лучше получить эти технологии уже упакованными и работающими. Итак, что именно вы пытаетесь сделать?
- person Ira Baxter; 23.09.2016
Я хочу реализовать символическое выполнение программ, написанных на определенном языке, которые имеют императивную и декларативную части (и особенно части выражений ocl). Я хочу знать, с чего мне начать. Также я прочитал ссылку выше о статическом анализе определенного языка и обнаружил сходство между этим способом статического анализа и тем, что вы сказали ранее для символического выполнения. Я хочу знать, в чем разница между этим способом статического анализа и символическим выполнением. И для символического выполнения, которое я хочу сделать, какие шаги должны быть предприняты по порядку?
- person any; 23.09.2016
Символическое выполнение и статический анализ сами по себе не представляют интереса. Ваш вопрос похож на то, что я хочу использовать набор инструментов плотника, и я вижу ценность в инструментах для сантехники... какой набор инструментов мне следует внедрить в первую очередь? Вы еще не обозначили свою настоящую цель, ИМХО. Я пересмотрел свой ответ, чтобы помочь прояснить различие между SA и SE, но они по-прежнему являются сложными темами, и вы не хотите реализовывать их самостоятельно, если рассчитываете достичь своей реальной цели в любой разумный период времени (вы читали Жизнь после тщательного разбора?). Если это неясно, вы не готовы это сделать.
- person Ira Baxter; 23.09.2016
Я хочу проверить предварительные/последующие условия или создание тестовых примеров программ, написанных на определенном языке.
- person any; 23.09.2016
Если вы действительно хотите проверить предварительные/последующие условия, вы можете подумать о доказательстве теорем (отсюда и этот термин). TP во многом похож на символьное выполнение в том смысле, что вы строите формулы о состоянии программы, но он также касается доказательства теорем, что на самом деле довольно сложно. Но символическое выполнение даст вам формулу для состояния программы на определенном пути (может быть, на всех путях, если вы сделаете это для всех путей), и теперь у вас есть что сопоставить с постусловием. Вы не ответили на вопрос, читали ли вы LifeAfterParsing.
- person Ira Baxter; 23.09.2016
Вы можете сгенерировать тестовые примеры из кода, перечислив пути потока управления через него к некоторому постусловию, и для каждого конкретного пути потока и каждого условного условия на этом пути сгенерируйте тестовую программу, которая заставит это условие быть истинным. Итак, теперь ваша тестовая программа выполняет путь, и тестируемая программа достигает постусловия, которое предположительно компилируется, и, таким образом, определяет, правильно ли постусловие для процедуры на этом пути. Чтобы протестировать всю функцию, вам нужно сгенерировать тесты для каждого пути; это может быть много путей. ...
- person Ira Baxter; 25.09.2016
Когда вы приступите к таким задачам, вам понадобится как можно больше машин статического анализа и символьного выполнения, потому что вы будете использовать каждую из них несколько раз, пытаясь достичь этой цели. Если вы попытаетесь выбрать только одно, вы обнаружите, что хотите и другое.
- person Ira Baxter; 25.09.2016
Мне очень нравится этот слайд из доклада Джулиана Коэна "Современный автоматический анализ программ". Короче говоря, люди любят делить программный анализ на две широкие категории: статический и динамический анализ. Но на самом деле существует широкий спектр методов анализа программ, от статических до динамических, от ручных до полностью автоматических. Символьное выполнение — интересный метод, который находится где-то между статическим и динамическим анализом и обычно применяется как полностью автоматический подход.
person
Ben Holland
schedule
10.11.2016
Благодарю. Знаете ли вы, какие ошибки может обнаружить статический анализ (например, компилятор), а символьное выполнение не может обнаружить?
- person any; 12.11.2016
Сложно сказать (особенно в комментарии). Статический анализ имеет дело с проблемами осуществимости пути, тогда как динамический анализ, как правило, имеет дело с охватом пути. Символический анализ находится где-то посередине и имеет дело со взрывом пространства состояний, логически разветвляя анализ на ветви и находя набор выполнимых ограничений. Большинство реализаций, которые я видел, тратят много времени на обработку в решателях SAT/SMT. На этот вопрос также трудно ответить, потому что многие реализации представляют собой смесь методов. Например, статический анализ может быть полностью автоматическим.
- person Ben Holland; 12.11.2016
Я создаю новый вопрос об этом в этой ссылке: stackoverflow.com/questions/38540082/
- person any; 13.11.2016
