diff --git a/lib/cretonne/meta/cdsl/xform.py b/lib/cretonne/meta/cdsl/xform.py index 2cae1c1236..f25068480c 100644 --- a/lib/cretonne/meta/cdsl/xform.py +++ b/lib/cretonne/meta/cdsl/xform.py @@ -5,6 +5,7 @@ from __future__ import absolute_import from .ast import Def, Var, Apply from .ti import ti_xform, TypeEnv, get_type_env from functools import reduce +from .typevar import TypeVar try: from typing import Union, Iterator, Sequence, Iterable, List, Dict # noqa @@ -12,7 +13,6 @@ try: from .ast import Expr, VarMap # noqa from .isa import TargetISA # noqa from .ti import TypeConstraint # noqa - from .typevar import TypeVar # noqa DefApply = Union[Def, Apply] except ImportError: pass @@ -86,6 +86,37 @@ class Rtl(object): return s + def is_concrete(self): + # type: (Rtl) -> bool + """Return True iff every Var in the self has a singleton type.""" + return all(v.get_typevar().singleton_type() is not None + for v in self.vars()) + + def cleanup_concrete_rtl(self): + # type: (Rtl) -> None + """ + Given that there is only 1 possible concrete typing T for self, assign + a singleton TV with the single type t=T[v] for each Var v \in self. + Its an error to call this on an Rtl with more than 1 possible typing. + """ + from .ti import ti_rtl, TypeEnv + # 1) Infer the types of all vars in res + typenv = get_type_env(ti_rtl(self, TypeEnv())) + typenv.normalize() + typenv = typenv.extract() + + # 2) Make sure there is only one possible type assignment + typings = list(typenv.concrete_typings()) + assert len(typings) == 1 + typing = typings[0] + + # 3) Assign the only possible type to each variable. + for v in typenv.vars: + if v.get_typevar().singleton_type() is not None: + continue + + v.set_typevar(TypeVar.singleton(typing[v].singleton_type())) + class XForm(object): """ @@ -279,6 +310,27 @@ class XForm(object): raise AssertionError( '{} not defined in dest pattern'.format(d)) + def apply(self, r, suffix=None): + # type: (Rtl, str) -> Rtl + """ + Given a concrete Rtl r s.t. r matches self.src, return the + corresponding concrete self.dst. If suffix is provided, any temporary + defs are renamed with '.suffix' appended to their old name. + """ + assert r.is_concrete() + s = self.src.substitution(r, {}) # type: VarMap + assert s is not None + + if (suffix is not None): + for v in self.dst.vars(): + if v.is_temp(): + assert v not in s + s[v] = Var(v.name + '.' + suffix) + + dst = self.dst.copy(s) + dst.cleanup_concrete_rtl() + return dst + class XFormGroup(object): """ diff --git a/lib/cretonne/meta/semantics/elaborate.py b/lib/cretonne/meta/semantics/elaborate.py index 0f2d10641d..4b7dc14ae3 100644 --- a/lib/cretonne/meta/semantics/elaborate.py +++ b/lib/cretonne/meta/semantics/elaborate.py @@ -4,8 +4,6 @@ equivalent primitive version. Its elaborated primitive version contains only primitive cretonne instructions, which map well to SMTLIB functions. """ from .primitives import GROUP as PRIMITIVES, prim_to_bv, prim_from_bv -from cdsl.ti import ti_rtl, TypeEnv, get_type_env -from cdsl.typevar import TypeVar from cdsl.xform import Rtl from cdsl.ast import Var @@ -18,60 +16,6 @@ except ImportError: TYPE_CHECKING = False -def is_rtl_concrete(r): - # type: (Rtl) -> bool - """Return True iff every Var in the Rtl r has a single type.""" - return all(v.get_typevar().singleton_type() is not None for v in r.vars()) - - -def cleanup_concrete_rtl(r): - # type: (Rtl) -> Rtl - """ - Given an Rtl r - 1) assert that there is only 1 possible concrete typing T for r - 2) Assign a singleton TV with the single type t \in T for each Var v \in r - """ - # 1) Infer the types of any of the remaining vars in res - typenv = get_type_env(ti_rtl(r, TypeEnv())) - typenv.normalize() - typenv = typenv.extract() - - # 2) Make sure there is only one possible type assignment - typings = list(typenv.concrete_typings()) - assert len(typings) == 1 - typing = typings[0] - - # 3) Assign the only possible type to each variable. - for v in typenv.vars: - if v.get_typevar().singleton_type() is not None: - continue - - v.set_typevar(TypeVar.singleton(typing[v].singleton_type())) - - return r - - -def apply(r, x, suffix=None): - # type: (Rtl, XForm, str) -> Rtl - """ - Given a concrete Rtl r and XForm x, s.t. r matches x.src, return the - corresponding concrete x.dst. If suffix is provided, any temporary defs are - renamed with '.suffix' appended to their old name. - """ - assert is_rtl_concrete(r) - s = x.src.substitution(r, {}) # type: VarMap - assert s is not None - - if (suffix is not None): - for v in x.dst.vars(): - if v.is_temp(): - assert v not in s - s[v] = Var(v.name + '.' + suffix) - - dst = x.dst.copy(s) - return cleanup_concrete_rtl(dst) - - def find_matching_xform(d): # type: (Def) -> XForm """ @@ -93,41 +37,10 @@ def find_matching_xform(d): if x.ti.permits({subst[v]: tv for (v, tv) in typing.items()}): res.append(x) - assert len(res) == 1 + assert len(res) == 1, "Couldn't find semantic transform for {}".format(d) return res[0] -def elaborate(r): - # type: (Rtl) -> Rtl - """ - Given an Rtl r, return a semantically equivalent Rtl r1 consisting only - primitive instructions. - """ - fp = False - primitives = set(PRIMITIVES.instructions) - idx = 0 - - while not fp: - assert is_rtl_concrete(r) - new_defs = [] # type: List[Def] - fp = True - - for d in r.rtl: - inst = d.expr.inst - - if (inst not in primitives): - transformed = apply(Rtl(d), find_matching_xform(d), str(idx)) - idx += 1 - new_defs.extend(transformed.rtl) - fp = False - else: - new_defs.append(d) - - r.rtl = tuple(new_defs) - - return r - - def cleanup_semantics(r, outputs): # type: (Rtl, Set[Var]) -> Rtl """ @@ -176,3 +89,37 @@ def cleanup_semantics(r, outputs): d.defs[0] not in live)] return Rtl(*new_defs) + + +def elaborate(r): + # type: (Rtl) -> Rtl + """ + Given a concrete Rtl r, return a semantically equivalent Rtl r1 containing + only primitive instructions. + """ + fp = False + primitives = set(PRIMITIVES.instructions) + idx = 0 + + outputs = r.definitions() + + while not fp: + assert r.is_concrete() + new_defs = [] # type: List[Def] + fp = True + + for d in r.rtl: + inst = d.expr.inst + + if (inst not in primitives): + t = find_matching_xform(d) + transformed = t.apply(Rtl(d), str(idx)) + idx += 1 + new_defs.extend(transformed.rtl) + fp = False + else: + new_defs.append(d) + + r.rtl = tuple(new_defs) + + return cleanup_semantics(r, outputs)