Я хотел бы смоделировать буферы памяти фиксированного размера и их операции доступа в Z3. Размер буферов может быть от пары байтов до сотен байтов. Стандартный способ, используемый несколькими существующими инструментами (например, KLEE), заключается в создании переменных массива в домене и диапазоне битовых векторов. Каждый буфер памяти получает такой массив, а чтение / запись в память кодируется с использованиемselect/store операции.

Увы, в моих тестах при использовании этого подхода Z3 (*) оказывается медленнее, чем STP. Прежде чем анализировать запросы более подробно, чтобы выяснить, что происходит, я хотел убедиться, что я использую «правильный» подход к кодированию операций с памятью в Z3 (поскольку, по общему признанию, STP был специально разработан для использования с массивами и битовыми векторами). ).

Так какой же самый эффективный способ представления буферов памяти в Z3? Пока я рассматриваю пару альтернатив:

Используйте утверждения указать начальные значения буфера памяти, вместо использования вложенныхstore-s. Однако, в моих предварительных тестах, это, кажется, замедляет Z3 еще больше.Используйте битовые векторы для кодирования буферов. Тем не менее, получающиеся битовые векторы могут быть довольно большими (~ 1000 с бит), и я не уверен, что Z3 или любой другой решатель справится с этим эффективно.Создайте отдельные переменные битового вектора для каждого байта памяти ииспользовать вложенныйite выражения направить доступ к памяти к соответствующим переменным. Однако, боюсь, это сильно усложнит модель и потребует квантификаторов.Используйте неинтерпретированные функции вместо массивов, но это требует переопределения аксиом массива таким образом, который может быть менее эффективным, чем собственная теория встроенных массивов Z3.

Есть ли лучшие подходы, которые мне не хватает?

(*) Стандартный неинкрементный решатель, ветвь Z3unstable@aba79802cfb5