python - 为什么这个 z3 方程失败了？

Question

我需要解决这段代码(C 中的代码)

if ( ((0xAAAAAAAAAAAAAAABLL * len_input_serial >> 64) >> 1)+ len_input_serial- 3 * ((0xAAAAAAAAAAAAAAABLL * len_input_serial >> 64) >> 1) != 14)
    return 0xFFFFFFFFLL;

这是我的 python 脚本

from z3 import *
len_input_serial = BitVec("serial_len",64)
solve(LShR(LShR(0xAAAAAAAAAAAAAAABL * len_input_serial,64),1) + len_input_serial - 3 * LShR(LShR(0xAAAAAAAAAAAAAAABL * len_input_serial,64),1) == 14)

但是这给了我[serial_len = 14]

我知道解决方案应该在 [42,38,40] 附近，那么这里出了什么问题？

Answer 1

这个表达式:

(0xAAAAAAAAAAAAAAABLL * len_input_serial >> 64) >> 1

始终等于0。如果将 64 位数量右移 64 位，则会得到 0。(请注意，您使用的是 LShr，它将其输入视为无符号数量。)

因此，整个事情简化为求解 len_input_serial == 14，这就是 Z3 产生的答案。

请注意，当您在 Python 中编写长整数(即 0x123L 等)时，您将获得无限精度。 (参见此处:Maximum value for long integer)。在 C 中，您(最有可能)得到 64 位整数。所以，你的 Z3 代码实际上是正确的；是 Python 在这里使用了更大的精度，从而导致了困惑。