math - 为什么 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)。