Как работает абстрактный интерпретатор?

Я пытаюсь создать абстрактный интерпретатор для C. Возможно, не для всей грамматики, а только для ее подмножества. Ранее я спрашивал, на каком языке использовать. Прежде чем продолжить, я хотел бы знать, как работает эта абстрактная интерпретация?

Я просмотрел ссылки Wiki и ссылки на лекции. Я понял логику и теорию, лежащую в основе этого. Я сделал свой анализ. Я совершенно не могу понять, как интерпретировать код. То есть исходный код у меня был. Теперь у меня есть предварительная обработка. Я также выполнил некоторую нормализацию кода, которая требуется для моего анализа. Теперь, как мне выполнить код построчно и извлечь из него данные по мере того, как я продолжаю его выполнять? (Скажите, пожалуйста, если это невозможно. Или есть способ правильно выполнить программу, которая достигнет моей цели). Я собираю информацию, такую ​​как адрес памяти динамически выделяемого пространства, адреса возврата вызова функции.

Ранее мне предлагали CIL, CIL - это в основном инструмент преобразования, преобразующий код в некоторую нормализованную форму, заботясь о многих аномалиях, но я не смог получить никакой информации, относящейся к моей проблеме.

У меня вопрос, как извлекать информацию построчно и какой язык предпочтительнее? Императивные языки или функциональные языки? Я уже несколько дней искал информацию об этом в Google, но бесполезно. Любые ссылки также приветствуются. Спасибо.

РЕДАКТИРОВАТЬ: У меня все еще есть сомнения. Я получил ту часть, где мы пытаемся построить виртуальную среду. Позвольте мне объяснить, что я пытаюсь сделать, чтобы это помогло обсуждению. Я в основном пытаюсь провести анализ указателей, который в основном сосредоточен на арифметике указателей. Теперь предположим, что у меня есть целочисленный указатель, и я выполняю арифметические операции с указателем, тогда я не могу быть уверен, указывает ли указатель на действительные данные.

Из того, что вы говорите, я понимаю, что нам нужно выделить места для переменных, но как насчет значений. если у меня есть что-то вроде ниже

int a=10;
int *p = &a;
p = p+4;

Здесь известны значения а и константа «4». Что, если я получу значение от пользователя или файла. В таком случае мне нужно выполнить настоящую программу. В то же время мне нужно фиксировать данные, такие как адрес. ниже,

int *p =(int *) malloc (sizeof(int));
*p= 15;
cout<<*p;
p = p+ino//some user input value;
cout<<*p;

Таким образом, в основном код должен быть выполнен, но более поздняя часть решения больше походила на синтаксический анализ файла C. Пожалуйста, поправьте меня, если я ошибаюсь.


c abstract interpreter
person bsoundra    schedule 29.01.2011    source источник
comment
Когда вы говорите «абстрактная интерпретация», вы имеете в виду технику анализа программ, в которой вы пытаетесь построить модель того, что программа может делать, или средства выполнения кода C без компиляции его в машинный код? В первом случае какой анализ вы пытаетесь провести? В последнем случае не могли бы вы подробнее рассказать о том, что вас сбивает с толку?   -  person templatetypedef    schedule 29.01.2011

Ответы (3)


arrow_upward
3
arrow_downward

Предполагая, что вы действительно говорите об абстрактной интерпретации, а не просто интерпретируете C ...

Абстрактная интерпретация опирается на две вещи - абстрактную область, решетку конечной высоты и абстрактную семантику, посредством чего применение семантики строки к значению в домене из предыдущей строки должно привести к появлению нового значения в домене, имеющего такую ​​же высоту. или выше.

т.е. если ваш домен является набором мощности {1,2,3,4}, а вход - {1,2,3}, единственными допустимыми выходами являются {1,2,3} или {1,2,3,4} (при обычном порядке набора)

Затем вы выполняете рекурсию с фиксированной точкой в ​​каждой строке и сохраняете вывод семантики со строкой и семантики в конце каждой функции с определением функции. То, как вы выбираете предметную область и интерпретируете набор, который вы получите, в огромной степени зависит от анализа, который вы пытаетесь провести, но таков план, насколько я понимаю ...

Я должен сказать, что я не эксперт в этом вопросе, но некоторые из моих коллег-исследователей уже говорили со мной об этом в прошлом, и я пришел к такому пониманию ...

Кроме того, вы можете так же легко запустить анализ в обратном направлении - начиная с конца функции и двигаясь вперед, и это будет более подходящим для некоторых видов анализа ...

person tobyodavies    schedule 29.01.2011
comment
+1 Это отличное описание абстрактной интерпретации. Я надеюсь, что это то, что имел в виду OP! - person templatetypedef; 29.01.2011
comment
Вы также развеяли мои сомнения. Судя по объяснению, я думаю, что я скорее пытаюсь интерпретировать код, чем абстрактную интерпретацию. Судя по требованию проблемы и ранее полученным ответам на вопросы, я подумал, что это абстрактная интерпретация. - person bsoundra; 29.01.2011
comment
Используемая решетка не обязательно должна быть конечной высоты (один из первых примеров - это анализ диапазонов интервалов для небольшого языка программирования без переполнений, а решетка целочисленных интервалов определенно не имеет конечной высоты). Семантические функции должны быть монотонными (x ‹y =› f (x) ‹f (y)), что не то же самое, что всегда возвращать вывод, превышающий ввод. - person Pascal Cuoq; 29.01.2011
comment
Если вы хотите выполнить умное распространение констант, то это форма абстрактной интерпретации. - person SK-logic; 29.01.2011
comment
@pascal true, но для гарантированного завершения абстрактной интерпретации для любого ввода решетка должна иметь конечную высоту (иначе монотонная функция могла бы продолжать расти бесконечно, и рекурсия с фиксированной точкой никогда не завершилась бы), также я пытался Объясните монотонность на простом английском языке с моим утверждением, учитывая, что домен и ко-домен совпадают, и используется рекурсия с фиксированной точкой, _1 _... это не верно? - person tobyodavies; 29.01.2011
comment
@tobyodavies Абстрактная интерпретация заканчивается решетками не конечной высоты благодаря введению оператора расширения (для описания операторов расширения часто используются слова «ускоритель сходимости»). И есть величина, которая увеличивается только во время распространения, пока не будет достигнута фиксированная точка, но это не результат семантической функции f относительно ее ввода, это u(n+1) = u(n) ∪ f(u(n)) (объединение новых значений со всеми предыдущими значениями на каждой итерации) - person Pascal Cuoq; 29.01.2011
comment
@Pascal, я вижу, с моей стороны требуется больше чтения: D или вы знаете, пора мне действительно сделать что-то полезное, а затем написать статью об этом ... но даже тогда я подозреваю, что чтение может быть связано;) - person tobyodavies; 29.01.2011
comment
@tobyodavies Привет, я случайно писал в блоге сообщение о конкретной проблеме абстрактной интерпретации программ на языке C. Пропустите до конца сообщения, там есть последовательность абстрактных состояний, демонстрирующих расширение в действии: blog.frama-c.com/index.php?post/2011/01/27/On-memcpy-1 - person Pascal Cuoq; 29.01.2011

arrow_upward
2
arrow_downward

CIL может выполнять преобразование SSA. Программу в форме SSA на удивление легко рассуждать о и частично оценить - вам просто нужно заменять именованные значения, игнорируя или объединяя значения, поступающие из phi -узлов. Итак, чтобы превратить CIL в правильный абстрактный интерпретатор, вам нужно только добавить пару преобразований после SSA (который уже существует). В качестве альтернативы вы можете выполнять такого рода преобразования поверх LLVM IR, созданного Clang.

person SK-logic    schedule 29.01.2011

arrow_upward
1
arrow_downward

Судя по тому, как вы формулируете проблему, кажется, что вы говорите о интерпретации, а не о абстрактной интерпретации. Интерпретация означает просто взять код C и запустить его самостоятельно, в вашем случае для извлечения некоторой информации из того, что происходит во время выполнения. Абстрактная интерпретация относится к процедуре статического анализа, в которой вы пытаетесь понять, на что способна программа, возможно, в целях оптимизации или, возможно, чтобы попытаться доказать правильность или отсутствие ошибок. Конечно, я могу ошибаться в этом, и в этом случае вы можете проигнорировать этот ответ.

Если вы пытаетесь написать интерпретатор, вам, вероятно, потребуется настроить виртуальную среду выполнения, в которой будет выполняться программа. То есть вы, вероятно, захотите создать гигантский массив байтов, который будет служить памятью программы, и вам потребуется поддерживать свой собственный указатель стека и распределитель кучи. Затем вы можете выполнить программу, перейдя по очереди и изменив состояние этой среды в зависимости от конкретной строки кода, который вы выполняете. Например, выполнение такого оператора, как

int a;

будет работать, увеличивая указатель стека на четыре байта, при выполнении чего-то вроде

a = 137;

будет искать, на какую часть глобального массива памяти ссылается a, а затем перезаписывать байты четырехбайтовым значением для 137. С этого момента отслеживание того, что происходит во время выполнения, должно быть относительно простым - до того, как ваш интерпретатор выполнит какой-либо конкретный оператор или оценит выражение, вы можете записать в журнал любые соответствующие детали.

Учтите, что это будет непросто. Вам придется вручную выделять и очищать кадры стека, поддерживать счетчик программ и т. Д. Однако это звучит очень весело, и я желаю вам удачи!

person templatetypedef    schedule 29.01.2011
comment
ответил правкой на вопрос из-за проблемы с форматированием. - person bsoundra; 29.01.2011