cranelift-codegen 0.24.0

Low-level code generator library
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
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()