当我输入正确时，为什么 Z3 说这个方程是不可满足的？

Question

给定一个简单的移位和异或运算，其中“输入”是符号：

input    = BitVec('input',32)
feedback = 0x8049d30
shiftreg = input ^ feedback
shiftreg = 0xffffffff & ((shiftreg << 8) | (shiftreg >> 24))
shiftreg = shiftreg ^ 0xcafebabe

s = Solver()
s.add(shiftreg == 0x804a008)
s.check()
# unsat

我们被告知这个方程是不可解的。如果打印，s包含：

[4294967295 &
 ((input ^ 134520112) << 8 | (input ^ 134520112) >> 24) ^
 3405691582 ==
 134520840]

但是，我可以轻松地创建一个示例来解决“输入”的这个方程。

want = 0x804a008
want ^= 0xcafebabe
want = 0xffffffff & ((want >> 8) | (want << 24))
want ^= 0x8049d30
print hex(want)
# 0xbec6672a

将我们的解决方案输入到 Z3 方程中，我们看到我们可以满足它。

input = 0xbec6672a
[4294967295 &
 ((input ^ 134520112) << 8 | (input ^ 134520112) >> 24) ^
 3405691582 ==
 134520840]
# True

为什么Z3找不到这个解决方案？

Answer 1

事实证明，在 Z3 中，移位运算符是算术移位而不是逻辑移位。

这意味着右移>>用符号位填充，而不是用零填充。

您必须使用逻辑右移 ( LShR) 函数才能获得正常行为。

input    = BitVec('input',32)
feedback = 0x8049d30
shiftreg = input ^ feedback
shiftreg = (shiftreg << 8) | LShR(shiftreg, 24)
shiftreg = shiftreg ^ 0xcafebabe

s = Solver()
s.add(shiftreg == 0x804a008)
s.check()
hex(s.model()[input].as_long())
# 0xbec6672a

在这个特定的例子中，移位操作实际上是一个旋转。Z3 有一个直接进行旋转的机制（在这种情况下，它将是RotateLeft(shiftreg, 8).