Add __slots__ to expressions

manticore/core/smtlib/constraints.py

@@ -158,7 +158,7 @@ def to_string(self, related_to=None, replace_constants=False):
                 if (
                     isinstance(expression, BoolEqual)
                     and isinstance(expression.operands[0], Variable)
-                    and isinstance(expression.operands[1], (Variable, Constant))
+                    and isinstance(expression.operands[1], (*Variable, *Constant))
                 ):
                     constant_bindings[expression.operands[0]] = expression.operands[1]
 
@@ -327,7 +327,7 @@ def migrate(self, expression, name_migration_map=None):
                     ).array
                 else:
                     raise NotImplemented(
-                        f"Unknown expression type {type(var)} encountered during expression migration"
+                        f"Unknown expression type {type(foreign_var)} encountered during expression migration"
                     )
                 # Update the var to var mapping
                 object_migration_map[foreign_var] = new_var

manticore/core/smtlib/expression.py

@@ -4,7 +4,7 @@
 
 import re
 import copy
-from typing import Union, Optional, Dict
+from typing import Union, Optional, Dict, List
 
 
 class ExpressionException(SmtlibError):
@@ -18,6 +18,8 @@ class ExpressionException(SmtlibError):
 class Expression:
     """ Abstract taintable Expression. """
 
+    __slots__ = ["_taint"]
+
     def __init__(self, taint: Union[tuple, frozenset] = ()):
         if self.__class__ is Expression:
             raise TypeError
@@ -110,66 +112,11 @@ def taint_with(arg, *taints, value_bits=256, index_bits=256):
     return arg
 
 
-class Variable(Expression):
-    def __init__(self, name: str, *args, **kwargs):
-        if self.__class__ is Variable:
-            raise TypeError
-        assert " " not in name
-        super().__init__(*args, **kwargs)
-        self._name = name
-
-    @property
-    def declaration(self):
-        pass
-
-    @property
-    def name(self):
-        return self._name
-
-    def __copy__(self, memo):
-        raise ExpressionException("Copying of Variables is not allowed.")
-
-    def __deepcopy__(self, memo):
-        raise ExpressionException("Copying of Variables is not allowed.")
-
-    def __repr__(self):
-        return "<{:s}({:s}) at {:x}>".format(type(self).__name__, self.name, id(self))
-
-
-class Constant(Expression):
-    def __init__(self, value: Union[bool, int], *args, **kwargs):
-        if self.__class__ is Constant:
-            raise TypeError
-        super().__init__(*args, **kwargs)
-        self._value = value
-
-    @property
-    def value(self):
-        return self._value
-
-
-class Operation(Expression):
-    def __init__(self, *operands, **kwargs):
-        if self.__class__ is Operation:
-            raise TypeError
-        # assert len(operands) > 0
-        # assert all(isinstance(x, Expression) for x in operands)
-        self._operands = operands
-
-        # If taint was not forced by a keyword argument, calculate default
-        if "taint" not in kwargs:
-            kwargs["taint"] = reduce(lambda x, y: x.union(y.taint), operands, frozenset())
-
-        super().__init__(**kwargs)
-
-    @property
-    def operands(self):
-        return self._operands
-
-
 ###############################################################################
 # Booleans
 class Bool(Expression):
+    __slots__: List[str] = []
+
     def __init__(self, *operands, **kwargs):
         super().__init__(*operands, **kwargs)
 
@@ -215,26 +162,61 @@ def __bool__(self):
         raise NotImplementedError("__bool__ for Bool")
 
 
-class BoolVariable(Bool, Variable):
-    def __init__(self, name, *args, **kwargs):
-        super().__init__(name, *args, **kwargs)
+class BoolVariable(Bool):
+    __slots__ = ["_name"]
+
+    def __init__(self, name: str, *args, **kwargs):
+        assert " " not in name
+        super().__init__(*args, **kwargs)
+        self._name = name
+
+    @property
+    def name(self):
+        return self._name
+
+    def __copy__(self, memo=""):
+        raise ExpressionException("Copying of Variables is not allowed.")
+
+    def __deepcopy__(self, memo=""):
+        raise ExpressionException("Copying of Variables is not allowed.")
+
+    def __repr__(self):
+        return "<{:s}({:s}) at {:x}>".format(type(self).__name__, self.name, id(self))
 
     @property
     def declaration(self):
         return f"(declare-fun {self.name} () Bool)"
 
 
-class BoolConstant(Bool, Constant):
+class BoolConstant(Bool):
+    __slots__ = ["_value"]
+
     def __init__(self, value: bool, *args, **kwargs):
-        super().__init__(value, *args, **kwargs)
+        self._value = value
+        super().__init__(*args, **kwargs)
 
     def __bool__(self):
         return self.value
 
+    @property
+    def value(self):
+        return self._value
+
+
+class BoolOperation(Bool):
+    __slots__ = ["_operands"]
 
-class BoolOperation(Operation, Bool):
     def __init__(self, *operands, **kwargs):
-        super().__init__(*operands, **kwargs)
+        self._operands = operands
+
+        # If taint was not forced by a keyword argument, calculate default
+        kwargs.setdefault("taint", reduce(lambda x, y: x.union(y.taint), operands, frozenset()))
+
+        super().__init__(**kwargs)
+
+    @property
+    def operands(self):
+        return self._operands
 
 
 class BoolNot(BoolOperation):
@@ -265,6 +247,8 @@ def __init__(self, cond: "Bool", true: "Bool", false: "Bool", **kwargs):
 class BitVec(Expression):
     """ This adds a bitsize to the Expression class """
 
+    __slots__ = ["size"]
+
     def __init__(self, size, *operands, **kwargs):
         super().__init__(*operands, **kwargs)
         self.size = size
@@ -465,18 +449,38 @@ def Bool(self):
         return self != 0
 
 
-class BitVecVariable(BitVec, Variable):
-    def __init__(self, *args, **kwargs):
-        super().__init__(*args, **kwargs)
+class BitVecVariable(BitVec):
+    __slots__ = ["_name"]
+
+    def __init__(self, size: int, name: str, *args, **kwargs):
+        assert " " not in name
+        super().__init__(size, *args, **kwargs)
+        self._name = name
+
+    @property
+    def name(self):
+        return self._name
+
+    def __copy__(self, memo=""):
+        raise ExpressionException("Copying of Variables is not allowed.")
+
+    def __deepcopy__(self, memo=""):
+        raise ExpressionException("Copying of Variables is not allowed.")
+
+    def __repr__(self):
+        return "<{:s}({:s}) at {:x}>".format(type(self).__name__, self.name, id(self))
 
     @property
     def declaration(self):
         return f"(declare-fun {self.name} () (_ BitVec {self.size}))"
 
 
-class BitVecConstant(BitVec, Constant):
+class BitVecConstant(BitVec):
+    __slots__ = ["_value"]
+
     def __init__(self, size: int, value: int, *args, **kwargs):
-        super().__init__(size, value, *args, **kwargs)
+        self._value = value
+        super().__init__(size, *args, **kwargs)
 
     def __bool__(self):
         return self.value != 0
@@ -489,10 +493,25 @@ def __eq__(self, other):
     def __hash__(self):
         return super().__hash__()
 
+    @property
+    def value(self):
+        return self._value
+
+
+class BitVecOperation(BitVec):
+    __slots__ = ["_operands"]
 
-class BitVecOperation(BitVec, Operation):
     def __init__(self, size, *operands, **kwargs):
-        super().__init__(size, *operands, **kwargs)
+        self._operands = operands
+
+        # If taint was not forced by a keyword argument, calculate default
+        kwargs.setdefault("taint", reduce(lambda x, y: x.union(y.taint), operands, frozenset()))
+
+        super().__init__(size, **kwargs)
+
+    @property
+    def operands(self):
+        return self._operands
 
 
 class BitVecAdd(BitVecOperation):
@@ -638,6 +657,8 @@ def __init__(self, a, b, *args, **kwargs):
 ###############################################################################
 # Array  BV32 -> BV8  or BV64 -> BV8
 class Array(Expression):
+    __slots__ = ["_index_bits", "_index_max", "_value_bits"]
+
     def __init__(
         self, index_bits: int, index_max: Optional[int], value_bits: int, *operands, **kwargs
     ):
@@ -862,20 +883,46 @@ def __radd__(self, other):
         return new_arr
 
 
-class ArrayVariable(Array, Variable):
-    def __init__(self, index_bits, index_max, value_bits, name, *operands, **kwargs):
-        super().__init__(index_bits, index_max, value_bits, name, **kwargs)
+class ArrayVariable(Array):
+    __slots__ = ["_name"]
+
+    def __init__(self, index_bits, index_max, value_bits, name, *args, **kwargs):
+        assert " " not in name
+        super().__init__(index_bits, index_max, value_bits, *args, **kwargs)
+        self._name = name
+
+    @property
+    def name(self):
+        return self._name
+
+    def __copy__(self, memo=""):
+        raise ExpressionException("Copying of Variables is not allowed.")
+
+    def __deepcopy__(self, memo=""):
+        raise ExpressionException("Copying of Variables is not allowed.")
+
+    def __repr__(self):
+        return "<{:s}({:s}) at {:x}>".format(type(self).__name__, self.name, id(self))
 
     @property
     def declaration(self):
         return f"(declare-fun {self.name} () (Array (_ BitVec {self.index_bits}) (_ BitVec {self.value_bits})))"
 
 
-class ArrayOperation(Array, Operation):
+class ArrayOperation(Array):
+    __slots__ = ["_operands"]
+
     def __init__(self, array: Array, *operands, **kwargs):
-        super().__init__(
-            array.index_bits, array.index_max, array.value_bits, array, *operands, **kwargs
-        )
+        self._operands = (array, *operands)
+
+        # If taint was not forced by a keyword argument, calculate default
+        kwargs.setdefault("taint", reduce(lambda x, y: x.union(y.taint), operands, frozenset()))
+
+        super().__init__(array.index_bits, array.index_max, array.value_bits, **kwargs)
+
+    @property
+    def operands(self):
+        return self._operands
 
 
 class ArrayStore(ArrayOperation):
@@ -1133,10 +1180,17 @@ def get(self, index, default=None):
         return BitVecITE(self._array.value_bits, is_known, value, default)
 
 
-class ArraySelect(BitVec, Operation):
-    def __init__(self, array: "Array", index: "BitVec", *args, **kwargs):
+class ArraySelect(BitVec):
+    __slots__ = ["_operands"]
+
+    def __init__(self, array: "Array", index: "BitVec", *operands, **kwargs):
         assert index.size == array.index_bits
-        super().__init__(array.value_bits, array, index, *args, **kwargs)
+        self._operands = (array, index, *operands)
+
+        # If taint was not forced by a keyword argument, calculate default
+        kwargs.setdefault("taint", reduce(lambda x, y: x.union(y.taint), operands, frozenset()))
+
+        super().__init__(array.value_bits, **kwargs)
 
     @property
     def array(self):
@@ -1146,6 +1200,10 @@ def array(self):
     def index(self):
         return self.operands[1]
 
+    @property
+    def operands(self):
+        return self._operands
+
     def __repr__(self):
         return f"<ArraySelect obj with index={self.index}:\n{self.array}>"
 
@@ -1204,3 +1262,8 @@ def __init__(
         assert true_value.size == size
         assert false_value.size == size
         super().__init__(size, condition, true_value, false_value, *args, **kwargs)
+
+
+Constant = (BitVecConstant, BoolConstant)
+Variable = (BitVecVariable, BoolVariable, ArrayVariable)
+Operation = (BitVecOperation, BoolOperation, ArrayOperation, ArraySelect)