cascada.algebraic.value module

Represent type of value properties.

`Value`	Represent value properties.
`WordValue`	Represent word value properties.
`BitValue`	Represent bit value properties.

class cascada.algebraic.value.Value(value)[source]

Bases: cascada.abstractproperty.property.Property

Represent value properties.

Given a function \(f\), a Value property pair \((\alpha, \beta)\) is a bit-vector Property \((\alpha, \beta)\) where the propagation probability is simply 1 if \(\beta = f(\alpha)\) otherwise 0, that is, the propagation probability is 0 or 1 depending on whether the output value is the image of the input value through \(f\).

This class is not meant to be instantiated but to provide a base class for the different representations of the value of a bit-vector (see BitValue or WordValue).

Internally, Value is a subclass of Property (as Difference). The Value methods inherited from Property requiring arguments of type Property should be called instead with arguments of type Value.

get_value()[source]

Return the value of the underlying bit-vector.

Subclasses of Value can represent the underlying bit-vector in different ways and return its value in different ways (i.e., not only as self.val).

class cascada.algebraic.value.WordValue(value)[source]

Bases: cascada.algebraic.value.Value

Represent word value properties.

The word value is a Value property where the underlying bit-vector value of the property is given as is (i.e., as a bit-vector Term).

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.algebraic.value import WordValue
>>> alpha = WordValue(Constant(0b001, 3))
>>> alpha, alpha.val
(WordValue(0b001), 0b001)
>>> alpha.get_value()
0b001
>>> alpha = WordValue(Variable("alpha", 3))
>>> alpha, alpha.val
(WordValue(alpha), alpha)

get_value()[source]: Return the value of the underlying bit-vector as self.val.

classmethod propagate(op, input_val)[source]

Propagate the given input WordValue through the given operation.

For any operation op and any input value input_val, the output value output_val is uniquely determined and its bit-vector value is f(input_val).

See Property.propagate for more information.

User-defined or new Operation op can store its associated WordValue algebraic.opmodel.OpModel in op.word_model, as this method first checks whether op has its associated algebraic.opmodel.OpModel stored in the class attribute word_model.

>>> from cascada.bitvector.core import Variable, Constant
>>> from cascada.bitvector.operation import BvXor, BvIdentity
>>> from cascada.algebraic.value import WordValue
>>> d1, d2 = WordValue(Variable("d1", 8)), WordValue(Constant(1, 8))
>>> WordValue.propagate(BvXor, [d1, d2])
WordValue(d1 ^ 0x01)
>>> WordValue.propagate(BvIdentity, d1)
WordModelId(WordValue(d1))

class cascada.algebraic.value.BitValue(value)[source]

Bases: cascada.algebraic.value.Value

Represent bit value properties.

The bit value is a Value property where the underlying bit-vector value of the property is given as the list of its bits (starting from the least significant bit (LSB) and ending in the MSB).

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.algebraic.value import BitValue
>>> alpha = BitValue(Constant(0b001, 3))
>>> alpha, alpha.val
(BitValue(0b001), 0b001)
>>> alpha.get_value()
(0b1, 0b0, 0b0)
>>> alpha = BitValue(Variable("alpha", 3))
>>> alpha, alpha.val
(BitValue(alpha), alpha)
>>> alpha.get_value()
(alpha[0], alpha[1], alpha[2])

get_value()[source]: Return the value of the underling bit-vector as the list of its bits.

classmethod propagate(op, input_val)[source]

Propagate the given input BitValue through the given operation.

For any operation op and any input value input_val, the output value is uniquely determined and its bit-vector value is f(input_val).

For some operations, the output value is given implicitly through a system of binary equations or constraints (see BitModelBvAdd). For these operations, this method return an algebraic.opmodel.OpModel.

See Property.propagate for more information.

User-defined or new Operation op can store its associated BitValue algebraic.opmodel.OpModel in op.bit_model, as this method first checks whether op has its associated algebraic.opmodel.OpModel stored in the class attribute bit_model.

>>> from cascada.bitvector.core import Variable, Constant
>>> from cascada.bitvector.operation import BvXor, Concat, BvIdentity
>>> from cascada.algebraic.value import BitValue
>>> d1, d2 = BitValue(Variable("d1", 2)), BitValue(Constant(1, 2))
>>> BitValue.propagate(BvXor, [d1, d2])
BitValue((d1[1]) :: ~(d1[0]))
>>> d1, d2 = BitValue(Variable("d1", 2)), BitValue(Variable("d2", 2))
>>> BitValue.propagate(Concat, [d1, d2])
BitValue(d1 :: (d2[1]) :: (d2[0]))
>>> BitValue.propagate(BvIdentity, d1)
BitValue(Id(d1[1]) :: Id(d1[0]))