diff --git a/lib/cretonne/meta/base/semantics.py b/lib/cretonne/meta/base/semantics.py new file mode 100644 index 0000000000..d85dad0682 --- /dev/null +++ b/lib/cretonne/meta/base/semantics.py @@ -0,0 +1,57 @@ +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.ast import Var +from cdsl.typevar import TypeSet +from cdsl.ti import InTypeset +import semantics.types # noqa + +x = Var('x') +y = Var('y') +a = Var('a') +xhi = Var('xhi') +yhi = Var('yhi') +ahi = Var('ahi') +xlo = Var('xlo') +ylo = Var('ylo') +alo = Var('alo') +lo = Var('lo') +hi = Var('hi') +bvx = Var('bvx') +bvy = Var('bvy') +bva = Var('bva') +bvlo = Var('bvlo') +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)))) + +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)))) + +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))) +]) diff --git a/lib/cretonne/meta/cdsl/instructions.py b/lib/cretonne/meta/cdsl/instructions.py index 0bbaccb353..ee9bf15e5e 100644 --- a/lib/cretonne/meta/cdsl/instructions.py +++ b/lib/cretonne/meta/cdsl/instructions.py @@ -12,11 +12,12 @@ try: from .ast import Expr, Apply, Var # noqa from .typevar import TypeVar # noqa from .ti import TypeConstraint # noqa + from .xform import XForm # List of operands for ins/outs: OpList = Union[Sequence[Operand], Operand] ConstrList = Union[Sequence[TypeConstraint], TypeConstraint] MaybeBoundInst = Union['Instruction', 'BoundInstruction'] - VarTyping = Dict[Var, TypeVar] + InstructionSemantics = List[XForm] except ImportError: pass @@ -119,6 +120,7 @@ class Instruction(object): self.outs = self._to_operand_tuple(outs) self.constraints = self._to_constraint_tuple(constraints) self.format = InstructionFormat.lookup(self.ins, self.outs) + self.semantics = None # type: InstructionSemantics # Opcode number, assigned by gen_instr.py. self.number = None # type: int @@ -334,6 +336,17 @@ class Instruction(object): from .ast import Apply # noqa return Apply(self, args) + def set_semantics(self, sem): + # type: (Union[XForm, InstructionSemantics]) -> None + """Set our semantics.""" + from semantics import verify_semantics + + if not isinstance(sem, list): + sem = [sem] + + verify_semantics(self, sem) + self.semantics = sem + class BoundInstruction(object): """ diff --git a/lib/cretonne/meta/cdsl/ti.py b/lib/cretonne/meta/cdsl/ti.py index ab4ae12f19..b80396b428 100644 --- a/lib/cretonne/meta/cdsl/ti.py +++ b/lib/cretonne/meta/cdsl/ti.py @@ -54,8 +54,8 @@ class TypeConstraint(object): """ Return true iff all typevars in the constraint are singletons. """ - tvs = filter(lambda x: isinstance(x, TypeVar), self._args()) - return [] == list(filter(lambda x: x.singleton_type() is None, tvs)) + return [] == list(filter(lambda x: x.singleton_type() is None, + self.tvs())) def __hash__(self): # type: () -> int @@ -69,6 +69,13 @@ class TypeConstraint(object): """ assert False, "Abstract" + def tvs(self): + # type: () -> Iterable[TypeVar] + """ + Return the typevars contained in this constraint. + """ + return filter(lambda x: isinstance(x, TypeVar), self._args()) + def is_trivial(self): # type: () -> bool """ @@ -218,6 +225,47 @@ class WiderOrEq(TypeConstraint): return typ1.wider_or_equal(typ2) +class SameWidth(TypeConstraint): + """ + Constraint specifying that two types have the same width. E.g. i32x2 has + the same width as i64x1, i16x4, f32x2, f64, b1x64 etc. + """ + def __init__(self, tv1, tv2): + # type: (TypeVar, TypeVar) -> None + self.tv1 = tv1 + self.tv2 = tv2 + + def _args(self): + # type: () -> Tuple[Any,...] + """ See TypeConstraint._args() """ + return (self.tv1, self.tv2) + + def is_trivial(self): + # type: () -> bool + """ See TypeConstraint.is_trivial() """ + # Trivially true + if (self.tv1 == self.tv2): + return True + + ts1 = self.tv1.get_typeset() + ts2 = self.tv2.get_typeset() + + # Trivially False + if len(ts1.widths().intersection(ts2.widths())) == 0: + return True + + return self.is_concrete() + + def eval(self): + # type: () -> bool + """ See TypeConstraint.eval() """ + assert self.is_concrete() + typ1 = self.tv1.singleton_type() + typ2 = self.tv2.singleton_type() + + return (typ1.width() == typ2.width()) + + class TypeEnv(object): """ Class encapsulating the neccessary book keeping for type inference. @@ -537,6 +585,10 @@ class TypeEnv(object): elif isinstance(constr, WiderOrEq): assert constr.tv1 in nodes and constr.tv2 in nodes edges.add((constr.tv1, constr.tv2, "dashed", "forward", ">=")) + elif isinstance(constr, SameWidth): + assert constr.tv1 in nodes and constr.tv2 in nodes + edges.add((constr.tv1, constr.tv2, "dashed", "none", + "same_width")) else: assert False, "Can't display constraint {}".format(constr) diff --git a/lib/cretonne/meta/cdsl/types.py b/lib/cretonne/meta/cdsl/types.py index 80b096cbc1..846cc442c9 100644 --- a/lib/cretonne/meta/cdsl/types.py +++ b/lib/cretonne/meta/cdsl/types.py @@ -59,6 +59,11 @@ class ValueType(object): """Return the number of lanes.""" assert False, "Abstract" + def width(self): + # type: () -> int + """Return the total number of bits of an instance of this type.""" + return self.lane_count() * self.lane_bits() + def wider_or_equal(self, other): # type: (ValueType) -> bool """ diff --git a/lib/cretonne/meta/cdsl/typevar.py b/lib/cretonne/meta/cdsl/typevar.py index 54a5c92cc0..2e7d4cb5cc 100644 --- a/lib/cretonne/meta/cdsl/typevar.py +++ b/lib/cretonne/meta/cdsl/typevar.py @@ -513,6 +513,13 @@ class TypeSet(object): assert len(types) == 1 return types[0] + def widths(self): + # type: () -> Set[int] + """ Return a set of the widths of all possible types in self""" + scalar_w = self.ints.union(self.floats.union(self.bools)) + scalar_w = scalar_w.union(self.bitvecs) + return set(w * l for l in self.lanes for w in scalar_w) + class TypeVar(object): """ diff --git a/lib/cretonne/meta/cdsl/xform.py b/lib/cretonne/meta/cdsl/xform.py index a43846a372..42655272b8 100644 --- a/lib/cretonne/meta/cdsl/xform.py +++ b/lib/cretonne/meta/cdsl/xform.py @@ -10,6 +10,8 @@ try: from typing import Union, Iterator, Sequence, Iterable, List, Dict # noqa from typing import Optional, Set # noqa from .ast import Expr, VarMap # noqa + from .ti import TypeConstraint # noqa + from .typevar import TypeVar # noqa DefApply = Union[Def, Apply] except ImportError: pass @@ -89,7 +91,8 @@ class XForm(object): An instruction transformation consists of a source and destination pattern. Patterns are expressed in *register transfer language* as tuples of - `ast.Def` or `ast.Expr` nodes. + `ast.Def` or `ast.Expr` nodes. A pattern may optionally have a sequence of + TypeConstraints, that additionally limit the set of cases when it applies. A legalization pattern must have a source pattern containing only a single instruction. @@ -111,8 +114,8 @@ class XForm(object): ) """ - def __init__(self, src, dst): - # type: (Rtl, Rtl) -> None + def __init__(self, src, dst, constraints=None): + # type: (Rtl, Rtl, Optional[Sequence[TypeConstraint]]) -> None self.src = src self.dst = dst # Variables that are inputs to the source pattern. @@ -146,6 +149,18 @@ class XForm(object): raw_ti.normalize() self.ti = raw_ti.extract() + def interp_tv(tv): + # type: (TypeVar) -> TypeVar + """ Convert typevars according to symtab """ + if not tv.name.startswith("typeof_"): + return tv + return symtab[tv.name[len("typeof_"):]].get_typevar() + + if constraints is not None: + for c in constraints: + type_m = {tv: interp_tv(tv) for tv in c.tvs()} + self.ti.add_constraint(c.translate(type_m)) + # Sanity: The set of inferred free typevars should be a subset of the # TVs corresponding to Vars appearing in src free_typevars = set(self.ti.free_typevars()) diff --git a/lib/cretonne/meta/semantics/__init__.py b/lib/cretonne/meta/semantics/__init__.py new file mode 100644 index 0000000000..d2c327c988 --- /dev/null +++ b/lib/cretonne/meta/semantics/__init__.py @@ -0,0 +1,55 @@ +"""Definitions for the semantics segment of the Cretonne language.""" +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.ti import VarTyping # noqa + from cdsl.instructions import Instruction, InstructionSemantics # noqa +except ImportError: + pass + + +def verify_semantics(inst, sem): + # type: (Instruction, 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. + """ + # 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) + + # 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()} + + for t in typenv.concrete_typings(): + matching_xforms = [x for (s, x) in sub_sem + if x.ti.permits(subst_typing(t, s))] + 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 new file mode 100644 index 0000000000..e6be0180e1 --- /dev/null +++ b/lib/cretonne/meta/semantics/elaborate.py @@ -0,0 +1,170 @@ +""" +Tools to elaborate a given Rtl with concrete types into its semantically +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 + +try: + from typing import TYPE_CHECKING, Dict, Union, List, Set, Tuple # noqa + from cdsl.xform import Rtl, XForm # noqa + from cdsl.ast import Var, Def, VarMap # noqa + from cdsl.ti import VarTyping # noqa +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 + """ + Given a concrete Def d, find the unique semantic XForm x in + d.expr.inst.semantics that applies to it. + """ + res = [] # type: List[XForm] + typing = {v: v.get_typevar() for v in d.vars()} # type: VarTyping + + for x in d.expr.inst.semantics: + subst = d.substitution(x.src.rtl[0], {}) + + if x.ti.permits({subst[v]: tv for (v, tv) in typing.items()}): + res.append(x) + + assert len(res) == 1 + 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 + """ + The elaboration process creates a lot of redundant instruction pairs of the + shape: + + a.0 << prim_from_bv(bva.0) + ... + bva.1 << prim_to_bv(a.0) + ... + + Contract these to ease manual inspection. + """ + new_defs = [] # type: List[Def] + subst_m = {v: v for v in r.vars()} # type: VarMap + definition = {} # type: Dict[Var, Def] + + # Pass 1: Remove redundant prim_to_bv + for d in r.rtl: + inst = d.expr.inst + + if (inst == prim_to_bv): + if d.expr.args[0] in definition: + assert isinstance(d.expr.args[0], Var) + def_loc = definition[d.expr.args[0]] + + if def_loc.expr.inst == prim_from_bv: + assert isinstance(def_loc.expr.args[0], Var) + subst_m[d.defs[0]] = def_loc.expr.args[0] + continue + + new_def = d.copy(subst_m) + + for v in new_def.defs: + assert v not in definition # Guaranteed by SSA + definition[v] = new_def + + new_defs.append(new_def) + + # Pass 2: Remove dead prim_from_bv + live = set(outputs) # type: Set[Var] + for d in new_defs: + live = live.union(d.uses()) + + new_defs = [d for d in new_defs if not (d.expr.inst == prim_from_bv and + d.defs[0] not in live)] + + return Rtl(*new_defs) diff --git a/lib/cretonne/meta/semantics/primitives.py b/lib/cretonne/meta/semantics/primitives.py new file mode 100644 index 0000000000..d5b6b35d8b --- /dev/null +++ b/lib/cretonne/meta/semantics/primitives.py @@ -0,0 +1,71 @@ +""" +Cretonne primitive instruction set. + +This module defines a primitive instruction set, in terms of which the base set +is described. Most instructions in this set correspond 1-1 with an SMTLIB +bitvector function. +""" +from __future__ import absolute_import +from cdsl.operands import Operand +from cdsl.typevar import TypeVar +from cdsl.instructions import Instruction, InstructionGroup +from cdsl.ti import SameWidth +import base.formats # noqa + +GROUP = InstructionGroup("primitive", "Primitive instruction set") + +BV = TypeVar('BV', 'A bitvector type.', bitvecs=True) +Real = TypeVar('Real', 'Any real type.', ints=True, floats=True, + bools=True, simd=True) + +x = Operand('x', BV, doc="A semantic value X") +y = Operand('x', BV, doc="A semantic value Y (same width as X)") +a = Operand('a', BV, doc="A semantic value A (same width as X)") + +real = Operand('real', Real, doc="A real cretonne value") +fromReal = Operand('fromReal', Real.to_bitvec(), + doc="A real cretonne value converted to a BV") + +prim_to_bv = Instruction( + 'prim_to_bv', r""" + Convert an SSA Value to a flat bitvector + """, + ins=(real), outs=(fromReal)) + +# Note that when converting from BV->real values, we use a constraint and not a +# derived function. This reflects that fact that to_bitvec() is not a +# bijection. +prim_from_bv = Instruction( + 'prim_from_bv', r""" + Convert a flat bitvector to a real SSA Value. + """, + ins=(x), outs=(real), + constraints=SameWidth(BV, Real)) + +xh = Operand('xh', BV.half_width(), + doc="A semantic value representing the upper half of X") +xl = Operand('xl', BV.half_width(), + doc="A semantic value representing the lower half of X") +bvsplit = Instruction( + 'bvsplit', r""" + """, + ins=(x), outs=(xh, xl)) + +xy = Operand('xy', BV.double_width(), + doc="A semantic value representing the concatenation of X and Y") +bvconcat = Instruction( + 'bvconcat', r""" + """, + ins=(x, y), outs=xy) + +bvadd = Instruction( + 'bvadd', r""" + Standard 2's complement addition. Equivalent to wrapping integer + addition: :math:`a := x + y \pmod{2^B}`. + + This instruction does not depend on the signed/unsigned interpretation + of the operands. + """, + ins=(x, y), outs=a) + +GROUP.close() diff --git a/lib/cretonne/meta/semantics/test_elaborate.py b/lib/cretonne/meta/semantics/test_elaborate.py new file mode 100644 index 0000000000..15d4178ae8 --- /dev/null +++ b/lib/cretonne/meta/semantics/test_elaborate.py @@ -0,0 +1,337 @@ +from __future__ import absolute_import +from base.instructions import vselect, vsplit, vconcat, iconst, iadd, bint +from base.instructions import b1, icmp, ireduce +from base.immediates import intcc +from base.types import i64, i8, b32, i32, i16, f32 +from cdsl.typevar import TypeVar +from cdsl.ast import Var +from cdsl.xform import Rtl +from unittest import TestCase +from .elaborate import cleanup_concrete_rtl, elaborate, is_rtl_concrete,\ + cleanup_semantics +from .primitives import prim_to_bv, bvsplit, prim_from_bv, bvconcat, bvadd +import base.semantics # noqa + + +def concrete_rtls_eq(r1, r2): + # type: (Rtl, Rtl) -> bool + """ + Check whether 2 concrete Rtls are equivalent. That is: + 1) They are structurally the same (i.e. there is a substitution between + them) + 2) Corresponding Vars between them have the same singleton type. + """ + assert is_rtl_concrete(r1) + assert is_rtl_concrete(r2) + + s = r1.substitution(r2, {}) + + if s is None: + return False + + for (v, v1) in s.items(): + if v.get_typevar().singleton_type() !=\ + v1.get_typevar().singleton_type(): + return False + + return True + + +class TestCleanupConcreteRtl(TestCase): + """ + Test cleanup_concrete_rtl(). cleanup_concrete_rtl() should take Rtls for + which we can infer a single concrete typing, and update the TypeVars + in-place to singleton TVs. + """ + def test_cleanup_concrete_rtl(self): + # type: () -> None + typ = i64.by(4) + x = Var('x') + lo = Var('lo') + hi = Var('hi') + + x.set_typevar(TypeVar.singleton(typ)) + r = Rtl( + (lo, hi) << vsplit(x), + ) + r1 = cleanup_concrete_rtl(r) + + s = r.substitution(r1, {}) + assert s is not None + assert s[x].get_typevar().singleton_type() == typ + assert s[lo].get_typevar().singleton_type() == i64.by(2) + assert s[hi].get_typevar().singleton_type() == i64.by(2) + + def test_cleanup_concrete_rtl_fail(self): + # type: () -> None + x = Var('x') + lo = Var('lo') + hi = Var('hi') + r = Rtl( + (lo, hi) << vsplit(x), + ) + + with self.assertRaises(AssertionError): + cleanup_concrete_rtl(r) + + def test_cleanup_concrete_rtl_ireduce(self): + # type: () -> None + x = Var('x') + y = Var('y') + x.set_typevar(TypeVar.singleton(i8.by(2))) + r = Rtl( + y << ireduce(x), + ) + + r1 = cleanup_concrete_rtl(r) + + s = r.substitution(r1, {}) + assert s is not None + assert s[x].get_typevar().singleton_type() == i8.by(2) + assert s[y].get_typevar().singleton_type() == i8.by(2) + + def test_cleanup_concrete_rtl_ireduce_bad(self): + # type: () -> None + x = Var('x') + y = Var('y') + x.set_typevar(TypeVar.singleton(i16.by(1))) + r = Rtl( + y << ireduce(x), + ) + + with self.assertRaises(AssertionError): + cleanup_concrete_rtl(r) + + def test_vselect_icmpimm(self): + # type: () -> None + x = Var('x') + y = Var('y') + z = Var('z') + w = Var('w') + v = Var('v') + zeroes = Var('zeroes') + imm0 = Var("imm0") + + zeroes.set_typevar(TypeVar.singleton(i32.by(4))) + z.set_typevar(TypeVar.singleton(f32.by(4))) + + r = Rtl( + zeroes << iconst(imm0), + y << icmp(intcc.eq, x, zeroes), + v << vselect(y, z, w), + ) + + r1 = cleanup_concrete_rtl(r) + + s = r.substitution(r1, {}) + assert s is not None + assert s[zeroes].get_typevar().singleton_type() == i32.by(4) + assert s[x].get_typevar().singleton_type() == i32.by(4) + assert s[y].get_typevar().singleton_type() == b32.by(4) + assert s[z].get_typevar().singleton_type() == f32.by(4) + assert s[w].get_typevar().singleton_type() == f32.by(4) + assert s[v].get_typevar().singleton_type() == f32.by(4) + + def test_bint(self): + # type: () -> None + x = Var('x') + y = Var('y') + z = Var('z') + w = Var('w') + v = Var('v') + u = Var('u') + + x.set_typevar(TypeVar.singleton(i32.by(8))) + z.set_typevar(TypeVar.singleton(i32.by(8))) + # TODO: Relax this to simd=True + v.set_typevar(TypeVar('v', '', bools=(1, 1), simd=(8, 8))) + + r = Rtl( + z << iadd(x, y), + w << bint(v), + u << iadd(z, w) + ) + + r1 = cleanup_concrete_rtl(r) + + s = r.substitution(r1, {}) + assert s is not None + assert s[x].get_typevar().singleton_type() == i32.by(8) + assert s[y].get_typevar().singleton_type() == i32.by(8) + assert s[z].get_typevar().singleton_type() == i32.by(8) + assert s[w].get_typevar().singleton_type() == i32.by(8) + assert s[u].get_typevar().singleton_type() == i32.by(8) + assert s[v].get_typevar().singleton_type() == b1.by(8) + + +class TestElaborate(TestCase): + """ + Test semantics elaboration. + """ + def setUp(self): + # type: () -> None + self.v0 = Var("v0") + self.v1 = Var("v1") + self.v2 = Var("v2") + self.v3 = Var("v3") + self.v4 = Var("v4") + self.v5 = Var("v5") + self.v6 = Var("v6") + self.v7 = Var("v7") + self.v8 = Var("v8") + self.v9 = Var("v9") + self.imm0 = Var("imm0") + self.IxN_nonscalar = TypeVar("IxN_nonscalar", "", ints=True, + scalars=False, simd=True) + self.TxN = TypeVar("TxN", "", ints=True, bools=True, floats=True, + scalars=False, simd=True) + self.b1 = TypeVar.singleton(b1) + + def test_elaborate_vsplit(self): + # type: () -> None + i32.by(4) # Make sure i32x4 exists. + i32.by(2) # Make sure i32x2 exists. + r = Rtl( + (self.v0, self.v1) << vsplit.i32x4(self.v2), + ) + sem = elaborate(cleanup_concrete_rtl(r)) + bvx = Var('bvx') + bvlo = Var('bvlo') + bvhi = Var('bvhi') + x = Var('x') + lo = Var('lo') + hi = Var('hi') + + assert concrete_rtls_eq(sem, cleanup_concrete_rtl(Rtl( + bvx << prim_to_bv.i32x4(x), + (bvlo, bvhi) << bvsplit.bv128(bvx), + lo << prim_from_bv.i32x2.bv64(bvlo), + hi << prim_from_bv.i32x2.bv64(bvhi)))) + + def test_elaborate_vconcat(self): + # type: () -> None + i32.by(4) # Make sure i32x4 exists. + i32.by(2) # Make sure i32x2 exists. + r = Rtl( + self.v0 << vconcat.i32x2(self.v1, self.v2), + ) + sem = elaborate(cleanup_concrete_rtl(r)) + bvx = Var('bvx') + bvlo = Var('bvlo') + bvhi = Var('bvhi') + x = Var('x') + lo = Var('lo') + hi = Var('hi') + + assert concrete_rtls_eq(sem, cleanup_concrete_rtl(Rtl( + bvlo << prim_to_bv.i32x2(lo), + bvhi << prim_to_bv.i32x2(hi), + bvx << bvconcat.bv64(bvlo, bvhi), + x << prim_from_bv.i32x4.bv128(bvx)))) + + 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') + + assert concrete_rtls_eq(sem, cleanup_concrete_rtl(Rtl( + bvx << prim_to_bv.i32(x), + bvy << prim_to_bv.i32(y), + bva << bvadd.bv32(bvx, bvy), + a << prim_from_bv.i32.bv32(bva)))) + + def test_elaborate_iadd_elaborate_1(self): + # type: () -> None + i32.by(2) # Make sure i32x2 exists. + r = Rtl( + self.v0 << iadd.i32x2(self.v1, self.v2), + ) + sem = cleanup_semantics(elaborate(cleanup_concrete_rtl(r)), + set([self.v0])) + x = Var('x') + y = Var('y') + a = Var('a') + bvx_1 = Var('bvx_1') + bvx_2 = Var('bvx_2') + bvx_5 = Var('bvx_5') + bvlo_1 = Var('bvlo_1') + bvlo_2 = Var('bvlo_2') + bvhi_1 = Var('bvhi_1') + bvhi_2 = Var('bvhi_2') + + bva_3 = Var('bva_3') + bva_4 = Var('bva_4') + + assert concrete_rtls_eq(sem, cleanup_concrete_rtl(Rtl( + bvx_1 << prim_to_bv.i32x2(x), + (bvlo_1, bvhi_1) << bvsplit.bv64(bvx_1), + bvx_2 << prim_to_bv.i32x2(y), + (bvlo_2, bvhi_2) << bvsplit.bv64(bvx_2), + bva_3 << bvadd.bv32(bvlo_1, bvlo_2), + bva_4 << bvadd.bv32(bvhi_1, bvhi_2), + bvx_5 << bvconcat.bv32(bva_3, bva_4), + a << prim_from_bv.i32x2.bv64(bvx_5)))) + + def test_elaborate_iadd_elaborate_2(self): + # type: () -> None + i8.by(4) # Make sure i32x2 exists. + r = Rtl( + self.v0 << iadd.i8x4(self.v1, self.v2), + ) + + sem = cleanup_semantics(elaborate(cleanup_concrete_rtl(r)), + set([self.v0])) + x = Var('x') + y = Var('y') + a = Var('a') + bvx_1 = Var('bvx_1') + bvx_2 = Var('bvx_2') + bvx_5 = Var('bvx_5') + bvx_10 = Var('bvx_10') + bvx_15 = Var('bvx_15') + + bvlo_1 = Var('bvlo_1') + bvlo_2 = Var('bvlo_2') + bvlo_6 = Var('bvlo_6') + bvlo_7 = Var('bvlo_7') + bvlo_11 = Var('bvlo_11') + bvlo_12 = Var('bvlo_12') + + bvhi_1 = Var('bvhi_1') + bvhi_2 = Var('bvhi_2') + bvhi_6 = Var('bvhi_6') + bvhi_7 = Var('bvhi_7') + bvhi_11 = Var('bvhi_11') + bvhi_12 = Var('bvhi_12') + + bva_8 = Var('bva_8') + bva_9 = Var('bva_9') + bva_13 = Var('bva_13') + bva_14 = Var('bva_14') + + assert concrete_rtls_eq(sem, cleanup_concrete_rtl(Rtl( + bvx_1 << prim_to_bv.i8x4(x), + (bvlo_1, bvhi_1) << bvsplit.bv32(bvx_1), + bvx_2 << prim_to_bv.i8x4(y), + (bvlo_2, bvhi_2) << bvsplit.bv32(bvx_2), + (bvlo_6, bvhi_6) << bvsplit.bv16(bvlo_1), + (bvlo_7, bvhi_7) << bvsplit.bv16(bvlo_2), + bva_8 << bvadd.bv8(bvlo_6, bvlo_7), + bva_9 << bvadd.bv8(bvhi_6, bvhi_7), + bvx_10 << bvconcat.bv8(bva_8, bva_9), + (bvlo_11, bvhi_11) << bvsplit.bv16(bvhi_1), + (bvlo_12, bvhi_12) << bvsplit.bv16(bvhi_2), + bva_13 << bvadd.bv8(bvlo_11, bvlo_12), + bva_14 << bvadd.bv8(bvhi_11, bvhi_12), + bvx_15 << bvconcat.bv8(bva_13, bva_14), + bvx_5 << bvconcat.bv16(bvx_10, bvx_15), + a << prim_from_bv.i8x4.bv32(bvx_5)))) diff --git a/lib/cretonne/meta/semantics/types.py b/lib/cretonne/meta/semantics/types.py new file mode 100644 index 0000000000..1221804fbd --- /dev/null +++ b/lib/cretonne/meta/semantics/types.py @@ -0,0 +1,9 @@ +""" +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)