Z3 example of finding parameters to a CRC-16 algorithm

gistfile1.txt

import crcmod
from z3 import *

# This is a CRC-16 algorithm coded to be able to use Z3's symbolic types
def crc16_py(buffer, initial, poly, xorout):
  crc = initial
  for b in buffer:
    crc = crc ^ (b << 8)
    for i in range(8):
      crc = If(crc & 0x8000 != 0, (crc << 1) ^ poly, crc << 1)
  return crc ^ xorout

# This is a CRC-16 implementation provided by a Python module
crc16 = crcmod.predefined.mkCrcFun('xmodem')


# Create symbolic variables for the parameters to our crc16 algorithm
initial = BitVec('initial', 16)
poly = BitVec('poly', 16)
xorout = BitVec('xorout', 16)

# Set up a solver and assert that the output of our algorithm should match the
# real one provided by the module
msg = b'hello zach'
s = Solver()
s.add(crc16_py(msg, initial, poly, xorout) == crc16(msg))
assert s.check() == sat

# All good, now what were the values?
print(s.model())