every_c.py

import re

#
# translation_unit :=
#   declaration |
#   translation_unit declaration
#
# declaration :=
#   "int" identifier ";" |
#   "float" identifier ";"
#

src = """
#ifdef A
    int
#endif
#ifdef B
    a
    ;
  #ifdef C
    float
  #endif
#endif
    b
    ;
"""

pp_lines = []

token = re.compile(r"([0-9]+|[a-zA-Z_][a-zA-Z0-9]*|[+\-*/!%&()=?:;<>.,^])")

ppvars = set()

for line in src.split("\n"):
	if line.strip(): print(line)
	line = line.strip()
	if not line:
		pass
	elif line[0] == "#" and (line[:2]+" ")[1] != "#":
		line = line[1:].strip()
		if line.startswith("ifdef "):
			name = line[6:].strip()
			ppvars.add(name)
			assert " " not in name
			pp_lines.append(("ifdef", name))
		elif line == "endif":
			pp_lines.append(("endif", None))
		else:
			assert False, line
	else:
		tokens = []
		while line:
			m = token.match(line)
			assert m, line
			tokens.append(line[:m.end()])
			line = line[m.end():].strip()
		pp_lines.append((None, tokens))

import z3

s = z3.Solver()
ppvars = {n: z3.Const(n, z3.BoolSort()) for n in ppvars}

def fancy_simplify(x, ppvars):
	t = z3.Then(z3.With("simplify"), "qe2", "smt")
	s = t.solver()
	mentioned_ppvars = set()
	def visit(node):
		if z3.is_const(node) and node in ppvars:
			mentioned_ppvars.add(node)
		for c in node.children():
			visit(c)
	visit(x)
	mentioned_ppvars = list(mentioned_ppvars)
	mentioned_ppvars.sort(key = lambda n: ppvars.index(n))
	if len(mentioned_ppvars) > 0:
		f = z3.Function("f", *[z3.BoolSort()]*(len(mentioned_ppvars)+1))
		s.add(z3.ForAll(mentioned_ppvars, f(*mentioned_ppvars) == x))
		s.check()
		m = s.model()
		xx = z3.simplify(m.eval(f(*mentioned_ppvars)))
		x = x if len(str(x)) < len(str(xx)) else xx
	return x

class Var:
	def __init__(self, initial_value):
		self.r = {initial_value: z3.BoolVal(True)}
		self.c = {initial_value: z3.BoolVal(True)}
		self.x = {}

		self.updated = z3.BoolVal(False)

	def __eq__(self, other):
		return self.c[other]

	def update(self, new, when=None):
		self.updated = z3.Or(self.updated, when)
		if new not in self.x:
			self.x[new] = when
		else:
			self.x[new] = z3.Or(self.x[new], when)

	def step(self, f):
		if f:
			elsewhen = z3.Not(self.updated)
			for v in self.c.keys():
				self.update(f(v), z3.And(self==v, elsewhen))

		self.c = self.x
		self.x = {}
		self.updated = z3.BoolVal(False)

	def simplify(self, cube, ppvars):

		hack = False

		if hack:
			conditions = []
			a = cube
			while z3.is_and(a):
				a, b = a.children()
				conditions.append(b)
			if str(a) != "True":
				conditions.append(a)

		vs = set(self.c.keys()) | set(self.r.keys())
		for v in vs:
			cc = self.c.get(v, z3.BoolVal(False))
			rr = self.r.get(v, z3.BoolVal(False))
			if hack:
				cc = z3.substitute(cc, *((c, z3.BoolVal(True)) for c in conditions))
			#x = z3.If(cube, cc, rr)
			x = z3.Or(z3.And(cube, cc), z3.And(z3.Not(cube), rr))
			x = z3.simplify(x)

			if True:
				x = fancy_simplify(x, ppvars)

			if x == z3.BoolVal(False) and v in self.c:
				del self.c[v]
			else:
				self.c[v] = x

		self.r = self.c.copy()

	def __iter__(self):
		return iter(sorted(self.c.items(), key=lambda a: str(a[0])))

scope = {}
state = Var(0)
last_type = Var(None)
last_name = Var(None)
conditions = []

for ty, tks in pp_lines:
	if ty == "ifdef":
		conditions.append(tks)
	elif ty == "endif":
		conditions.pop(-1)
	elif ty == None:
		#print("{:5}{}".format("".join(conditions)+">", " ".join(tks)))
		#print("{:15} {}".format(("#if "+" && ".join(conditions)) if conditions else "", " ".join(tks)))
		if conditions:
			cube = ppvars[conditions[0]]
			for cc in conditions[1:]:
				cube = z3.And(cube, ppvars[cc])
			ncube = z3.Not(cube)
		else:
			cube = z3.BoolVal(True)
			ncube = z3.BoolVal(False)
		for tk in tks:

			if tk in ("int", "float"):
				state.update(1, state==0)
				last_type.update(tk, state==0)

			elif tk == ";":
				state.update(0, state==2)
				for v, vp in last_name:
					for t, tp in last_type:
						scope.setdefault(v, Var(None)).update(t, z3.And(vp, tp, state==2))

			else:
				state.update(2, state==1)
				last_name.update(tk, state==1)

			state.step(lambda s: 99)
			last_type.step(lambda t: t)
			last_name.step(lambda t: t)
			for v in scope.keys():
				scope[v].step(lambda t: t)

		state.simplify(cube, list(ppvars.values()))
		last_type.simplify(cube, list(ppvars.values()))
		last_name.simplify(cube, list(ppvars.values()))
		for v in scope.keys():
			scope[v].simplify(cube, list(ppvars.values()))

		if False:
			for v, p in state:
				print(" state", v, p)
			print()
			for v, p in last_type:
				print(" type", v, p)
			print()
			for v, p in last_name:
				print(" name", v, p)
			print()
			for n, z in scope.items():
				if n is None:
					continue
				print("", n)
				for v, p in z:
					print(" ", v, p)
			print()

print()
print("Scope at end of file:")
for n, z in scope.items():
	if n is None:
		continue
	for v, p in z:
		if v is None:
			readable = "undeclared {};".format(n)
		else:
			readable = "{} {};".format(v, n)
		print("  {:15} // when {}".format(readable, p))
print()

if False:
	print("#define A")
	print("#define C")
	for n, z in scope.items():
		if n is None:
			continue
		ov = "fff"
		for v, p in z:
			pp = z3.simplify(z3.substitute(p,
				(ppvars["A"], z3.BoolVal(True)),
				(ppvars["B"], z3.BoolVal(False)),
				(ppvars["C"], z3.BoolVal(True))))
			if pp == z3.BoolVal(True):
				assert ov is "fff"
				ov = v
			elif pp == z3.BoolVal(False):
				pass
			else:
				assert False
		assert ov != "fff"
		if ov is None:
			print("  // {};".format(n))
		else:
			print("  {} {};".format(ov, n))

	print()

print("Parse error condition:", fancy_simplify(state==99, list(ppvars.values())))
print()