From 8135735e10f6aa68e100160a44ae5675a457b96b Mon Sep 17 00:00:00 2001 From: Eric Kilmer Date: Mon, 1 Mar 2021 15:19:03 -0500 Subject: [PATCH] Expressions use multiple inheritance for Constant, Variable, Operation --- manticore/core/smtlib/constraints.py | 2 +- manticore/core/smtlib/expression.py | 229 ++++++++++----------------- tests/other/test_smtlibv2.py | 110 +++++-------- 3 files changed, 132 insertions(+), 209 deletions(-) diff --git a/manticore/core/smtlib/constraints.py b/manticore/core/smtlib/constraints.py index ba7aae9e1..942551208 100644 --- a/manticore/core/smtlib/constraints.py +++ b/manticore/core/smtlib/constraints.py @@ -185,7 +185,7 @@ def to_string(self, replace_constants: bool = False) -> str: 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] diff --git a/manticore/core/smtlib/expression.py b/manticore/core/smtlib/expression.py index df607e567..65a82a6d4 100644 --- a/manticore/core/smtlib/expression.py +++ b/manticore/core/smtlib/expression.py @@ -70,10 +70,8 @@ class Expression(object, metaclass=XSlotted, abstract=True): __xslots__: Tuple[str, ...] = ("_taint",) def __init__(self, *, taint: Union[tuple, frozenset] = (), **kwargs): - if self.__class__ is Expression: - raise TypeError - super().__init__() self._taint = frozenset(taint) + super().__init__() def __repr__(self): return "<{:s} at {:x}{:s}>".format(type(self).__name__, id(self), self.taint and "-T" or "") @@ -161,6 +159,70 @@ def taint_with(arg, *taints, value_bits=256, index_bits=256): return arg +class Variable(Expression, abstract=True): + """ An Expression that has a name """ + + __xslots__: Tuple[str, ...] = ("_name",) + + def __init__(self, *, name: str, **kwargs): + """An Expression that has a name + :param name: The Variable name + """ + super().__init__(**kwargs) + self._name = name + + @property + def name(self) -> str: + return self._name + + def __repr__(self): + return "<{:s}({:s}) at {:x}>".format(type(self).__name__, self.name, id(self)) + + def __copy__(self, memo=""): + raise ExpressionException("Copying of Variables is not allowed.") + + def __deepcopy__(self, memo=""): + raise ExpressionException("Copying of Variables is not allowed.") + + +class Constant(Expression, abstract=True): + """ An Expression that has a concrete Python value """ + + __xslots__: Tuple[str, ...] = ("_value",) + + def __init__(self, *, value: Union[bool, int], **kwargs): + """An Expression that has a name + :param name: The Variable name + """ + super().__init__(**kwargs) + self._value = value + + @property + def value(self) -> Union[bool, int]: + return self._value + + +class Operation(Expression, abstract=True): + """ An Expression that contains operands that are also Expressions. """ + + __xslots__: Tuple[str, ...] = ("_operands",) + + def __init__(self, *, operands: Tuple[Expression, ...], **kwargs): + """An operation has operands + :param operands: A tuple of expression operands + """ + self._operands = operands + taint = kwargs.get("taint") + # If taint was not forced by a keyword argument, calculate default + if taint is None: + kwargs["taint"] = frozenset({y for x in operands for y in x.taint}) + super().__init__(**kwargs) + + @property + def operands(self) -> Tuple[Expression, ...]: + return self._operands + + ############################################################################### # Booleans class Bool(Expression, abstract=True): @@ -217,63 +279,24 @@ def __bool__(self): raise NotImplementedError("__bool__ for Bool") -class BoolVariable(Bool): - __xslots__: Tuple[str, ...] = ("_name",) - - def __init__(self, *, name: str, **kwargs): - assert " " not in name - super().__init__(**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)) - +class BoolVariable(Bool, Variable): @property def declaration(self): return f"(declare-fun {self.name} () Bool)" -class BoolConstant(Bool): - __xslots__: Tuple[str, ...] = ("_value",) - +class BoolConstant(Bool, Constant): def __init__(self, *, value: bool, **kwargs): - super().__init__(**kwargs) - self._value = value + super().__init__(value=bool(value), **kwargs) def __bool__(self): return self.value - @property - def value(self): - return self._value - -class BoolOperation(Bool, abstract=True): +class BoolOperation(Bool, Operation, abstract=True): """ An operation that results in a Bool """ - __xslots__: Tuple[str, ...] = ("_operands",) - - def __init__(self, *, operands: Tuple, **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 + pass class BoolNot(BoolOperation): @@ -506,39 +529,16 @@ def Bool(self): return self != 0 -class BitVecVariable(BitVec): - __xslots__: Tuple[str, ...] = ("_name",) - - def __init__(self, *, size: int, name: str, **kwargs): - assert " " not in name - super().__init__(size=size, **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)) - +class BitVecVariable(BitVec, Variable): @property def declaration(self): return f"(declare-fun {self.name} () (_ BitVec {self.size}))" -class BitVecConstant(BitVec): - __xslots__: Tuple[str, ...] = ("_value",) - +class BitVecConstant(BitVec, Constant): def __init__(self, *, size: int, value: int, **kwargs): MASK = (1 << size) - 1 - self._value = value & MASK - super().__init__(size=size, **kwargs) + super().__init__(size=size, value=value & MASK, **kwargs) def __bool__(self): return self.value != 0 @@ -551,10 +551,6 @@ def __eq__(self, other): def __hash__(self): return super().__hash__() - @property - def value(self): - return self._value - @property def signed_value(self): if self._value & self.signmask: @@ -563,22 +559,11 @@ def signed_value(self): return self._value -class BitVecOperation(BitVec, abstract=True): +class BitVecOperation(BitVec, Operation, abstract=True): """ An operation that results in a BitVec """ - __xslots__: Tuple[str, ...] = ("_operands",) - def __init__(self, *, size, operands: Tuple, **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=size, **kwargs) - - @property - def operands(self): - return self._operands + super().__init__(size=size, operands=operands, **kwargs) class BitVecAdd(BitVecOperation): @@ -971,55 +956,34 @@ def __radd__(self, other): return new_arr -class ArrayVariable(Array): - __xslots__: Tuple[str, ...] = ("_name",) - +class ArrayVariable(Array, Variable): def __init__(self, *, index_bits, index_max, value_bits, name, **kwargs): - assert " " not in name super().__init__( - index_bits=index_bits, index_max=index_max, value_bits=value_bits, **kwargs + index_bits=index_bits, index_max=index_max, value_bits=value_bits, name=name, **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): +class ArrayOperation(Array, Operation): """An operation that result in an Array""" - __xslots__: Tuple[str, ...] = ("_operands",) - def __init__(self, *, array: Array, operands: Tuple, **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__( index_bits=array.index_bits, index_max=array.index_max, value_bits=array.value_bits, + operands=(array, *operands), **kwargs, ) @property - def operands(self): - return self._operands + def array(self) -> Array: + arr = self.operands[0] + assert isinstance(arr, Array) + return arr class ArrayStore(ArrayOperation): @@ -1028,13 +992,9 @@ def __init__(self, *, array: "Array", index: "BitVec", value: "BitVec", **kwargs assert value.size == array.value_bits super().__init__(array=array, operands=(index, value), **kwargs) - @property - def array(self): - return self.operands[0] - @property def name(self): - return self.operands[0].name + return self.array.name @property def index(self): @@ -1076,6 +1036,7 @@ def __init__(self, *, array: Union["Array", "ArrayProxy"], offset: int, size: in raise ValueError("Array expected") if isinstance(array, ArrayProxy): array = array._array + # NOTE: Needed for calls to `cast_index` self._operands = (array,) super().__init__( array=array, operands=(self.cast_index(offset), self.cast_index(size)), **kwargs @@ -1084,10 +1045,6 @@ def __init__(self, *, array: Union["Array", "ArrayProxy"], offset: int, size: in self._slice_offset = offset self._slice_size = size - @property - def array(self): - return self._operands[0] - @property def underlying_variable(self): return self.array.underlying_variable @@ -1344,18 +1301,11 @@ def get(self, index, default=None): ) -class ArraySelect(BitVec): - __xslots__: Tuple[str, ...] = ("_operands",) - +class ArraySelect(BitVecOperation): def __init__(self, *, array: "Array", index: "BitVec", **kwargs): assert isinstance(array, Array) assert index.size == array.index_bits - self._operands = (array, index) - - # If taint was not forced by a keyword argument, calculate default - kwargs.setdefault("taint", frozenset({y for x in self._operands for y in x.taint})) - - super().__init__(size=array.value_bits, **kwargs) + super().__init__(size=array.value_bits, operands=(array, index), **kwargs) @property def array(self): @@ -1445,8 +1395,3 @@ def true_value(self): @property def false_value(self): return self.operands[2] - - -Constant = (BitVecConstant, BoolConstant) -Variable = (BitVecVariable, BoolVariable, ArrayVariable) -Operation = (BitVecOperation, BoolOperation, ArrayOperation, ArraySelect) diff --git a/tests/other/test_smtlibv2.py b/tests/other/test_smtlibv2.py index 50d1d21ed..2b8656839 100644 --- a/tests/other/test_smtlibv2.py +++ b/tests/other/test_smtlibv2.py @@ -134,9 +134,9 @@ def check(ty: Type, pickle_size=None, sizeof=None, **kwargs): # Can not instantiate an Expression for ty in ( Expression, - # Constant, # These are actually tuples of types - # Variable, - # Operation, + Constant, + Variable, + Operation, BoolOperation, BitVecOperation, ArrayOperation, @@ -169,52 +169,52 @@ def check(ty: Type, pickle_size=None, sizeof=None, **kwargs): x = BoolVariable(name="x") y = BoolVariable(name="y") z = BoolVariable(name="z") - check(BoolEqual, a=x, b=y, pickle_size=168, sizeof=56) - check(BoolAnd, a=x, b=y, pickle_size=166, sizeof=56) - check(BoolOr, a=x, b=y, pickle_size=165, sizeof=56) - check(BoolXor, a=x, b=y, pickle_size=166, sizeof=56) - check(BoolNot, value=x, pickle_size=143, sizeof=56) - check(BoolITE, cond=z, true=x, false=y, pickle_size=189, sizeof=56) + check(BoolEqual, a=x, b=y, pickle_size=167, sizeof=56) + check(BoolAnd, a=x, b=y, pickle_size=165, sizeof=56) + check(BoolOr, a=x, b=y, pickle_size=164, sizeof=56) + check(BoolXor, a=x, b=y, pickle_size=165, sizeof=56) + check(BoolNot, value=x, pickle_size=142, sizeof=56) + check(BoolITE, cond=z, true=x, false=y, pickle_size=188, sizeof=56) bvx = BitVecVariable(size=32, name="bvx") bvy = BitVecVariable(size=32, name="bvy") - check(UnsignedGreaterThan, a=bvx, b=bvy, pickle_size=197, sizeof=56) - check(GreaterThan, a=bvx, b=bvy, pickle_size=189, sizeof=56) - check(UnsignedGreaterOrEqual, a=bvx, b=bvy, pickle_size=200, sizeof=56) - check(GreaterOrEqual, a=bvx, b=bvy, pickle_size=192, sizeof=56) - check(UnsignedLessThan, a=bvx, b=bvy, pickle_size=194, sizeof=56) - check(LessThan, a=bvx, b=bvy, pickle_size=186, sizeof=56) - check(UnsignedLessOrEqual, a=bvx, b=bvy, pickle_size=197, sizeof=56) - check(LessOrEqual, a=bvx, b=bvy, pickle_size=189, sizeof=56) - - check(BitVecOr, a=bvx, b=bvy, pickle_size=190, sizeof=64) - check(BitVecXor, a=bvx, b=bvy, pickle_size=191, sizeof=64) - check(BitVecAnd, a=bvx, b=bvy, pickle_size=191, sizeof=64) - check(BitVecNot, a=bvx, pickle_size=162, sizeof=64) - check(BitVecNeg, a=bvx, pickle_size=162, sizeof=64) - check(BitVecAdd, a=bvx, b=bvy, pickle_size=191, sizeof=64) - check(BitVecMul, a=bvx, b=bvy, pickle_size=191, sizeof=64) - check(BitVecSub, a=bvx, b=bvy, pickle_size=191, sizeof=64) - check(BitVecDiv, a=bvx, b=bvy, pickle_size=191, sizeof=64) - check(BitVecMod, a=bvx, b=bvy, pickle_size=191, sizeof=64) - check(BitVecUnsignedDiv, a=bvx, b=bvy, pickle_size=199, sizeof=64) - check(BitVecRem, a=bvx, b=bvy, pickle_size=191, sizeof=64) - check(BitVecUnsignedRem, a=bvx, b=bvy, pickle_size=199, sizeof=64) - - check(BitVecShiftLeft, a=bvx, b=bvy, pickle_size=197, sizeof=64) - check(BitVecShiftRight, a=bvx, b=bvy, pickle_size=198, sizeof=64) - check(BitVecArithmeticShiftLeft, a=bvx, b=bvy, pickle_size=207, sizeof=64) - check(BitVecArithmeticShiftRight, a=bvx, b=bvy, pickle_size=208, sizeof=64) - - check(BitVecZeroExtend, operand=bvx, size_dest=122, pickle_size=180, sizeof=72) - check(BitVecSignExtend, operand=bvx, size_dest=122, pickle_size=180, sizeof=72) - check(BitVecExtract, operand=bvx, offset=0, size=8, pickle_size=189, sizeof=80) + check(UnsignedGreaterThan, a=bvx, b=bvy, pickle_size=196, sizeof=56) + check(GreaterThan, a=bvx, b=bvy, pickle_size=188, sizeof=56) + check(UnsignedGreaterOrEqual, a=bvx, b=bvy, pickle_size=199, sizeof=56) + check(GreaterOrEqual, a=bvx, b=bvy, pickle_size=191, sizeof=56) + check(UnsignedLessThan, a=bvx, b=bvy, pickle_size=193, sizeof=56) + check(LessThan, a=bvx, b=bvy, pickle_size=185, sizeof=56) + check(UnsignedLessOrEqual, a=bvx, b=bvy, pickle_size=196, sizeof=56) + check(LessOrEqual, a=bvx, b=bvy, pickle_size=188, sizeof=56) + + check(BitVecOr, a=bvx, b=bvy, pickle_size=189, sizeof=64) + check(BitVecXor, a=bvx, b=bvy, pickle_size=190, sizeof=64) + check(BitVecAnd, a=bvx, b=bvy, pickle_size=190, sizeof=64) + check(BitVecNot, a=bvx, pickle_size=161, sizeof=64) + check(BitVecNeg, a=bvx, pickle_size=161, sizeof=64) + check(BitVecAdd, a=bvx, b=bvy, pickle_size=190, sizeof=64) + check(BitVecMul, a=bvx, b=bvy, pickle_size=190, sizeof=64) + check(BitVecSub, a=bvx, b=bvy, pickle_size=190, sizeof=64) + check(BitVecDiv, a=bvx, b=bvy, pickle_size=190, sizeof=64) + check(BitVecMod, a=bvx, b=bvy, pickle_size=190, sizeof=64) + check(BitVecUnsignedDiv, a=bvx, b=bvy, pickle_size=198, sizeof=64) + check(BitVecRem, a=bvx, b=bvy, pickle_size=190, sizeof=64) + check(BitVecUnsignedRem, a=bvx, b=bvy, pickle_size=198, sizeof=64) + + check(BitVecShiftLeft, a=bvx, b=bvy, pickle_size=196, sizeof=64) + check(BitVecShiftRight, a=bvx, b=bvy, pickle_size=197, sizeof=64) + check(BitVecArithmeticShiftLeft, a=bvx, b=bvy, pickle_size=206, sizeof=64) + check(BitVecArithmeticShiftRight, a=bvx, b=bvy, pickle_size=207, sizeof=64) + + check(BitVecZeroExtend, operand=bvx, size_dest=122, pickle_size=179, sizeof=72) + check(BitVecSignExtend, operand=bvx, size_dest=122, pickle_size=179, sizeof=72) + check(BitVecExtract, operand=bvx, offset=0, size=8, pickle_size=188, sizeof=80) check( BitVecConcat, operands=(bvx, bvy), size_dest=(bvx.size + bvy.size), - pickle_size=194, + pickle_size=193, sizeof=64, ) check( @@ -223,14 +223,14 @@ def check(ty: Type, pickle_size=None, sizeof=None, **kwargs): condition=x, true_value=bvx, false_value=bvy, - pickle_size=231, + pickle_size=230, sizeof=64, ) a = ArrayVariable(index_bits=32, value_bits=32, index_max=324, name="name") - check(ArraySlice, array=a, offset=0, size=10, pickle_size=326, sizeof=136) + check(ArraySlice, array=a, offset=0, size=10, pickle_size=325, sizeof=136) check(ArraySelect, array=a, index=bvx, pickle_size=255, sizeof=64) - check(ArrayStore, array=a, index=bvx, value=bvy, pickle_size=286, sizeof=120) + check(ArrayStore, array=a, index=bvx, value=bvy, pickle_size=285, sizeof=120) check(ArrayProxy, array=a, default=0, pickle_size=222, sizeof=120) def all_subclasses(cls) -> Set[Type]: @@ -1224,28 +1224,6 @@ def testRelated(self): # and send in all the other stuff self.assertNotIn("AA", cs.related_to(bb1 == bb1).to_string()) - def test_API(self): - """ - As we've split up the Constant, Variable, and Operation classes to avoid using multiple inheritance, - this test ensures that their expected properties are still present on their former subclasses. Doesn't - check the types or behavior, but hopefully will at least help avoid footguns related to defining new - Constant/Variable/Operation types in the future. - """ - for cls in Constant: - attrs = ["value"] - for attr in attrs: - self.assertTrue(hasattr(cls, attr), f"{cls.__name__} is missing attribute {attr}") - - for cls in Variable: - attrs = ["name", "declaration", "__copy__", "__deepcopy__"] - for attr in attrs: - self.assertTrue(hasattr(cls, attr), f"{cls.__name__} is missing attribute {attr}") - - for cls in Operation: - attrs = ["operands"] - for attr in attrs: - self.assertTrue(hasattr(cls, attr), f"{cls.__name__} is missing attribute {attr}") - def test_signed_unsigned_LT_simple(self): cs = ConstraintSet() a = cs.new_bitvec(32)