Open-Source Projects: Issueshttps://forge.ispras.ru/https://forge.ispras.ru/favicon.ico?16490126692021-03-23T13:17:44ZOpen-Source Projects
Redmine MicroTESK - Task #10764 (New): Поддержка алтернативного формата вывода SMT-LIB представления маши...https://forge.ispras.ru/issues/107642021-03-23T13:17:44ZPavel Putropavel.putro@ispras.ru
Для использования в рамках задачи SyGuS необходима поддержка формата вывода базовых блоков машинного кода в виде единых функций. Данные функции должны принимать на вход и возвращать единственный параметр типа State, представляющий текущее состояние машины (регистры + память). Тип State должен вычисляться путём анализа NML модели и иметь единый формат для всех базовых блоков.<br />Тип State должен включать:
<ol>
<li>регистры общего назначения</li>
<li>массив памяти</li>
<li>регистры специального назначения</li>
<li>Флаги (если не встроены в регистры специального назначения)</li>
<li>Отдельный булевый параметр - условие перехода.</li>
</ol>
Тип State не должен включать
<ol>
<li>временные переменные типа tmp_dword и т. п.</li>
<li>безымянные промежуточные значения типа %123</li>
</ol>
<p>Пример определения типа State на SMT-LIB:<br /><pre>
(declare-datatypes ((State 0))
(((cons (XREG (Array (_ BitVec 5) (_ BitVec 32))) (MEM (Array (_ BitVec 32) (_ BitVec 8))) (zf Bool) (sf Bool) (jc Bool)))))
</pre><br />Для удобства использования типа State и сокращения объёма генерируемого кода желательно определить аксессоры для записи и чтения данных:</p>
<pre>
(define-fun get_reg ((s State) (r (_ BitVec 5))) (_ BitVec 32) (select (XREG s) r))
(define-fun set_reg ((s State) (r (_ BitVec 5)) (v (_ BitVec 32))) State (cons (store (XREG s) r v) (MEM s) (zf s) (sf s) (jc s)))
(define-fun get_mem ((s State) (r (_ BitVec 5))) (_ BitVec 8) (select (MEM s) (get_reg s r)))
(define-fun set_mem ((s State) (r (_ BitVec 5)) (v (_ BitVec 8))) State (cons (XREG s) (store (MEM s) (get_reg s r) v) (zf s) (sf s) (jc s)))
</pre>
<p>Сама функция в таком случае может быть реализована через цепочку let-выражений в виде:<br /><pre>
(define-fun memset-O1_block_2 ((s State)) State
(let ((s1 (set_mem s (_ bv10 5) ((_ extract 7 0) (get_reg s (_ bv11 5))))))
(let ((s2 (set_reg s1 (_ bv12 5) (bvsub (get_reg s1 (_ bv12 5)) (_ bv1 32)))))
(let ((s3 (set_reg s2 (_ bv14 5) (bvadd (get_reg s2 (_ bv14 5)) (_ bv1 32)))))
s3))))
</pre><br />Стоит также заметить, что в формате генерации функции по базовому блоку, а не по каждой конкретной инструкции отдельно, остаётся возможным применять оптимизации, используемые в текущем представлении модели.</p> MicroTESK - Bug #10566 (New): Отсутствует поддержка тернарного оператора в mirhttps://forge.ispras.ru/issues/105662020-11-10T09:06:12ZPavel Putropavel.putro@ispras.ru
<p>Наличие тернарного оператора в NML модели приводит к падению при выполнении команды symexecute.</p> MicroTESK - Bug #9843 (Closed): MicroTESK версии mir игнорирует параметр binary-file-use-big-endianhttps://forge.ispras.ru/issues/98432019-10-01T21:46:03ZPavel Putropavel.putro@ispras.ru
<p>В файле etc/settings.xml присутствует параметр binary-file-use-big-endian, который корректно обрабатывается основной версией инструмента, однако игнорируется версией mir.</p>
<p>Кроме того расположение этого параметра в файле глобальных настроек некорректно - такой параметр различается для каждой модели процессора и должен располагаться в файле параметров модели.</p> MicroTESK - Bug #9787 (Closed): Некорректное восстановление 64-х битных чисел из памяти.https://forge.ispras.ru/issues/97872019-08-12T19:40:00ZPavel Putropavel.putro@ispras.ru
<p>Для примера была использована модель risc-v 64-bit. В архиве содержится бинарный и ассемблерный код функции size_test, которая принимает параметром аргумент типа size_t (64-bit) и его же возвращает в качестве результата. Также приложен вывод функции symexecute - smt-lib код. В подпапке size_test_merged содержатся два smt-lib файла, block_0_target_0.smt2 и block_0_target_0_fixed.smt2, в которых к коду функций была добавлена цель верификации, при этом в файле _fixed ошибка исправлена (получен вердикт unsat).<br />Суть ошибки:<br />Ошибка возникает при загрузке из памяти 64-х битных чисел больших, чем 2^32-1. В ассемблерном файле строка 5, <br />в nml представлении:</p>
<p>tmp_dword<63..32> = MEM[mem_index + 1];<br />tmp_dword<31..0> = MEM[mem_index];</p>
<p>В smt-lib представлении (block_0_target_0.smt2 строки ~ с 1244 по 1263) с комментариями: <br /><pre>
(assert
(=
%158
(select MEM!25 %157))) ; <--- загрузка из памяти старших 4-х байт числа.
(assert
(=
%160 ; <--- знаковое расширение до 64 битов. в данном случае ошибка не возникает из-за сдвига,
((_ sign_extend 32) %158))) ; однако несколько некорректно - лучше заменить на беззнаковое.
(assert
(=
%161
(bvand tmp_dword!1 #b0000000000000000000000000000000000000000000000000000000000000000))) ; <--- операция не имеет ?? смысла и не влияет на итоговый результат
(assert
(=
%162
(bvshl %160 #b0000000000000000000000000000000000000000000000000000000000100000))) ; <--- побитовый сдвиг на 32
(assert
(=
%159
(bvor %161 %162))) ; <--- склейка частей, а по факту одной части и ноля
(assert
(= tmp_dword!2 %159))
(assert
(=
%163
(select MEM!25 %154))) ; <--- загрузка младших 4-х байт числа.
(assert
(=
%165
((_ sign_extend 32) %163))) ; <--- знаковое расширение числа. Впоследствии приводит к ошибке при склейке частей. Необходимо заменить на беззнаковое.
(assert
(= ; <--- а здесь главная ошибка - некорректная битовая маска приводит к занулению
%166 ; ранее подготовленных старших 4-х байт числа. корректная маска содержи 32 единицы
(bvand %159 #b0000000000000000000000000000000000000000000000000000000000000000))) ; в старших битах.
(assert
(=
%167
(bvshl %165 #b0000000000000000000000000000000000000000000000000000000000000000))) ; <--- сдвиг на 0.
(assert
(=
%164
(bvor %166 %167))) <--- итоговая склейка двух половин числа
</pre></p> MicroTESK - Bug #9395 (Closed): Symexecute не учитывает неявные преобразования типов в nml моделяхhttps://forge.ispras.ru/issues/93952018-11-22T11:39:22ZPavel Putropavel.putro@ispras.ru
<p>В модели RISC-V в массив памяти с 62-х битным индексом производится запись по индексу размерностью 64 бит, что обрабатывается MicroTESK при компиляции и генерации модели, однако Symexecute не учитывает то, что smt-lib таких неявных преобразований не позволяет. Пример из файла riscv_rv32i.nml (строка 350).</p>
<p>tmp_index = tmp_address >> 2;</p>
<p>if tmp_address<1..0> == 0 then // Word-aligned address<br /> tmp_word = MEM[tmp_index];</p>
<p>Генерация smt по данному коду приводит к ошибке солвера:<br />(error "array select not indexed with correct type for array")</p>
<p>На всякий случай прикладываю бинарный код.</p> MicroTESK - Bug #9364 (Closed): Некорректная генерация smt-lib формулhttps://forge.ispras.ru/issues/93642018-11-06T10:38:04ZPavel Putropavel.putro@ispras.ru
<p>Обнаружено 2 бага связанных с генерацией smt-lib формул. В приложенных файлах содержится бинарный код, некорректный и исправленный smt-lib код.<br />Для воспроизведения результатов в конец файлов были добавлены пред- и постусловия.</p>
<ol>
<li>Ошибка связанная с трансляцией NML выражения (файл powerpc_mmu.nml строка 239):<br /><code>rd = zero_extend(WORD, temp64<31+8*zero_extend(card(6),temp_lo_index)..24+8*zero_extend(card(6),temp_lo_index)><br /> ::temp64<23+8*zero_extend(card(6),temp_lo_index)..16+8*zero_extend(card(6),temp_lo_index)><br /> ::temp64<15+8*zero_extend(card(6),temp_lo_index)..8+8*zero_extend(card(6),temp_lo_index)><br /> ::temp64<7+8*zero_extend(card(6),temp_lo_index)..0+8*zero_extend(card(6),temp_lo_index)>);</code><br />Данный код и ему подобный транслируются в SMT-LIB выражение (Строка 2321, встречается и в других местах):<br /><code>(= op_2_instruction.operation.load_general_0.powerpc_load_0.rd!7 __tmp_33!1)<br /> (=<br /> ((_ zero_extend 4) __tmp_33!1)<br /> (concat<br /> ((_ extract<br /> 8<br /> 0)<br /> (bvlshr<br /> temp64!21<br /> ((_ zero_extend<br /> 58)<br /> (bvadd<br /> #b011000<br /> (bvmul<br /> #b001000<br /> ((_ zero_extend 3) temp_lo_index!3))))))<br /> ((_ extract<br /> 8<br /> 0)<br /> (bvlshr<br /> temp64!21<br /> ((_ zero_extend<br /> 58)<br /> (bvadd<br /> #b010000<br /> (bvmul<br /> #b001000<br /> ((_ zero_extend 3) temp_lo_index!3))))))<br /> ((_ extract<br /> 8<br /> 0)<br /> (bvlshr<br /> temp64!21<br /> ((_ zero_extend<br /> 58)<br /> (bvadd<br /> #b001000<br /> (bvmul<br /> #b001000<br /> ((_ zero_extend 3) temp_lo_index!3))))))<br /> ((_ extract<br /> 8<br /> 0)<br /> (bvlshr<br /> temp64!21<br /> ((_ zero_extend<br /> 58)<br /> (bvadd<br /> #b000000<br /> (bvmul<br /> #b001000<br /> ((_ zero_extend 3) temp_lo_index!3))))))))</code><br />В данном выражении из 32-х битного числа выделяется по девять (вместо 8 бит), которые затем конкатинируются в 36-и битное число которое связывается с расширенным до 36-и бит результатом операции. В результате получается некорректное значение. Для исправления необходимо считывать по 8 бит (заменить (extract 8 0 ...) на (extract 7 0 ...) (строка 2242 в исправленной версии)), а также убрать излишнее расширение до 36 бит.</li>
<li>Вторая ошибка связанна с некорректным использованием состояний регистров и памяти при генерации формул и вероятно распространяется на всё сохраняемое состояние NML модели. Проявляется в: <br />строке 1605:<br />(store MEM!6 temp_address!2 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_4!2) (Использовать MEM!1 вместо MEM!6)<br />строке 1639:<br />(ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_12!1 MEM!13 MEM!6) (Использовать MEM!1 вместо MEM!6)<br />строке 2235:<br />(store GPR!8 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.i!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!6) (Использовать GPR!4 вместо GPR!8)<br />и строке 2317:<br />(store GPR!8 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.i!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!7) (Использовать GPR!4 вместо GPR!8)<br />Однако это не все ошибки, которые удалось найти, поскольку, если в добавочном коде исправить строку<br />(assert (= (select GPR!1 (_ bv1 5)) (_ bv4096 32)))<br />на строку<br />(assert (= (select GPR!1 (_ bv1 5)) (_ bv4095 32)))<br />с целью проверки пути при котором возникает переход через границу ячейки памяти, солвер выдаёт вердикт unsat даже без постусловия (помечено комментарием unsat) на результат.</li>
</ol> MicroTESK - Bug #8486 (Closed): Отсутствие связывания констант в smt формулах, генерируемых на ос...https://forge.ispras.ru/issues/84862017-10-06T20:31:49ZPavel Putropavel.putro@ispras.ru
<p>Насколько мне удалось проанализировать: в текущей генерируемой модели отсутствует связывание между собой констант для разных инструкций. Иными словами, если существуют две инструкции (процессор PowerPC):<br />addi r3, r0, 17;<br />addi r3, r3, 25;<br />Из модели нельзя понять что в обоих инструкциях используется регистр r3. Похожая ситуация скорее всего и с памятью т.к. значения аргументов инструкций игнорируется, будь то номер регистра или иная константа. И даже если вручную прописать все эти значения (добавить соответствующий assert) модель всё равно будет содержать неопределённость, что указывает на то, что игнорируется также часть констант из модели. На основе описанных выше инструкций мной был составлен тест для модели PowerPC (приложен в файле 42.bin). Если модель будет сгенерированна правильно, то значение GPR [3] должно будет всегда равняться 42, т.е. smt-решатель (я использовал cvc4 и z3) не сможет доказать обратного (здесь надо сделать оговорку: поскольку значение CIA (Program Counter) явно не задаётся, а определяется тестовым шаблоном, решатель попытался присвоить ему значение равное 2^64, после чего решение потеряло смысл. Следовательно при генерации его возможно также следует задавать более явно).<br />Предлагаю использовать данный тест для первоначальной проверки корректности будущих версий генератора.<br />На всякий случай прикладываю сгенерированный smt.</p>
<p>Также напоминаю что файл маппинга smt переменных на регистры и память всё ещё не генерируется.</p> MicroTESK for PowerPC - Bug #7775 (Closed): Описание MMU инструкцийhttps://forge.ispras.ru/issues/77752016-12-01T16:42:02ZPavel Putropavel.putro@ispras.ru
<p>В описание mmu инструкций (powerpc_mmu.nml) используются имена sw и lw, которых я не нашел ни в одном мануале. При этом инструкция lw, представляющая собой инструкцию lwa, вообще недоступна на х32 процессорах, в том числе на E500MC.<br />Надо ли оставить/переделать/заменить эти инструкции?</p> MicroTESK for PowerPC - Task #7743 (Closed): Коммит 905af510: Sub instruction addedhttps://forge.ispras.ru/issues/77432016-11-21T09:47:59ZPavel Putropavel.putro@ispras.ru
<p>Добавил описание инструкций subf и subf., однако не под своим именем, т.к. гит был настроен на старый проект. Также заметил что из комментариев пропали все специальные символы такие как ← и.т.д., хотя в файле перед отправкой они были. Прошу проверить правильность описания инструкции и сообщить если есть какие-то проблемы. У меня тесты выполняются без ошибок.</p> MicroTESK for PowerPC - Bug #7719 (Closed): Ошибка при попытке запуска тестовых шаблоновhttps://forge.ispras.ru/issues/77192016-11-11T19:00:59ZPavel Putropavel.putro@ispras.ru
<p>При попытке запуска любого из тестовых шаблонов выдаёт сообщение об ошибке. Модель генерируется без ошибок. Используется ОС windows 10 и java 8 (7 версия недоступна в открытом доступе).</p>
<p>Текст ошибки:</p>
<pre>
D:\work\microtesk\microtesk\arch\powerpc\templates>generate powerpc instruction_alu.rb
D:\work\microtesk\microtesk\arch\powerpc\templates>java -ea -jar "D:\work\microtesk\microtesk/lib/jars/microtesk.jar" -g powerpc instruction_alu.rb
Loaded template PowerPCBaseTemplate defined in D:/work/microtesk/microtesk/arch/powerpc/templates/powerpc_base.rb
Loaded template InstructionALU defined in D:/work/microtesk/microtesk/arch/powerpc/templates/instruction_alu.rb
Processing template InstructionALU defined in D:/work/microtesk/microtesk/arch/powerpc/templates/instruction_alu.rb...
Instance number: 1
Error: Failed to load the ru.ispras.microtesk.model.powerpc.mmu.sim.Model class from D:\work\microtesk\microtesk\lib\jars\models.jar. Reason: ru.ispras.microtesk.model.powerpc.mmu.sim.Model
********************************************************************************
ATTENTION! An unexpected error has occurred:
java.lang.IllegalArgumentException: Settings were not loaded.
The program will be terminated. Please contact us at:
microtesk-support@ispras.ru
We are sorry for the inconvenience.
Exception stack:
java.lang.IllegalArgumentException: Settings were not loaded.
at ru.ispras.fortress.util.InvariantChecks.checkTrue(ru/ispras/fortress/util/InvariantChecks.java:53)
at ru.ispras.fortress.util.InvariantChecks.checkNotNull(ru/ispras/fortress/util/InvariantChecks.java:107)
at ru.ispras.microtesk.test.sequence.engine.EngineContext.<init>(ru/ispras/microtesk/test/sequence/engine/EngineContext.java:69)
at ru.ispras.microtesk.test.TestEngine.newTemplate(ru/ispras/microtesk/test/TestEngine.java:218)
at RUBY.generate(D:/work/microtesk/microtesk/lib/ruby/template.rb:915)
at RUBY.main(D:\work\microtesk\microtesk/lib/ruby/microtesk.rb:35)
at org.jruby.RubyHash.each(org/jruby/RubyHash.java:1342)
at RUBY.main(D:\work\microtesk\microtesk/lib/ruby/microtesk.rb:31)
at RUBY.(root)(D:\work\microtesk\microtesk/lib/ruby/microtesk.rb:54)
at ru.ispras.microtesk.test.TestEngine.processTemplate(ru/ispras/microtesk/test/TestEngine.java:169)
at ru.ispras.microtesk.test.TestEngine.generate(ru/ispras/microtesk/test/TestEngine.java:158)
at ru.ispras.microtesk.MicroTESK.generate(ru/ispras/microtesk/MicroTESK.java:200)
at ru.ispras.microtesk.MicroTESK.main(ru/ispras/microtesk/MicroTESK.java:70)
********************************************************************************
</pre>