trailofbits/manticore
1
0
Fork 0
mirror of https://github.com/trailofbits/manticore.git synced 2026-10-11 22:29:55 +00:00
Code Issues Packages Projects Releases Wiki Activity

Use Slots on all Expression objects (#2394)

Browse Source 
* XSlotted metaclass to force all Expressions to use slots

* Add test for slots. Also small refactor for abstract classes and operands arguments

* Remove pickle data file belonging to deleted test
This commit is contained in:
Eric Kilmer
2021-03-12 09:27:30 -05:00
committed by GitHub
parent dd57db819b
commit 29061a2450
8 changed files with 298 additions and 77 deletions
Download Patch File Download Diff File Expand all files Collapse all files
manticore/core/smtlib/expression.py
+107 -28
View File
@@ -4,7 +4,7 @@ import uuid
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 @@ class Bool(Expression):
class BoolVariable(Bool):
__slots__ = ["_name"]
__xslots__: Tuple[str, ...] = ("_name",)
def __init__(self, name: str, *args, **kwargs):
assert " " not in name
@@ -195,11 +244,11 @@ class BoolVariable(Bool):
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 @@ class BoolConstant(Bool):
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 @@ class BoolITE(BoolOperation):
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 @@ class BitVec(Expression):
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 @@ class BitVecVariable(BitVec):
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 @@ class BitVecConstant(BitVec):
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 @@ class UnsignedGreaterOrEqual(BoolOperation):
###############################################################################
# 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 @@ class Array(Expression):
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 @@ class Array(Expression):
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 @@ class Array(Expression):
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 @@ class Array(Expression):
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 @@ class ArrayVariable(Array):
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 @@ class ArrayStore(ArrayOperation):
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 @@ class ArraySlice(ArrayOperation):
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 @@ class ArrayProxy(Array):
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 @@ class ArraySelect(BitVec):
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 @@ class BitVecSignExtend(BitVecOperation):
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 @@ class BitVecZeroExtend(BitVecOperation):
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 @@ class BitVecExtract(BitVecOperation):
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)
manticore/core/smtlib/operators.py
+1 -1
View File
@@ -163,7 +163,7 @@ def CONCAT(total_size, *args):
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:
manticore/core/smtlib/visitors.py
+2 -2
View File
@@ -594,7 +594,7 @@ class ArithmeticSimplifier(Visitor):
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 @@ class ArithmeticSimplifier(Visitor):
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:
tests/ethereum/test_general.py
+2 -2
View File
@@ -16,7 +16,7 @@ from manticore import ManticoreError
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 @@ class EthTests(unittest.TestCase):
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"
tests/native/test_register.py
+2 -2
View File
@@ -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 @@ class RegisterTest(unittest.TestCase):
def test_Bool(self):
r = Register(32)
b = Bool()
b = BoolVariable(name="B")
r.write(b)
self.assertIs(r.read(), b)
tests/other/data/ErrRelated.pkl.gz
BIN
View File
Binary file not shown.
tests/other/test_smtlibv2.py
+181 -37
View File
@@ -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 @@ from manticore import config
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 @@ class Z3Specific(unittest.TestCase):
"""
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
tox.ini
+3 -5
View File
@@ -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