diff --git a/manticore/core/smtlib/expression.py b/manticore/core/smtlib/expression.py index 5aea0210ca..009910b9d3 100644 --- a/manticore/core/smtlib/expression.py +++ b/manticore/core/smtlib/expression.py @@ -4,7 +4,7 @@ import re import copy -from typing import Union, Optional, Dict, List +from typing import Union, Optional, Dict, Tuple class ExpressionException(SmtlibError): @@ -15,10 +15,59 @@ class ExpressionException(SmtlibError): pass -class Expression: +class XSlotted(type): + """ + Metaclass that will propagate slots on multi-inheritance classes + Every class should define __xslots__ (instead of __slots__) + + class Base(object, metaclass=XSlotted, abstract=True): + pass + + class A(Base, abstract=True): + __xslots__ = ('a',) + pass + + class B(Base, abstract=True): + __xslots__ = ('b',) + pass + + class C(A, B): + pass + + # Normal case / baseline + class X(object): + __slots__ = ('a', 'b') + + c = C() + c.a = 1 + c.b = 2 + + x = X() + x.a = 1 + x.b = 2 + + import sys + print (sys.getsizeof(c),sys.getsizeof(x)) #same value + """ + + def __new__(cls, clsname, bases, attrs, abstract=False): + xslots = frozenset(attrs.get("__xslots__", ())) + # merge the xslots of all the bases with the one defined here + for base in bases: + xslots = xslots.union(getattr(base, "__xslots__", ())) + attrs["__xslots__"] = tuple(xslots) + if abstract: + attrs["__slots__"] = tuple() + else: + attrs["__slots__"] = attrs["__xslots__"] + attrs["__hash__"] = object.__hash__ + return super().__new__(cls, clsname, bases, attrs) + + +class Expression(object, metaclass=XSlotted, abstract=True): """ Abstract taintable Expression. """ - __slots__ = ["_taint"] + __xslots__: Tuple[str, ...] = ("_taint",) def __init__(self, taint: Union[tuple, frozenset] = ()): if self.__class__ is Expression: @@ -114,8 +163,8 @@ def taint_with(arg, *taints, value_bits=256, index_bits=256): ############################################################################### # Booleans -class Bool(Expression): - __slots__: List[str] = [] +class Bool(Expression, abstract=True): + """Bool expressions represent symbolic value of truth""" def __init__(self, *operands, **kwargs): super().__init__(*operands, **kwargs) @@ -169,7 +218,7 @@ def __bool__(self): class BoolVariable(Bool): - __slots__ = ["_name"] + __xslots__: Tuple[str, ...] = ("_name",) def __init__(self, name: str, *args, **kwargs): assert " " not in name @@ -195,11 +244,11 @@ def declaration(self): class BoolConstant(Bool): - __slots__ = ["_value"] + __xslots__: Tuple[str, ...] = ("_value",) def __init__(self, value: bool, *args, **kwargs): - self._value = value super().__init__(*args, **kwargs) + self._value = value def __bool__(self): return self.value @@ -209,8 +258,10 @@ def value(self): return self._value -class BoolOperation(Bool): - __slots__ = ["_operands"] +class BoolOperation(Bool, abstract=True): + """ An operation that results in a Bool """ + + __xslots__: Tuple[str, ...] = ("_operands",) def __init__(self, *operands, **kwargs): self._operands = operands @@ -250,10 +301,10 @@ def __init__(self, cond: "Bool", true: "Bool", false: "Bool", **kwargs): super().__init__(cond, true, false, **kwargs) -class BitVec(Expression): - """ This adds a bitsize to the Expression class """ +class BitVec(Expression, abstract=True): + """ BitVector expressions have a fixed bit size """ - __slots__ = ["size"] + __xslots__: Tuple[str, ...] = ("size",) def __init__(self, size, *operands, **kwargs): super().__init__(*operands, **kwargs) @@ -456,7 +507,7 @@ def Bool(self): class BitVecVariable(BitVec): - __slots__ = ["_name"] + __xslots__: Tuple[str, ...] = ("_name",) def __init__(self, size: int, name: str, *args, **kwargs): assert " " not in name @@ -482,7 +533,7 @@ def declaration(self): class BitVecConstant(BitVec): - __slots__ = ["_value"] + __xslots__: Tuple[str, ...] = ("_value",) def __init__(self, size: int, value: int, *args, **kwargs): MASK = (1 << size) - 1 @@ -512,8 +563,10 @@ def signed_value(self): return self._value -class BitVecOperation(BitVec): - __slots__ = ["_operands"] +class BitVecOperation(BitVec, abstract=True): + """ An operation that results in a BitVec """ + + __xslots__: Tuple[str, ...] = ("_operands",) def __init__(self, size, *operands, **kwargs): self._operands = operands @@ -670,8 +723,15 @@ def __init__(self, a, b, *args, **kwargs): ############################################################################### # Array BV32 -> BV8 or BV64 -> BV8 -class Array(Expression): - __slots__ = ["_index_bits", "_index_max", "_value_bits"] +class Array(Expression, abstract=True): + """An Array expression is an unmutable mapping from bitvector to bitvector + + array.index_bits is the number of bits used for addressing a value + array.value_bits is the number of bits used in the values + array.index_max counts the valid indexes starting at 0. Accessing outside the bound is undefined + """ + + __xslots__: Tuple[str, ...] = ("_index_bits", "_index_max", "_value_bits") def __init__( self, index_bits: int, index_max: Optional[int], value_bits: int, *operands, **kwargs @@ -764,7 +824,7 @@ def store(self, index, value): def write(self, offset, buf): if not isinstance(buf, (Array, bytearray)): - raise TypeError("Array or bytearray expected got {:s}".format(type(buf))) + raise TypeError(f"Array or bytearray expected got {type(buf)}") arr = self for i, val in enumerate(buf): arr = arr.store(offset + i, val) @@ -820,18 +880,18 @@ def read_BE(self, address, size): bytes = [] for offset in range(size): bytes.append(self.get(address + offset, 0)) - return BitVecConcat(size * self.value_bits, *bytes) + return BitVecConcat(size * self.value_bits, tuple(bytes)) def read_LE(self, address, size): address = self.cast_index(address) bytes = [] for offset in range(size): bytes.append(self.get(address + offset, 0)) - return BitVecConcat(size * self.value_bits, *reversed(bytes)) + return BitVecConcat(size * self.value_bits, tuple(reversed(bytes))) def write_BE(self, address, value, size): address = self.cast_index(address) - value = BitVec(size * self.value_bits).cast(value) + value = BitVecConstant(size * self.value_bits, value=0).cast(value) array = self for offset in range(size): array = array.store( @@ -842,7 +902,7 @@ def write_BE(self, address, value, size): def write_LE(self, address, value, size): address = self.cast_index(address) - value = BitVec(size * self.value_bits).cast(value) + value = BitVecConstant(size * self.value_bits, value=0).cast(value) array = self for offset in reversed(range(size)): array = array.store( @@ -903,7 +963,7 @@ def __radd__(self, other): class ArrayVariable(Array): - __slots__ = ["_name"] + __xslots__: Tuple[str, ...] = ("_name",) def __init__(self, index_bits, index_max, value_bits, name, *args, **kwargs): assert " " not in name @@ -929,7 +989,9 @@ def declaration(self): class ArrayOperation(Array): - __slots__ = ["_operands"] + """An operation that result in an Array""" + + __xslots__: Tuple[str, ...] = ("_operands",) def __init__(self, array: Array, *operands, **kwargs): self._operands = (array, *operands) @@ -989,6 +1051,8 @@ def __setstate__(self, state): class ArraySlice(ArrayOperation): + __xslots__: Tuple[str, ...] = ("_slice_offset", "_slice_size") + def __init__( self, array: Union["Array", "ArrayProxy"], offset: int, size: int, *args, **kwargs ): @@ -1033,6 +1097,15 @@ def store(self, index, value): class ArrayProxy(Array): + __xslots__: Tuple[str, ...] = ( + "constraints", + "_default", + "_concrete_cache", + "_written", + "_array", + "_name", + ) + def __init__(self, array: Array, default: Optional[int] = None): self._default = default self._concrete_cache: Dict[int, int] = {} @@ -1229,7 +1302,7 @@ def get(self, index, default=None): class ArraySelect(BitVec): - __slots__ = ["_operands"] + __xslots__: Tuple[str, ...] = ("_operands",) def __init__(self, array: "Array", index: "BitVec", *operands, **kwargs): assert index.size == array.index_bits @@ -1257,6 +1330,8 @@ def __repr__(self): class BitVecSignExtend(BitVecOperation): + __xslots__: Tuple[str, ...] = ("extend",) + def __init__(self, operand: "BitVec", size_dest: int, *args, **kwargs): assert size_dest >= operand.size super().__init__(size_dest, operand, *args, **kwargs) @@ -1264,6 +1339,8 @@ def __init__(self, operand: "BitVec", size_dest: int, *args, **kwargs): class BitVecZeroExtend(BitVecOperation): + __xslots__: Tuple[str, ...] = ("extend",) + def __init__(self, size_dest: int, operand: "BitVec", *args, **kwargs): assert size_dest >= operand.size super().__init__(size_dest, operand, *args, **kwargs) @@ -1271,6 +1348,8 @@ def __init__(self, size_dest: int, operand: "BitVec", *args, **kwargs): class BitVecExtract(BitVecOperation): + __xslots__: Tuple[str, ...] = ("_begining", "_end") + def __init__(self, operand: "BitVec", offset: int, size: int, *args, **kwargs): assert offset >= 0 and offset + size <= operand.size super().__init__(size, operand, *args, **kwargs) @@ -1291,7 +1370,7 @@ def end(self): class BitVecConcat(BitVecOperation): - def __init__(self, size_dest: int, *operands, **kwargs): + def __init__(self, size_dest: int, operands: Tuple, **kwargs): assert all(isinstance(x, BitVec) for x in operands) assert size_dest == sum(x.size for x in operands) super().__init__(size_dest, *operands, **kwargs) diff --git a/manticore/core/smtlib/operators.py b/manticore/core/smtlib/operators.py index 969679b566..79e2f0c614 100644 --- a/manticore/core/smtlib/operators.py +++ b/manticore/core/smtlib/operators.py @@ -163,7 +163,7 @@ def cast(x): return BitVecConstant(arg_size, x) return x - return BitVecConcat(total_size, *list(map(cast, args))) + return BitVecConcat(total_size, tuple(map(cast, args))) else: return args[0] else: diff --git a/manticore/core/smtlib/visitors.py b/manticore/core/smtlib/visitors.py index ec6e446e89..f18b66b9f2 100644 --- a/manticore/core/smtlib/visitors.py +++ b/manticore/core/smtlib/visitors.py @@ -594,7 +594,7 @@ def visit_BitVecConcat(self, expression, *operands): if last_o is not None: new_operands.append(last_o) if changed: - return BitVecConcat(expression.size, *new_operands) + return BitVecConcat(expression.size, tuple(new_operands)) op = operands[0] value = None @@ -648,7 +648,7 @@ def visit_BitVecExtract(self, expression, *operands): if size == 0: assert expression.size == sum([x.size for x in new_operands]) return BitVecConcat( - expression.size, *reversed(new_operands), taint=expression.taint + expression.size, tuple(reversed(new_operands)), taint=expression.taint ) if begining >= item.size: diff --git a/tests/ethereum/test_general.py b/tests/ethereum/test_general.py index 799456298b..abcaf1b918 100644 --- a/tests/ethereum/test_general.py +++ b/tests/ethereum/test_general.py @@ -16,7 +16,7 @@ from manticore.core.plugin import Plugin from manticore.core.smtlib import ConstraintSet, operators from manticore.core.smtlib import Z3Solver -from manticore.core.smtlib.expression import BitVec +from manticore.core.smtlib.expression import BitVec, BitVecVariable from manticore.core.smtlib.visitors import to_constant from manticore.core.state import TerminateState from manticore.ethereum import ( @@ -1382,7 +1382,7 @@ def will_evm_execute_instruction_callback(self, state, i, *args, **kwargs): class EthHelpersTest(unittest.TestCase): def setUp(self): - self.bv = BitVec(256) + self.bv = BitVecVariable(256, name="BVV") def test_concretizer(self): policy = "SOME_NONSTANDARD_POLICY" diff --git a/tests/native/test_register.py b/tests/native/test_register.py index e099fc2923..0663e811bb 100644 --- a/tests/native/test_register.py +++ b/tests/native/test_register.py @@ -1,6 +1,6 @@ import unittest -from manticore.core.smtlib import Bool, BitVecConstant +from manticore.core.smtlib import Bool, BoolVariable, BitVecConstant from manticore.native.cpu.register import Register @@ -47,7 +47,7 @@ def test_bool_write_nonflag(self): def test_Bool(self): r = Register(32) - b = Bool() + b = BoolVariable(name="B") r.write(b) self.assertIs(r.read(), b) diff --git a/tests/other/data/ErrRelated.pkl.gz b/tests/other/data/ErrRelated.pkl.gz deleted file mode 100644 index eb1036567c..0000000000 Binary files a/tests/other/data/ErrRelated.pkl.gz and /dev/null differ diff --git a/tests/other/test_smtlibv2.py b/tests/other/test_smtlibv2.py index 3050b900fd..11d4236cfd 100644 --- a/tests/other/test_smtlibv2.py +++ b/tests/other/test_smtlibv2.py @@ -1,5 +1,7 @@ import unittest import os +import sys +from typing import Set, Type from manticore.core.smtlib import ( ConstraintSet, @@ -26,43 +28,6 @@ DIRPATH = os.path.dirname(__file__) -class RegressionTest(unittest.TestCase): - def test_related_to(self): - import gzip - import pickle, sys - - filename = os.path.abspath(os.path.join(DIRPATH, "data", "ErrRelated.pkl.gz")) - - # A constraint set and a contraint caught in the act of making related_to fail - constraints, constraint = pickle.loads(gzip.open(filename, "rb").read()) - - Z3Solver.instance().can_be_true.cache_clear() - ground_truth = Z3Solver.instance().can_be_true(constraints, constraint) - self.assertEqual(ground_truth, False) - - Z3Solver.instance().can_be_true.cache_clear() - self.assertEqual( - ground_truth, - Z3Solver.instance().can_be_true(constraints.related_to(constraints), constraint), - ) - - # Replace - new_constraint = Operators.UGE( - Operators.SEXTEND(BitVecConstant(256, 0x1A), 256, 512) * BitVecConstant(512, 1), - 0x00000000000000000000000000000000000000000000000000000000000000010000000000000000000000000000000000000000000000000000000000000000, - ) - self.assertEqual(translate_to_smtlib(constraint), translate_to_smtlib(new_constraint)) - - Z3Solver.instance().can_be_true.cache_clear() - self.assertEqual(ground_truth, Z3Solver.instance().can_be_true(constraints, new_constraint)) - - Z3Solver.instance().can_be_true.cache_clear() - self.assertEqual( - ground_truth, - Z3Solver.instance().can_be_true(constraints.related_to(new_constraint), new_constraint), - ) - - """ class Z3Specific(unittest.TestCase): _multiprocess_can_split_ = True @@ -100,6 +65,185 @@ def test_check_solver_undefined(self): """ +class ExpressionPropertiesTest(unittest.TestCase): + _multiprocess_can_split_ = True + + def test_xslotted(self): + """Test that XSlotted multi inheritance classes uses same amount + of memory than a single class object with slots + """ + + class Base(object, metaclass=XSlotted, abstract=True): + __xslots__ = ("t",) + pass + + class A(Base, abstract=True): + __xslots__ = ("a",) + pass + + class B(Base, abstract=True): + __xslots__ = ("b",) + pass + + class C(A, B): + pass + + class X(object): + __slots__ = ("t", "a", "b") + + c = C() + c.a = 1 + c.b = 2 + c.t = 10 + + x = X() + x.a = 1 + x.b = 2 + x.t = 20 + + self.assertEqual(sys.getsizeof(c), sys.getsizeof(x)) + + def test_Expression(self): + # Used to check if all Expression have test + checked = set() + + def check(ty: Type, pickle_size=None, sizeof=None, **kwargs): + x = ty(**kwargs) + """ + print( + type(x), + "\n Pickle size:", + len(pickle_dumps(x)), + "\n GetSizeOf:", + sys.getsizeof(x), + "\n Slotted:", + not hasattr(x, "__dict__"), + ) + """ + self.assertEqual(len(pickle_dumps(x)), pickle_size) + if sys.version_info[1] == 6: # Python 3.6 + self.assertEqual(sys.getsizeof(x), sizeof) + elif sys.version_info[1] == 7: # Python 3.7 + self.assertEqual(sys.getsizeof(x), sizeof + 8) + elif sys.version_info[1] >= 8: # Python 3.8+ + self.assertEqual(sys.getsizeof(x), sizeof - 8) + self.assertFalse(hasattr(x, "__dict__")) # slots! + self.assertTrue(hasattr(x, "_taint")) # taint! + checked.add(ty) + + # Can not instantiate an Expression + for ty in ( + Expression, + # Constant, # These are actually tuples of types + # Variable, + # Operation, + BoolOperation, + BitVecOperation, + ArrayOperation, + BitVec, + Bool, + Array, + ): + self.assertRaises(Exception, ty, ()) + self.assertTrue(hasattr(ty, "__doc__")) + self.assertTrue(ty.__doc__, ty) + checked.add(ty) + + # The test numbers are taken from Python 3.6.13 (the oldest supported version) + # New pythons could use a different number of bytes. Look at the 'check' function + check(BitVecVariable, size=32, name="name", pickle_size=113, sizeof=64) + check(BoolVariable, name="name", pickle_size=102, sizeof=56) + check( + ArrayVariable, + index_bits=32, + value_bits=8, + index_max=100, + name="name", + pickle_size=150, + sizeof=80, + ) + check(BitVecConstant, size=32, value=10, pickle_size=109, sizeof=64) + check(BoolConstant, value=False, pickle_size=97, sizeof=56) + + # But you can instantiate a BoolOr + 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) + + 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( + BitVecConcat, + operands=(bvx, bvy), + size_dest=(bvx.size + bvy.size), + pickle_size=194, + sizeof=64, + ) + check( + BitVecITE, + size=bvx.size, + condition=x, + true_value=bvx, + false_value=bvy, + pickle_size=231, + 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=244, sizeof=136) + check(ArraySelect, array=a, index=bvx, pickle_size=255, sizeof=64) + check(ArrayStore, array=a, index=bvx, value=bvy, pickle_size=281, sizeof=120) + check(ArrayProxy, array=a, default=0, pickle_size=222, sizeof=120) + + def all_subclasses(cls) -> Set[Type]: + return {cls}.union( + set(cls.__subclasses__()).union( + [s for c in cls.__subclasses__() for s in all_subclasses(c)] + ) + ) + + all_types = all_subclasses(Expression) + self.assertSetEqual(checked, all_types) + + class ExpressionTest(unittest.TestCase): _multiprocess_can_split_ = True diff --git a/tox.ini b/tox.ini index e132e3b0f8..18383b7df6 100644 --- a/tox.ini +++ b/tox.ini @@ -1,11 +1,9 @@ [tox] -envlist = py3{6,7} +envlist = py3{6,7,8,9} [testenv] -deps = - .[dev] -commands = nosetests tests -install_command = pip install --no-binary keystone-engine {opts} {packages} +deps = .[dev] +commands = pytest -n auto tests [testenv:pep8] deps = flake8