爲什麼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開發人員可以對此進行評論嗎？）