cascada.bitvector.context module

Provide context managers to modify the creation and evaluation of bit-vector expressions.

StatefulContext	Base class for context managers with history.
Cache	Control the Cache context.
Simplification	Control the Simplification context.
PrimaryOperationEvaluation	Control the PrimaryOperationEvaluation context.
SecondaryOperationEvaluation	Control the SecondaryOperationEvaluation context.
Validation	Control the Validation context.
Memoization	Control the Memoization context.
MemoizationTable	Store bit-vector expressions with unique identifiers.

class cascada.bitvector.context.StatefulContext(new_context)

Bases: contextlib.AbstractContextManager

Base class for context managers with history.

class cascada.bitvector.context.Cache(new_context)

Bases: cascada.bitvector.context.StatefulContext

Control the Cache context.

Control whether or not the cache is used operating with bit-vectors. By default, the cache is enabled.

Note that the Cache context cannot be enabled when the Simplification or PrimaryOperationEvaluation context are disabled, or when SecondaryOperationEvaluation is enabled.

class cascada.bitvector.context.Simplification(new_context)

Bases: cascada.bitvector.context.StatefulContext

Control the Simplification context.

Control whether or not bit-vector expressions are automatically simplified. By default, automatic simplification is enabled.

>>> from cascada.bitvector.core import Variable
>>> from cascada.bitvector.context import Simplification
>>> x, y = Variable("x", 8), Variable("y", 8)
>>> (x | y) | x
x | y
>>> with Simplification(False):
...     expr = (x | y) | x
>>> expr
x | y | x

When the Simplification context is disabled, the Cache context is also disabled.

Note

Disabling Simplification and Validation speeds up non-symbolic computations with bit-vectors.

class cascada.bitvector.context.PrimaryOperationEvaluation(new_context)

Bases: cascada.bitvector.context.StatefulContext

Control the PrimaryOperationEvaluation context.

Control whether PrimaryOperation objects with symbolic inputs are evaluated (True by default).

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.bitvector.context import PrimaryOperationEvaluation
>>> Constant(1, 8) - Constant(1, 8) + Variable("x", 8) - Variable("x", 8)
0x00
>>> with PrimaryOperationEvaluation(False):
...     expr = Constant(1, 8) - Constant(1, 8) + Variable("x", 8) - Variable("x", 8)
>>> expr
(0x00 + x) - x
>>> expr.doit()
0x00

When the PrimaryOperationEvaluation context is disabled, the Simplification and Cache contexts are also disabled.

class cascada.bitvector.context.SecondaryOperationEvaluation(new_context)

Bases: cascada.bitvector.context.StatefulContext

Control the SecondaryOperationEvaluation context.

Control whether SecondaryOperation objects with symbolic inputs are evaluated (False by default).

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.bitvector.context import SecondaryOperationEvaluation
>>> from cascada.bitvector.secondaryop import BvMaj
>>> BvMaj(Constant(1, 8), Constant(1, 8), Constant(2, 8))
0x01
>>> expr = BvMaj(Variable("x", 8), Variable("y", 8), Variable("z", 8))
>>> expr
BvMaj(x, y, z)
>>> expr.doit()
(x & y) | (x & z) | (y & z)
>>> with SecondaryOperationEvaluation(True):
...     BvMaj(Variable("x", 8), Variable("y", 8), Variable("z", 8))
(x & y) | (x & z) | (y & z)

When the SecondaryOperation context is enabled, the Cache context is disabled.

class cascada.bitvector.context.Validation(new_context)

Bases: cascada.bitvector.context.StatefulContext

Control the Validation context.

Control whether or not arguments of bit-vector operators are validated (e.g., the integer value when creating a Constant fits for the width given). By default, validation of arguments is enabled.

Note that when it is disabled, Automatic Constant Conversion is no longer available (see Operation).

>>> from cascada.bitvector.core import Constant
>>> from cascada.bitvector.context import Validation
>>> Constant(1, 8) + 1
0x02
>>> with Validation(False):
...     Constant(1, 5) + 2
Traceback (most recent call last):
 ...
AttributeError: 'int' object has no attribute 'width'

Note

Disabling Simplification and Validation speeds up non-symbolic computations with bit-vectors.

class cascada.bitvector.context.Memoization(new_context)

Bases: cascada.bitvector.context.StatefulContext

Control the Memoization context.

Control whether or not bit-vector operations are evaluated in the memoization mode. By default, it is disabled.

In the memoization mode, the result of each bit-vector operation is stored in a table (with a unique identifier). When the same inputs occurs again, the result is retrieved from the table. See also Memoization.

Note that in the memoization mode, bit-vector operations don’t return the actual values but their identifiers in the memoization table. The actual values can be obtained from the MemoizationTable.

>>> from cascada.bitvector.core import Variable
>>> from cascada.bitvector.context import Memoization, MemoizationTable
>>> x, y, z = Variable("x", 8), Variable("y", 8), Variable("z", 8),
>>> ~((x + y) ^ ((z + 1) & y))
~((x + y) ^ ((z + 0x01) & y))
>>> non_memoized_expr = (z + 1)
>>> lut = MemoizationTable()
>>> with Memoization(lut):
...     expr = ~((x + y) ^ (non_memoized_expr & y))
>>> expr
x3
>>> lut
MemoizationTable([(x0, x + y), (x1, (z + 0x01) & y), (x2, x0 ^ x1), (x3, ~x2)])

The Memoization context is useful to efficiently compute large symbolic expressions since the identifiers are used instead of the full expressions.

>>> from cascada.bitvector.core import Variable
>>> from cascada.bitvector.context import Memoization, MemoizationTable
>>> x = Variable("x", 8)
>>> expr = x
>>> for i in range(3): expr += expr
>>> expr
x + x + x + x + x + x + x + x
>>> lut = MemoizationTable()
>>> with Memoization(lut):
...     expr = x
...     for i in range(3): expr += expr
>>> expr
x2
>>> lut  
MemoizationTable([(x0, x + x), (x1, x0 + x0), (x2, x1 + x1)])

When the Memoization context is enabled, the Simplification and Cache contexts are disabled.

class cascada.bitvector.context.MemoizationTable(id_prefix='x')

Bases: collections.abc.MutableMapping

Store bit-vector expressions with unique identifiers.

The MemoizationTable is a dictionary-like structure (implementing the usual methods of a dictionary and some additional methods, and remembering the order entries were added as collections.Counter) used for evaluating bit-vector operations in the memoization mode (see Memoization).

>>> from cascada.bitvector.core import Variable
>>> from cascada.bitvector.context import Memoization, MemoizationTable
>>> x, y = Variable("x", 8), Variable("y", 8)
>>> lut = MemoizationTable()
>>> with Memoization(lut):
...     expr = ~(x + y)
>>> lut
MemoizationTable([(x0, x + y), (x1, ~x0)])
>>> lut[Variable("x0", 8)]
x + y
>>> lut.get_id(x + y)
x0
>>> lut.add_op(Variable("x1", 8) & Variable("z", 8))
x2
>>> lut
MemoizationTable([(x0, x + y), (x1, ~x0), (x2, x1 & z)])
>>> lut.replace_id(Variable("x0", 8), Variable("x_0", 8))
>>> lut
MemoizationTable([(x_0, x + y), (x1, ~x_0), (x2, x1 & z)])

classmethod from_list_of_assignments(assignments, new_id_prefix=None)

Returns a new MemoizationTable with the given list of assignments.

The argument assignments is a list of pairs (Variable, Operation) where the variable represents the output of the operation.

add_op(expr)

Add an bit-vector expression and return its identifier.

get_id(expr)

Return the identifier of a bit-vector expression.

contain_op(expr)

Check if the bit-vector expression is stored.

replace_id(old_id, new_id)

Replace the old identifier by the given new identifier.

clear()

Empty the table.