Project

General

Profile

Actions

Bug #8486

closed

Отсутствие связывания констант в smt формулах, генерируемых на основе бинарного кода (команда symexecute).

Added by Pavel Putro about 7 years ago. Updated about 5 years ago.

Status:
Closed
Priority:
Urgent
Assignee:
Category:
Symexecutor
Target version:
Start date:
10/06/2017
Due date:
% Done:

0%

Estimated time:
Detected in build:
svn
Platform:
Published in build:
2.4.46-beta-191025

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

42.bin (8 Bytes) 42.bin Pavel Putro, 10/06/2017 11:01 PM
42.bin.smt2 (9.66 KB) 42.bin.smt2 Pavel Putro, 10/06/2017 11:28 PM
42.bin.smt2 (9.93 KB) 42.bin.smt2 Оригиал Pavel Putro, 01/18/2018 12:35 AM
42.bin_fixed.smt2 (10.6 KB) 42.bin_fixed.smt2 Исправленный Pavel Putro, 01/18/2018 12:35 AM
storeload.bin.smt2 (68.4 KB) storeload.bin.smt2 Pavel Putro, 01/24/2018 01:12 AM
storeload.bin_fixed.smt2 (68.6 KB) storeload.bin_fixed.smt2 Pavel Putro, 01/24/2018 01:12 AM
storeload.bin (12 Bytes) storeload.bin Pavel Putro, 01/24/2018 01:12 AM
addsub.bin (8 Bytes) addsub.bin Pavel Putro, 01/24/2018 01:12 AM
addsub.bin.smt2 (32.5 KB) addsub.bin.smt2 Pavel Putro, 01/24/2018 01:12 AM
addsub.bin_fixed.smt2 (32.7 KB) addsub.bin_fixed.smt2 Pavel Putro, 01/24/2018 01:12 AM
abs_1.bin (72 Bytes) abs_1.bin Pavel Putro, 01/24/2018 01:25 AM
Actions

Also available in: Atom PDF