我怎样才能只检查 z3 中的存在？

Question

我需要 z3 中的一些临时变量，我不需要计算值只需要检查它是否存在就足够了。

这是我正在做的（简单形式）：

import z3

def maj(a, b, c):
    return (a & b) ^ (a & c) ^ (b & c)

def func(a, b, c):
    a = z3.RotateRight(a, 5) ^ z3.BitVecVal(0xafaf, 16)
    b = z3.RotateRight(b, 2) ^ z3.RotateRight(b, 7)
    c = z3.RotateRight(c, 11) ^ z3.LShR(c, 3)
    return a + c, b + c, maj(a + b, a + c, b + c)

solver = z3.SolverFor('QF_BV')
some_var = 0x0000
_x = z3.BitVec('x', 16)
x = _x
y = z3.BitVecVal(some_var, 16)
c = z3.BitVec('c', 16)
for i in range(16):
    x, y, c = func(x, y, c)
solver.add(c == z3.BitVecVal(0xff00, 16))
print(solver.check())
model = solver.model()
print(model[_x].as_long())

我需要

x

的值但不需要

c

的值只知道有一些变量就足够了。 如果我为

c

传递一些固定常数，它运行得更快（但它可能是

unsat

）

也使用

z3.Var(1, z3.BitVecSort(16))

给出

unknown

作为答案。

有什么办法吗？

Answer 1

你的问题有点模棱两可：我认为你确实关心

c

的最终值为

0xff00

，但你不关心它的初始值是多少？因为你一直在变异

c

，所以不清楚你想约束哪一个。

如果是这样的话，即，如果您希望

c

的最终值为

0xff00

并且不关心初始值是什么，那么您所做的就可以了。您只是不应该期望求解器能够快速提出解决方案。这看起来很像某种加密/扰码器例程，而 SMT 求解器——或与此相关的任何其他求解器——在设计上并不擅长处理此类问题。它们倾向于对单向函数进行编码，因此您不应期望开箱即用的通用约束求解器可以轻松对其进行逆向工程。可以做到，但不会很快。

如果你真的不关心 c 的

final

值是多少（这是一件奇怪的事情，但我想它可能有一个用例），那么典型的方式解决这个问题的方法是使用量词。它有点符合您的要求：“有一些

c

，我不在乎它是什么。”那么，让我们编写代码。我们需要做一些改变。首先，我们需要量词，因此适当设置求解器：

solver = z3.SolverFor('BV')

然后：

final_c = z3.BitVec('final_c', 16)
solver.add(z3.Exists([final_c], c == final_c))

请注意，

final_c

的声明是一个技术问题。您将无法访问它的值。这只是为了确保

c

存在一些可以达到的最终值。 （即，整件事不是

unsat

。）

有了这些变化，如果你运行程序，你会看到它说：

Traceback (most recent call last):
  File "/Users/leventerkok/qq/b.py", line 27, in <module>
    print(model[_x].as_long())
AttributeError: 'NoneType' object has no attribute 'as_long'

这是因为模型根本不关心

_x

；它注意到这是可满足的，并没有费心去计算

_x

。但是我们可以要求它给我们一个这样的值：

model = solver.model()
print(model.evaluate(_x, model_completion=True))

这打印：

sat
0

所以，有一种方法可以运行你的方程式，一切都从

x = 0

开始。好吧，这不是很有趣，但是没有任何额外的限制它确实有意义：从

x = 0

和适当的

y/c

开始，您确实可以展开这个计算。

最后，不要使用

z3.Var(1, BitVecSort(16))

。那些是 lambda-vars，你永远不应该伸手去拿。 （在我看来，z3 将它们暴露给最终用户是一个设计缺陷，但并非一切都是完美的！）