diff options
Diffstat (limited to 'miasm/expression/smt2_helper.py')
| -rw-r--r-- | miasm/expression/smt2_helper.py | 296 |
1 files changed, 0 insertions, 296 deletions
diff --git a/miasm/expression/smt2_helper.py b/miasm/expression/smt2_helper.py deleted file mode 100644 index 53d323e8..00000000 --- a/miasm/expression/smt2_helper.py +++ /dev/null @@ -1,296 +0,0 @@ -# Helper functions for the generation of SMT2 expressions -# The SMT2 expressions will be returned as a string. -# The expressions are divided as follows -# -# - generic SMT2 operations -# - definitions of SMT2 structures -# - bit vector operations -# - array operations - -# generic SMT2 operations - -def smt2_eq(a, b): - """ - Assignment: a = b - """ - return "(= {} {})".format(a, b) - - -def smt2_implies(a, b): - """ - Implication: a => b - """ - return "(=> {} {})".format(a, b) - - -def smt2_and(*args): - """ - Conjunction: a and b and c ... - """ - # transform args into strings - args = [str(arg) for arg in args] - return "(and {})".format(' '.join(args)) - - -def smt2_or(*args): - """ - Disjunction: a or b or c ... - """ - # transform args into strings - args = [str(arg) for arg in args] - return "(or {})".format(' '.join(args)) - - -def smt2_ite(cond, a, b): - """ - If-then-else: cond ? a : b - """ - return "(ite {} {} {})".format(cond, a, b) - - -def smt2_distinct(*args): - """ - Distinction: a != b != c != ... - """ - # transform args into strings - args = [str(arg) for arg in args] - return "(distinct {})".format(' '.join(args)) - - -def smt2_assert(expr): - """ - Assertion that @expr holds - """ - return "(assert {})".format(expr) - - -# definitions - -def declare_bv(bv, size): - """ - Declares an bit vector @bv of size @size - """ - return "(declare-fun {} () {})".format(bv, bit_vec(size)) - - -def 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 - """ - return "(declare-fun {} () (Array {} {}))".format(a, bv1, bv2) - - -def 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 - """ - return "(_ bv{} {})".format(v, size) - - -def bit_vec(size): - """ - Returns a bit vector of size @size - """ - return "(_ BitVec {})".format(size) - - -# bit vector operations - -def bvadd(a, b): - """ - Addition: a + b - """ - return "(bvadd {} {})".format(a, b) - - -def bvsub(a, b): - """ - Subtraction: a - b - """ - return "(bvsub {} {})".format(a, b) - - -def bvmul(a, b): - """ - Multiplication: a * b - """ - return "(bvmul {} {})".format(a, b) - - -def bvand(a, b): - """ - Bitwise AND: a & b - """ - return "(bvand {} {})".format(a, b) - - -def bvor(a, b): - """ - Bitwise OR: a | b - """ - return "(bvor {} {})".format(a, b) - - -def bvxor(a, b): - """ - Bitwise XOR: a ^ b - """ - return "(bvxor {} {})".format(a, b) - - -def bvneg(bv): - """ - Unary minus: - bv - """ - return "(bvneg {})".format(bv) - - -def bvsdiv(a, b): - """ - Signed division: a / b - """ - return "(bvsdiv {} {})".format(a, b) - - -def bvudiv(a, b): - """ - Unsigned division: a / b - """ - return "(bvudiv {} {})".format(a, b) - - -def bvsmod(a, b): - """ - Signed modulo: a mod b - """ - return "(bvsmod {} {})".format(a, b) - - -def bvurem(a, b): - """ - Unsigned modulo: a mod b - """ - return "(bvurem {} {})".format(a, b) - - -def bvshl(a, b): - """ - Shift left: a << b - """ - return "(bvshl {} {})".format(a, b) - - -def bvlshr(a, b): - """ - Logical shift right: a >> b - """ - return "(bvlshr {} {})".format(a, b) - - -def bvashr(a, b): - """ - Arithmetic shift right: a a>> b - """ - return "(bvashr {} {})".format(a, b) - - -def 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 - """ - - # define constant - s = bit_vec_val(size, size) - - # shift = b & (size - 1) - shift = bvand(b, bvsub(s, bit_vec_val(1, size))) - - # (a << shift) | (a >> size - shift) - rotate = bvor(bvshl(a, shift), - bvlshr(a, bvsub(s, shift))) - - return rotate - - -def 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 - """ - - # define constant - s = bit_vec_val(size, size) - - # shift = b & (size - 1) - shift = bvand(b, bvsub(s, bit_vec_val(1, size))) - - # (a >> shift) | (a << size - shift) - rotate = bvor(bvlshr(a, shift), - bvshl(a, bvsub(s, shift))) - - return rotate - - -def bv_extract(high, low, bv): - """ - Extracts bits from a bit vector - :param high: end bit - :param low: start bit - :param bv: bit vector - """ - return "((_ extract {} {}) {})".format(high, low, bv) - - -def bv_concat(a, b): - """ - Concatenation of two SMT2 expressions - """ - return "(concat {} {})".format(a, b) - - -# array operations - -def array_select(array, index): - """ - Reads from an SMT2 array at index @index - :param array: SMT2 array - :param index: SMT2 expression, index of the array - """ - return "(select {} {})".format(array, index) - - -def 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 - """ - return "(store {} {} {})".format(array, index, value) |