Я пытаюсь понять, как работают двигатели Symbolic Execution. В этой статье рассматриваются методы использования C. В них упоминается символическая память:
3.1 Полностью символьная память
На самом высоком уровне общности движок может рассматривать адреса памяти как полностью символические...
Представление памяти в компактной форме. Этот подход был использован в [32], который сопоставляет символьные, а не конкретные адресные выражения с данными, представляя возможные альтернативные состояния, возникающие в результате обращения к памяти с использованием символьных адресов в компактной неявной форме.
Эта статья также немного углубляется в символические кучи для Java:
4.1 Символическое представление состояния
Символическое состояние s состоит из символической кучи H, оценки полей примитивного типа, условия пути PC и счетчика программ.
Мне интересно, что на практике означает эта символическая куча. Для меня это означает, что все структуры данных, используемые при символическом выполнении, будут использовать символическую память, а не фактическую память. Это означает, что такие структуры, как массивы, должны иметь символические модели. Мне интересно на высоком уровне, как выглядят эти модели. Я не понимаю, как вы можете «символически моделировать длину массива». В моей голове это целое число, поэтому оно будет целым числом. А вот как символическое значение, интересно, что это значит. Я еще не вижу. Интересно, можно ли объяснить на высоком уровне, как можно символически моделировать некоторые структуры данных, такие как массивы или структуры с некоторыми другими значениями полей, поэтому это было бы полезно при символическом выполнении.
В этой старой статье упоминается:
Можно также определить альтернативную семантику «символического выполнения» для языка программирования, где реальные объекты данных не обязательно должны использоваться, но могут быть представлены произвольными символами.
Не уверен, как это выглядит.
