Add insturction semantics. Add semantics for vsplit,vconcat,iadd. Add initial tests

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)))
+])

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):
     """

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)
 

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
         """

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):
     """

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())

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)

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)

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()

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))))

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)