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

Fix for #141 (#142)

Browse Source 
* Add Atom and Literal base classes to CDSL Ast. Change substitution() and copy() on Def/Apply/Rtl to support substituting Var->Union[Var, Literal]. Check in Apply() constructor kinds of passed in Literals respect instruction signature

* Change verify_semantics to check all possible instantiations of enumerated immediates (needed to descrive icmp). Add all bitvector comparison primitives and bvite; Change set_semantics to optionally accept XForms; Add semantics for icmp; Fix typing errors in semantics/{smtlib, elaborate, __init__}.py after the change of VarMap->VarAtomMap

* Forgot macros.py

* Nit obscured by testing with mypy enabled present.

* Typo
This commit is contained in:
d1m0
2017-08-14 20:19:47 -07:00
committed by Jakob Stoklund Olesen
parent 591f6c1632
commit 66da171050
13 changed files with 415 additions and 137 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -1,9 +1,11 @@
"""Definitions for the semantics segment of the Cretonne 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 Var # 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
@@ -16,34 +18,60 @@ def verify_semantics(inst, src, xforms):
"""
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.
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 instruction
assert len(src.rtl) == 1
# 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 structurally equivalent to src
# 1) For all XForms x, x.src is a single instance of inst
for x in xforms:
assert src.substitution(x.src, {}) is not None,\
"XForm {} doesn't describe instruction {}.".format(x, src)
assert len(x.src.rtl) == 1 and x.src.rtl[0].expr.inst == inst
# 2) Any possible typing for the instruction should be covered by
# exactly ONE semantic XForm
src = src.copy({})
typenv = get_type_env(ti_rtl(src, TypeEnv()))
typenv.normalize()
typenv = typenv.extract()
variants = [src] # type: List[Rtl]
for t in typenv.concrete_typings():
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)
# 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
assert len(matching_xforms) == 1,\
("Possible typing {} of {} not matched by exactly one case " +
": {}").format(t, inst, matching_xforms)
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)

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

@@ -10,7 +10,7 @@ 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, VarMap # noqa
from cdsl.ast import Def, VarAtomMap # noqa
from cdsl.ti import VarTyping # noqa
except ImportError:
TYPE_CHECKING = False
@@ -34,7 +34,13 @@ def find_matching_xform(d):
if (subst is None):
continue
if x.ti.permits({subst[v]: tv for (v, tv) in typing.items()}):
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)
@@ -60,7 +66,7 @@ def cleanup_semantics(r, outputs):
...
"""
new_defs = [] # type: List[Def]
subst_m = {v: v for v in r.vars()} # type: VarMap
subst_m = {v: v for v in r.vars()} # type: VarAtomMap
definition = {} # type: Dict[Var, Def]
prim_to_bv_map = {} # type: Dict[Var, Def]

45
lib/cretonne/meta/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()

58
lib/cretonne/meta/semantics/primitives.py
View File

@@ -10,6 +10,8 @@ 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")
@@ -22,26 +24,40 @@ Real = TypeVar('Real', 'Any real type.', ints=True, floats=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 cretonne value")
fromReal = Operand('fromReal', Real.to_bitvec(),
doc="A real cretonne 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))
# 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=(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(),
@@ -67,12 +83,40 @@ bvadd = Instruction(
of the operands.
""",
ins=(x, y), outs=a)
#
# Bitvector comparisons
cmp_res = Operand('cmp_res', BV1, doc="Single bit boolean")
#
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 comparison""",
ins=(x, y), outs=cmp_res)
'bvult', r"""Unsigned bitvector less than""",
ins=(x, y), outs=cond)
# Extensions
ToBV = TypeVar('ToBV', 'A bitvector type.', bitvecs=True)

50
lib/cretonne/meta/semantics/smtlib.py
View File

@@ -14,7 +14,7 @@ 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 VarMap # noqa
from cdsl.ast import VarAtomMap, Atom # noqa
from cdsl.ti import VarTyping # noqa
if TYPE_CHECKING:
from z3 import ExprRef, BitVecRef # noqa
@@ -137,13 +137,13 @@ def to_smt(r):
def equivalent(r1, r2, inp_m, out_m):
# type: (Rtl, Rtl, VarMap, VarMap) -> List[ExprRef]
# type: (Rtl, Rtl, VarAtomMap, VarAtomMap) -> List[ExprRef]
"""
Given:
- concrete source Rtl r1
- concrete dest Rtl r2
- VarMap inp_m mapping r1's non-bitvector inputs to r2
- VarMap out_m mapping r1's non-bitvector outputs to 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.
@@ -156,17 +156,31 @@ def equivalent(r1, r2, inp_m, out_m):
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.
# 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()}
dst_m = {v: Var(v.name + ".b", v.get_typevar()) for v in r2.vars()}
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 = {src_m[k]: dst_m[v] for (k, v) in inp_m.items()}
out_m = {src_m[k]: dst_m[v] for (k, v) in out_m.items()}
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)
@@ -175,12 +189,14 @@ def equivalent(r1, r2, inp_m, out_m):
# Build an expression for the equality of real Cretone inputs of r1 and r2
args_eq_exp = [] # type: List[ExprRef]
for v in r1.free_vars():
args_eq_exp.append(mk_eq(m1[v], m2[inp_m[v]]))
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 Cretone 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 toghether
@@ -196,20 +212,22 @@ def xform_correct(x, 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()}
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 = {}
out_m = {}
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_m[v]] = dst_m[v]
inp_m[src_v] = dst_m[v]
elif v.is_output():
out_m[src_m[v]] = dst_m[v]
out_m[src_v] = dst_m[v]
# Get the primitive semantic Rtls for src and dst
prim_src = elaborate(src)

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

@@ -1,7 +1,7 @@
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
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
@@ -9,7 +9,7 @@ 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
bvult, bv_from_imm64, bvite
import base.semantics # noqa
@@ -366,9 +366,12 @@ class TestElaborate(TestCase):
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),
)
@@ -378,10 +381,12 @@ class TestElaborate(TestCase):
bvx << prim_to_bv.i32(x),
bvy << prim_to_bv.i32(y),
bva << bvadd.bv32(bvx, bvy),
bvc_out << bvult.bv32(bva, bvx),
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)