Moving issymbolic to smtlib (#1456)

* Moving issymbolic to smtlib

Performance optimization avoiding runtime imports

* adding blank line for code style

* Moving istainted as well

* code style

* Fixes test import

* Better imports

manticore/__init__.py

@@ -6,7 +6,7 @@
 
 from .utils import config, log
 from .utils.log import set_verbosity
-from .utils.helpers import issymbolic, istainted
+from .core.smtlib import issymbolic, istainted
 from .ethereum.manticore import ManticoreEVM
 
 __all__ = [issymbolic.__name__, istainted.__name__, ManticoreEVM.__name__, set_verbosity.__name__]

manticore/core/plugin.py

@@ -4,7 +4,7 @@
 import pstats
 import threading
 
-from ..utils.helpers import issymbolic
+from .smtlib import issymbolic
 
 logger = logging.getLogger(__name__)
 

manticore/core/smtlib/__init__.py

@@ -1,4 +1,4 @@
-from .expression import Expression, Bool, BitVec, Array, BitVecConstant  # noqa
+from .expression import Expression, Bool, BitVec, Array, BitVecConstant, issymbolic  # noqa
 from .constraints import ConstraintSet  # noqa
 from .solver import *  # noqa
 from . import operators as Operators  # noqa

manticore/core/smtlib/expression.py

@@ -1,6 +1,9 @@
 from functools import reduce
 import uuid
 
+import re
+import copy
+
 
 class Expression:
     """ Abstract taintable Expression. """
@@ -24,6 +27,78 @@ def taint(self):
         return self._taint
 
 
+def issymbolic(value):
+    """
+        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
+        """
+    return isinstance(value, Expression)
+
+
+def istainted(arg, taint=None):
+    """
+    Helper to determine whether an object if tainted.
+    :param arg: a value or Expression
+    :param taint: a regular expression matching a taint value (eg. 'IMPORTANT.*'). If None, this function checks for any taint value.
+    """
+
+    if not issymbolic(arg):
+        return False
+    if taint is None:
+        return len(arg.taint) != 0
+    for arg_taint in arg.taint:
+        m = re.match(taint, arg_taint, re.DOTALL | re.IGNORECASE)
+        if m:
+            return True
+    return False
+
+
+def get_taints(arg, taint=None):
+    """
+    Helper to list an object taints.
+    :param arg: a value or Expression
+    :param taint: a regular expression matching a taint value (eg. 'IMPORTANT.*'). If None, this function checks for any taint value.
+    """
+
+    if not issymbolic(arg):
+        return
+    for arg_taint in arg.taint:
+        if taint is not None:
+            m = re.match(taint, arg_taint, re.DOTALL | re.IGNORECASE)
+            if m:
+                yield arg_taint
+        else:
+            yield arg_taint
+    return
+
+
+def taint_with(arg, taint, value_bits=256, index_bits=256):
+    """
+    Helper to taint a value.
+    :param arg: a value or Expression
+    :param taint: a regular expression matching a taint value (eg. 'IMPORTANT.*'). If None, this function checks for any taint value.
+    """
+
+    tainted_fset = frozenset((taint,))
+
+    if not issymbolic(arg):
+        if isinstance(arg, int):
+            arg = BitVecConstant(value_bits, arg)
+            arg._taint = tainted_fset
+        else:
+            raise ValueError("type not supported")
+
+    else:
+        arg = copy.copy(arg)
+        arg._taint |= tainted_fset
+
+    return arg
+
+
 class Variable(Expression):
     def __init__(self, name, *args, **kwargs):
         if self.__class__ is Variable:

manticore/core/smtlib/operators.py

@@ -10,7 +10,7 @@
     BoolConstant,
     BoolITE,
 )
-from ...utils.helpers import issymbolic
+from . import issymbolic
 import math
 
 

manticore/core/smtlib/solver.py

@@ -26,7 +26,7 @@
 from .visitors import *
 from ...exceptions import Z3NotFoundError, SolverError, SolverUnknown, TooManySolutions
 from ...utils import config
-from ...utils.helpers import issymbolic
+from . import issymbolic
 
 logger = logging.getLogger(__name__)
 consts = config.get_group("smt")

manticore/core/state.py

@@ -1,8 +1,7 @@
 import copy
 import logging
 
-from .smtlib import solver, Bool
-from ..utils.helpers import issymbolic
+from .smtlib import solver, Bool, issymbolic
 from ..utils.event import Eventful
 
 logger = logging.getLogger(__name__)

manticore/ethereum/abi.py

@@ -5,8 +5,7 @@
 import sha3
 
 from . import abitypes
-from ..utils.helpers import issymbolic
-from ..core.smtlib import Array, Operators, BitVec, ArrayVariable, ArrayProxy
+from ..core.smtlib import Array, Operators, BitVec, ArrayVariable, ArrayProxy, issymbolic
 from ..exceptions import EthereumError
 
 logger = logging.getLogger(__name__)

manticore/ethereum/detectors.py

@@ -3,8 +3,15 @@
 import logging
 from contextlib import contextmanager
 
-from ..core.smtlib import Operators, Constant, simplify
-from ..utils.helpers import istainted, issymbolic, taint_with, get_taints
+from ..core.smtlib import (
+    Operators,
+    Constant,
+    simplify,
+    istainted,
+    issymbolic,
+    get_taints,
+    taint_with,
+)
 from ..core.plugin import Plugin
 
 

manticore/ethereum/manticore.py

@@ -25,6 +25,7 @@
     BoolConstant,
     BoolOperation,
     Expression,
+    issymbolic,
 )
 from ..core.state import TerminateState, AbandonState
 from .account import EVMContract, EVMAccount, ABI
@@ -34,7 +35,7 @@
 from ..exceptions import EthereumError, DependencyError, NoAliveStates
 from ..platforms import evm
 from ..utils import config, log
-from ..utils.helpers import PickleSerializer, issymbolic
+from ..utils.helpers import PickleSerializer
 
 logger = logging.getLogger(__name__)
 

manticore/native/cpu/abstractcpu.py

@@ -11,13 +11,12 @@
 from .disasm import init_disassembler
 from ..memory import ConcretizeMemory, InvalidMemoryAccess, FileMap, AnonMap
 from ..memory import LazySMemory
-from ...core.smtlib import Expression, BitVec, Operators, Constant
+from ...core.smtlib import Expression, BitVec, Operators, Constant, issymbolic
 from ...core.smtlib import visitors
 from ...core.smtlib.solver import Z3Solver
 from ...utils.emulate import ConcreteUnicornEmulator
 from ...utils.event import Eventful
 from ...utils.fallback_emulator import UnicornEmulator
-from ...utils.helpers import issymbolic
 
 from capstone import CS_ARCH_ARM64, CS_ARCH_X86, CS_ARCH_ARM
 from capstone.arm64 import ARM64_REG_ENDING

manticore/native/cpu/arm.py

@@ -8,8 +8,7 @@
 from .abstractcpu import instruction as abstract_instruction
 from .bitwise import *
 from .register import Register
-from ...core.smtlib import Operators, BitVecConstant
-from ...utils.helpers import issymbolic
+from ...core.smtlib import Operators, BitVecConstant, issymbolic
 
 logger = logging.getLogger(__name__)
 

manticore/native/cpu/x86.py

@@ -19,9 +19,8 @@
 )
 
 
-from ...core.smtlib import Operators, BitVec, Bool, BitVecConstant, operator, visitors
+from ...core.smtlib import Operators, BitVec, Bool, BitVecConstant, operator, visitors, issymbolic
 from ..memory import ConcretizeMemory
-from ...utils.helpers import issymbolic
 from functools import reduce
 
 logger = logging.getLogger(__name__)

manticore/native/manticore.py

@@ -12,9 +12,8 @@
 from .state import State
 from ..core.manticore import ManticoreBase
 from ..core.smtlib import ConstraintSet
-from ..core.smtlib.solver import Z3Solver
+from ..core.smtlib.solver import Z3Solver, issymbolic
 from ..utils import log, config
-from ..utils.helpers import issymbolic
 
 logger = logging.getLogger(__name__)
 

manticore/native/memory.py

@@ -9,9 +9,10 @@
     BitVec,
     BitVecConstant,
     expression,
+    issymbolic,
 )
 from ..native.mappings import mmap, munmap
-from ..utils.helpers import issymbolic, interval_intersection
+from ..utils.helpers import interval_intersection
 
 import functools
 import logging

manticore/native/models.py

@@ -3,7 +3,7 @@
 """
 
 from .cpu.abstractcpu import ConcretizeArgument
-from ..utils.helpers import issymbolic
+from ..core.smtlib import issymbolic
 from ..core.smtlib.solver import Z3Solver
 from ..core.smtlib.operators import ITEBV, ZEXTEND
 

manticore/platforms/decree.py

@@ -6,7 +6,6 @@
 from ..native.memory import SMemory32, Memory32
 from ..core.smtlib import *
 from ..core.state import TerminateState
-from ..utils.helpers import issymbolic
 from ..binary import CGCElf
 from ..platforms.platform import Platform
 import logging

manticore/platforms/evm.py

@@ -6,7 +6,6 @@
 import inspect
 from functools import wraps
 from typing import List, Set, Tuple, Union
-from ..utils.helpers import issymbolic, get_taints, taint_with, istainted
 from ..platforms.platform import *
 from ..core.smtlib import (
     Z3Solver,
@@ -21,6 +20,10 @@
     translate_to_smtlib,
     to_constant,
     simplify,
+    issymbolic,
+    get_taints,
+    istainted,
+    taint_with,
 )
 from ..core.state import Concretize, TerminateState
 from ..utils.event import Eventful

manticore/platforms/linux.py

@@ -21,14 +21,13 @@
 from . import linux_syscalls
 from .linux_syscall_stubs import SyscallStubs
 from ..core.state import TerminateState
-from ..core.smtlib import ConstraintSet, Operators, Expression
+from ..core.smtlib import ConstraintSet, Operators, Expression, issymbolic
 from ..core.smtlib.solver import Z3Solver
 from ..exceptions import SolverError
 from ..native.cpu.abstractcpu import Syscall, ConcretizeArgument, Interruption
 from ..native.cpu.cpufactory import CpuFactory
 from ..native.memory import SMemory32, SMemory64, Memory32, Memory64, LazySMemory32, LazySMemory64
 from ..platforms.platform import Platform, SyscallNotImplemented, unimplemented
-from ..utils.helpers import issymbolic
 
 logger = logging.getLogger(__name__)
 

manticore/utils/emulate.py

@@ -10,8 +10,7 @@
 from unicorn.arm_const import *
 from unicorn.x86_const import *
 
-from .helpers import issymbolic
-from ..core.smtlib import Operators, solver
+from ..core.smtlib import Operators, solver, issymbolic
 from ..native.memory import MemoryException
 
 logger = logging.getLogger(__name__)

manticore/utils/fallback_emulator.py

@@ -2,7 +2,7 @@
 
 from ..native.memory import MemoryException
 
-from .helpers import issymbolic
+from ..core.smtlib import issymbolic
 
 ######################################################################
 # Abstract classes for capstone/unicorn based cpus