使用 z3 其中约束取决于函数的输出

Question

我想用 z3 来解决这个案例。输入是一个 10 个字符的字符串。输入的每个字符都是一个可打印字符 (ASCII)。输入应该是这样的，当使用输入作为参数调用 calc2() 函数时，结果应该是：0x0009E38E1FB7629B。在这种情况下如何使用 z3py？通常我只会添加独立方程作为对 z3 的约束。在这种情况下，我不确定如何使用 z3。def calc2(input):    result = 0    for i in range(len(input)):        r1 = (result << 0x5) & 0xffffffffffffffff        r2 = result >> 0x1b        r3 = (r1 ^ r2)        result = (r3 ^ ord(input[i]))    return resultif __name__ == "__main__":        input = sys.argv[1]        result = calc2(input)        if result == 0x0009E38E1FB7629B:             print "solved"更新：我尝试了以下操作，但是它没有给我正确的答案：from z3 import *def calc2(input):    result = 0    for i in range(len(input)):        r1 = (result << 0x5) & 0xffffffffffffffff        r2 = result >> 0x1b        r3 = (r1 ^ r2)        result = r3 ^ Concat(BitVec(0, 56), input[i])    return resultif __name__ == "__main__":    s = Solver()    X = [BitVec('x' + str(i), 8) for i in range(10)]    s.add(calc2(X) == 0x0009E38E1FB7629B)    if s.check() == sat:        print(s.model())

Answer 1

您可以在 Z3 中对 calc2 进行编码。您需要将循环展开 1,2,3,4,..,n 次（对于 n = 预期的最大输入大小），仅此而已。（您实际上不需要展开循环，您可以使用 z3py 创建约束）