0

我想解决的公式在 C 中如下所示:

#define foo(w,x,y) ((((w)*(x)*(y)+31) & ~31) / 8)  
WORD w,x,y,z;  
y = 24;  
if( (foo(w,x,y) * z) == -1 )  
    printf("yeah!");  

我通过以下方式将其重写为 z3py:

from z3 import *
w= BitVec('w',16)
x= BitVec('x',16)
z= BitVec('z',16)
y= BitVecVal(24,16)
solve( (UDiv( (w*x*y+31) & ~31, 8 )) * z == 0xffffffff)

有什么建议么 ?
PS:请注意,尝试以这种形式求解公式:
solve( (UDiv( (w*x*y+31), 8 )) * z == 0xffffffff)
是可能的,所以我不能相信按位运算会导致这个公式无法满足。

4

2 回答 2

0

C 程序不会为我打印任何内容。Z3说“没有解决方案”。所以,是一致的。

您的 C 程序是否打印“是的!”?如果是这样,你不是在大端机器上吗?我在 x86 机器上试过你的例子。

于 2014-02-13T11:49:41.990 回答
0

我认为 Z3 的行为没有任何问题。为什么你认为公式应该是可满足的?

A = (w*x*y+31) & ~31 - 暗示最右边的 5 位将始终为零

B = UDiv( A & ~31, 8 ) (等于逻辑右移 3 位)——意味着最右边的 2 位将始终为零。

C = B * z - 这将始终有 2 个最右边的位为零

c == 0xffffffff - 这是不可能的

如果您将常数更改为 0xfffffffc,那么您将得到一个解决方案。

于 2014-02-13T13:24:18.967 回答