miasm.expression.smt2_helper Namespace Reference

Functions
def	smt2_eq (a, b)
def	smt2_implies (a, b)
def	smt2_and (*args)
def	smt2_or (*args)
def	smt2_ite (cond, a, b)
def	smt2_distinct (*args)
def	smt2_assert (expr)
def	declare_bv (bv, size)
def	declare_array (a, bv1, bv2)
def	bit_vec_val (v, size)
def	bit_vec (size)
def	bvadd (a, b)
def	bvsub (a, b)
def	bvmul (a, b)
def	bvand (a, b)
def	bvor (a, b)
def	bvxor (a, b)
def	bvneg (bv)
def	bvsdiv (a, b)
def	bvudiv (a, b)
def	bvsmod (a, b)
def	bvurem (a, b)
def	bvshl (a, b)
def	bvlshr (a, b)
def	bvashr (a, b)
def	bv_rotate_left (a, b, size)
def	bv_rotate_right (a, b, size)
def	bv_extract (high, low, bv)
def	bv_concat (a, b)
def	array_select (array, index)
def	array_store (array, index, value)

Function Documentation

array_select()

def miasm.expression.smt2_helper.array_select	(		array,
			index
	)

Reads from an SMT2 array at index @index
:param array: SMT2 array
:param index: SMT2 expression, index of the array

Here is the caller graph for this function:

array_store()

def miasm.expression.smt2_helper.array_store	(		array,
			index,
			value
	)

Writes an value into an SMT2 array at address @index
:param array: SMT array
:param index: SMT2 expression, index of the array
:param value: SMT2 expression, value to write

bit_vec()

def miasm.expression.smt2_helper.bit_vec

(

size

)

Returns a bit vector of size @size

Here is the caller graph for this function:

bit_vec_val()

def miasm.expression.smt2_helper.bit_vec_val	(		v,
			size
	)

Declares a bit vector value
:param v: int, value of the bit vector
:param size: size of the bit vector

Here is the caller graph for this function:

bv_concat()

def miasm.expression.smt2_helper.bv_concat	(		a,
			b
	)

Concatenation of two SMT2 expressions

Here is the caller graph for this function:

bv_extract()

def miasm.expression.smt2_helper.bv_extract	(		high,
			low,
			bv
	)

Extracts bits from a bit vector
:param high: end bit
:param low: start bit
:param bv: bit vector

Here is the caller graph for this function:

bv_rotate_left()

def miasm.expression.smt2_helper.bv_rotate_left	(		a,
			b,
			size
	)

Rotates bits of a to the left b times: a <<< b

Since ((_ rotate_left b) a) does not support
symbolic values for b, the implementation is
based on a C implementation.

Therefore, the rotation will be computed as
a << (b & (size - 1))) | (a >> (size - (b & (size - 1))))

:param a: bit vector
:param b: bit vector
:param size: size of a

Here is the call graph for this function:

Here is the caller graph for this function:

bv_rotate_right()

def miasm.expression.smt2_helper.bv_rotate_right	(		a,
			b,
			size
	)

Rotates bits of a to the right b times: a >>> b

Since ((_ rotate_right b) a) does not support
symbolic values for b, the implementation is
based on a C implementation.

Therefore, the rotation will be computed as
a >> (b & (size - 1))) | (a << (size - (b & (size - 1))))

:param a: bit vector
:param b: bit vector
:param size: size of a

Here is the call graph for this function:

Here is the caller graph for this function:

bvadd()

def miasm.expression.smt2_helper.bvadd	(		a,
			b
	)

Addition: a + b

Here is the caller graph for this function:

bvand()

def miasm.expression.smt2_helper.bvand	(		a,
			b
	)

Bitwise AND: a & b

Here is the caller graph for this function:

bvashr()

def miasm.expression.smt2_helper.bvashr	(		a,
			b
	)

Arithmetic shift right: a a>> b

Here is the caller graph for this function:

bvlshr()

def miasm.expression.smt2_helper.bvlshr	(		a,
			b
	)

Logical shift right: a >> b

Here is the caller graph for this function:

bvmul()

def miasm.expression.smt2_helper.bvmul	(		a,
			b
	)

Multiplication: a * b

Here is the caller graph for this function:

bvneg()

def miasm.expression.smt2_helper.bvneg

(

bv

)

Unary minus: - bv

Here is the caller graph for this function:

bvor()

def miasm.expression.smt2_helper.bvor	(		a,
			b
	)

Bitwise OR: a | b

Here is the caller graph for this function:

bvsdiv()

def miasm.expression.smt2_helper.bvsdiv	(		a,
			b
	)

Signed division: a / b

Here is the caller graph for this function:

bvshl()

def miasm.expression.smt2_helper.bvshl	(		a,
			b
	)

Shift left: a << b

Here is the caller graph for this function:

bvsmod()

def miasm.expression.smt2_helper.bvsmod	(		a,
			b
	)

Signed modulo: a mod b

Here is the caller graph for this function:

bvsub()

def miasm.expression.smt2_helper.bvsub	(		a,
			b
	)

Subtraction: a - b

Here is the caller graph for this function:

bvudiv()

def miasm.expression.smt2_helper.bvudiv	(		a,
			b
	)

Unsigned division: a / b

Here is the caller graph for this function:

bvurem()

def miasm.expression.smt2_helper.bvurem	(		a,
			b
	)

Unsigned modulo: a mod b

Here is the caller graph for this function:

bvxor()

def miasm.expression.smt2_helper.bvxor	(		a,
			b
	)

Bitwise XOR: a ^ b

Here is the caller graph for this function:

declare_array()

def miasm.expression.smt2_helper.declare_array	(		a,
			bv1,
			bv2
	)

Declares an SMT2 array represented as a map
from a bit vector to another bit vector.
:param a: array name
:param bv1: SMT2 bit vector
:param bv2: SMT2 bit vector

Here is the caller graph for this function:

declare_bv()

def miasm.expression.smt2_helper.declare_bv	(		bv,
			size
	)

Declares an bit vector @bv of size @size

Here is the call graph for this function:

Here is the caller graph for this function:

smt2_and()

def miasm.expression.smt2_helper.smt2_and

(

*

args

)

Conjunction: a and b and c ...

Here is the caller graph for this function:

smt2_assert()

def miasm.expression.smt2_helper.smt2_assert

(

expr

)

Assertion that @expr holds

Here is the caller graph for this function:

smt2_distinct()

def miasm.expression.smt2_helper.smt2_distinct

(

*

args

)

Distinction: a != b != c != ...

Here is the caller graph for this function:

smt2_eq()

def miasm.expression.smt2_helper.smt2_eq	(		a,
			b
	)

Assignment: a = b

Here is the caller graph for this function:

smt2_implies()

def miasm.expression.smt2_helper.smt2_implies	(		a,
			b
	)

Implication: a => b

smt2_ite()

def miasm.expression.smt2_helper.smt2_ite	(		cond,
			a,
			b
	)

If-then-else: cond ? a : b

Here is the caller graph for this function:

smt2_or()

def miasm.expression.smt2_helper.smt2_or

(

*

args

)

Disjunction: a or b or c ...