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

moved crates in lib/ to src/, renamed crates, modified some files' text (#660)

Browse Source 
moved crates in lib/ to src/, renamed crates, modified some files' text (#660)
This commit is contained in:
lazypassion
2019-01-28 18:56:54 -05:00
committed by Dan Gohman
parent 54959cf5bb
commit 747ad3c4c5
508 changed files with 94 additions and 92 deletions
Download Patch File Download Diff File Expand all files Collapse all files

77
cranelift/codegen/meta-python/semantics/__init__.py Normal file
View File

@@ -0,0 +1,77 @@
"""Definitions for the semantics segment of the Cranelift language."""
from cdsl.ti import TypeEnv, ti_rtl, get_type_env
from cdsl.operands import ImmediateKind
from cdsl.ast import Var
try:
from typing import List, Dict, Tuple # noqa
from cdsl.ast import VarAtomMap # 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, src, xforms):
# type: (Instruction, Rtl, InstructionSemantics) -> None
"""
Verify that the semantics transforms in xforms correctly describe the
instruction described by the src Rtl. This involves checking that:
0) src is a single instance of inst
1) For all x \\in xforms x.src is a single instance of inst
2) For any concrete values V of Literals in inst:
For all concrete typing T of inst:
Exists single x \\in xforms that applies to src conretazied to
V and T
"""
# 0) The source rtl is always a single instance of inst
assert len(src.rtl) == 1 and src.rtl[0].expr.inst == inst
# 1) For all XForms x, x.src is a single instance of inst
for x in xforms:
assert len(x.src.rtl) == 1 and x.src.rtl[0].expr.inst == inst
variants = [src] # type: List[Rtl]
# 2) For all enumerated immediates, compute all the possible
# versions of src with the concrete value filled in.
for i in inst.imm_opnums:
op = inst.ins[i]
if not (isinstance(op.kind, ImmediateKind) and
op.kind.is_enumerable()):
continue
new_variants = [] # type: List[Rtl]
for rtl_var in variants:
s = {v: v for v in rtl_var.vars()} # type: VarAtomMap
arg = rtl_var.rtl[0].expr.args[i]
assert isinstance(arg, Var)
for val in op.kind.possible_values():
s[arg] = val
new_variants.append(rtl_var.copy(s))
variants = new_variants
# For any possible version of the src with concrete enumerated immediates
for src in variants:
# 2) Any possible typing should be covered by exactly ONE semantic
# XForm
src = src.copy({})
typenv = get_type_env(ti_rtl(src, TypeEnv()))
typenv.normalize()
typenv = typenv.extract()
for t in typenv.concrete_typings():
matching_xforms = [] # type: List[XForm]
for x in xforms:
if src.substitution(x.src, {}) is None:
continue
# 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, src.rtl[0], matching_xforms)

146
cranelift/codegen/meta-python/semantics/elaborate.py Normal file
View File

@@ -0,0 +1,146 @@
"""
Tools to elaborate a given Rtl with concrete types into its semantically
equivalent primitive version. Its elaborated primitive version contains only
primitive cranelift instructions, which map well to SMTLIB functions.
"""
from .primitives import GROUP as PRIMITIVES, prim_to_bv, prim_from_bv
from cdsl.xform import Rtl
from cdsl.ast import Var
try:
from typing import TYPE_CHECKING, Dict, Union, List, Set, Tuple # noqa
from cdsl.xform import XForm # noqa
from cdsl.ast import Def, VarAtomMap # noqa
from cdsl.ti import VarTyping # noqa
except ImportError:
TYPE_CHECKING = False
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], {})
# There may not be a substitution if there are concrete Enumerator
# values in the src pattern. (e.g. specifying the semantics of icmp.eq,
# icmp.ge... as separate transforms)
if (subst is None):
continue
inner_typing = {} # type: VarTyping
for (v, tv) in typing.items():
inner_v = subst[v]
assert isinstance(inner_v, Var)
inner_typing[inner_v] = tv
if x.ti.permits(inner_typing):
res.append(x)
assert len(res) == 1, "Couldn't find semantic transform for {}".format(d)
return res[0]
def cleanup_semantics(r, outputs):
# type: (Rtl, Set[Var]) -> Rtl
"""
The elaboration process creates a lot of redundant prim_to_bv conversions.
Cleanup the following cases:
1) prim_to_bv/prim_from_bv pair:
a.0 << prim_from_bv(bva.0)
...
bva.1 << prim_to_bv(a.0) <-- redundant, replace by bva.0
...
2) prim_to_bv/prim_to-bv pair:
bva.0 << prim_to_bv(a)
...
bva.1 << prim_to_bv(a) <-- redundant, replace by bva.0
...
"""
new_defs = [] # type: List[Def]
subst_m = {v: v for v in r.vars()} # type: VarAtomMap
definition = {} # type: Dict[Var, Def]
prim_to_bv_map = {} # 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):
arg = d.expr.args[0]
df = d.defs[0]
assert isinstance(arg, Var)
if arg in definition:
def_loc = definition[arg]
if def_loc.expr.inst == prim_from_bv:
assert isinstance(def_loc.expr.args[0], Var)
subst_m[df] = def_loc.expr.args[0]
continue
if arg in prim_to_bv_map:
subst_m[df] = prim_to_bv_map[arg].defs[0]
continue
prim_to_bv_map[arg] = d
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)
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
res = Rtl(*r.rtl)
outputs = res.definitions()
while not fp:
assert res.is_concrete()
new_defs = [] # type: List[Def]
fp = True
for d in res.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)
res.rtl = tuple(new_defs)
return cleanup_semantics(res, outputs)

45
cranelift/codegen/meta-python/semantics/macros.py Normal file
View File

@@ -0,0 +1,45 @@
"""
Useful semantics "macro" instructions built on top of
the primitives.
"""
from __future__ import absolute_import
from cdsl.operands import Operand
from cdsl.typevar import TypeVar
from cdsl.instructions import Instruction, InstructionGroup
from base.types import b1
from base.immediates import imm64
from cdsl.ast import Var
from cdsl.xform import Rtl
from semantics.primitives import bv_from_imm64, bvite
import base.formats # noqa
GROUP = InstructionGroup("primitive_macros", "Semantic macros instruction set")
AnyBV = TypeVar('AnyBV', bitvecs=True, doc="")
x = Var('x')
y = Var('y')
imm = Var('imm')
a = Var('a')
#
# Bool-to-bv1
#
BV1 = TypeVar("BV1", bitvecs=(1, 1), doc="")
bv1_op = Operand('bv1_op', BV1, doc="")
cond_op = Operand("cond", b1, doc="")
bool2bv = Instruction(
'bool2bv', r"""Convert a b1 value to a 1-bit BV""",
ins=cond_op, outs=bv1_op)
v1 = Var('v1')
v2 = Var('v2')
bvone = Var('bvone')
bvzero = Var('bvzero')
bool2bv.set_semantics(
v1 << bool2bv(v2),
Rtl(
bvone << bv_from_imm64(imm64(1)),
bvzero << bv_from_imm64(imm64(0)),
v1 << bvite(v2, bvone, bvzero)
))
GROUP.close()

133
cranelift/codegen/meta-python/semantics/primitives.py Normal file
View File

@@ -0,0 +1,133 @@
"""
Cranelift 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 WiderOrEq
from base.types import b1
from base.immediates import imm64
import base.formats # noqa
GROUP = InstructionGroup("primitive", "Primitive instruction set")
BV = TypeVar('BV', 'A bitvector type.', bitvecs=True)
BV1 = TypeVar('BV1', 'A single bit bitvector.', bitvecs=(1, 1))
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)")
cond = Operand('b', TypeVar.singleton(b1), doc='A b1 value')
real = Operand('real', Real, doc="A real cranelift value")
fromReal = Operand('fromReal', Real.to_bitvec(),
doc="A real cranelift value converted to a BV")
#
# BV Conversion/Materialization
#
prim_to_bv = Instruction(
'prim_to_bv', r"""
Convert an SSA Value to a flat bitvector
""",
ins=(real), outs=(fromReal))
prim_from_bv = Instruction(
'prim_from_bv', r"""
Convert a flat bitvector to a real SSA Value.
""",
ins=(fromReal), outs=(real))
N = Operand('N', imm64)
bv_from_imm64 = Instruction(
'bv_from_imm64', r"""Materialize an imm64 as a bitvector.""",
ins=(N), outs=a)
#
# Generics
#
bvite = Instruction(
'bvite', r"""Bitvector ternary operator""",
ins=(cond, x, y), outs=a)
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)
#
# Bitvector comparisons
#
bveq = Instruction(
'bveq', r"""Unsigned bitvector equality""",
ins=(x, y), outs=cond)
bvne = Instruction(
'bveq', r"""Unsigned bitvector inequality""",
ins=(x, y), outs=cond)
bvsge = Instruction(
'bvsge', r"""Signed bitvector greater or equal""",
ins=(x, y), outs=cond)
bvsgt = Instruction(
'bvsgt', r"""Signed bitvector greater than""",
ins=(x, y), outs=cond)
bvsle = Instruction(
'bvsle', r"""Signed bitvector less than or equal""",
ins=(x, y), outs=cond)
bvslt = Instruction(
'bvslt', r"""Signed bitvector less than""",
ins=(x, y), outs=cond)
bvuge = Instruction(
'bvuge', r"""Unsigned bitvector greater or equal""",
ins=(x, y), outs=cond)
bvugt = Instruction(
'bvugt', r"""Unsigned bitvector greater than""",
ins=(x, y), outs=cond)
bvule = Instruction(
'bvule', r"""Unsigned bitvector less than or equal""",
ins=(x, y), outs=cond)
bvult = Instruction(
'bvult', r"""Unsigned bitvector less than""",
ins=(x, y), outs=cond)
# Extensions
ToBV = TypeVar('ToBV', 'A bitvector type.', bitvecs=True)
x1 = Operand('x1', ToBV, doc="")
bvzeroext = Instruction(
'bvzeroext', r"""Unsigned bitvector extension""",
ins=x, outs=x1, constraints=WiderOrEq(ToBV, BV))
bvsignext = Instruction(
'bvsignext', r"""Signed bitvector extension""",
ins=x, outs=x1, constraints=WiderOrEq(ToBV, BV))
GROUP.close()

241
cranelift/codegen/meta-python/semantics/smtlib.py Normal file
View File

@@ -0,0 +1,241 @@
"""
Tools to emit SMTLIB bitvector queries encoding concrete RTLs containing only
primitive instructions.
"""
from .primitives import GROUP as PRIMITIVES, prim_from_bv, prim_to_bv, bvadd,\
bvult, bvzeroext, bvsplit, bvconcat, bvsignext
from cdsl.ast import Var
from cdsl.types import BVType
from .elaborate import elaborate
from z3 import BitVec, ZeroExt, SignExt, And, Extract, Concat, Not, Solver,\
unsat, BoolRef, BitVecVal, If
from z3.z3core import Z3_mk_eq
try:
from typing import TYPE_CHECKING, Tuple, Dict, List # noqa
from cdsl.xform import Rtl, XForm # noqa
from cdsl.ast import VarAtomMap, Atom # noqa
from cdsl.ti import VarTyping # noqa
if TYPE_CHECKING:
from z3 import ExprRef, BitVecRef # noqa
Z3VarMap = Dict[Var, BitVecRef]
except ImportError:
TYPE_CHECKING = False
# Use this for constructing a == b instead of == since MyPy doesn't
# accept overloading of __eq__ that doesn't return bool
def mk_eq(e1, e2):
# type: (ExprRef, ExprRef) -> ExprRef
"""Return a z3 expression equivalent to e1 == e2"""
return BoolRef(Z3_mk_eq(e1.ctx_ref(), e1.as_ast(), e2.as_ast()), e1.ctx)
def to_smt(r):
# type: (Rtl) -> Tuple[List[ExprRef], Z3VarMap]
"""
Encode a concrete primitive Rtl r sa z3 query.
Returns a tuple (query, var_m) where:
- query is a list of z3 expressions
- var_m is a map from Vars v with non-BVType to their correspodning z3
bitvector variable.
"""
assert r.is_concrete()
# Should contain only primitives
primitives = set(PRIMITIVES.instructions)
assert set(d.expr.inst for d in r.rtl).issubset(primitives)
q = [] # type: List[ExprRef]
m = {} # type: Z3VarMap
# Build declarations for any bitvector Vars
var_to_bv = {} # type: Z3VarMap
for v in r.vars():
typ = v.get_typevar().singleton_type()
if not isinstance(typ, BVType):
continue
var_to_bv[v] = BitVec(v.name, typ.bits)
# Encode each instruction as a equality assertion
for d in r.rtl:
inst = d.expr.inst
exp = None # type: ExprRef
# For prim_to_bv/prim_from_bv just update var_m. No assertion needed
if inst == prim_to_bv:
assert isinstance(d.expr.args[0], Var)
m[d.expr.args[0]] = var_to_bv[d.defs[0]]
continue
if inst == prim_from_bv:
assert isinstance(d.expr.args[0], Var)
m[d.defs[0]] = var_to_bv[d.expr.args[0]]
continue
if inst in [bvadd, bvult]: # Binary instructions
assert len(d.expr.args) == 2 and len(d.defs) == 1
lhs = d.expr.args[0]
rhs = d.expr.args[1]
df = d.defs[0]
assert isinstance(lhs, Var) and isinstance(rhs, Var)
if inst == bvadd: # Normal binary - output type same as args
exp = (var_to_bv[lhs] + var_to_bv[rhs])
else:
assert inst == bvult
exp = (var_to_bv[lhs] < var_to_bv[rhs])
# Comparison binary - need to convert bool to BitVec 1
exp = If(exp, BitVecVal(1, 1), BitVecVal(0, 1))
exp = mk_eq(var_to_bv[df], exp)
elif inst == bvzeroext:
arg = d.expr.args[0]
df = d.defs[0]
assert isinstance(arg, Var)
fromW = arg.get_typevar().singleton_type().width()
toW = df.get_typevar().singleton_type().width()
exp = mk_eq(var_to_bv[df], ZeroExt(toW-fromW, var_to_bv[arg]))
elif inst == bvsignext:
arg = d.expr.args[0]
df = d.defs[0]
assert isinstance(arg, Var)
fromW = arg.get_typevar().singleton_type().width()
toW = df.get_typevar().singleton_type().width()
exp = mk_eq(var_to_bv[df], SignExt(toW-fromW, var_to_bv[arg]))
elif inst == bvsplit:
arg = d.expr.args[0]
assert isinstance(arg, Var)
arg_typ = arg.get_typevar().singleton_type()
width = arg_typ.width()
assert (width % 2 == 0)
lo = d.defs[0]
hi = d.defs[1]
exp = And(mk_eq(var_to_bv[lo],
Extract(width//2-1, 0, var_to_bv[arg])),
mk_eq(var_to_bv[hi],
Extract(width-1, width//2, var_to_bv[arg])))
elif inst == bvconcat:
assert isinstance(d.expr.args[0], Var) and \
isinstance(d.expr.args[1], Var)
lo = d.expr.args[0]
hi = d.expr.args[1]
df = d.defs[0]
# Z3 Concat expects hi bits first, then lo bits
exp = mk_eq(var_to_bv[df], Concat(var_to_bv[hi], var_to_bv[lo]))
else:
assert False, "Unknown primitive instruction {}".format(inst)
q.append(exp)
return (q, m)
def equivalent(r1, r2, inp_m, out_m):
# type: (Rtl, Rtl, VarAtomMap, VarAtomMap) -> List[ExprRef]
"""
Given:
- concrete source Rtl r1
- concrete dest Rtl r2
- VarAtomMap inp_m mapping r1's non-bitvector inputs to r2
- VarAtomMap out_m mapping r1's non-bitvector outputs to r2
Build a query checking whether r1 and r2 are semantically equivalent.
If the returned query is unsatisfiable, then r1 and r2 are equivalent.
Otherwise, the satisfying example for the query gives us values
for which the two Rtls disagree.
"""
# Sanity - inp_m is a bijection from the set of inputs of r1 to the set of
# inputs of r2
assert set(r1.free_vars()) == set(inp_m.keys())
assert set(r2.free_vars()) == set(inp_m.values())
# Note that the same rule is not expected to hold for out_m due to
# temporaries/intermediates. out_m specified which values are enough for
# equivalence.
# Rename the vars in r1 and r2 with unique suffixes to avoid conflicts
src_m = {v: Var(v.name + ".a", v.get_typevar()) for v in r1.vars()} # type: VarAtomMap # noqa
dst_m = {v: Var(v.name + ".b", v.get_typevar()) for v in r2.vars()} # type: VarAtomMap # noqa
r1 = r1.copy(src_m)
r2 = r2.copy(dst_m)
def _translate(m, k_m, v_m):
# type: (VarAtomMap, VarAtomMap, VarAtomMap) -> VarAtomMap
"""Obtain a new map from m, by mapping m's keys with k_m and m's values
with v_m"""
res = {} # type: VarAtomMap
for (k, v) in m1.items():
new_k = k_m[k]
new_v = v_m[v]
assert isinstance(new_k, Var)
res[new_k] = new_v
return res
# Convert inp_m, out_m in terms of variables with the .a/.b suffixes
inp_m = _translate(inp_m, src_m, dst_m)
out_m = _translate(out_m, src_m, dst_m)
# Encode r1 and r2 as SMT queries
(q1, m1) = to_smt(r1)
(q2, m2) = to_smt(r2)
# Build an expression for the equality of real Cranelift inputs of
# r1 and r2
args_eq_exp = [] # type: List[ExprRef]
for (v1, v2) in inp_m.items():
assert isinstance(v2, Var)
args_eq_exp.append(mk_eq(m1[v1], m2[v2]))
# Build an expression for the equality of real Cranelift outputs of
# r1 and r2
results_eq_exp = [] # type: List[ExprRef]
for (v1, v2) in out_m.items():
assert isinstance(v2, Var)
results_eq_exp.append(mk_eq(m1[v1], m2[v2]))
# Put the whole query together
return q1 + q2 + args_eq_exp + [Not(And(*results_eq_exp))]
def xform_correct(x, typing):
# type: (XForm, VarTyping) -> bool
"""
Given an XForm x and a concrete variable typing for x check whether x is
semantically preserving for the concrete typing.
"""
assert x.ti.permits(typing)
# Create copies of the x.src and x.dst with their concrete types
src_m = {v: Var(v.name, typing[v]) for v in x.src.vars()} # type: VarAtomMap # noqa
src = x.src.copy(src_m)
dst = x.apply(src)
dst_m = x.dst.substitution(dst, {})
# Build maps for the inputs/outputs for src->dst
inp_m = {} # type: VarAtomMap
out_m = {} # type: VarAtomMap
for v in x.src.vars():
src_v = src_m[v]
assert isinstance(src_v, Var)
if v.is_input():
inp_m[src_v] = dst_m[v]
elif v.is_output():
out_m[src_v] = dst_m[v]
# Get the primitive semantic Rtls for src and dst
prim_src = elaborate(src)
prim_dst = elaborate(dst)
asserts = equivalent(prim_src, prim_dst, inp_m, out_m)
s = Solver()
s.add(*asserts)
return s.check() == unsat

392
cranelift/codegen/meta-python/semantics/test_elaborate.py Normal file
View File

@@ -0,0 +1,392 @@
from __future__ import absolute_import
from base.instructions import vselect, vsplit, vconcat, iconst, iadd, bint
from base.instructions import b1, icmp, ireduce, iadd_cout
from base.immediates import intcc, imm64
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 elaborate
from .primitives import prim_to_bv, bvsplit, prim_from_bv, bvconcat, bvadd, \
bvult, bv_from_imm64, bvite
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 r1.is_concrete()
assert r2.is_concrete()
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')
r = Rtl(
(lo, hi) << vsplit(x),
)
r1 = r.copy({})
s = r.substitution(r1, {})
s[x].set_typevar(TypeVar.singleton(typ))
r1.cleanup_concrete_rtl()
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):
r.cleanup_concrete_rtl()
def test_cleanup_concrete_rtl_ireduce(self):
# type: () -> None
x = Var('x')
y = Var('y')
r = Rtl(
y << ireduce(x),
)
r1 = r.copy({})
s = r.substitution(r1, {})
s[x].set_typevar(TypeVar.singleton(i8.by(2)))
r1.cleanup_concrete_rtl()
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):
r.cleanup_concrete_rtl()
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")
r = Rtl(
zeroes << iconst(imm0),
y << icmp(intcc.eq, x, zeroes),
v << vselect(y, z, w),
)
r1 = r.copy({})
s = r.substitution(r1, {})
s[zeroes].set_typevar(TypeVar.singleton(i32.by(4)))
s[z].set_typevar(TypeVar.singleton(f32.by(4)))
r1.cleanup_concrete_rtl()
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')
r = Rtl(
z << iadd(x, y),
w << bint(v),
u << iadd(z, w)
)
r1 = r.copy({})
s = r.substitution(r1, {})
s[x].set_typevar(TypeVar.singleton(i32.by(8)))
s[z].set_typevar(TypeVar.singleton(i32.by(8)))
# TODO: Relax this to simd=True
s[v].set_typevar(TypeVar('v', '', bools=(1, 1), simd=(8, 8)))
r1.cleanup_concrete_rtl()
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),
)
r.cleanup_concrete_rtl()
sem = elaborate(r)
bvx = Var('bvx')
bvlo = Var('bvlo')
bvhi = Var('bvhi')
x = Var('x')
lo = Var('lo')
hi = Var('hi')
exp = Rtl(
bvx << prim_to_bv.i32x4(x),
(bvlo, bvhi) << bvsplit.bv128(bvx),
lo << prim_from_bv.i32x2(bvlo),
hi << prim_from_bv.i32x2(bvhi)
)
exp.cleanup_concrete_rtl()
assert concrete_rtls_eq(sem, exp)
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),
)
r.cleanup_concrete_rtl()
sem = elaborate(r)
bvx = Var('bvx')
bvlo = Var('bvlo')
bvhi = Var('bvhi')
x = Var('x')
lo = Var('lo')
hi = Var('hi')
exp = Rtl(
bvlo << prim_to_bv.i32x2(lo),
bvhi << prim_to_bv.i32x2(hi),
bvx << bvconcat.bv64(bvlo, bvhi),
x << prim_from_bv.i32x4(bvx)
)
exp.cleanup_concrete_rtl()
assert concrete_rtls_eq(sem, exp)
def test_elaborate_iadd_simple(self):
# type: () -> None
i32.by(2) # Make sure i32x2 exists.
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),
)
r.cleanup_concrete_rtl()
sem = elaborate(r)
exp = Rtl(
bvx << prim_to_bv.i32(x),
bvy << prim_to_bv.i32(y),
bva << bvadd.bv32(bvx, bvy),
a << prim_from_bv.i32(bva)
)
exp.cleanup_concrete_rtl()
assert concrete_rtls_eq(sem, exp)
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),
)
r.cleanup_concrete_rtl()
sem = elaborate(r)
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')
exp = 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(bvx_5)
)
exp.cleanup_concrete_rtl()
assert concrete_rtls_eq(sem, exp)
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),
)
r.cleanup_concrete_rtl()
sem = elaborate(r)
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')
exp = 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(bvx_5)
)
exp.cleanup_concrete_rtl()
assert concrete_rtls_eq(sem, exp)
def test_elaborate_iadd_cout_simple(self):
# type: () -> None
x = Var('x')
y = Var('y')
a = Var('a')
c_out = Var('c_out')
bvc_out = Var('bvc_out')
bc_out = Var('bc_out')
bvx = Var('bvx')
bvy = Var('bvy')
bva = Var('bva')
bvone = Var('bvone')
bvzero = Var('bvzero')
r = Rtl(
(a, c_out) << iadd_cout.i32(x, y),
)
r.cleanup_concrete_rtl()
sem = elaborate(r)
exp = Rtl(
bvx << prim_to_bv.i32(x),
bvy << prim_to_bv.i32(y),
bva << bvadd.bv32(bvx, bvy),
bc_out << bvult.bv32(bva, bvx),
bvone << bv_from_imm64(imm64(1)),
bvzero << bv_from_imm64(imm64(0)),
bvc_out << bvite(bc_out, bvone, bvzero),
a << prim_from_bv.i32(bva),
c_out << prim_from_bv.b1(bvc_out)
)
exp.cleanup_concrete_rtl()
assert concrete_rtls_eq(sem, exp)