arxpy.bitvector.operation module

Provide the common bit-vector operators.

class arxpy.bitvector.operation.Operation

Bases: arxpy.bitvector.core.Term

Represent bit-vector operations.

A bit-vector operation takes some bit-vector operands (i.e. Term) and some scalar operands (i.e. int), and returns a single bit-vector term. Often, operator is used to denote the operation as a function (without operands) and operation is used to denote the application of a operator to some operands.

This class is not meant to be instantiated but to provide a base class for the different types of bit-vector operations.

arity

a pair of number specifying the number of bit-vector operands (at least one) and scalar operands.

is_symmetric

True if the operator is symmetric with respect to its operands. Operators with scalar operands cannot be symmetric.

is_simple

True if the operator is simple, that is, all its operands are bit-vector of the same width. Simple operators allow Automatic Constant Conversion, that is, instead of passing all arguments as bit-vector types, it is possible to pass arguments as plain integers.

>>> from arxpy.bitvector.core import Constant
>>> (Constant(1, 8) + 1).vrepr()
'Constant(0b00000010, width=8)'

operand_types

a list specifying the types of the operands (optional if all operands are bit-vectors)

alt_name

an alternative name used when printing (optional)

unary_symbol

a symbol used when printing (optional)

infix_symbol

a symbol used when printing (optional)

classmethod condition(*args)

Check if the operands verify the restrictions of the operator.

output_width()

Return the bit-width of the resulting bit-vector.

classmethod eval(*args)

Evaluate the operator with given operands.

This is an internal method. To evaluate a bit-vector operation, use the operator ().

classmethod class_key()

Return the key (identifier) of the class for sorting.

property formula_size

The formula size of the operation.

class arxpy.bitvector.operation.BvNot

Bases: arxpy.bitvector.operation.Operation

Bitwise negation operation.

It overrides the operator ~. See Operation for more information.

>>> from arxpy.bitvector.core import Constant, Variable
>>> from arxpy.bitvector.operation import BvNot
>>> BvNot(Constant(0b1010101, 7))
0b0101010
>>> ~Constant(0b1010101, 7)
0b0101010
>>> ~Variable("x", 8)
~x

classmethod output_width(x)

Return the bit-width of the resulting bit-vector.

classmethod eval(x)

Evaluate the operator with given operands.

This is an internal method. To evaluate a bit-vector operation, use the operator ().

class arxpy.bitvector.operation.BvAnd

Bases: arxpy.bitvector.operation.Operation

Bitwise AND (logical conjunction) operation.

It overrides the operator & and provides Automatic Constant Conversion. See Operation for more information.

>>> from arxpy.bitvector.core import Constant, Variable
>>> from arxpy.bitvector.operation import BvAnd
>>> BvAnd(Constant(5, 8), Constant(3, 8))
0x01
>>> BvAnd(Constant(5, 8), 3)
0x01
>>> Constant(5, 8) & 3
0x01
>>> Variable("x", 8) & Variable("y", 8)
x & y

classmethod condition(x, y)

Check if the operands verify the restrictions of the operator.

classmethod output_width(x, y)

Return the bit-width of the resulting bit-vector.

classmethod eval(x, y)

Evaluate the operator with given operands.

This is an internal method. To evaluate a bit-vector operation, use the operator ().

class arxpy.bitvector.operation.BvOr

Bases: arxpy.bitvector.operation.Operation

Bitwise OR (logical disjunction) operation.

It overrides the operator | and provides Automatic Constant Conversion. See Operation for more information.

>>> from arxpy.bitvector.core import Constant, Variable
>>> from arxpy.bitvector.operation import BvOr
>>> BvOr(Constant(5, 8), Constant(3, 8))
0x07
>>> BvOr(Constant(5, 8), 3)
0x07
>>> Constant(5, 8) | 3
0x07
>>> Variable("x", 8) | Variable("y", 8)
x | y

classmethod condition(x, y)

Check if the operands verify the restrictions of the operator.

classmethod output_width(x, y)

Return the bit-width of the resulting bit-vector.

classmethod eval(x, y)

Evaluate the operator with given operands.

This is an internal method. To evaluate a bit-vector operation, use the operator ().

class arxpy.bitvector.operation.BvXor

Bases: arxpy.bitvector.operation.Operation

Bitwise XOR (exclusive-or) operation.

It overrides the operator ^ and provides Automatic Constant Conversion. See Operation for more information.

>>> from arxpy.bitvector.core import Constant, Variable
>>> from arxpy.bitvector.operation import BvXor
>>> BvXor(Constant(5, 8), Constant(3, 8))
0x06
>>> BvXor(Constant(5, 8), 3)
0x06
>>> Constant(5, 8) ^ 3
0x06
>>> Variable("x", 8) ^ Variable("y", 8)
x ^ y

classmethod condition(x, y)

Check if the operands verify the restrictions of the operator.

classmethod output_width(x, y)

Return the bit-width of the resulting bit-vector.

classmethod eval(x, y)

Evaluate the operator with given operands.

This is an internal method. To evaluate a bit-vector operation, use the operator ().

class arxpy.bitvector.operation.BvComp

Bases: arxpy.bitvector.operation.Operation

Equality operator.

Provides Automatic Constant Conversion. See Operation for more information.

>>> from arxpy.bitvector.core import Constant, Variable
>>> from arxpy.bitvector.operation import BvComp
>>> BvComp(Constant(1, 8), Constant(2, 8))
0b0
>>> BvComp(Constant(1, 8), 2)
0b0
>>> BvComp(Constant(1, 8), Variable("y", 8))
0x01 == y

The operator == is used for exact structural equality testing and it returns either True or False. On the other hand, BvComp performs symbolic equality testing and it leaves the relation unevaluated if it cannot prove the objects are equal (or unequal).

>>> Variable("x", 8) == Variable("y", 8)
False
>>> BvComp(Variable("x", 8), Variable("y", 8))  # symbolic equality
x == y

classmethod condition(x, y)

Check if the operands verify the restrictions of the operator.

classmethod output_width(x, y)

Return the bit-width of the resulting bit-vector.

classmethod eval(x, y)

Evaluate the operator with given operands.

This is an internal method. To evaluate a bit-vector operation, use the operator ().

class arxpy.bitvector.operation.BvUlt

Bases: arxpy.bitvector.operation.Operation

Unsigned less than operator.

It overrides < and provides Automatic Constant Conversion. See Operation for more information.

>>> from arxpy.bitvector.core import Constant, Variable
>>> from arxpy.bitvector.operation import BvUlt
>>> BvUlt(Constant(1, 8), Constant(2, 8))
0b1
>>> BvUlt(Constant(1, 8), 2)
0b1
>>> Constant(1, 8) < 2
0b1
>>> Constant(1, 8) < Variable("y", 8)
0x01 < y

classmethod condition(x, y)

Check if the operands verify the restrictions of the operator.

classmethod output_width(x, y)

Return the bit-width of the resulting bit-vector.

classmethod eval(x, y)

Evaluate the operator with given operands.

This is an internal method. To evaluate a bit-vector operation, use the operator ().

class arxpy.bitvector.operation.BvUle

Bases: arxpy.bitvector.operation.Operation

Unsigned less than or equal operator.

It overrides <= and provides Automatic Constant Conversion. See Operation for more information.

>>> from arxpy.bitvector.core import Constant, Variable
>>> from arxpy.bitvector.operation import BvUle
>>> BvUle(Constant(2, 8), Constant(2, 8))
0b1
>>> BvUle(Constant(2, 8), 2)
0b1
>>> Constant(2, 8) <= 2
0b1
>>> Constant(2, 8) <= Variable("y", 8)
0x02 <= y

classmethod condition(x, y)

Check if the operands verify the restrictions of the operator.

classmethod output_width(x, y)

Return the bit-width of the resulting bit-vector.

classmethod eval(x, y)

Evaluate the operator with given operands.

This is an internal method. To evaluate a bit-vector operation, use the operator ().

class arxpy.bitvector.operation.BvUgt

Bases: arxpy.bitvector.operation.Operation

Unsigned greater than operator.

It overrides > and provides Automatic Constant Conversion. See Operation for more information.

>>> from arxpy.bitvector.core import Constant, Variable
>>> from arxpy.bitvector.operation import BvUgt
>>> BvUgt(Constant(1, 8), Constant(2, 8))
0b0
>>> BvUgt(Constant(1, 8), 2)
0b0
>>> Constant(1, 8) > 2
0b0
>>> Constant(1, 8) > Variable("y", 8)
0x01 > y

classmethod condition(x, y)

Check if the operands verify the restrictions of the operator.

classmethod output_width(x, y)

Return the bit-width of the resulting bit-vector.

classmethod eval(x, y)

Evaluate the operator with given operands.

This is an internal method. To evaluate a bit-vector operation, use the operator ().

class arxpy.bitvector.operation.BvUge

Bases: arxpy.bitvector.operation.Operation

Unsigned greater than or equal operator.

It overrides >= and provides Automatic Constant Conversion. See Operation for more information.

>>> from arxpy.bitvector.core import Constant, Variable
>>> from arxpy.bitvector.operation import BvUgt
>>> BvUge(Constant(2, 8), Constant(2, 8))
0b1
>>> BvUge(Constant(2, 8), 2)
0b1
>>> Constant(2, 8) >= 2
0b1
>>> Constant(2, 8) >= Variable("y", 8)
0x02 >= y

classmethod condition(x, y)

Check if the operands verify the restrictions of the operator.

classmethod output_width(x, y)

Return the bit-width of the resulting bit-vector.

classmethod eval(x, y)

Evaluate the operator with given operands.

This is an internal method. To evaluate a bit-vector operation, use the operator ().

class arxpy.bitvector.operation.BvShl

Bases: arxpy.bitvector.operation.Operation

Shift left operation.

It overrides << and provides Automatic Constant Conversion. See Operation for more information.

>>> from arxpy.bitvector.core import Constant, Variable
>>> from arxpy.bitvector.operation import BvShl
>>> BvShl(Constant(0b10001, 5), Constant(1, 5))
0b00010
>>> BvShl(Constant(0b10001, 5), 1)
0b00010
>>> Constant(0b10001, 5) << 1
0b00010
>>> Variable("x", 8) << Variable("y", 8)
x << y

classmethod condition(x, y)

Check if the operands verify the restrictions of the operator.

classmethod output_width(x, y)

Return the bit-width of the resulting bit-vector.

classmethod eval(x, y)

Evaluate the operator with given operands.

This is an internal method. To evaluate a bit-vector operation, use the operator ().

class arxpy.bitvector.operation.BvLshr

Bases: arxpy.bitvector.operation.Operation

Logical right shift operation.

It overrides >> and provides Automatic Constant Conversion. See Operation for more information.

>>> from arxpy.bitvector.core import Constant, Variable
>>> from arxpy.bitvector.operation import BvLshr
>>> BvLshr(Constant(0b10001, 5), Constant(1, 5))
0b01000
>>> BvLshr(Constant(0b10001, 5), 1)
0b01000
>>> Constant(0b10001, 5) >> 1
0b01000
>>> Variable("x", 8) >> Variable("y", 8)
x >> y

classmethod condition(x, y)

Check if the operands verify the restrictions of the operator.

classmethod output_width(x, y)

Return the bit-width of the resulting bit-vector.

classmethod eval(x, y)

Evaluate the operator with given operands.

This is an internal method. To evaluate a bit-vector operation, use the operator ().

class arxpy.bitvector.operation.RotateLeft

Bases: arxpy.bitvector.operation.Operation

Circular left rotation operation.

>>> from arxpy.bitvector.core import Constant, Variable
>>> from arxpy.bitvector.operation import RotateLeft
>>> RotateLeft(Constant(150, 8), 2)
0x5a
>>> RotateLeft(Variable("x", 8), 2)
x <<< 2

classmethod condition(x, r)

Check if the operands verify the restrictions of the operator.

classmethod output_width(x, r)

Return the bit-width of the resulting bit-vector.

classmethod eval(x, r)

Evaluate the operator with given operands.

This is an internal method. To evaluate a bit-vector operation, use the operator ().

class arxpy.bitvector.operation.RotateRight

Bases: arxpy.bitvector.operation.Operation

Circular right rotation operation.

It provides Automatic Constant Conversion. See Operation for more information.

>>> from arxpy.bitvector.core import Constant, Variable
>>> from arxpy.bitvector.operation import RotateRight
>>> RotateRight(Constant(150, 8), 3)
0xd2
>>> RotateRight(Variable("x", 8), 3)
x >>> 3

classmethod condition(x, r)

Check if the operands verify the restrictions of the operator.

classmethod output_width(x, r)

Return the bit-width of the resulting bit-vector.

classmethod eval(x, r)

Evaluate the operator with given operands.

This is an internal method. To evaluate a bit-vector operation, use the operator ().

class arxpy.bitvector.operation.Ite

Bases: arxpy.bitvector.operation.Operation

If-then-else operator.

Ite(b, x, y) returns x if b == 0b1 and y otherwise.

>>> from arxpy.bitvector.core import Constant, Variable
>>> from arxpy.bitvector.operation import Ite
>>> Ite(Constant(0, 1), Constant(0b11, 2), Constant(0b00, 2))
0b00
>>> Ite(Constant(1, 1), Constant(0x1, 4), Constant(0x0, 4))
0x1

classmethod condition(b, x, y)

Check if the operands verify the restrictions of the operator.

classmethod output_width(b, x, y)

Return the bit-width of the resulting bit-vector.

classmethod eval(b, x, y)

Evaluate the operator with given operands.

This is an internal method. To evaluate a bit-vector operation, use the operator ().

class arxpy.bitvector.operation.Extract

Bases: arxpy.bitvector.operation.Operation

Extraction of bits.

Extract(t, i, j) extracts the bits from position i down position j (end points included, position 0 corresponding to the least significant bit).

It overrides the operation [], that is, Extract(t, i, j) is equivalent to t[i:j].

Note that the indices can be omitted when they point the most significant bit or the least significant bit. For example, if t is a bit-vector of length n, then t[n-1:j] = t[:j] and t[i:0] = t[i:]

Warning

In python, given a list l, l[i:j] denotes the elements from position i up to (but no included) position j. Note that with bit-vectors, the order of the arguments is swapped and both end points are included.

For example, for a given list l and bit-vector t, l[0:1] == l[0] and t[1:0] == (t[0], t[1]).

>>> from arxpy.bitvector.core import Constant, Variable
>>> from arxpy.bitvector.operation import Extract
>>> Extract(Constant(0b11100, 5), 4, 2,)
0b111
>>> Constant(0b11100, 5)[4:2]
0b111
>>> Variable("x", 8)[4:2]
x[4:2]
>>> Variable("x", 8)[7:0]
x

classmethod condition(t, i, j)

Check if the operands verify the restrictions of the operator.

classmethod output_width(t, i, j)

Return the bit-width of the resulting bit-vector.

classmethod eval(x, i, j)

Evaluate the operator with given operands.

This is an internal method. To evaluate a bit-vector operation, use the operator ().

class arxpy.bitvector.operation.Concat

Bases: arxpy.bitvector.operation.Operation

Concatenation operation.

Given the bit-vectors \((x_{n-1}, \dots, x_0)\) and \((y_{m-1}, \dots, y_0)\), Concat(x, y) returns the bit-vector \((x_{n-1}, \dots, x_0, y_{m-1}, \dots, y_0)\).

>>> from arxpy.bitvector.core import Constant, Variable
>>> from arxpy.bitvector.operation import Concat
>>> Concat(Constant(0x12, 8), Constant(0x345, 12))
0x12345
>>> Concat(Variable("x", 8), Variable("y", 8))
x :: y

classmethod output_width(x, y)

Return the bit-width of the resulting bit-vector.

classmethod eval(x, y)

Evaluate the operator with given operands.

This is an internal method. To evaluate a bit-vector operation, use the operator ().

class arxpy.bitvector.operation.ZeroExtend

Bases: arxpy.bitvector.operation.Operation

Extend with zeroes preserving the unsigned value.

>>> from arxpy.bitvector.core import Constant, Variable
>>> from arxpy.bitvector.operation import ZeroExtend
>>> ZeroExtend(Constant(0x12, 8), 4)
0x012
>>> ZeroExtend(Variable("x", 8), 4)
0x0 :: x

classmethod condition(x, i)

Check if the operands verify the restrictions of the operator.

classmethod output_width(x, i)

Return the bit-width of the resulting bit-vector.

classmethod eval(x, i)

Evaluate the operator with given operands.

This is an internal method. To evaluate a bit-vector operation, use the operator ().

class arxpy.bitvector.operation.Repeat

Bases: arxpy.bitvector.operation.Operation

Concatenate a bit-vector with itself a given number of times.

>>> from arxpy.bitvector.core import Constant, Variable
>>> from arxpy.bitvector.operation import Repeat
>>> Repeat(Constant(0x1, 4), 4)
0x1111
>>> Repeat(Variable("x", 8), 4)
x :: x :: x :: x

classmethod condition(x, i)

Check if the operands verify the restrictions of the operator.

classmethod output_width(x, i)

Return the bit-width of the resulting bit-vector.

classmethod eval(x, i)

Evaluate the operator with given operands.

This is an internal method. To evaluate a bit-vector operation, use the operator ().

class arxpy.bitvector.operation.BvNeg

Bases: arxpy.bitvector.operation.Operation

Unary minus operation.

It overrides the unary operator -. See Operation for more information.

>>> from arxpy.bitvector.core import Constant, Variable
>>> from arxpy.bitvector.operation import BvNeg
>>> BvNeg(Constant(1, 8))
0xff
>>> -Constant(1, 8)
0xff
>>> BvNeg(Variable("x", 8))
-x

classmethod output_width(x)

Return the bit-width of the resulting bit-vector.

classmethod eval(x)

Evaluate the operator with given operands.

This is an internal method. To evaluate a bit-vector operation, use the operator ().

class arxpy.bitvector.operation.BvAdd

Bases: arxpy.bitvector.operation.Operation

Modular addition operation.

It overrides the operator + and provides Automatic Constant Conversion. See Operation for more information.

>>> from arxpy.bitvector.core import Constant, Variable
>>> from arxpy.bitvector.operation import BvAdd
>>> BvAdd(Constant(1, 8), Constant(2, 8))
0x03
>>> BvAdd(Constant(1, 8), 2)
0x03
>>> Constant(1, 8) + 2
0x03
>>> Variable("x", 8) + Variable("y", 8)
x + y

classmethod condition(x, y)

Check if the operands verify the restrictions of the operator.

classmethod output_width(x, y)

Return the bit-width of the resulting bit-vector.

classmethod eval(x, y)

Evaluate the operator with given operands.

This is an internal method. To evaluate a bit-vector operation, use the operator ().

class arxpy.bitvector.operation.BvSub

Bases: arxpy.bitvector.operation.Operation

Modular subtraction operation.

It overrides the operator - and provides Automatic Constant Conversion. See Operation for more information.

>>> from arxpy.bitvector.core import Constant, Variable
>>> from arxpy.bitvector.operation import BvSub
>>> BvSub(Constant(1, 8), Constant(2, 8))
0xff
>>> BvSub(Constant(1, 8), 2)
0xff
>>> Constant(1, 8) - 2
0xff
>>> Variable("x", 8) - Variable("y", 8)
x - y

classmethod condition(x, y)

Check if the operands verify the restrictions of the operator.

classmethod output_width(x, y)

Return the bit-width of the resulting bit-vector.

classmethod eval(x, y)

Evaluate the operator with given operands.

This is an internal method. To evaluate a bit-vector operation, use the operator ().

class arxpy.bitvector.operation.BvMul

Bases: arxpy.bitvector.operation.Operation

Modular multiplication operation.

It overrides the operator * and provides Automatic Constant Conversion. See Operation for more information.

>>> from arxpy.bitvector.core import Constant, Variable
>>> from arxpy.bitvector.operation import BvMul
>>> BvMul(Constant(4, 8), Constant(3, 8))
0x0c
>>> BvMul(Constant(4, 8), 3)
0x0c
>>> Constant(4, 8) * 3
0x0c
>>> Variable("x", 8) * Variable("y", 8)
x * y

classmethod condition(x, y)

Check if the operands verify the restrictions of the operator.

classmethod output_width(x, y)

Return the bit-width of the resulting bit-vector.

classmethod eval(x, y)

Evaluate the operator with given operands.

This is an internal method. To evaluate a bit-vector operation, use the operator ().

class arxpy.bitvector.operation.BvUdiv

Bases: arxpy.bitvector.operation.Operation

Unsigned and truncated division operation.

It overrides the operator / and provides Automatic Constant Conversion. See Operation for more information.

>>> from arxpy.bitvector.core import Constant, Variable
>>> from arxpy.bitvector.operation import BvUdiv
>>> BvUdiv(Constant(0x0c, 8), Constant(3, 8))
0x04
>>> BvUdiv(Constant(0x0c, 8), 3)
0x04
>>> Constant(0x0c, 8) / 3
0x04
>>> Variable("x", 8) / Variable("y", 8)
x / y

classmethod condition(x, y)

Check if the operands verify the restrictions of the operator.

classmethod output_width(x, y)

Return the bit-width of the resulting bit-vector.

classmethod eval(x, y)

Evaluate the operator with given operands.

This is an internal method. To evaluate a bit-vector operation, use the operator ().

class arxpy.bitvector.operation.BvUrem

Bases: arxpy.bitvector.operation.Operation

Unsigned remainder (modulus) operation.

Usage:

>>> from arxpy.bitvector.core import Constant, Variable
>>> from arxpy.bitvector.operation import BvUrem
>>> BvUrem(Constant(0x0d, 8), Constant(3, 8))
0x01
>>> BvUrem(Constant(0x0d, 8), 3)
0x01
>>> Constant(0x0d, 8) % 3
0x01
>>> Variable("x", 8) % Variable("y", 8)
x % y

classmethod condition(x, y)

Check if the operands verify the restrictions of the operator.

classmethod output_width(x, y)

Return the bit-width of the resulting bit-vector.

classmethod eval(x, y)

Evaluate the operator with given operands.

This is an internal method. To evaluate a bit-vector operation, use the operator ().