cascada.bitvector.core module

Provide the basic bit-vector types.

Term	Represent bit-vector terms.
Constant	Represent bit-vector constants.
Variable	Represent bit-vector variables.
bitvectify	Convert the argument t to a bit-vector Term of bit-width width.

class cascada.bitvector.core.Term(*args, width)

Bases: sympy.core.basic.Basic

Represent bit-vector terms.

Bit-vector terms are constants, variables and operations applied to terms.

Bit-vector terms support many operations with the standard operators symbols (<=, +, ^, etc.). See operation for more information.

This class is not meant to be instantiated but to provide a base class for the different types of terms.

Note that Term inherits the methods of the SymPy class Basic; many of these methods work with bit-vector terms out of the box.

property width

The bit-width of the term.

formula_size()

Return the formula size of the bit-vector term.

As defined in Complexity of Fixed-Size Bit-Vector Logics.

vrepr()

Return an executable string representation.

This method returns a string so that the relation eval(expr.vrepr())) == expr holds when expr is a Term.

srepr()

Return a short string representation.

This method returns a short string describing the bit-vector term, as opposed to vrepr which returns a long and executable string representation.

crepr()

Return a C code representation.

This method returns a string with an expression in the C programming language that evaluates to self.

Bit-vector widths larger than 128 are not supported.

>>> from cascada.bitvector.core import Constant, Variable
>>> (Variable("a", 4) * Constant(2, 4)).crepr()
'(a * 0x2U) & 0xfU'
>>> (Variable("a", 8) < Constant(1, 8)).crepr()
'(_Bool)((a < 0x1U) & 0x1U)'
>>> Variable('a', 8)[2:1].crepr()
'(a >> 0x1U) & 0x3U'
>>> Constant(1, 96).crepr()
'((__uint128)(0x1ULL)) & (((__uint128)(0xffffffffULL) << 64) | ((__uint128)(0xffffffffffffffffULL)))'

doit(eval_sec_ops=True, sort_symmetric_args=False)

Evaluate the term.

Similar to Sympy’s doit method, this method evaluate the term in case it was not evaluated by default (like SecondaryOperation objects).

If eval_sec_ops is True, the evaluation is done with the context SecondaryOperationEvaluation enabled.

If sort_symmetric_args is True, arguments of symmetric Operation objects are sorted.

See also PrimaryOperationEvaluation and SecondaryOperationEvaluation.

class_key()

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

atoms(*types)

Returns the atoms that form the current object.

This can be used to get all the bit-vectors of type Constant or the bit-vectors of type Variable from a bit-vector expression.

For more information see SymPy’s atoms method. This method is similar to the SymPy variant but this method doesn’t throw an exception when one of the arguments is of type ‘int’.

>>> from cascada.bitvector.core import Constant, Variable
>>> expr = Constant(1, 4) + Variable("a", 4)
>>> expr.atoms(Constant)
{0x1}
>>> expr.atoms(Variable)
{a}

class cascada.bitvector.core.Constant(val, width)

Bases: sympy.core.basic.Atom, cascada.bitvector.core.Term

Represent bit-vector constants.

Bit-vector constants are interpreted as unsigned integers in base 2, that is, a bit-vector \((x_{n-1}, \dots, x_1, x_0)\), where \(x_0\) or x[0] denotes the LSB located at position 0, represents the non-negative integer \(x_0 + 2 x_1 + \dots + 2^{n-1} x_{n-1}\).

Parameters

• val – the integer value.

• width – the bit-width.

>>> from cascada.bitvector.core import Constant
>>> Constant(3, 12)
0x003
>>> Constant(0b11, 12)
0x003
>>> Constant(0x003, 12)
0x003
>>> Constant(3, 12).vrepr()
'Constant(0x003, width=12)'

classmethod class_key()

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

property val

The integer represented by the bit-vector constant.

formula_size()

The formula size of the constant.

bin()

Return the python-like binary representation.

>>> from cascada.bitvector.core import Constant
>>> print(Constant(3, 4).bin())
0b0011
>>> print(Constant(4, 6).bin())
0b000100

hex()

Return the python-like hexadecimal representation.

>>> from cascada.bitvector.core import Constant
>>> print(Constant(3, 4).hex())
0x3

oct()

Return the python-like octal representation.

>>> from cascada.bitvector.core import Constant
>>> print(Constant(4, 6).oct())
0o04

class cascada.bitvector.core.Variable(name, width, **kwargs)

Bases: sympy.core.basic.Atom, cascada.bitvector.core.Term

Represent bit-vector variables.

Parameters

• name – the name of the variable.

• width – the bit-width.

>>> from cascada.bitvector.core import Variable
>>> Variable("x", 12)
x
>>> Variable("x", 12).vrepr()
"Variable('x', width=12)"

property name

The name of the variable.

formula_size()

The formula size of the variable.

cascada.bitvector.core.bitvectify(t, width)

Convert the argument t to a bit-vector Term of bit-width width.

>>> from cascada.bitvector.core import bitvectify
>>> print(bitvectify(0, 8).vrepr())
Constant(0b00000000, width=8)
>>> print(bitvectify("x", 8).vrepr())
Variable('x', width=8)