Project

General

Profile

Bug #9364

Некорректная генерация smt-lib формул

Added by Pavel Putro about 1 month ago. Updated 22 days ago.

Status:
Open
Priority:
Urgent
Category:
-
Target version:
-
Start date:
11/06/2018
Due date:
% Done:

0%

Estimated time:
Detected in build:
svn
Platform:
Published in build:

Description

Обнаружено 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) на результат.
storeload.bin (12 Bytes) storeload.bin Бинарный код Pavel Putro, 11/06/2018 01:34 PM
storeload.bin.smt2 (147 KB) storeload.bin.smt2 smt-lib некорректный Pavel Putro, 11/06/2018 01:34 PM
storeload.bin_fixed_partial.smt2 (147 KB) storeload.bin_fixed_partial.smt2 smt-lib частично исправленный Pavel Putro, 11/06/2018 01:34 PM
storeload.s (47 Bytes) storeload.s Код ассемблера Pavel Putro, 11/06/2018 01:36 PM

History

#1 Updated by Alexander Kamkin 22 days ago

  • Assignee set to Artem Kotsynyak
  • Status changed from New to Open

Also available in: Atom PDF