（Z3Py）BitVec類型轉換，「那種不匹配」錯誤

Question

我試圖連接兩個8位字節和一個16字：

from z3 import * 

byte1 = BitVec('byte1', 8) 
byte2 = BitVec('byte2', 8) 
word = BitVec('word', 16) 
s = Solver() 
s.add(word==(byte1<<8) | byte2) 

但我發現了錯誤：

WARNING: invalid function application, sort mismatch on argument at position 2 
WARNING: (define = (bv 16) (bv 16) Bool) applied to: 
word of sort (bv 16) 
(bvor (bvshl byte1 bv[8:8]) byte2) of sort (bv 8) 
... 
z3types.Z3Exception: 'type error' 

什麼是正確的方法來做到這一點？

Answer 1

您需要使用符號或零擴展名來修改類型錯誤，方法是更改​​表達式中的位數。對於每個文檔分別是：

http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.html#-SignExt

http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.html#-ZeroExt

例如（rise4fun鏈路：http://rise4fun.com/Z3Py/872）：

byte1 = BitVec('byte1', 8) 
byte2 = BitVec('byte2', 8) 
word = BitVec('word', 16) 
s = Solver() 
Pz = word == (ZeroExt(8, byte1) <<8) | (ZeroExt(8, byte2)) 
Ps = word == (SignExt(8, byte1) <<8) | (SignExt(8, byte2)) 
print Pz 
print Ps 
s.add(Pz) 
s.add(Ps) 
s.add(word == 0xffff) 
print s 
print s.check() 
print s.model() # word is 65535, each byte is 255