PlaidCTF 2015 "RE GEX" solver

re_gex_solver.py

#!/usr/bin/env python
#
# PlaidCTF 2015 "RE GEX" solver
# @zxcvgm
#

from z3 import *


def bitpos(pos): return (170 - pos) * 3

def parse(pattern, bv):
	pos = 0
	i = 0

	pattern_conditions = []

	while i < len(pattern):
		if pattern[i] == '.':
			n = 0
			if i + 1 >= len(pattern) or pattern[i+1] != '{':
				i += 1
				n = 1
			else:
				i += 2
				n = ''
				while pattern[i] != '}':
					n += pattern[i]
					i += 1

				i += 1
				n = int(n)

			pos += n

		elif pattern[i] == '[':
			chars = ''
			i += 1
			while pattern[i] != ']':
				chars += pattern[i]
				i += 1

			i += 1

			char_class_cond = And(*[(bv >> bitpos(pos) & 7) != 'plaidctf'.find(c) for c in chars])
			pattern_conditions.append(char_class_cond)

			pos += 1

		else:
			assert False, 'unknown char %s at pos %d' % (pattern[i], i)

	return pattern_conditions


# read patterns
f = open('regex_patterns.txt', 'rb')
patterns = [l.strip() for l in f]
f.close()

bv = BitVec('pattern', 171 * 3)
solver = Solver()

all_conditions = []
for p in patterns:
	pp = parse(p, bv)
	all_conditions.append(Or(*pp))

solver.add(And(*all_conditions))
#print solver
assert solver.check() == sat

pattern = solver.model()[bv].as_long()
pattern_txt = ''.join('plaidctf'[pattern >> bitpos(i) & 7] for i in xrange(171))

print pattern_txt