我们能否在 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 中的输入以利用已知字符?
最佳答案
当然。由于您要为输入的每个字符生成符号输入,因此只需为您知道的元素添加相应的断言即可:
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但我认为使用纯符号输入并添加约束更好,因为它简化了编程。一开始就没有创建符号变量所节省的微小性能是不值得的。
关于python - 使用固定字符在 Z3 中定义位向量,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/53808203/