Dev exp unsound

manticore/core/smtlib/expression.py

@@ -40,13 +40,13 @@ def taint(self):
 
 def issymbolic(value) -> bool:
     """
-        Helper to determine whether an object is symbolic (e.g checking
-        if data read from memory is symbolic)
+    Helper to determine whether an object is symbolic (e.g checking
+    if data read from memory is symbolic)
 
-        :param object value: object to check
-        :return: whether `value` is symbolic
-        :rtype: bool
-        """
+    :param object value: object to check
+    :return: whether `value` is symbolic
+    :rtype: bool
+    """
     return isinstance(value, Expression)
 
 
@@ -293,6 +293,9 @@ def __mul__(self, other):
     def __mod__(self, other):
         return BitVecMod(self, self.cast(other))
 
+    def __pow__(self, other):
+        return BitVecPow(self, self.cast(other))
+
     # object.__divmod__(self, other)
     # object.__pow__(self, other[, modulo])
 
@@ -543,6 +546,11 @@ def __init__(self, a, b, *args, **kwargs):
         super().__init__(a.size, a, b, *args, **kwargs)
 
 
+class BitVecPow(BitVecOperation):
+    def __init__(self, a, b, *args, **kwargs):
+        super().__init__(a.size, a, b, *args, **kwargs)
+
+
 class BitVecDiv(BitVecOperation):
     def __init__(self, a, b, *args, **kwargs):
         super().__init__(a.size, a, b, *args, **kwargs)
@@ -676,7 +684,7 @@ class Array(Expression):
     def __init__(
         self, index_bits: int, index_max: Optional[int], value_bits: int, *operands, **kwargs
     ):
-        assert index_bits in (32, 64, 256)
+        assert index_bits in (8, 32, 64, 256)
         assert value_bits in (8, 16, 32, 64, 256)
         assert index_max is None or index_max >= 0 and index_max < 2 ** index_bits
         self._index_bits = index_bits

manticore/core/smtlib/visitors.py

@@ -930,6 +930,9 @@ def bindings(self):
         ArraySelect: "select",
     }
 
+    def visit_BitVecPow(self, expression, base, exponent):
+        return f"((_ int2bv {expression.size})  ( ^ (bv2int {base}) (bv2int {exponent}) ))"
+
     def visit_BitVecConstant(self, expression):
         assert isinstance(expression, BitVecConstant)
         if expression.size == 1: