Bug #8486
closedОтсутствие связывания констант в smt формулах, генерируемых на основе бинарного кода (команда symexecute).
0%
Description
Насколько мне удалось проанализировать: в текущей генерируемой модели отсутствует связывание между собой констант для разных инструкций. Иными словами, если существуют две инструкции (процессор PowerPC):
addi r3, r0, 17;
addi r3, r3, 25;
Из модели нельзя понять что в обоих инструкциях используется регистр r3. Похожая ситуация скорее всего и с памятью т.к. значения аргументов инструкций игнорируется, будь то номер регистра или иная константа. И даже если вручную прописать все эти значения (добавить соответствующий assert) модель всё равно будет содержать неопределённость, что указывает на то, что игнорируется также часть констант из модели. На основе описанных выше инструкций мной был составлен тест для модели PowerPC (приложен в файле 42.bin). Если модель будет сгенерированна правильно, то значение GPR [3] должно будет всегда равняться 42, т.е. smt-решатель (я использовал cvc4 и z3) не сможет доказать обратного (здесь надо сделать оговорку: поскольку значение CIA (Program Counter) явно не задаётся, а определяется тестовым шаблоном, решатель попытался присвоить ему значение равное 2^64, после чего решение потеряло смысл. Следовательно при генерации его возможно также следует задавать более явно).
Предлагаю использовать данный тест для первоначальной проверки корректности будущих версий генератора.
На всякий случай прикладываю сгенерированный smt.
Также напоминаю что файл маппинга smt переменных на регистры и память всё ещё не генерируется.
Files