Z3python异或总和?

本文介绍了Z3python异或总和?的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！

问题描述

我目前正在尝试使用 z3python 求解一些方程，但遇到了我无法处理的情况.

我需要对某些 BitVecs 与特定的非 ascii 字符值进行异或，并将它们相加以检查校验和.这是一个例子:

pbInput = [BitVec("{}".format(i), 8) for i in range(KEY_LEN)]密码 = "\xff\xff\xde\x8e\xae"solver.add(Xor(pbInput[0], password[0]) + Xor(pbInput[3], password[3]) == 300)

它导致 z3 类型异常:z3.z3types.Z3Exception:值无法转换为 Z3 布尔值.

我找到了这篇文章，并尝试将函数应用于我的密码 字符串，将此行添加到我的脚本中:password = Function(password, StringSort(), IntSort(), BitVecSort(8))但当然它失败了，因为字符串不是 ASCII 字符串.我不在乎它是一个字符串，我试着只做 Xor(pbInput[x] ^ 0xff)，但这也不起作用.我找不到关于这种特殊情况的任何文档.

这是完整的追溯.

回溯(最近一次调用最后一次):文件solve.py"，第 18 行，在 <module> 中(异或(pbInput[0]，密码[0])文件/usr/local/lib/python2.7/dist-packages/z3/z3.py"，第1555行，异或a = s.cast(a)文件/usr/local/lib/python2.7/dist-packages/z3/z3.py"，第1310行，演员表_z3_assert(self.eq(val.sort()), "值不能转换成 Z3 布尔值")文件/usr/local/lib/python2.7/dist-packages/z3/z3.py"，第 91 行，在 _z3_assert 中引发 Z3Exception(msg)z3.z3types.Z3Exception:无法将值转换为 Z3 布尔值

如果您对我如何执行此操作有任何想法，请提前致谢！

解决方案

您的代码中有两个问题.

Xor 仅用于 Bool 值；对于位向量，只需使用 ^
在传递给xor

ord

您没有提供完整的程序(这总是有帮助的！)，但以下是您在 z3py 中编写该部分作为完整程序的方式:

from z3 import *求解器 = 求解器()KEY_LEN = 10pbInput = [BitVec("c_{}".format(i), 8) for i in range(KEY_LEN)]密码 = "\xff\xff\xde\x8e\xae"solver.add((pbInput[0] ^ ord(password[0])) + (pbInput[3] ^ ord(password[3])) == 300)打印solver.check()打印solver.model()

打印:

sat[c_3 = 0，c_0 = 97]

(我给变量取了更好的名字以便更好地区分.)所以，它告诉我们解决方案是:

>>>(0xff ^ 97) + (0x8e ^ 0)300

这确实是您所要求的.

I'm currently trying to solve some equation with z3python, and I am coming across a situation I could not deal with.

I need to xor certain BitVecs with specific non ascii char values, and sum them up to check a checksum.Here is an example :

pbInput = [BitVec("{}".format(i), 8) for i in range(KEY_LEN)]
password = "\xff\xff\xde\x8e\xae"
solver.add(Xor(pbInput[0], password[0]) + Xor(pbInput[3], password[3]) == 300)

It results in a z3 type exception :z3.z3types.Z3Exception: Value cannot be converted into a Z3 Boolean value.

I found this post and tried to apply a function to my password string, adding this line to my script :password = Function(password, StringSort(), IntSort(), BitVecSort(8))But of course it fails as the string isn't an ASCII string.I don't care about it being a string, I tried to just do Xor(pbInput[x] ^ 0xff), but this doesn't work either. I could not find any documentation on this particular situation.

EDIT :Here is the full traceback.

Traceback (most recent call last):
  File "solve.py", line 18, in <module>
    (Xor(pbInput[0], password[0])
  File "/usr/local/lib/python2.7/dist-packages/z3/z3.py", line 1555, in Xor
    a = s.cast(a)
  File "/usr/local/lib/python2.7/dist-packages/z3/z3.py", line 1310, in cast
    _z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value")
  File "/usr/local/lib/python2.7/dist-packages/z3/z3.py", line 91, in _z3_assert
    raise Z3Exception(msg)
z3.z3types.Z3Exception: Value cannot be converted into a Z3 Boolean value

Thanks in advance if you have any idea about how I could do this operation!

解决方案

There are two problems in your code.

Xor is for Bool values only; for bit-vectors simply use ^
Use the function ord to convert characters to integers before passing to xor

You didn't give your full program (which is always helpful!), but here's how you'd write that section in z3py as a full program:

from z3 import *

solver = Solver()
KEY_LEN = 10

pbInput = [BitVec("c_{}".format(i), 8) for i in range(KEY_LEN)]
password = "\xff\xff\xde\x8e\xae"
solver.add((pbInput[0] ^ ord(password[0])) + (pbInput[3] ^ ord(password[3])) == 300)

print solver.check()
print solver.model()

This prints:

sat
[c_3 = 0, c_0 = 97]

(I gave the variables better names to distinguish more properly.) So, it's telling us the solution is:

>>> (0xff ^ 97) + (0x8e ^ 0)
300

Which is indeed what you asked for.

这篇关于Z3python异或总和?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！