python - 使用固定字符在 Z3 中定义位向量

Question

我们能否在 Z3 中定义输入 BitVec()，以便我们知道输入的一部分以及我们希望 Z3 解决的另一部分？

作为示例，在下面的代码中，我定义了一个位向量来表示 10 个字符的字符串。

from z3 import *

s = Solver()

input = [BitVec("input%s" % i, 8) for i in range(10)]

s.add(gen(input) == 0xAABBCCDD)

在上面的示例中，gen() 是一个使用输入生成 DWORD 的函数。

现在，假设我已经知道输入的前几个字符。例如，输入始终采用以下格式:CHECKXXXXX

其中，X是未知字符。

现在如何定义 Z3 中的输入以利用已知字符？

Answer 1

当然。由于您要为输入的每个字符生成符号输入，因此只需为您知道的元素添加相应的断言即可:

from z3 import *

s = Solver()

input = [BitVec("input%s" % i, 8) for i in range(10)]

known = "CHECK"
s.add([input[i] == ord(known[i]) for i in range(len(known))])

print s.check()
print s.model()

打印:

sat
[input4 = 75,
 input3 = 67,
 input2 = 69,
 input1 = 72,
 input0 = 67]

这正是您想要的。现在，您可以调用 gen 函数并进一步约束 input 的其他部分以获得完整模型。

或者，您可以使用 BitVecVal 函数直接创建常量位向量，而不必首先创建符号变体:https://z3prover.github.io/api/html/namespacez3py.html#a74d306d60d4cc4432907f58306b41686但我认为使用纯符号输入并添加约束更好，因为它简化了编程。一开始就没有创建符号变量所节省的微小性能是不值得的。