Solving Pinball Overflow Factoring Problem with Z3

overflow-factorying-with-z3.py

from functools import reduce

from z3 import *

# Setup some constants
UINT16_MAX = 65535
TARGET = 0x020c020c  # This is the target value we are looking for

# Create the z3 solver
s = Solver()

# Create 10 BitVec symbolic variables
inputs = []
for i in range(10):
    inputs.append(BitVec(str(i), 32))  # z3 can't mix bit lengths so have to use 32 bit here but constrain to 16 bit
    s.add(inputs[i] >= 0, ULT(inputs[i], UINT16_MAX))  # Has to be unsigned >= 0 and 16 bit max < UINT16_MAX

# The product of all inputs must have the last 16 bits equal to our target
constraint = reduce((lambda x, y: x * y), inputs)
s.add(ZeroExt(32-16, constraint) == TARGET)

# You can optionally add some extra constraints if you need some of the bytes to be certain values
s.add(inputs[0] == 260)
s.add(inputs[1] == 1)

# Maybe you want some of the values to start with certain bits (0xff in this case)
s.add(Extract(15, 8, inputs[2]) == 0xff)

# Attempt to solve
if s.check().r != 1:
    print('Not satisfiable')
else:
    m = s.model()

    # Print results
    results = []
    for i in range(10):
        value = m[inputs[i]].as_long()
        results.append(value)
        print(hex(value))

    # Calculate result
    product = reduce((lambda x, y: x * y), results)
    print("")
    print(hex(product & 0xffffffff))

# Result:
#
# 0x0104       =260
# 0x0001       =1
# 0xffd7       starts with 0xff
# 0x65bb
# 0xde71
# 0xc30f
# 0xf25d
# 0x263f
# 0x77dd
# 0xc5b7
#
# 0x20C020C   Our target