Convert to src-layout ta/nix

1 files changed, 296 insertions, 0 deletions

diff --git a/src/miasm/expression/smt2_helper.py b/src/miasm/expression/smt2_helper.py
new file mode 100644
index 00000000..53d323e8
--- /dev/null
+++ b/src/miasm/expression/smt2_helper.py
@@ -0,0 +1,296 @@
+# 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)