我需要解这个代码(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]
左右,那么这里出了什么问题?你知道吗
此表达式:
总是等价于
0
。如果将64位量右移64位,则得到0。(请注意,您使用的是LShr
,它将其输入视为无符号量。)因此,整个过程简化为求解
len_input_serial == 14
,这就是Z3产生的答案。你知道吗请注意,在Python中编写长整数(即0x123L等)时,可以获得无限精度。(参见此处:Maximum value for long integer)。在C语言中,很可能是64位整数。因此,您的Z3代码实际上是正确的;是Python在这里使用了更高的精度,因此造成了混乱。你知道吗
相关问题 更多 >
编程相关推荐