Add primitive bvult, bvzeroext; Add semantics for bextend, icmp (partial - only for <) iadd_cout

This commit is contained in:
Dimo
2017-07-26 19:12:11 -07:00
committed by Jakob Stoklund Olesen
parent 3fd43fd006
commit e346bd50c8
2 changed files with 62 additions and 2 deletions

View File

@@ -1,7 +1,8 @@
from __future__ import absolute_import
from semantics.primitives import prim_to_bv, prim_from_bv, bvsplit, bvconcat,\
bvadd
from .instructions import vsplit, vconcat, iadd
bvadd, bvult, bvzeroext
from .instructions import vsplit, vconcat, iadd, iadd_cout, icmp, bextend
from .immediates import intcc
from cdsl.xform import Rtl
from cdsl.ast import Var
from cdsl.typevar import TypeSet
@@ -10,6 +11,9 @@ from cdsl.ti import InTypeset
x = Var('x')
y = Var('y')
a = Var('a')
b = Var('b')
c_out = Var('c_out')
bvc_out = Var('bvc_out')
xhi = Var('xhi')
yhi = Var('yhi')
ahi = Var('ahi')
@@ -21,6 +25,7 @@ hi = Var('hi')
bvx = Var('bvx')
bvy = Var('bvy')
bva = Var('bva')
bva_wide = Var('bva_wide')
bvlo = Var('bvlo')
bvhi = Var('bvhi')
@@ -56,3 +61,42 @@ iadd.set_semantics(
alo << iadd(xlo, ylo),
ahi << iadd(xhi, yhi),
a << vconcat(alo, ahi)))
iadd_cout.set_semantics(
(a, c_out) << iadd_cout(x, y),
Rtl(
bvx << prim_to_bv(x),
bvy << prim_to_bv(y),
bva << bvadd(bvx, bvy),
bvc_out << bvult(bva, bvx),
a << prim_from_bv(bva),
c_out << prim_from_bv(bvc_out)
))
bextend.set_semantics(
a << bextend(x),
(Rtl(
bvx << prim_to_bv(x),
bvy << bvzeroext(bvx),
a << prim_from_bv(bvy)
), [InTypeset(x.get_typevar(), ScalarTS)]),
Rtl((xlo, xhi) << vsplit(x),
alo << bextend(xlo),
ahi << bextend(xhi),
a << vconcat(alo, ahi)))
icmp.set_semantics(
a << icmp(intcc.ult, x, y),
(Rtl(
bvx << prim_to_bv(x),
bvy << prim_to_bv(y),
bva << bvult(bvx, bvy),
bva_wide << bvzeroext(bva),
a << prim_from_bv(bva_wide),
), [InTypeset(x.get_typevar(), ScalarTS)]),
Rtl((xlo, xhi) << vsplit(x),
(ylo, yhi) << vsplit(y),
alo << icmp(intcc.ult, xlo, ylo),
ahi << icmp(intcc.ult, xhi, yhi),
b << vconcat(alo, ahi),
a << bextend(b)))

View File

@@ -9,11 +9,13 @@ 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
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)
@@ -66,4 +68,18 @@ bvadd = Instruction(
""",
ins=(x, y), outs=a)
# Bitvector comparisons
cmp_res = Operand('cmp_res', BV1, doc="Single bit boolean")
bvult = Instruction(
'bvult', r"""Unsigned bitvector comparison""",
ins=(x, y), outs=cmp_res)
# 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))
GROUP.close()