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

Answer 2

我相信“（shiftreg >> 24）”被解释为算术右移在Z3的Python API：http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.html（见RSHIFT）。我想你期待一个逻辑右移。首先，让我们重新编码成SMT2这一点。

(declare-fun input() (_ BitVec 32)) 
(define-fun feedback() (_ BitVec 32) #x08049d30) 
(define-fun shiftreg0() (_ BitVec 32) 
    (bvxor feedback input)) 
(define-fun shiftreg1() (_ BitVec 32) 
    (bvand #xffffffff 
     (bvor (bvshl shiftreg0 #x00000008) 
       (bvlshr shiftreg0 #x00000018)))) 
(define-fun shiftreg2() (_ BitVec 32) 
    (bvxor shiftreg1 #xcafebabe)) 

(assert (= shiftreg2 #x0804a008)) 
(check-sat) 

我们可以检查，这确实是使用你喜欢的QFBV解算器（Z3，cvc4等坐）。它是坐着的，坐在“（= input＃xbec6672a）”的位置，现在改变“（bvlshr shiftreg0＃x00000018）”到“（bvashr shiftreg0＃x00000018）”。让我们来看一下shiftreg0的最高位是否为1下面的说法确实使问题不成立。

(assert (not (= ((_ extract 31 31) shiftreg0) #b1))) 

因此我们知道“（bvashr shiftreg0＃x00000018）”将被迫在1秒转移的前24位。因此我们知道bvlshr和bvashr在这个例子中必须有不同的表现。

至于为什么最终评价是真的，我只能猜测。 （我怀疑z3无法推断python界面中所有常量运算符的宽度，并且在内部有一个0在挂起33位宽的常量，这个Z3开发人员可以对此进行评论吗？）