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