使用 Python Z3,我有一个字节数组,可以使用 Select 读取 1 个字节,如下所示。
MI = BitVecSort(32)
MV = BitVecSort(8)
Mem = Array('Mem', MI, MV)
pmt = BitVec('pmt', 32)
pmt2 = BitVec('pmt2', 8)
g = True
g = And(g, pmt2 == Select(Mem, pmt))
到目前为止,这没问题。但是,现在我想从 Mem 数组中读取 4 个字节,如下所示。
t3 = BitVec('t3', 32)
g = And(g, t3 == Select(Mem, pmt))
事实证明这是错误的,因为 t3 是 32 位的,而不是 8 位的,而 Mem 是 8 位的数组。
问题是:如何使用Select读出4个字节,而不是上面例子中的1个字节?
我想我可以创建一个新函数来读出 4 个字节,比方说 Select4(),但我不确定如何在 Z3 python 中创建一个函数。
非常感谢!
我们可以将Select4
定义为
def Select4(M, I):
return Concat(Select(M, I + 3), Select(M, I + 2), Select(M, I+1), Select(M, I))
Concat
操作本质上是附加四个位向量。 Z3 还支持Extract
操作。这两个操作可用于对 C 等编程语言中可用的转换操作进行编码。
这是完整的示例(也可在线获得 here ):
MI = BitVecSort(32)
MV = BitVecSort(8)
Mem = Array('Mem', MI, MV)
pmt = BitVec('pmt', 32)
pmt2 = BitVec('pmt2', 8)
def Select4(M, I):
return Concat(Select(M, I + 3), Select(M, I + 2), Select(M, I+1), Select(M, I))
g = True
g = And(g, pmt2 == Select(Mem, pmt))
t3 = BitVec('t3', 32)
g = And(g, t3 == Select4(Mem, pmt))
solve(g, pmt2 > 10)
我是一名优秀的程序员,十分优秀!