z3_test.py

#!/usr/bin/env python3
#
# https://z3prover.github.io/api/html/namespacez3py.html
# https://ericpony.github.io/z3py-tutorial/guide-examples.htm

import sys

from z3 import *

def add_constraints(solver, badbytes, *vars):
    for v in vars:
        # Ensure the parameters are within ASCII range
        solver.add(v > 0)
        solver.add(v < 0x80)

        # Also weed out any badbytes
        [solver.add(v != b) for b in badbytes]

def z3_model_solve(solver, badbytes, *vars):
    add_constraints(solver, badbytes, *vars)
    solver.check()

    try:
        model = solver.model()
        results = {}
        for v in vars:
            results[v] = model[v].as_long()
        return results
    except Z3Exception:
        return None

def z3_model_2(byte, badbytes):
    x, y = Ints('x y')
    s = Solver()
    s.add(x + y == byte)

    m = z3_model_solve(s, badbytes, x, y)
    if m:
        print(f'{hex(byte)} solved: ', end='')
        print(m)
        return True
    else:
        return None


def z3_model_3(byte, badbytes):
    x, y, z = Ints('x y z')
    s = Solver()
    s.add(x + y + z == byte)

    m = z3_model_solve(s, badbytes, x, y, z)
    if m:
        print(f'{hex(byte)} solved: ', end='')
        print(m)
        return True
    else:
        return None

def main():
    badbytes = [0x00, 0x14, 0x15, 0x30]
    byte = 0xff

    if not z3_model_2(byte, badbytes):
        print(f'{hex(byte)} not solvable with two parameters; attempting with three')
        z3_model_3(byte, badbytes)
    

if __name__ == '__main__':
    main()