Преобразование слова в набор байтов в Z3 - PullRequest
Новая
       9

Преобразование слова в набор байтов в Z3

0 голосов
/ 19 февраля 2019

Я выполняю следующий тест в Z3 / Python: 

def test_converting_word_into_byte_array():
    bytes_in_word = 4
    word_size = 8 * bytes_in_word
    word = BitVec('word', word_size)
    word_in_bytes = Array('bytes(word)', BitVecSort(word_size), BitVecSort(8))
    read = BitVec('read', word_size)
    pointer = BitVecVal(0, word_size)
    answer_array = Array('final(word)', BitVecSort(word_size), BitVecSort(8))

    solver = Solver()
    solver.add(word == BitVecVal(2, word_size))
    for byte in range(bytes_in_word):
        solver.add(Select(word_in_bytes, byte) == Extract(word_size - 1 - 8 * byte, word_size - 1 - 7 - 8 * byte, word))
    new_array = Lambda([read],
        If(
            And(ULE(pointer, read), ULE(read, pointer + bytes_in_word - 1)),
            Select(word_in_bytes, read - pointer),
            Select(K(BitVecSort(word_size), BitVecVal(0, 8)), read)))
    solver.add(answer_array == new_array)

    assert str(solver.check()) == "sat"
    print(solver.model())

Хотя решение удовлетворительное, в конечном итоге модель решателя кажется неправильной: 

[final(word) = Lambda(k!0, 2),
 bytes(word) = Lambda(k!0, If(k!0 == 3, 2, 0)),
 word = 2]

Вопрос

Почему final(word) принимает значение 2, когда оно должно быть эквивалентно bytes(word) из-за того, как установлено условие If?

1 Ответ

0 голосов
/ 20 февраля 2019

Вы используете массивы как лямбды в вашей программе.Лямбда не является частью официального языка SMTLib, (http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf),, поэтому трудно точно сказать, должно ли это быть разрешено и каковы будут последствия. Но, как вы выяснили, это кажетсябыть поддерживаемым расширением z3, и вы обнаружили ошибку!

Пожалуйста, сообщите об этом на их проблемном сайте: https://github.com/Z3Prover/z3/issues.

Примечание. Кодировка Python действительно устраняет проблему и делает еедействительно трудно читать. Вот что мне удалось создать как гораздо более простой для чтения тест SMTLib: 

(set-logic ALL)

(declare-fun inp () (Array Int Int))
(declare-fun out () (Array Int Int))

(assert (= (select inp 0) 0))
(assert (= (select inp 1) 0))
(assert (= (select inp 2) 1))

(assert (= out (lambda ((i Int))
                       (ite (and (<= 0 i) (<= i 2))
                            (select inp i)
                            0))))

(check-sat)

(get-value ((select inp 0)))
(get-value ((select inp 1)))
(get-value ((select inp 2)))
(get-value ((select out 0)))
(get-value ((select out 1)))
(get-value ((select out 2)))

Для этого z3 сообщает: 

sat
(((select inp 0) 0))
(((select inp 1) 0))
(((select inp 2) 1))
(((select out 0) 2))
(((select out 1) 2))
(((select out 2) 2))

Но ясно, что мыожидаем эквивалентности в диапазоне 0-2. Я настоятельно рекомендую вам сообщить об этой версии проблемы SMTLib вместо исходного Python.

NB. Такое смешивание лямбда-выражений и массивов определенно является расширением Z3.Например, вот что CVC4 говорит в тесте: 

(error "Subexpressions must have a common base type:
Equation: (= out (lambda ((i Int)) (ite (and (<= 0 i) (<= i 2)) (select inp i) 0)))
Type 1: (Array Int Int)
Type 2: (-> Int Int)
")

Итак, вы используете расширение, специфичное для z3. Хотя это и неплохо, об этом следует помнить.

...