cascada.bitvector.ssa module

Represent bit-vector functions and their representation in static single assignment (SSA) form.

`BvFunction`	Represent fixed-width bit-vector functions.
`RoundBasedFunction`	Represent round-based fixed-width bit-vector functions.
`SSAReturn`	Subclass of `BvIdentity` used to denote the returned variables in `SSA`.
`SSA`	Represent a `BvFunction` as a static single assignment program.
`get_random_bvfunction`	Return a random `BvFunction` with given shape.

class cascada.bitvector.ssa.BvFunction(*args, **options)[source]

Bases: object

Represent fixed-width bit-vector functions.

A BvFunction takes fixed-width Constant operands and return a tuple of fixed-width Constant.

Similar to Operation, BvFunction is evaluated using the operator () and provides Automatic Constant Conversion.

Note

BvFunction only supports Constant operands and must return a tuple of Constant values (as opposed to Operation that accepts Term and scalar operands and returns a single Term).

BvFunction does not support returned values that independent of the inputs.

This class is not meant to be instantiated but to provide a base class for bit-vector functions with fixed operands. To define a bit-vector function, subclass BvFunction, set the class attributes input_widths and output_widths and implement eval with bit-vector operations.

>>> from cascada.bitvector.ssa import BvFunction
>>> class MyFoo(BvFunction):
...     input_widths, output_widths = [8, 8], [8, 8]
...     @classmethod
...     def eval(cls, x, y):  return x ^ y, x
>>> MyFoo.get_name()
'MyFoo'
>>> MyFoo(1, 1)  # automatic conversion from int to Constant
(0x00, 0x01)

input_widths: a list containing the widths of the inputs

output_widths: a list containing the widths of the outputs

classmethod get_name()[source]: Return the name of the function (by default cls.__name__).

classmethod vrepr()[source]

Return an executable string representation.

This method returns a string so that eval(cls.vrepr()) returns a new BvFunction object with the same content.

classmethod eval(*args)[source]: Evaluate the function (internal method).

classmethod to_ssa(input_names, id_prefix, decompose_sec_ops=False, **ssa_options)[source]

Return the SSA object of the bit-vector function.

Parameters

input_names – the names for the input variables
id_prefix – the prefix to denote the intermediate variables
decompose_sec_ops – if decompose_sec_ops is True, SecondaryOperation objects within the bit-vector function are replaced by their decompositions into PrimaryOperation objects.
ssa_options – options passed to the __init__ method of SSA.

classmethod log_msg(format_string, format_field_objects=None)[source]

Log a message during the evaluation of the bit-vector function.

This method is meant to be used within eval to log the values of internal variables. At the beggining of each evaluation, messages logged from the last evaluation are automatically removed.

>>> from cascada.bitvector.ssa import BvFunction
>>> class MyFoo(BvFunction):
...     input_widths, output_widths = [8, 8], [8, 8]
...     @classmethod
...     def eval(cls, x, y):
...         cls.log_msg('input variables = [{}, {}]', [x, y])
...         return x ^ y, x
>>> MyFoo(0, 1)
(0x01, 0x00)
>>> MyFoo.get_formatted_logged_msgs()
['input variables = [0x00, 0x01]']

Parameters

format_string – a Python format string
format_field_objects – an optional list with the objects that will replace the format fields in the format_string (i.e., the arguments associated to format_string.format())

classmethod get_formatted_logged_msgs()[source]

Return the list of logged messages.

If the bit-vector function includes log_msg calls in its eval, this method return the list of messages logged in the last evaluation with the format field objects applied. Otherwise, an exception is raised.

See also printing.dotprinting.

Parameters

input_names – the names for the input variables
repeat – whether to use different nodes for common subexpressions (default True)
vrepr_label – wheter to use the verbose representation (Term.vrepr) to label the nodes (default False)
kwargs – additional arguments passed to printing.dotprinting

>>> from cascada.bitvector.ssa import BvFunction
>>> class MyFoo(BvFunction):
...     input_widths, output_widths = [8], [8, 8]
...     @classmethod
...     def eval(cls, x):  return x, x ^ 1
>>> print(MyFoo.dotprinting(["x"], repeat=False))  
digraph{
# Graph style
"ordering"="out"
"rankdir"="TD"
#########
# Nodes #
#########
"Tuple(Variable('x', width=8), BvXor(Variable('x', width=8), Constant(0b00000001, width=8)))"
    ["color"="grey", "label"="Tuple", "shape"="ellipse"];
"Variable('x', width=8)" ["color"="aquamarine3", "label"="x", "shape"="box"];
"BvXor(Variable('x', width=8), Constant(0b00000001, width=8))"
    ["color"="black", "label"="BvXor", "shape"="ellipse"];
"Constant(0b00000001, width=8)" ["color"="blue1", "label"="0x01", "shape"="box"];

#########
# Edges #
#########
"Tuple(Variable('x', width=8), BvXor(Variable('x', width=8), Constant(0b00000001, width=8)))" ->
    "Variable('x', width=8)";
"Tuple(Variable('x', width=8), BvXor(Variable('x', width=8), Constant(0b00000001, width=8)))" ->
    "BvXor(Variable('x', width=8), Constant(0b00000001, width=8))";
"BvXor(Variable('x', width=8), Constant(0b00000001, width=8))" -> "Variable('x', width=8)";
"BvXor(Variable('x', width=8), Constant(0b00000001, width=8))" -> "Constant(0b00000001, width=8)";
}

class cascada.bitvector.ssa.RoundBasedFunction(*args, **options)[source]

Bases: cascada.bitvector.ssa.BvFunction

Represent round-based fixed-width bit-vector functions.

A RoundBasedFunction is a BvFunction that can be decomposed into rounds, where in each round some subroutine is computed (not necessarily the same). Moreoever, the next round not only can use the outputs of the previous round but also any of the previous variables computed.

In practice, the eval method of RoundBasedFunction depends on the class attribute num_rounds, which can be changed by calling the method set_num_rounds.

This class is not meant to be instantiated but to provide a base class for round-based bit-vector functions with fixed operands. To define such a function, subclass RoundBasedFunction, set the class attributes input_widths and output_widths and implement eval with bit-vector operations (similar as BvFunction). Moreover, set the class attribute num_rounds and implement set_num_rounds.

>>> from cascada.bitvector.ssa import RoundBasedFunction
>>> class MyFoo(RoundBasedFunction):
...     input_widths, output_widths, num_rounds = [8, 8], [8, 8], 1
...     @classmethod
...     def eval(cls, x, y):
...         for _ in range(cls.num_rounds):  x, y = y, x + 1
...         return x, y
...     @classmethod
...     def set_num_rounds(cls, new_num_rounds):  cls.num_rounds = new_num_rounds
>>> MyFoo.get_name()
'MyFoo_1R'
>>> MyFoo(0, 0)
(0x00, 0x01)
>>> MyFoo.set_num_rounds(2)
>>> MyFoo.get_name()
'MyFoo_2R'
>>> MyFoo(0, 0)
(0x01, 0x01)

num_rounds: the number of rounds

classmethod get_name()[source]: Return the class name and the current number of rounds.

classmethod to_ssa(input_names, id_prefix, decompose_sec_ops=False, **ssa_options)[source]

Return the SSA object of the round-based bit-vector function.

This method calls BvFunction.to_ssa with the same argument list, and stores the round outputs in the SSA object if add_round_outputs calls were added in eval.

classmethod set_num_rounds(new_num_rounds)[source]: Set RoundBasedFunction.num_rounds and update input_widths and output_widths if necessary.

classmethod set_num_rounds_and_return(new_num_rounds)[source]: Call set_num_rounds and return cls.

classmethod vrepr()[source]

Return an executable string representation.

This method returns a string so that eval(cls.vrepr()) returns a new RoundBasedFunction object with the same content.

classmethod add_round_outputs(*args)[source]

Store the current round outputs in the evaluation of the round-based function.

This method is meant to be used within eval to store the outputs of each round. At the beggining of each evaluation, round ouputs stored in the last evaluation are automatically removed.

>>> from cascada.bitvector.core import Variable
>>> from cascada.bitvector.ssa import RoundBasedFunction
>>> class MyFoo(RoundBasedFunction):
...     input_widths, output_widths, num_rounds = [8, 8], [8, 8], 1
...     @classmethod
...     def eval(cls, x, y):
...         for _ in range(cls.num_rounds):
...             x, y = y, x + 1
...             cls.add_round_outputs(x, y)
...         return x, y
...     @classmethod
...     def set_num_rounds(cls, new_num_rounds):  cls.num_rounds = new_num_rounds
>>> MyFoo.set_num_rounds(3)
>>> MyFoo(0, 0)
(0x01, 0x02)
>>> MyFoo.get_rounds_outputs()
((0x00, 0x01), (0x01, 0x01), (0x01, 0x02))
>>> MyFoo(Variable("x", 8), Variable("y", 8), symbolic_inputs=True)
(y + 0x01, x + 0x02)
>>> MyFoo.get_rounds_outputs()
((y, x + 0x01), (x + 0x01, y + 0x01), (y + 0x01, x + 0x02))

Parameters: args – a list of bit-vectors representing the outputs of the current round.

classmethod get_rounds_outputs()[source]

Return the list of round outputs obtained in the last evaluation.

See also add_round_outputs.

class cascada.bitvector.ssa.SSAReturn(**kwargs)[source]

Bases: cascada.bitvector.operation.BvIdentity

Subclass of BvIdentity used to denote the returned variables in SSA.

Note that both BvIdentity and SSAReturn have the same string representation (but different Term.vrepr).

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.bitvector.operation import BvIdentity
>>> from cascada.bitvector.ssa import SSAReturn
>>> BvIdentity(Constant(0x1, 4)), SSAReturn(Constant(0x1, 4))
(0x1, 0x1)
>>> BvIdentity(Variable("x", 8)), SSAReturn(Variable("x", 8))
(Id(x), Id(x))
>>> BvIdentity(Variable("x", 8)).vrepr(), SSAReturn(Variable("x", 8)).vrepr()
("BvIdentity(Variable('x', width=8))", "SSAReturn(Variable('x', width=8))")

class cascada.bitvector.ssa.SSA(input_vars, output_vars, assignments, replace_multiuse_vars=False)[source]

Bases: object

Represent a BvFunction as a static single assignment program.

An SSA object represents a decomposition of a BvFunction into a list of simple assignments \(x_{i+1} \leftarrow f_i(x_i)\), similar as the method memoization_table for Operation objects. Recall a simple assignment is given by the output Variable \(x_{i+1}\) representing the output of the given Operation \(f_i(x_i)\), where \(x_i\) is an input or previous output Variable, a Constant, a scalar, or a list of them (but not an Operation object).

An SSA object is defined for

A list of Variable objects representing the inputs of the bit-vector function.
A list of Variable objects representing the outputs of the function.
The list of of assignments as a collections.OrderedDict mapping each intermediate Variable \(x_{i+1}\) to the Operation \(f_i(x_i)\).

The assignments might contain variables not defined in previous assignments nor contained in the input variables. These variables are called external variables and are stored in the attribute external_vars.

Apart from these three initialization argument, if the initialization argument replace_multiuse_vars is set to True, variables appearing two or more times in the list of assignments (as arguments of Operation objects excluding BvIdentity) are replaced by new variables (ending in __d where d is the occurrence index) that are used only once. In this case, the mapping from the old multiuse variables to the new singleuse variables is stored in multiuse_var2singleuse_vars. In other words, new variables are created to uniquely label each branch of the forking subroutine (see LinearModelFreeBranch).

Note

For example, with replace_multiuse_vars=True the assignment list (a0, x + 1), (a1, x & 1) is replaced by (x__0, Id(x)), (x__1, Id(x)) (a0, x__0 + 1), (a1, x__1 & 1).

SSA objects can be easily created from BvFunction.to_ssa.

Note

When initializing the SSA object, external variables are automatically obtained, redundant assignments are automatically removed (and a warning is printed in this case), and partial operations are automatically created from operations with constant or scalar operands.

Moreover, additional assignments with the operations BvIdentity and SSAReturn might be added at the end. These last assignemnts are added to ensure that each output variable of the SSA has a unique name (ending in _out) and to ensure that the output variables of the last assignments are actually the output variables of the SSA. If these assignments are already present in the given list of assigments no additional ones are added.

>>> from cascada.bitvector.ssa import BvFunction
>>> class MyFoo(BvFunction):
...     input_widths, output_widths = [8, 8], [8, 8]
...     @classmethod
...     def eval(cls, x, y):  return x ^ y, x
>>> MyFoo.to_ssa(["x", "y"], "a")  
SSA(input_vars=[x, y], output_vars=[a0_out, x_out],
    assignments=[(a0, x ^ y), (a0_out, Id(a0)), (x_out, Id(x))])
>>> ssa = MyFoo.to_ssa(["x", "y"], "a", replace_multiuse_vars=True)
>>> ssa  
SSA(input_vars=[x, y], output_vars=[a0_out, x_out],
    assignments=[(x__0, Id(x)), (x__1, Id(x)), (a0, x__0 ^ y), (a0_out, Id(a0)), (x_out, Id(x__1))])
>>> ssa.multiuse_var2singleuse_vars, ssa.singleuse_var2multiuse_var
(OrderedDict([(x, [x__0, x__1])]), OrderedDict([(x__0, x), (x__1, x)]))
>>> last_assignments = list(ssa.assignments.items())[-len(ssa.output_vars):]
>>> for var, expr in last_assignments: print(var.vrepr(), ", ", expr.vrepr(), sep="")
Variable('a0_out', width=8), SSAReturn(Variable('a0', width=8))
Variable('x_out', width=8), SSAReturn(Variable('x__1', width=8))

input_vars: a list of Variable objects representing the inputs.

output_vars: a list of Variable objects representing the outputs.

assignments: a collections.OrderedDict containing the assignments (Variable, Operation) of the SSA program.

external_vars: a list of Variable objects which appear in the assignments but are not defined in previous assignments nor contained in the input variables.

multiuse_var2singleuse_vars: an empty dictionary if the initialization argument replace_multiuse_vars is set to False, otherwise a collections.OrderedDict mapping the old multiuse variables to the new singleused variables.

singleuse_var2multiuse_var: the inverse mapping of multiuse_var2singleuse_vars.

vrepr()[source]

Return an executable string representation.

This method returns a string so that eval(self.vrepr()) returns a new SSA object with the same content.

>>> from cascada.bitvector.core import Variable
>>> from cascada.bitvector.operation import BvXor, BvIdentity
>>> from cascada.bitvector.ssa import BvFunction
>>> z = Variable("z", 8)
>>> class MyFoo(BvFunction):
...     input_widths, output_widths = [8, 8], [8, 8]
...     @classmethod
...     def eval(cls, x, y):  return y ^ z, x ^ 1
>>> MyFoo.to_ssa(["x", "y"], "i").vrepr()  
"SSA(input_vars=[Variable('x', width=8), Variable('y', width=8)],
    output_vars=[Variable('i0_out', width=8), Variable('i1_out', width=8)],
    assignments=[(Variable('i0', width=8), BvXor(Variable('y', width=8), Variable('z', width=8))),
        (Variable('i1', width=8),
            make_partial_operation(BvXor, (None, Constant(0b00000001, width=8)))(Variable('x', width=8))),
        (Variable('i0_out', width=8), SSAReturn(Variable('i0', width=8))),
        (Variable('i1_out', width=8), SSAReturn(Variable('i1', width=8)))])"

get_C_code(C_function_name)[source]

Return two strings (header and body) of a C function evalauting the SSA.

This method returns two strings (the function header and the function body) of a function in the C programming language that computes the SSA.

The C function is of void type and its list of arguments consists of the input variables, the external variables (if any) and the output variables. The output variables are defined as pointers to store the results.

See also crepr.

>>> from cascada.bitvector.core import Variable
>>> from cascada.bitvector.operation import BvXor, BvIdentity
>>> from cascada.bitvector.ssa import BvFunction
>>> z = Variable("z", 8)
>>> class MyFoo(BvFunction):
...     input_widths, output_widths = [8, 8], [8, 8]
...     @classmethod
...     def eval(cls, x, y):  return y ^ z, x ^ 1
>>> header, body = MyFoo.to_ssa(["x", "y"], "i").get_C_code("MyFoo")
>>> header
'void MyFoo(uint8_t x, uint8_t y, uint8_t z, uint8_t *i0_out, uint8_t *i1_out);'
>>> print(body)  
#include <stdint.h>
void MyFoo(uint8_t x, uint8_t y, uint8_t z, uint8_t *i0_out, uint8_t *i1_out){
    uint8_t i0 = y ^ z;
    uint8_t i1 = x ^ 0x1U;
    *i0_out = i0;
    *i1_out = i1;
};

eval(input_vals, external_var2val=None, C_code=False, **kwargs)[source]

Evaluate the SSA with Constant inputs and return the Constant outputs.

If some external variable is not given, it is replaced by the zero bit-vector.

>>> from cascada.bitvector.core import Variable, Constant
>>> from cascada.bitvector.ssa import BvFunction
>>> z = Variable("z", 8)
>>> class MyFoo(BvFunction):
...     input_widths, output_widths = [8, 8], [8, 8]
...     @classmethod
...     def eval(cls, x, y):  return y ^ z, x
>>> my_ssa = MyFoo.to_ssa(["x", "y"], "i")
>>> my_ssa  
SSA(input_vars=[x, y], output_vars=[i0_out, x_out], external_vars=[z],
    assignments=[(i0, y ^ z), (i0_out, Id(i0)), (x_out, Id(x))])
>>> my_ssa.external_vars
(z,)
>>> my_ssa.eval([Constant(0, 8), Constant(0, 8)])
(0x00, 0x00)

Parameters

input_vals – a list of Constant objects representing the inputs.
external_var2val – a dictionary mapping the external variables to its Constant values.
C_code – whether to evaluate the SSA by compiling and running its C code (see also get_C_code).

to_bvfunction()[source]

Return a BvFunction that evaluates self.

The returned BvFunction stores self in the _ssa attribute. Moreover, the method BvFunction.to_ssa of the returned BvFunction raises an exception unless it is called with the same arguments that were used to create _ssa (in this case _ssa is returned).

>>> from cascada.bitvector.ssa import BvFunction
>>> class MyFoo(BvFunction):
...     input_widths, output_widths = [8, 8], [8, 8]
...     @classmethod
...     def eval(cls, x, y):  return x ^ y, x
>>> MyFoo.to_ssa(["x", "y"], "a")  
SSA(input_vars=[x, y], output_vars=[a0_out, x_out],
    assignments=[(a0, x ^ y), (a0_out, Id(a0)), (x_out, Id(x))])
>>> MyFoo_v2 = MyFoo.to_ssa(["x", "y"], "a").to_bvfunction()
>>> MyFoo_v2.to_ssa(["x", "y"], "a")  
SSA(input_vars=[x, y], output_vars=[a0_out, x_out],
    assignments=[(a0, x ^ y), (a0_out, Id(a0)), (x_out, Id(x))])

copy()[source]

Return a deep copy of self.

>>> from cascada.bitvector.ssa import BvFunction
>>> class MyFoo(BvFunction):
...     input_widths, output_widths = [8, 8], [8, 8]
...     @classmethod
...     def eval(cls, x, y):  return x ^ y, x
>>> ssa = MyFoo.to_ssa(["x", "y"], "a")
>>> ssa  
SSA(input_vars=[x, y], output_vars=[a0_out, x_out],
    assignments=[(a0, x ^ y), (a0_out, Id(a0)), (x_out, Id(x))])
>>> ssa_copy = ssa.copy()
>>> ssa_copy  
SSA(input_vars=[x, y], output_vars=[a0_out, x_out],
    assignments=[(a0, x ^ y), (a0_out, Id(a0)), (x_out, Id(x))])
>>> ssa_copy.input_vars = tuple()
>>> ssa_copy.output_vars = tuple()
>>> ssa_copy.assignments = collections.OrderedDict()
>>> ssa_copy
SSA(input_vars=[], output_vars=[], assignments=[])
>>> ssa  
SSA(input_vars=[x, y], output_vars=[a0_out, x_out],
    assignments=[(a0, x ^ y), (a0_out, Id(a0)), (x_out, Id(x))])

split(var_separators)[source]

Split into multiple SSA objects given the list of variable separators.

Given the SSA \(s\), this method returns a list of SSA objects \(s_1, s_2, ..., s_n\), such that their composition \(s_n \circ s_{n-1} \dots \circ s_1\) is functionally equivalent to \(s\).

The argument var_separators is a list containing lists of variables. The \(i\)-th variable list denote the last variables of \(s_i\). In other words, the list of assignments of \(s_{i+1}\) immediately starts after the last assignments of the last variable in var_separators[i].

To split into \(n\) SSA objects, var_separators must contain \(n-1\) lists, as the variable list for \(s_n\) is not given (its last variables are the output variables of \(s\)).

>>> from cascada.bitvector.core import Variable
>>> from cascada.bitvector.ssa import BvFunction
>>> z = Variable("z", 8)
>>> var_separators = []
>>> class MyFoo(BvFunction):
...     input_widths, output_widths = [8], [8]
...     @classmethod
...     def eval(cls, x0):
...         var_separators.clear()
...         x1, y1 = (x0 + x0), x0
...         non_used_var = x1 + y1
...         var_separators.append([x1, y1, non_used_var])
...         return [(x1 | y1) & z]
>>> ssa = MyFoo.to_ssa(["x"], "a")
>>> ssa  
SSA(input_vars=[x], output_vars=[a3_out], external_vars=[z],
    assignments=[(a0, x + x), (a2, a0 | x), (a3, a2 & z), (a3_out, Id(a3))])
>>> var_separators
[[a0, x, a1]]
>>> for sub_ssa in ssa.split(var_separators): print(sub_ssa)  
SSA(input_vars=[x], output_vars=[a0_out, x_out],
    assignments=[(a0, x + x), (a0_out, Id(a0)), (x_out, Id(x))])
SSA(input_vars=[a0, x], output_vars=[a3_out], external_vars=[z],
    assignments=[(a2, a0 | x), (a3, a2 & z), (a3_out, Id(a3))])

get_round_separators()[source]

Return the round separators if the SSA was obtained from a RoundBasedFunction.

If the SSA object was obtained from RoundBasedFunction.to_ssa of a RoundBasedFunction including add_round_outputs calls in its eval, this method returns a list with the round outputs delimiting the rounds. Otherwise, None is returned.

In the first case, this list contains num_rounds - 1 entries, where the i-th entry is the list of outputs of the i-th round. In particular, the outputs of the last round are not included in this list.

The list returned by this method is meant to be used as the argument of split to get the SSA object of each round.

>>> from cascada.bitvector.ssa import RoundBasedFunction
>>> class MyFoo(RoundBasedFunction):
...     input_widths, output_widths, num_rounds = [8, 8], [8, 8], 1
...     @classmethod
...     def eval(cls, x, y):
...         for _ in range(cls.num_rounds):
...             x, y = y, x + 1
...             cls.add_round_outputs(x, y)
...         return x, y
...     @classmethod
...     def set_num_rounds(cls, new_num_rounds):  cls.num_rounds = new_num_rounds
>>> MyFoo.set_num_rounds(3)
>>> ssa = MyFoo.to_ssa(["x", "y"], "a")
>>> ssa  
SSA(input_vars=[x, y], output_vars=[a1_out, a2_out],
    assignments=[(a0, x + 0x01), (a1, y + 0x01), (a2, a0 + 0x01),
        (a1_out, Id(a1)), (a2_out, Id(a2))])
>>> round_separators = ssa.get_round_separators()
>>> round_separators
((y, a0), (a0, a1))
>>> for sub_ssa in ssa.split(round_separators): print(sub_ssa)  
SSA(input_vars=[x, y], output_vars=[y_out, a0_out],
    assignments=[(a0, x + 0x01), (y_out, Id(y)), (a0_out, Id(a0))])
SSA(input_vars=[y, a0], output_vars=[a0_out, a1_out],
    assignments=[(a1, y + 0x01), (a0_out, Id(a0)), (a1_out, Id(a1))])
SSA(input_vars=[a0, a1], output_vars=[a1_out, a2_out],
    assignments=[(a2, a0 + 0x01), (a1_out, Id(a1)), (a2_out, Id(a2))])

dotprinting(repeat=True, vrepr_label=False, **kwargs)[source]

Return the DOT description of the expression tree of the assignments.