Learning Z3py - Is there support for arrays and loops

Question

I'm going through Z3py and have a question with how to use the API in a couple specific cases. The code below is a simplified version of something I would ultimately like to use Z3 for. Some of my questions are: 1. Is there a way to create an arbitrarily long array of values like the variable 'a' below? 2. Can you access each element of the array in loops through Z3py? 3. Is it possible to assign a result back into an original variable or is a new variable needed? Will the conversion to CNF automatically add a unique id? (ie a += b)

Overall, I'm lost on how to apply the Z3py API for something like the below algorithm where the solution depends on 'b'. Any help or hints is/are appreciated, thank you.

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"

Answer 1

We can accomplish that by writing a Python program that produces a Z3 expression. We use Python loops and lists (we can also use arrays) in this program, but these lists contain Z3 "symbolic" expressions instead of Python values. The resultant list d is a list of Z3 expressions containing b. Then, we ask Z3 to find a b such that elements of d are "equal" to the characters in the string '\xbd\x23\x43\x23\x40\x23\x41\x23'. Here is the code:

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()