Bug #8486: Отсутствие связывания констант в smt формулах, генерируемых на основе бинарного кода (команда symexecute). - MicroTESK - Open-Source Projects

Actions

Copy link

Bug #8486

closed

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

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

Status:

Closed

Priority:

Urgent

Assignee:

Pavel Putro

Category:

Symexecutor

Target version:

2.4

Start date:

10/06/2017

Due date:

% Done:

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

Download all 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

Updated by Andrei Tatarnikov over 7 years ago

Assignee set to Artem Kotsynyak
Priority changed from Normal to Urgent

Updated by Andrei Tatarnikov about 7 years ago

Status changed from New to Feedback
Assignee changed from Artem Kotsynyak to Pavel Putro

Updated by Pavel Putro about 7 years ago

File 42.bin.smt2 42.bin.smt2 added
File 42.bin_fixed.smt2 42.bin_fixed.smt2 added

Протестировал исправленный symexecute. Нашел 3 ошибки при исправлении которых тестовый пример начинает правильно доказываться.

1) Отсутствуют значения по умолчанию для CIA и SKIPOP. Для CIA оно должно задаваться через аргумент командной строки (по умолчанию можно взять 0). SKIPOP на текущий момент не используется в модели, однако из-за того, что солвер считает что его значение не определено он может поставить его в 1 и пропустить инструкцию. Вероятно в модели необходимо явно указать что это 0, однако я не могу понять как и где это сделать.

2) Переменные модели, которые сохраняют значения от инструкции к инструкции (такие как GPR CIA temp) порождают новые состояния только внутри одной инструкции, а при переходе к следующей их состояния переиспользуятся. Необходимо добавить порождение новых состояний на протяжении всей программы.

3) В инструкции powerpc addi некорректно смоделировалось присваивание переменной temp внутри инструкции if по обоим ветвям. При последующем использовании переменной temp используется её изначальное состояние, вместо модифицированного.

В перекреплённых файлах оригинальная версия smt и исправленная. Для проверки использовался cvc4.

Updated by Pavel Putro about 7 years ago

File storeload.bin.smt2 storeload.bin.smt2 added
File storeload.bin_fixed.smt2 storeload.bin_fixed.smt2 added
File storeload.bin storeload.bin added
File addsub.bin addsub.bin added
File addsub.bin.smt2 addsub.bin.smt2 added
File addsub.bin_fixed.smt2 addsub.bin_fixed.smt2 added
File abs_1.bin abs_1.bin added

Посмотрел исправленный вариант. С тестом 42.bin проблем больше нет.

Нашел ещё одну ошибку: при передачи регистров из одних функций другим внутри nml кода (к примеру в internal функции), Генерируется код передачи их по значениям вместо индексов. Это неверный подход, поскольку в таком случае вызываемая функция просто потеряет информацию о номере. Кроме того этот код никак не связывает значение регистра и его номер.

Для иллюстрации создал 2 теста:

1) addsub.bin (параметры r3 r4)

add r5, r3, r4
   subf r3, r0, r5
   r3 = r3 + r4 - r0

2) storeload.bin (параметры r1(stack) r3) (также проверяет взаимодействие с памятью, здесь проблем не обнаружено)

stw r3, -24(r1)
   xor r3, r3, r3
   lwz r3, -24(r1)
   r3=r3

Данные тесты параметризованы. Инициализация параметров (а также CIA) показана сразу после окончания декларации констант.
Также на всякий случай приложу тест с abs. Его отличие в том что его создал компилятор, по крайней мере там не должно быть unsat.

P.S. Для удобства отладки было бы неплохо отсортировать содержимое get-value и declare-const. Так удобнее будет отследить изменение состояния.

Updated by Artem Kotsynyak about 7 years ago

Pavel Putro wrote:

Посмотрел исправленный вариант. С тестом 42.bin проблем больше нет.

Нашел ещё одну ошибку: при передачи регистров из одних функций другим внутри nml кода (к примеру в internal функции), Генерируется код передачи их по значениям вместо индексов. Это неверный подход, поскольку в таком случае вызываемая функция просто потеряет информацию о номере. Кроме того этот код никак не связывает значение регистра и его номер.

Для иллюстрации создал 2 теста:

1) addsub.bin (параметры r3 r4)

add r5, r3, r4
subf r3, r0, r5
r3 = r3 + r4 - r0

2) storeload.bin (параметры r1(stack) r3) (также проверяет взаимодействие с памятью, здесь проблем не обнаружено)

stw r3, -24(r1)
xor r3, r3, r3
lwz r3, -24(r1)
r3=r3

Данные тесты параметризованы. Инициализация параметров (а также CIA) показана сразу после окончания декларации констант.
Также на всякий случай приложу тест с abs. Его отличие в том что его создал компилятор, по крайней мере там не должно быть unsat.

P.S. Для удобства отладки было бы неплохо отсортировать содержимое get-value и declare-const. Так удобнее будет отследить изменение состояния.

Вообще связывание есть, но оно косвенное:
1) для чтения

     (= op_0_instruction.operation.add_general_0.ra!1 op_0_instruction.operation.ra!1)
     (=
       (select GPR!1 op_0_instruction.operation.add_general_0.ra.i!1)
       __tmp_0!1
    )
     (= op_0_instruction.operation.add_general_0.ra!1 __tmp_0!1)

2) для записи

     (= op_0_instruction.operation.add_general_0.rd!1 op_0_instruction.operation.rd!1)
     (=
       GPR!2
       (store GPR!1 op_0_instruction.operation.add_general_0.rd.i!1 op_0_instruction.operation.add_general_0.rd.tmp_1!2)
    )
     (= op_0_instruction.operation.add_general_0.rd.tmp_1!2 __tmp_2!1)
     (= op_0_instruction.operation.add_general_0.rd!2 __tmp_2!1)

С другой стороны, вижу неполное описание при записи (регистр внутри функции после записи не связывается с регистром исходной функции), но пока не уверен, оказывает ли она какое-либо влияние: любое косвенное обращение через GPR последней версии всё равно остаётся корректным.

#12

Updated by Alexander Kamkin over 5 years ago

Category set to Symexecutor
Status changed from Feedback to Resolved
Target version set to 2.4
Published in build set to 2.4.46-beta-191025

#13

Updated by Alexander Kamkin over 5 years ago

Status changed from Resolved to Closed

Actions

Copy link

Also available in: Atom PDF

Project

General

Custom queries

Profile

MicroTESK

Bug #8486

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

Updated by Andrei Tatarnikov over 7 years ago

Updated by Andrei Tatarnikov about 7 years ago

Updated by Pavel Putro about 7 years ago

Updated by Andrei Tatarnikov about 7 years ago

Updated by Andrei Tatarnikov about 7 years ago

Updated by Andrei Tatarnikov about 7 years ago

Updated by Andrei Tatarnikov about 7 years ago

Updated by Pavel Putro about 7 years ago

Updated by Artem Kotsynyak about 7 years ago

Updated by Pavel Putro about 7 years ago

Updated by Artem Kotsynyak about 7 years ago

Updated by Alexander Kamkin over 5 years ago

Updated by Alexander Kamkin over 5 years ago