From e346bd50c89cddbc520a8c4d98d7d11de08cc5fc Mon Sep 17 00:00:00 2001 From: Dimo Date: Wed, 26 Jul 2017 19:12:11 -0700 Subject: [PATCH] Add primitive bvult, bvzeroext; Add semantics for bextend, icmp (partial - only for <) iadd_cout --- lib/cretonne/meta/base/semantics.py | 48 ++++++++++++++++++++++- lib/cretonne/meta/semantics/primitives.py | 16 ++++++++ 2 files changed, 62 insertions(+), 2 deletions(-) diff --git a/lib/cretonne/meta/base/semantics.py b/lib/cretonne/meta/base/semantics.py index b4315d8255..cdf071f7d9 100644 --- a/lib/cretonne/meta/base/semantics.py +++ b/lib/cretonne/meta/base/semantics.py @@ -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))) diff --git a/lib/cretonne/meta/semantics/primitives.py b/lib/cretonne/meta/semantics/primitives.py index 70fc196d5d..62d936bc31 100644 --- a/lib/cretonne/meta/semantics/primitives.py +++ b/lib/cretonne/meta/semantics/primitives.py @@ -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()