为什么这个 z3 方程失败了? [英] Why this z3 equation is failing?

问题描述

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

I need to solve this code (the code in C)

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

这是我的python脚本

that's my python script

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] 附近，所以这里有什么问题?

I know the solution should be around [42,38,40], so what's wrong here ?

推荐答案

这个表达式:

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

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

Is always equivalent to 0. If you right shift a 64-bit quantity to the right by 64 bits, you get 0. (Note that you are using LShr, which treats its input as an unsigned quantity.)

因此，整个过程简化为解决 len_input_serial == 14，这是 Z3 产生的答案.

Therefore the whole thing simplifies to solving len_input_serial == 14, which is the answer Z3 is producing.

请注意，当您在 Python 中编写一个长整数(即 0x123L 等)时，您将获得无限精度.(参见此处:长整数的最大值).在 C 中，你得到(最有可能的)64 位整数.因此，您的 Z3 代码实际上是正确的；是 Python 在这里使用了更高的精度，因此造成了混乱.

Note that when you write a long integer in Python (i.e., 0x123L etc.), you get infinite precision. (See here: Maximum value for long integer). In C, you get (most-likely) 64-bit integer. So, your Z3 code is actually correct; it's Python that's using a bigger precision here and thus causing the confusion.

这篇关于为什么这个 z3 方程失败了?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！