5

我正在浏览 Z3py，并且对如何在几个特定情况下使用 API 有疑问。下面的代码是我最终想使用 Z3 的简化版本。我的一些问题是： 1. 有没有办法创建一个任意长的值数组，比如下面的变量“a”？2、可以通过Z3py循环访问数组的每个元素吗？3. 是否可以将结果分配回原始变量或是否需要新变量？转换为 CNF 会自动添加唯一的 id 吗？（即 a += b）

总的来说，我不知道如何将 Z3py API 应用于以下算法，其中解决方案取决于“b”。感谢您提供任何帮助或提示，谢谢。

import sys
import struct

a = "\xff\x33\x01\x88\x02\x11\x03\x55"
b = sys.stdin.read(1) #a byte of user input - value 'a' is good
c = ''
d = ''

for x in range(len(a)):
    c +=  struct.pack( 'B', int(a[x].encode('hex'), 16)^int(b.encode('hex'), 16) )

print c.encode('hex')

second = '\x23\x23'
x = 0
while x < len(c):
    d += struct.pack( 'h', int(c[x:x+1].encode('hex'), 16)^int(second.encode('hex'), 16) )
    x += 2

print d.encode('hex')

if d == '\xbd\x23\x43\x23\x40\x23\x41\x23':
    print "Good"
else:
    print "Bad"
4

1 回答 1

7

我们可以通过编写一个生成 Z3 表达式的 Python 程序来实现这一点。我们在这个程序中使用 Python 循环和列表（我们也可以使用数组），但是这些列表包含 Z3“符号”表达式而不是 Python 值。结果列表d是包含 的 Z3 表达式列表b。然后，我们要求 Z3 找到一个b使得 的元素d与字符串中的字符“相等”的元素'\xbd\x23\x43\x23\x40\x23\x41\x23'。这是代码：

from z3 import *

def str2array(a):
    """
    Convert a string into a list of Z3 bit-vector values of size 8
    """
    return [ BitVecVal(int(a[x].encode('hex'), 16), 8) for x in range(len(a)) ]

a = str2array("\xff\x33\x01\x88\x02\x11\x03\x55")
# 'a' is a list of Z3 bitvector constants.
print "a:", a
# The elements of 'a' may look like Python integers but they are Z3 expressions.
# We can use the method sexpr() to get these values in SMT 2.0 syntax.
print [ a_i.sexpr() for a_i in a ]

# b is a Z3 symbolic variable.
b = BitVec('b', 8)

# We compute a list 'c' of Z3 expressions from 'a' and 'b'.
# We use Python list comprehensions but we can also use a for-loop.
c = [ a_i ^ b for a_i in a ] 

print "c:", c

second = '\x23\x23'
# We convert 'second' in a Z3 bit-vector value of size 16
second = BitVecVal(int(second.encode('hex'), 16), 16)
print "second:", second

# The Z3 operation Concat concatenates two or more bit-vector expressions.
d = []
x = 0
while x < len(c):
    # c[x] is a Bit-vector of size 8, second is a Bit-vector of size 16.
    # In Z3, we have to do the "casting" ourselves.
    # We use ZeroExt(8, c[x]) to convert c[x] into a Bit-vector of size 16,
    # by adding 0-bits.
    d.append(ZeroExt(8, c[x]) ^ second)
    x += 2
print "d:", d

goal = str2array('\xbd\x23\x43\x23\x40\x23\x41\x23')
print "goal:", goal
# Note that, len(goal) == 2*len(d)
# We can use Concat to concatenate adjacent elements.

# We want each element of d[i] == Concat(goal[2*i], goal[2*i+1])
# We can use Z3 to find the 'b' that will satisfy these constraints

s = Solver()
# 's' is a Z3 solver object
i = 0
while i < len(d):
    s.add(d[i] == Concat(goal[2*i+1], goal[2*i]))
    i += 1
print s
# Now, 's' contains a set of equational constraints.
print s.check()
print s.model()
于 2012-12-15T04:54:35.990 回答