(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