Learning Z3py - Gibt es Unterstützung für Arrays und Loops

Question

Ich gehe durch Z3py und habe eine Frage mit der Verwendung der API in einigen speziellen Fällen. Der folgende Code ist eine vereinfachte Version von etwas, für das ich letztendlich Z3 verwenden möchte. Einige meiner Fragen sind: 1. Gibt es eine Möglichkeit, eine beliebig lange Reihe von Werten wie die Variable 'a' unten zu erstellen? 2. Können Sie auf jedes Element des Arrays in Schleifen durch Z3py zugreifen? 3. Ist es möglich, ein Ergebnis in eine Originalvariable zurückzuverweisen oder wird eine neue Variable benötigt? Wird die Konvertierung zu CNF automatisch eine eindeutige ID hinzufügen? (dh a + = b)

Insgesamt bin ich verloren, wie man die Z3py API für etwas wie den folgenden Algorithmus anwendet, wo die Lösung von 'b' abhängt. Jede Hilfe oder Hinweise ist/sind dankbar, danke.

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

Wir können das erreichen, indem wir ein Python-Programm schreiben, das einen Z3-Ausdruck erzeugt. Wir verwenden Python-Schleifen und Listen (wir können auch Arrays verwenden) in diesem Programm, aber diese Listen enthalten Z3 "symbolische" Ausdrücke anstelle von Python-Werten. Die resultierende Liste d ist eine Liste von Z3-Ausdrücken, die b enthalten. Dann bitten wir Z3, eine b zu finden, so dass Elemente von d "gleich" sind mit den Zeichen in der Zeichenkette '\xbd\x23\x43\x23\x40\x23\x41\x23'. Hier ist der 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()