From 9258283e145d6a59dff5f25a503674065d84ad0d Mon Sep 17 00:00:00 2001 From: Dimo Date: Fri, 21 Jul 2017 16:46:20 -0700 Subject: [PATCH] Documentation nits; Sematnics syntax cleanup --- lib/cretonne/meta/base/semantics.py | 53 +++++++++-------- lib/cretonne/meta/cdsl/ast.py | 14 +++-- lib/cretonne/meta/cdsl/instructions.py | 25 +++++--- lib/cretonne/meta/cdsl/types.py | 18 ++++-- lib/cretonne/meta/cdsl/typevar.py | 8 ++- lib/cretonne/meta/cdsl/xform.py | 2 +- lib/cretonne/meta/semantics/__init__.py | 59 ++++++++----------- lib/cretonne/meta/semantics/elaborate.py | 1 + lib/cretonne/meta/semantics/test_elaborate.py | 8 +-- lib/cretonne/meta/semantics/types.py | 9 --- 10 files changed, 103 insertions(+), 94 deletions(-) delete mode 100644 lib/cretonne/meta/semantics/types.py diff --git a/lib/cretonne/meta/base/semantics.py b/lib/cretonne/meta/base/semantics.py index d85dad0682..b4315d8255 100644 --- a/lib/cretonne/meta/base/semantics.py +++ b/lib/cretonne/meta/base/semantics.py @@ -2,11 +2,10 @@ from __future__ import absolute_import from semantics.primitives import prim_to_bv, prim_from_bv, bvsplit, bvconcat,\ bvadd from .instructions import vsplit, vconcat, iadd -from cdsl.xform import XForm, Rtl +from cdsl.xform import Rtl from cdsl.ast import Var from cdsl.typevar import TypeSet from cdsl.ti import InTypeset -import semantics.types # noqa x = Var('x') y = Var('y') @@ -28,30 +27,32 @@ bvhi = Var('bvhi') ScalarTS = TypeSet(lanes=(1, 1), ints=True, floats=True, bools=True) vsplit.set_semantics( - XForm(Rtl((lo, hi) << vsplit(x)), - Rtl(bvx << prim_to_bv(x), - (bvlo, bvhi) << bvsplit(bvx), - lo << prim_from_bv(bvlo), - hi << prim_from_bv(bvhi)))) + (lo, hi) << vsplit(x), + Rtl( + bvx << prim_to_bv(x), + (bvlo, bvhi) << bvsplit(bvx), + lo << prim_from_bv(bvlo), + hi << prim_from_bv(bvhi) + )) vconcat.set_semantics( - XForm(Rtl(x << vconcat(lo, hi)), - Rtl(bvlo << prim_to_bv(lo), - bvhi << prim_to_bv(hi), - bvx << bvconcat(bvlo, bvhi), - x << prim_from_bv(bvx)))) + x << vconcat(lo, hi), + Rtl( + bvlo << prim_to_bv(lo), + bvhi << prim_to_bv(hi), + bvx << bvconcat(bvlo, bvhi), + x << prim_from_bv(bvx) + )) -iadd.set_semantics([ - XForm(Rtl(a << iadd(x, y)), - Rtl(bvx << prim_to_bv(x), - bvy << prim_to_bv(y), - bva << bvadd(bvx, bvy), - a << prim_from_bv(bva)), - constraints=[InTypeset(x.get_typevar(), ScalarTS)]), - XForm(Rtl(a << iadd(x, y)), - Rtl((xlo, xhi) << vsplit(x), - (ylo, yhi) << vsplit(y), - alo << iadd(xlo, ylo), - ahi << iadd(xhi, yhi), - a << vconcat(alo, ahi))) -]) +iadd.set_semantics( + a << iadd(x, y), + (Rtl(bvx << prim_to_bv(x), + bvy << prim_to_bv(y), + bva << bvadd(bvx, bvy), + a << prim_from_bv(bva)), + [InTypeset(x.get_typevar(), ScalarTS)]), + Rtl((xlo, xhi) << vsplit(x), + (ylo, yhi) << vsplit(y), + alo << iadd(xlo, ylo), + ahi << iadd(xhi, yhi), + a << vconcat(alo, ahi))) diff --git a/lib/cretonne/meta/cdsl/ast.py b/lib/cretonne/meta/cdsl/ast.py index c5e6d58def..86e2805497 100644 --- a/lib/cretonne/meta/cdsl/ast.py +++ b/lib/cretonne/meta/cdsl/ast.py @@ -102,15 +102,17 @@ class Def(object): def vars(self): # type: () -> Set[Var] - """ Return the set of all Vars that appear in self""" + """Return the set of all Vars in self that correspond to SSA values""" return self.definitions().union(self.uses()) def substitution(self, other, s): # type: (Def, VarMap) -> Optional[VarMap] """ If the Defs self and other agree structurally, return a variable - substitution to transform self ot other. Two Defs agree structurally - if the contained Apply's agree structurally. + substitution to transform self to other. Otherwise return None. Two + Defs agree structurally if there exists a Var substitution, that can + transform one into the other. See Apply.substitution() for more + details. """ s = self.expr.substitution(other.expr, s) @@ -378,7 +380,7 @@ class Apply(Expr): def vars(self): # type: () -> Set[Var] - """ Return the set of all Vars that appear in self""" + """Return the set of all Vars in self that correspond to SSA values""" res = set() for i in self.inst.value_opnums: arg = self.args[i] @@ -390,8 +392,8 @@ class Apply(Expr): # type: (Apply, VarMap) -> Optional[VarMap] """ If the application self and other agree structurally, return a variable - substitution to transform self ot other. Two applications agree - structurally if: + substitution to transform self to other. Otherwise return None. Two + applications agree structurally if: 1) They are over the same instruction 2) Every Var v in self, maps to a single Var w in other. I.e for each use of v in self, w is used in the corresponding place in diff --git a/lib/cretonne/meta/cdsl/instructions.py b/lib/cretonne/meta/cdsl/instructions.py index ee9bf15e5e..9d23dea89e 100644 --- a/lib/cretonne/meta/cdsl/instructions.py +++ b/lib/cretonne/meta/cdsl/instructions.py @@ -9,15 +9,16 @@ try: from typing import Union, Sequence, List, Tuple, Any, TYPE_CHECKING # noqa from typing import Dict # noqa if TYPE_CHECKING: - from .ast import Expr, Apply, Var # noqa + from .ast import Expr, Apply, Var, Def # noqa from .typevar import TypeVar # noqa from .ti import TypeConstraint # noqa - from .xform import XForm + from .xform import XForm, Rtl # List of operands for ins/outs: OpList = Union[Sequence[Operand], Operand] ConstrList = Union[Sequence[TypeConstraint], TypeConstraint] MaybeBoundInst = Union['Instruction', 'BoundInstruction'] - InstructionSemantics = List[XForm] + InstructionSemantics = Sequence[XForm] + RtlCase = Union[Rtl, Tuple[Rtl, Sequence[TypeConstraint]]] except ImportError: pass @@ -336,15 +337,23 @@ class Instruction(object): from .ast import Apply # noqa return Apply(self, args) - def set_semantics(self, sem): - # type: (Union[XForm, InstructionSemantics]) -> None + def set_semantics(self, src, *dsts): + # type: (Union[Def, Apply], *RtlCase) -> None """Set our semantics.""" from semantics import verify_semantics + from .xform import XForm, Rtl - if not isinstance(sem, list): - sem = [sem] + sem = [] # type: List[XForm] + for dst in dsts: + if isinstance(dst, Rtl): + sem.append(XForm(Rtl(src).copy({}), dst)) + else: + assert isinstance(dst, tuple) + sem.append(XForm(Rtl(src).copy({}), dst[0], + constraints=dst[1])) + + verify_semantics(self, Rtl(src), sem) - verify_semantics(self, sem) self.semantics = sem diff --git a/lib/cretonne/meta/cdsl/types.py b/lib/cretonne/meta/cdsl/types.py index 846cc442c9..53a1dd79ad 100644 --- a/lib/cretonne/meta/cdsl/types.py +++ b/lib/cretonne/meta/cdsl/types.py @@ -89,10 +89,7 @@ class ScalarType(ValueType): self._vectors = dict() # type: Dict[int, VectorType] # Assign numbers starting from 1. (0 is VOID). ValueType.all_scalars.append(self) - # Numbers are only valid for Cretone types that get emitted to Rust. - # This excludes BVTypes - self.number = len([x for x in ValueType.all_scalars - if not isinstance(x, BVType)]) + self.number = len(ValueType.all_scalars) assert self.number < 16, 'Too many scalar types' def __repr__(self): @@ -249,7 +246,7 @@ class BoolType(ScalarType): return self.bits -class BVType(ScalarType): +class BVType(ValueType): """A flat bitvector type. Used for semantics description only.""" def __init__(self, bits): @@ -268,7 +265,11 @@ class BVType(ScalarType): @staticmethod def with_bits(bits): # type: (int) -> BVType - typ = ValueType.by_name('bv{:d}'.format(bits)) + name = 'bv{:d}'.format(bits) + if name not in ValueType._registry: + return BVType(bits) + + typ = ValueType.by_name(name) if TYPE_CHECKING: return cast(BVType, typ) else: @@ -278,3 +279,8 @@ class BVType(ScalarType): # type: () -> int """Return the number of bits in a lane.""" return self.bits + + def lane_count(self): + # type: () -> int + """Return the number of lane. For BVtypes always 1.""" + return 1 diff --git a/lib/cretonne/meta/cdsl/typevar.py b/lib/cretonne/meta/cdsl/typevar.py index 2e7d4cb5cc..988d34aaf8 100644 --- a/lib/cretonne/meta/cdsl/typevar.py +++ b/lib/cretonne/meta/cdsl/typevar.py @@ -501,7 +501,8 @@ class TypeSet(object): for bits in self.bools: yield by(types.BoolType.with_bits(bits), nlanes) for bits in self.bitvecs: - yield by(types.BVType.with_bits(bits), nlanes) + assert nlanes == 1 + yield types.BVType.with_bits(bits) def get_singleton(self): # type: () -> types.ValueType @@ -572,12 +573,17 @@ class TypeVar(object): def singleton(typ): # type: (types.ValueType) -> TypeVar """Create a type variable that can only assume a single type.""" + scalar = None # type: ValueType if isinstance(typ, types.VectorType): scalar = typ.base lanes = (typ.lanes, typ.lanes) elif isinstance(typ, types.ScalarType): scalar = typ lanes = (1, 1) + else: + assert isinstance(typ, types.BVType) + scalar = typ + lanes = (1, 1) ints = None floats = None diff --git a/lib/cretonne/meta/cdsl/xform.py b/lib/cretonne/meta/cdsl/xform.py index 42655272b8..3d3f25a3c7 100644 --- a/lib/cretonne/meta/cdsl/xform.py +++ b/lib/cretonne/meta/cdsl/xform.py @@ -55,7 +55,7 @@ class Rtl(object): def vars(self): # type: () -> Set[Var] - """ Return the set of all Vars that appear in self""" + """Return the set of all Vars in self that correspond to SSA values""" return reduce(lambda x, y: x.union(y), [d.vars() for d in self.rtl], set([])) diff --git a/lib/cretonne/meta/semantics/__init__.py b/lib/cretonne/meta/semantics/__init__.py index d2c327c988..8caf792259 100644 --- a/lib/cretonne/meta/semantics/__init__.py +++ b/lib/cretonne/meta/semantics/__init__.py @@ -4,52 +4,45 @@ from cdsl.ti import TypeEnv, ti_rtl, get_type_env try: from typing import List, Dict, Tuple # noqa from cdsl.ast import Var # noqa - from cdsl.xform import XForm # noqa + from cdsl.xform import XForm, Rtl # noqa from cdsl.ti import VarTyping # noqa from cdsl.instructions import Instruction, InstructionSemantics # noqa except ImportError: pass -def verify_semantics(inst, sem): - # type: (Instruction, InstructionSemantics) -> None +def verify_semantics(inst, src, xforms): + # type: (Instruction, Rtl, InstructionSemantics) -> None """ - Verify that the semantics sem correctly describes the instruction inst. - This involves checking that: - 1) For all XForms x \in sem, x.src consists of a single instance of - inst - 2) For any possible concrete typing of inst there is exactly 1 XForm x - in sem that applies. + Verify that the semantics transforms in xforms correctly describe the + instruction described by the src Rtl. This involves checking that: + 1) For all XForms x \in xforms, there is a Var substitution form src to + x.src + 2) For any possible concrete typing of src there is exactly 1 XForm x + in xforms that applies. """ - # 1) The source rtl is always a single instance of inst. - for xform in sem: - assert len(xform.src.rtl) == 1 and\ - xform.src.rtl[0].expr.inst == inst,\ - "XForm {} doesn't describe instruction {}."\ - .format(xform, inst) + # 0) The source rtl is always a single instruction + assert len(src.rtl) == 1 + + # 1) For all XForms x, x.src is structurally equivalent to src + for x in xforms: + assert src.substitution(x.src, {}) is not None,\ + "XForm {} doesn't describe instruction {}.".format(x, src) # 2) Any possible typing for the instruction should be covered by # exactly ONE semantic XForm - inst_rtl = sem[0].src - typenv = get_type_env(ti_rtl(inst_rtl, TypeEnv())) - - # This bit is awkward. Concrete typing is defined in terms of the vars - # of one Rtl. We arbitrarily picked that Rtl to be sem[0].src. For any - # other XForms in sem, we must build a substitution form - # sem[0].src->sem[N].src, before we can check if sem[N] permits one of - # the concrete typings of our Rtl. - # TODO: Can this be made cleaner? - subst = [inst_rtl.substitution(x.src, {}) for x in sem] - assert not any(x is None for x in subst) - sub_sem = list(zip(subst, sem)) # type: List[Tuple[Dict[Var, Var], XForm]] # noqa - - def subst_typing(typing, sub): - # type: (VarTyping, Dict[Var, Var]) -> VarTyping - return {sub[v]: tv for (v, tv) in typing.items()} + typenv = get_type_env(ti_rtl(src, TypeEnv())) + typenv.normalize() + typenv = typenv.extract() for t in typenv.concrete_typings(): - matching_xforms = [x for (s, x) in sub_sem - if x.ti.permits(subst_typing(t, s))] + matching_xforms = [] # type: List[XForm] + for x in xforms: + # Translate t using x.symtab + t = {x.symtab[str(v)]: tv for (v, tv) in t.items()} + if (x.ti.permits(t)): + matching_xforms.append(x) + assert len(matching_xforms) == 1,\ ("Possible typing {} of {} not matched by exactly one case " + ": {}").format(t, inst, matching_xforms) diff --git a/lib/cretonne/meta/semantics/elaborate.py b/lib/cretonne/meta/semantics/elaborate.py index e6be0180e1..9cd92c1f06 100644 --- a/lib/cretonne/meta/semantics/elaborate.py +++ b/lib/cretonne/meta/semantics/elaborate.py @@ -81,6 +81,7 @@ def find_matching_xform(d): for x in d.expr.inst.semantics: subst = d.substitution(x.src.rtl[0], {}) + assert subst is not None if x.ti.permits({subst[v]: tv for (v, tv) in typing.items()}): res.append(x) diff --git a/lib/cretonne/meta/semantics/test_elaborate.py b/lib/cretonne/meta/semantics/test_elaborate.py index 15d4178ae8..4cbfe07bf9 100644 --- a/lib/cretonne/meta/semantics/test_elaborate.py +++ b/lib/cretonne/meta/semantics/test_elaborate.py @@ -232,16 +232,16 @@ class TestElaborate(TestCase): def test_elaborate_iadd_simple(self): # type: () -> None i32.by(2) # Make sure i32x2 exists. - r = Rtl( - self.v0 << iadd.i32(self.v1, self.v2), - ) - sem = elaborate(cleanup_concrete_rtl(r)) x = Var('x') y = Var('y') a = Var('a') bvx = Var('bvx') bvy = Var('bvy') bva = Var('bva') + r = Rtl( + a << iadd.i32(x, y), + ) + sem = elaborate(cleanup_concrete_rtl(r)) assert concrete_rtls_eq(sem, cleanup_concrete_rtl(Rtl( bvx << prim_to_bv.i32(x), diff --git a/lib/cretonne/meta/semantics/types.py b/lib/cretonne/meta/semantics/types.py deleted file mode 100644 index 1221804fbd..0000000000 --- a/lib/cretonne/meta/semantics/types.py +++ /dev/null @@ -1,9 +0,0 @@ -""" -The semantics.types module predefines all the Cretone primitive bitvector -types. -""" -from cdsl.types import BVType -from cdsl.typevar import MAX_BITVEC, int_log2 - -for width in range(0, int_log2(MAX_BITVEC)+1): - BVType(2**width)