T0b1/wasmtime
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Documentation nits; Sematnics syntax cleanup

Browse Source
This commit is contained in:
Dimo
2017-07-21 16:46:20 -07:00
committed by Jakob Stoklund Olesen
parent 40c86d58b9
commit 9258283e14
10 changed files with 103 additions and 94 deletions
Download Patch File Download Diff File Expand all files Collapse all files

29
lib/cretonne/meta/base/semantics.py
View File

@@ -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),
(lo, hi) << vsplit(x),
Rtl(
bvx << prim_to_bv(x),
(bvlo, bvhi) << bvsplit(bvx),
lo << prim_from_bv(bvlo),
hi << prim_from_bv(bvhi))))
hi << prim_from_bv(bvhi)
))
vconcat.set_semantics(
XForm(Rtl(x << vconcat(lo, hi)),
Rtl(bvlo << prim_to_bv(lo),
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 << prim_from_bv(bvx)
))
iadd.set_semantics([
XForm(Rtl(a << iadd(x, y)),
Rtl(bvx << prim_to_bv(x),
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)),
constraints=[InTypeset(x.get_typevar(), ScalarTS)]),
XForm(Rtl(a << iadd(x, y)),
[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)))
])

14
lib/cretonne/meta/cdsl/ast.py
View File

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

25
lib/cretonne/meta/cdsl/instructions.py
View File

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

18
lib/cretonne/meta/cdsl/types.py
View File

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

8
lib/cretonne/meta/cdsl/typevar.py
View File

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

2
lib/cretonne/meta/cdsl/xform.py
View File

@@ -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([]))

59
lib/cretonne/meta/semantics/__init__.py
View File

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

1
lib/cretonne/meta/semantics/elaborate.py
View File

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

8
lib/cretonne/meta/semantics/test_elaborate.py
View File

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

9
lib/cretonne/meta/semantics/types.py
View File

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