cascada.bitvector.operation module

Provide the common bit-vector operators.

Operation	Represent bit-vector operations.
PrimaryOperation	Represent the primary bit-vector operations.
SecondaryOperation	Represent secondary bit-vector operations.
PartialOperation	Represent bit-vector operations with fixed operands.
make_partial_operation	Return a new PartialOperation subclass with the given base operator and fixed arguments.
BvNot	Bitwise negation operation.
BvAnd	Bitwise AND (logical conjunction) operation.
BvOr	Bitwise OR (logical disjunction) operation.
BvXor	Bitwise XOR (exclusive-or) operation.
BvComp	Equality operator.
BvUlt	Unsigned less than operator.
BvUle	Unsigned less than or equal operator.
BvUgt	Unsigned greater than operator.
BvUge	Unsigned greater than or equal operator.
BvShl	Shift left operation.
BvLshr	Logical right shift operation.
RotateLeft	Circular left rotation operation.
RotateRight	Circular right rotation operation.
Ite	If-then-else operator.
Extract	Extraction of bits.
Concat	Concatenation operation.
BvNeg	Unary minus operation.
BvAdd	Modular addition operation.
BvSub	Modular subtraction operation.
BvMul	Modular multiplication operation.
BvUdiv	Unsigned and truncated division operation.
BvUrem	Unsigned remainder (modulus) operation.
BvIdentity	The identity operation.
zero_extend	Extend with zeroes preserving the unsigned value.
repeat	Concatenate a bit-vector with itself a given number of times.

class cascada.bitvector.operation.Operation(**kwargs)

Bases: cascada.bitvector.core.Term

Represent bit-vector operations.

A bit-vector operation is a mathematical function that 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 Python class representing the mathematical function (without operands) and operation is used to denote the application of an operator to some operands.

A particular operator (a subclass of Operation) can be evaluated by instantiating an object with the operands as the object arguments. The instantiation internally calls the method eval, containing the logic of the operator. This behaviour is similar as those of the SymPy classes Add or Mul.

Unless the Simplification context is disabled (enabled by default), many of the operations automatically simplify complex expressions by applying basic rules from Boolean algebra. Moreoever, operations are also affected by other context managers such as Cache, PrimaryOperationEvaluation, SecondaryOperationEvaluation, Validation or Memoization.

This class is not meant to be instantiated but to provide a base class for the two types of operations: PrimaryOperation and SecondaryOperation.

Note

New bit-vector operations can be defined by subclassing SecondaryOperation (see BvMaj as example). It is also possible to define new bit-vector operations by subclassing PrimaryOperation, but this is not recommended.

arity

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

is_symmetric

True if the operator is symmetric with respect to its operands (a permutation of the inputs does not change the output). 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 cascada.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 that assumes the list args has been parsed. To evaluate a bit-vector operation, instantiate a new object with the operands as the object arguments (i.e., use the Python operator ()).

formula_size()

The formula size of the operation.

memoization_table(id_prefix='x', decompose_sec_ops=True)

Return a decomposition of the current operation into simple assignments.

Given an Operation object \(F(a_1, a_2, \dots)\), this method decomposes it into a list of simple assignments \(x_{i+1} \leftarrow f_i(x_i)\) such that the last output variable \(x_{n}\) represents the output of \(F(a_1, a_2, \dots)\). The i-th assignment is given by:

• the output Variable \(x_{i+1}\) that represents the output of \(f_i(x_i)\),

• the Operation object \(f_i(x_i)\) where the input \(x_i\) is a previous output Variable, an input Variable (of \(F(a_1, a_2, \dots)\)), a Constant, a scalar, o a list of them but not an Operation object.

The list of assignments is given as a MemoizationTable, and it is obtained by re-evaluating the current operation under the Memoization context.

The argument id_prefix is the string prefix used to name intermediate variables and the argument decompose_sec_ops determines whether to use the context SecondaryOperationEvaluation. In other words, if decompose_sec_ops is True, SecondaryOperation objects are not allowed in the list of assignments and they are replaced by their decomposition into PrimaryOperation objects.

>>> from cascada.bitvector.core import Variable
>>> from cascada.bitvector.secondaryop import BvMaj
>>> expr = 1 + BvMaj(2, Variable("a_1", 8), 3 | Variable("a_2", 8))
>>> expr.memoization_table()  
MemoizationTable([(x0, a_2 | 0x03), (x1, 0x02 & a_1), (x2, 0x02 & x0),
(x3, x1 | x2), (x4, a_1 & x0), (x5, x3 | x4), (x6, x5 + 0x01), (x7, Id(x6))])
>>> expr.memoization_table(decompose_sec_ops=False)
MemoizationTable([(x0, a_2 | 0x03), (x1, BvMaj(0x02, a_1, x0)), (x2, x1 + 0x01), (x3, Id(x2))])

class cascada.bitvector.operation.PrimaryOperation(**kwargs)

Bases: cascada.bitvector.operation.Operation

Represent the primary bit-vector operations.

The primary bit-vector operations are those basic operations that are included in the bit-vector theory of the SMT_LIBv2 format.

The primary operations are BvAnd, BvOr, BvXor, BvComp, BvUlt, BvUle, BvUgt, BvUge, BvShl, BvLshr, RotateLeft, RotateRight, Concat, BvAdd, BvSub, BvMul, BvUdiv, BvUrem, BvNeg, BvNot, Extract, Ite and BvIdentity.

This class is not meant to be instantiated but to provide a base class to define primary operators.

classmethod class_key()

Nice order of classes.

class cascada.bitvector.operation.SecondaryOperation(**kwargs)

Bases: cascada.bitvector.operation.Operation

Represent secondary bit-vector operations.

Secondary bit-vector operations are those bit-vector operations that are not primary operations (see PrimaryOperation). Secondary operations must be defined in terms of primary operations.

By default, secondary operations are fully evaluated (Operation.eval is used) if all the operands are scalar or Constant objects (see also context.SecondaryOperationEvaluation). On the other hand, pre_eval is always called in the evaluation (even with symbolic inputs).

This class is not meant to be instantiated but to provide a base class to define secondary operators.

classmethod pre_eval(*args)

Evaluate the operator before Operation.eval.

This is an internal method that assumes the list args has been parsed.

classmethod class_key()

Nice order of classes.

formula_size()

The formula size of the operation.

class cascada.bitvector.operation.PartialOperation

Bases: object

Represent bit-vector operations with fixed operands.

Given a base operator \((x, y) \mapsto f(x, y)\), a partial operator is a function obtained by fixing some of the inputs to constants, e.g., \(x \mapsto f(x, y=0)\).

This class is not meant to be instantiated but to provide a base class for bit-vector operations with fixed operands generated through make_partial_operation. PartialOperation subclasses generated by make_partial_operation are also subclasses of PrimaryOperation or SecondaryOperation depending on the type of the base operator.

base_op

a subclass of Operation denoting the base operator.

fixed_args

a tuple with the same length as the number of operands of the base function containing None, scalar or Constant elements. If fixed_args[i] is None, the i-th operand is not fixed; otherwise, the i-th operand is replaced with fixed_args[i].

cascada.bitvector.operation.make_partial_operation(base_op, fixed_args)

Return a new PartialOperation subclass with the given base operator and fixed arguments.

The argument fixed_args is a tuple, with the same length as the number of operands of the base operator, containing None, scalar or Constant elements. If fixed_args[i] is None, the i-th operand is not fixed; otherwise, the i-th operand is replaced with fixed_args[i].

The resulting class is also a subclass of PrimaryOperation or SecondaryOperation, depending on the type of the base operator.

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.bitvector.operation import BvAdd, Extract, make_partial_operation
>>> from cascada.bitvector.secondaryop import BvMaj
>>> BvAddCte = make_partial_operation(BvAdd, tuple([None, Constant(1, 4)]))
>>> BvAddCte.__name__
'BvAdd_{·, 0x1}'
>>> expr = BvAddCte(Variable("a", 4))
>>> expr
a + 0x1
>>> expr.vrepr()
"make_partial_operation(BvAdd, (None, Constant(0b0001, width=4)))(Variable('a', width=4))"
>>> ExtractLSB = make_partial_operation(Extract, tuple([None, 0, 0]))
>>> ExtractLSB.__name__
'Extract_{·, 0, 0}'
>>> ExtractLSB(Extract(Variable("a", 4), 2, 0))  # result is simplified
a[0]
>>> BvCteMaj = make_partial_operation(BvMaj, tuple([None, None, Constant(1, 4)]))
>>> BvCteMaj.__name__
'BvMaj_{·, ·, 0x1}'
>>> BvCteMaj(Variable("a", 4), Variable("a", 4))
a
>>> expr = BvCteMaj(Variable("a", 4), Variable("b", 4))
>>> expr
BvMaj_{·, ·, 0x1}(a, b)
>>> expr.doit()
(a & b) | (a & 0x1) | (b & 0x1)
>>> expr.memoization_table()
MemoizationTable([(x0, a & b), (x1, a & 0x1), (x2, x0 | x1), (x3, b & 0x1), (x4, x2 | x3), (x5, Id(x4))])
>>> BvCteMaj_v2 = make_partial_operation(BvCteMaj, tuple([Constant(2, 4), None]))
>>> BvCteMaj_v2.__name__
'BvMaj_{0x2, ·, 0x1}'
>>> BvCteMaj_v2(Variable("a", 4))
BvMaj_{0x2, ·, 0x1}(a)

class cascada.bitvector.operation.BvNot(**kwargs)

Bases: cascada.bitvector.operation.PrimaryOperation

Bitwise negation operation.

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

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.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 that assumes the list args has been parsed. To evaluate a bit-vector operation, instantiate a new object with the operands as the object arguments (i.e., use the Python operator ()).

class cascada.bitvector.operation.BvAnd(**kwargs)

Bases: cascada.bitvector.operation.PrimaryOperation

Bitwise AND (logical conjunction) operation.

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

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.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 that assumes the list args has been parsed. To evaluate a bit-vector operation, instantiate a new object with the operands as the object arguments (i.e., use the Python operator ()).

class cascada.bitvector.operation.BvOr(**kwargs)

Bases: cascada.bitvector.operation.PrimaryOperation

Bitwise OR (logical disjunction) operation.

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

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.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 that assumes the list args has been parsed. To evaluate a bit-vector operation, instantiate a new object with the operands as the object arguments (i.e., use the Python operator ()).

class cascada.bitvector.operation.BvXor(**kwargs)

Bases: cascada.bitvector.operation.PrimaryOperation

Bitwise XOR (exclusive-or) operation.

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

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.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 that assumes the list args has been parsed. To evaluate a bit-vector operation, instantiate a new object with the operands as the object arguments (i.e., use the Python operator ()).

class cascada.bitvector.operation.BvComp(**kwargs)

Bases: cascada.bitvector.operation.PrimaryOperation

Equality operator.

Provides Automatic Constant Conversion. See PrimaryOperation for more information.

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.bitvector.operation import BvComp
>>> BvComp(Constant(1, 8), Constant(2, 8))
0b0
>>> BvComp(Constant(1, 8), 2)
0b0
>>> x, y = Variable("x", 8), Variable("y", 8)
>>> BvComp(Constant(1, 8), Variable("y", 8))
0x01 == y
>>> bool(BvComp(x + y, y + x))
True

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).

>>> x == y
False
>>> BvComp(x, y)  # 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 that assumes the list args has been parsed. To evaluate a bit-vector operation, instantiate a new object with the operands as the object arguments (i.e., use the Python operator ()).

class cascada.bitvector.operation.BvUlt(**kwargs)

Bases: cascada.bitvector.operation.PrimaryOperation

Unsigned less than operator.

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

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.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 that assumes the list args has been parsed. To evaluate a bit-vector operation, instantiate a new object with the operands as the object arguments (i.e., use the Python operator ()).

class cascada.bitvector.operation.BvUle(**kwargs)

Bases: cascada.bitvector.operation.PrimaryOperation

Unsigned less than or equal operator.

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

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.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 that assumes the list args has been parsed. To evaluate a bit-vector operation, instantiate a new object with the operands as the object arguments (i.e., use the Python operator ()).

class cascada.bitvector.operation.BvUgt(**kwargs)

Bases: cascada.bitvector.operation.PrimaryOperation

Unsigned greater than operator.

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

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.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 that assumes the list args has been parsed. To evaluate a bit-vector operation, instantiate a new object with the operands as the object arguments (i.e., use the Python operator ()).

class cascada.bitvector.operation.BvUge(**kwargs)

Bases: cascada.bitvector.operation.PrimaryOperation

Unsigned greater than or equal operator.

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

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.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 that assumes the list args has been parsed. To evaluate a bit-vector operation, instantiate a new object with the operands as the object arguments (i.e., use the Python operator ()).

class cascada.bitvector.operation.BvShl(**kwargs)

Bases: cascada.bitvector.operation.PrimaryOperation

Shift left operation.

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

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.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 that assumes the list args has been parsed. To evaluate a bit-vector operation, instantiate a new object with the operands as the object arguments (i.e., use the Python operator ()).

class cascada.bitvector.operation.BvLshr(**kwargs)

Bases: cascada.bitvector.operation.PrimaryOperation

Logical right shift operation.

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

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.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 that assumes the list args has been parsed. To evaluate a bit-vector operation, instantiate a new object with the operands as the object arguments (i.e., use the Python operator ()).

class cascada.bitvector.operation.RotateLeft(**kwargs)

Bases: cascada.bitvector.operation.PrimaryOperation

Circular left rotation operation.

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.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 that assumes the list args has been parsed. To evaluate a bit-vector operation, instantiate a new object with the operands as the object arguments (i.e., use the Python operator ()).

class cascada.bitvector.operation.RotateRight(**kwargs)

Bases: cascada.bitvector.operation.PrimaryOperation

Circular right rotation operation.

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

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.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 that assumes the list args has been parsed. To evaluate a bit-vector operation, instantiate a new object with the operands as the object arguments (i.e., use the Python operator ()).

class cascada.bitvector.operation.Ite(**kwargs)

Bases: cascada.bitvector.operation.PrimaryOperation

If-then-else operator.

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

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.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 that assumes the list args has been parsed. To evaluate a bit-vector operation, instantiate a new object with the operands as the object arguments (i.e., use the Python operator ()).

class cascada.bitvector.operation.Extract(**kwargs)

Bases: cascada.bitvector.operation.PrimaryOperation

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 not 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 cascada.bitvector.core import Constant, Variable
>>> from cascada.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 that assumes the list args has been parsed. To evaluate a bit-vector operation, instantiate a new object with the operands as the object arguments (i.e., use the Python operator ()).

class cascada.bitvector.operation.Concat(**kwargs)

Bases: cascada.bitvector.operation.PrimaryOperation

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 cascada.bitvector.core import Constant, Variable
>>> from cascada.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 that assumes the list args has been parsed. To evaluate a bit-vector operation, instantiate a new object with the operands as the object arguments (i.e., use the Python operator ()).

class cascada.bitvector.operation.BvNeg(**kwargs)

Bases: cascada.bitvector.operation.PrimaryOperation

Unary minus operation.

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

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.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 that assumes the list args has been parsed. To evaluate a bit-vector operation, instantiate a new object with the operands as the object arguments (i.e., use the Python operator ()).

class cascada.bitvector.operation.BvAdd(**kwargs)

Bases: cascada.bitvector.operation.PrimaryOperation

Modular addition operation.

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

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.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 that assumes the list args has been parsed. To evaluate a bit-vector operation, instantiate a new object with the operands as the object arguments (i.e., use the Python operator ()).

class cascada.bitvector.operation.BvSub(**kwargs)

Bases: cascada.bitvector.operation.PrimaryOperation

Modular subtraction operation.

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

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.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 that assumes the list args has been parsed. To evaluate a bit-vector operation, instantiate a new object with the operands as the object arguments (i.e., use the Python operator ()).

class cascada.bitvector.operation.BvMul(**kwargs)

Bases: cascada.bitvector.operation.PrimaryOperation

Modular multiplication operation.

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

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.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 that assumes the list args has been parsed. To evaluate a bit-vector operation, instantiate a new object with the operands as the object arguments (i.e., use the Python operator ()).

class cascada.bitvector.operation.BvUdiv(**kwargs)

Bases: cascada.bitvector.operation.PrimaryOperation

Unsigned and truncated division operation.

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

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.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 that assumes the list args has been parsed. To evaluate a bit-vector operation, instantiate a new object with the operands as the object arguments (i.e., use the Python operator ()).

class cascada.bitvector.operation.BvUrem(**kwargs)

Bases: cascada.bitvector.operation.PrimaryOperation

Unsigned remainder (modulus) operation.

Usage:

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.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 that assumes the list args has been parsed. To evaluate a bit-vector operation, instantiate a new object with the operands as the object arguments (i.e., use the Python operator ()).

class cascada.bitvector.operation.BvIdentity(**kwargs)

Bases: cascada.bitvector.operation.PrimaryOperation

The identity operation.

Return the same value when the input is constant and a BvIdentity object when the input is symbolic:

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.bitvector.operation import BvIdentity
>>> BvIdentity(Constant(0x1, 4))
0x1
>>> BvIdentity(Variable("x", 8))
Id(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 that assumes the list args has been parsed. To evaluate a bit-vector operation, instantiate a new object with the operands as the object arguments (i.e., use the Python operator ()).

cascada.bitvector.operation.zero_extend(x, i)

Extend with zeroes preserving the unsigned value.

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

cascada.bitvector.operation.repeat(x, i)

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

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