将单词转换为 Z3 中的字节集

Question

我运行下面的测试在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]

问题

由于 If 条件的设置方式，为什么 final(word) 取 2 的值，而它应该等同于 bytes(word)？

Answer 1

您在程序中使用数组作为 lambda。 Lambda 不是官方 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.

注意。这种 lambda 和数组的混合绝对是 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 的扩展。虽然这不是一件坏事，但要牢记这一点。

将单词转换为 Z3 中的字节集

Converting a word into set of bytes in Z3

python

z3

z3py