Project

General

Profile

Actions
Copy link

Bug #8486

closed

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

Added by Pavel Putro over 6 years ago. Updated over 4 years ago.

Status:
Closed
Priority:
Urgent
Assignee:
Pavel Putro
Category:
Symexecutor
Target version:
2.4
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

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
Actions
Copy link
 #1

Updated by Andrei Tatarnikov over 6 years ago

  • Assignee set to Artem Kotsynyak
  • Priority changed from Normal to Urgent
Actions
Copy link
 #2

Updated by Andrei Tatarnikov over 6 years ago

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

Павел, я включил константы и номера регистров в формулу. Посмотрите. Так лучше? Этого достаточно?

Actions
Copy link Download all files
 #3

Updated by Pavel Putro over 6 years ago

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

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

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

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

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

Actions
Copy link
 #4

Updated by Andrei Tatarnikov about 6 years ago

Убрал SKIPOP из спецификации за ненадобностью.

Actions
Copy link
 #5

Updated by Andrei Tatarnikov about 6 years ago

Сделал формат SMT-файлов читаемым (выражения выводятся в столбик) для упрощения отладки.

Actions
Copy link
 #6

Updated by Andrei Tatarnikov about 6 years ago

Исправил проблему 2: a6523de

Actions
Copy link
 #7

Updated by Andrei Tatarnikov about 6 years ago

Проблема 3 тоже вроде не наблюдается больше.

Actions
Copy link Download all files
 #8

Updated by Pavel Putro about 6 years ago

Посмотрел исправленный вариант. С тестом 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. Так удобнее будет отследить изменение состояния.

Actions
Copy link
 #9

Updated by Artem Kotsynyak about 6 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 последней версии всё равно остаётся корректным.

Actions
Copy link
 #10

Updated by Pavel Putro about 6 years ago

По вашему примеру:
Константа op_0_instruction.operation.ra!1 более нигде не используется и её значение неизвестно в момент связывания. Вместо неё инициализируется константа op_0_instruction.operation.ra.i!1 (как аргумент операции add), однако она также нигде не используется. Из-за отсутствия связывания индексов регистров между внутренней функцией и обёрткой, солвер не понимает к какому регистру в gpr обращается внутренняя функция. В исправленной версии в GPR r3 в итоге записывается сумма r4 и r3, чего не происходит в оригинальной.

Actions
Copy link
 #11

Updated by Artem Kotsynyak about 6 years ago

Pavel Putro wrote:

По вашему примеру:
Константа op_0_instruction.operation.ra!1 более нигде не используется и её значение неизвестно в момент связывания. Вместо неё инициализируется константа op_0_instruction.operation.ra.i!1 (как аргумент операции add), однако она также нигде не используется. Из-за отсутствия связывания индексов регистров между внутренней функцией и обёрткой, солвер не понимает к какому регистру в gpr обращается внутренняя функция. В исправленной версии в GPR r3 в итоге записывается сумма r4 и r3, чего не происходит в оригинальной.

Исправлено в ef75731c.

Actions
Copy link
 #12

Updated by Alexander Kamkin over 4 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
Actions
Copy link
 #13

Updated by Alexander Kamkin over 4 years ago

  • Status changed from Resolved to Closed
Actions
Copy link

Also available in: Atom PDF