Arybo reference

class arybo.lib.MBA(nbits)

Represents an MBA (Miwed Boolean Arithmetic) space of a fixed number of bits.

from_vec(v)

Get an MBAVariable object with the vector’s values.

Args:

v: a pytanque vector holding boolean expressions

Returns:

An MBAVariable object with the vector’s values

permut2expr(P)

Convert a substitution table into an arybo application

Args:

P: list of integers. The list must not contain more than 2**nbits elements.

Returns:

A tuple containing an MBAVariable object with the result and the symbolic input variable used in this object. A typical use case is to feed these into vectorial_decomp.

Example:

>>> mba = MBA(4)
>>> P = [i^7 for i in range(16)]
>>> E,X = mba.permut2expr(P)
>>> E.vectorial_decomp([X])
App NL = Vec([
0,
0,
0,
0
])
AffApp matrix = Mat([
[1, 0, 0, 0]
[0, 1, 0, 0]
[0, 0, 1, 0]
[0, 0, 0, 1]
])
AffApp cst = Vec([
1,
1,
1,
0
])

var(name)

Get an n-bit named symbolic variable

Returns:

An MBAVariable object representing a symbolic variable

Example:

>>> mba.var('x')
Vec([
x0,
x1,
x2,
x3
])

class arybo.lib.MBAVariable(mba, arg)

Represents a symbolic variable in a given MBA space.

This object is the main object to use when computing expressions with arybo. It supports both the arithmetic and boolean logic, allowing the computation of expressions that use both arithmetics. The corresponding Python operators are overloaded, allowing to directly write expressions like this:

>>> x = mba.var('x')
>>> e = ((x+7)|10)//9

It internally holds a pytanque.Vector object that represents the n-bit expressions associated with this symbolic variable.

always_expand_esf(v=True)

Specify whether ESF should always be expanded

always_simplify(v=True)

If v is true, force a call to simplify each time an operation is done

at(idx)

Returns the boolean expression of the idx-th bit

eval(values)

Evaluates the expression to an integer

values is a dictionnary that associates n-bit variables to integer values. Every symbolic variables used in the expression must be represented.

For instance, let x and y 4-bit variables, and e = x+y:

>>> mba = MBA(4)
>>> x = mba.var('x')
>>> y = mba.var('y')
>>> e = x+y

To evaluate e with x=4 and y=5, we can do:

>>> e.eval({x: 4, y: 5})
9

If a variable is missing from values, an exception will occur. (x or y in the example above)

evaluate(values)

Evaluates the expression to an integer

values is a dictionnary that associates n-bit variables to integer values. Every symbolic variables used in the expression must be represented.

For instance, let x and y 4-bit variables, and e = x+y:

>>> mba = MBA(4)
>>> x = mba.var('x')
>>> y = mba.var('y')
>>> e = x+y

To evaluate e with x=4 and y=5, we can do:

>>> e.eval({x: 4, y: 5})
9

If a variable is missing from values, an exception will occur. (x or y in the example above)

expand_esf()

Expand ESF in the expression

expand_esf_and_simplify()

Expand and simplify the expression

sext(n)

Sign-extend the variable to n bits.

n bits must be stricly larger than the actual number of bits, or a ValueError is thrown

simplify()

Simplify the expression

to_bytes()

Convert the expression to bytes if possible (that is only immediates are present).

A current limitation is that the number of bits must be a multiple of 8.

to_cst()

Convert the expression to a constant if possible (that is only immediates are present)

vec

Returns the underlying vector object

vector

Returns the underlying vector object

vectorial_decomp(symbols)

Compute the vectorial decomposition of the expression according to the given symbols.

symbols is a list that represents the input of the resulting application. They are considerated as a flatten vector of bits.

Args:

symbols: TODO

Returns:

An pytanque.App object

Example:

>>> mba = MBA(4)
>>> x = mba.var('x')
>>> y = mba.var('y')
>>> e = x^y^6
>>> e.vectorial_decomp([x,y])
App NL = Vec([
0,
0,
0,
0
])
AffApp matrix = Mat([
    [1, 0, 0, 0, 1, 0, 0, 0]
    [0, 1, 0, 0, 0, 1, 0, 0]
    [0, 0, 1, 0, 0, 0, 1, 0]
    [0, 0, 0, 1, 0, 0, 0, 1]
    ])
AffApp cst = Vec([
    0,
    1,
    1,
    0
    ])

zext(n)

Zero-extend the variable to n bits.

n bits must be stricly larger than the actual number of bits, or a ValueError is thrown

arybo.lib.exprs_asm.asm_binary(exprs, dst_reg, sym_to_reg, triple_or_target=None)

Compile and assemble an expression for a given architecture.

Arguments:

• exprs: list of expressions to convert. This can represent a graph of expressions.
• dst_reg: final register on which to store the result of the last expression. This is represented by a tuple (“reg_name”, reg_size_bits). Example: (“rax”, 64)
• sym_to_reg: a dictionnary that maps Arybo variable name to registers (described as tuple, see dst_reg). Example: {“x”: (“rdi”,64), “y”: (“rsi”, 64)}
• triple_or_target: LLVM architecture triple to use. Use by default the host architecture. Example: “x86_64-unknown-unknown”

Output:

• binary stream of the assembled expression for the given target

Here is an example that will compile and assemble “x+y” for x86_64:

from arybo.lib import MBA 
from arybo.lib import mba_exprs
from arybo.lib.exprs_asm import asm_binary
mba = MBA(64)
x = mba.var("x")
y = mba.var("y")
e = mba_exprs.ExprBV(x) + mba_exprs.ExprBV(y)
code = asm_binary([e], ("rax", 64), {"x": ("rdi", 64), "y": ("rsi", 64)}, "x86_64-unknown-unknown")
print(code.hex())

which outputs 488d0437 (which is equivalent to lea rax,[rdi+rsi*1]).

arybo.lib.exprs_asm.asm_module(exprs, dst_reg, sym_to_reg, triple_or_target=None)

Generate an LLVM module for a list of expressions

Arguments:

• See arybo.lib.exprs_asm.asm_binary() for a description of the list of arguments

Output:

• An LLVM module with one function named “__arybo”, containing the translated expression.

See arybo.lib.exprs_asm.asm_binary() for an usage example.

arybo.lib.boolean_expr_solve(e, X, v=1)

arybo.tools.tritonast2arybo(e, use_exprs=True, use_esf=False, context=None)

Convert a subset of Triton’s AST into Arybo’s representation

Args:

e: Triton AST use_esf: use ESFs when creating the final expression context: dictionnary that associates Triton expression ID to arybo expressions

Returns:

An arybo.lib.MBAVariable object

arybo.tools.tritonexprs2arybo(exprs)