MicroTESK

Обнаружено 2 бага связанных с генерацией smt-lib формул. В приложенных файлах содержится бинарный код, некорректный и исправленный smt-lib код.
Для воспроизведения результатов в конец файлов были добавлены пред- и постусловия.

1. Ошибка связанная с трансляцией NML выражения (файл powerpc_mmu.nml строка 239):
   rd = zero_extend(WORD, temp64<31+8*zero_extend(card(6),temp_lo_index)..24+8*zero_extend(card(6),temp_lo_index)>
::temp64<23+8*zero_extend(card(6),temp_lo_index)..16+8*zero_extend(card(6),temp_lo_index)>
::temp64<15+8*zero_extend(card(6),temp_lo_index)..8+8*zero_extend(card(6),temp_lo_index)>
::temp64<7+8*zero_extend(card(6),temp_lo_index)..0+8*zero_extend(card(6),temp_lo_index)>);
   Данный код и ему подобный транслируются в SMT-LIB выражение (Строка 2321, встречается и в других местах):
   (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd!7 __tmp_33!1)
(=
((_ zero_extend 4) __tmp_33!1)
(concat
((_ extract
8
0)
(bvlshr
temp64!21
((_ zero_extend
58)
(bvadd
#b011000
(bvmul
#b001000
((_ zero_extend 3) temp_lo_index!3))))))
((_ extract
8
0)
(bvlshr
temp64!21
((_ zero_extend
58)
(bvadd
#b010000
(bvmul
#b001000
((_ zero_extend 3) temp_lo_index!3))))))
((_ extract
8
0)
(bvlshr
temp64!21
((_ zero_extend
58)
(bvadd
#b001000
(bvmul
#b001000
((_ zero_extend 3) temp_lo_index!3))))))
((_ extract
8
0)
(bvlshr
temp64!21
((_ zero_extend
58)
(bvadd
#b000000
(bvmul
#b001000
((_ zero_extend 3) temp_lo_index!3))))))))
   В данном выражении из 32-х битного числа выделяется по девять (вместо 8 бит), которые затем конкатинируются в 36-и битное число которое связывается с расширенным до 36-и бит результатом операции. В результате получается некорректное значение. Для исправления необходимо считывать по 8 бит (заменить (extract 8 0 ...) на (extract 7 0 ...) (строка 2242 в исправленной версии)), а также убрать излишнее расширение до 36 бит.
2. Вторая ошибка связанна с некорректным использованием состояний регистров и памяти при генерации формул и вероятно распространяется на всё сохраняемое состояние NML модели. Проявляется в:
   строке 1605:
   (store MEM!6 temp_address!2 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_4!2) (Использовать MEM!1 вместо MEM!6)
   строке 1639:
   (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_12!1 MEM!13 MEM!6) (Использовать MEM!1 вместо MEM!6)
   строке 2235:
   (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)
   и строке 2317:
   (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)
   Однако это не все ошибки, которые удалось найти, поскольку, если в добавочном коде исправить строку
   (assert (= (select GPR!1 (_ bv1 5)) (_ bv4096 32)))
   на строку
   (assert (= (select GPR!1 (_ bv1 5)) (_ bv4095 32)))
   с целью проверки пути при котором возникает переход через границу ячейки памяти, солвер выдаёт вердикт unsat даже без постусловия (помечено комментарием unsat) на результат.