Mypy support (#1544)

* linux: Add return 0 for success on sys_pipe2

* mypy: Initial config file to ignore modules without typing info

* mypy: types manticore/platforms/linux.py

* mypy: manticore/ethereum/manticore.py

* Ignore error because mypy doesn't support decorated @Property's

* mypy: manticore/ethereum/solidity.py

* Ignore error because mypy doesn't support decorated @Property's

* mypy: manticore/ethereum/detectors.py

* Use Python's Enum class for DetectorClassification

* mypy: manticore/platforms/cgcrandom.py

* Set as byte string

* mypy: manticore/binary/binary.py

* mypy: manticore/utils/event.py

* mypy: manticore/ethereum/abitypes

* Use actual ResourceWarning class instead of string name

* mypy: manticore/utils/config.py

* mypy: manticore/core/workspace.py

* Support both Python 3.6 and Python 3.7 with nullcontext. Ignore the
mypy error because it checks against Python 3.6 and Manticore does not
explicitly claim support for Python 3.7

* mypy: manticore/core/manticore

* Ignore mypy error on sync, at_running, at_not_running:

  Self argument missing for a non-static method (or an invalid type for
  self)

* Ignore type info for unsupported decorators on @Property fields

* mypy: manticore/platforms/evm.py

* Ignore error of already defined variable when setting member variable
of class transaction

* Remove redundant get_nonce call

* Move property setter next to property definition

* mypy: manticore/core/smtlib/solver.py

* Fix instance where no match was found in regex

* mypy: Add mypy to travis and setup.py

* Lock to specific mypy and black tool versions

* Rename "format" stage to "lint"

* Add text about mypy to CONTRIBUTING.md

* Revert black tool upgrade to 19.3b0

* Fix typing issues introduced by SHA3 branch

.travis.yml

@@ -7,7 +7,7 @@ python:
   - 3.6.6
 
 stages:
-  - format
+  - lint
   - prepare
   - test
   - submit
@@ -37,10 +37,13 @@ cache:
 
 jobs:
   include:
-    - stage: format
-      env: TEST_TYPE=format
+    - stage: lint
+      env: TEST_TYPE=lint
       script:
-        - git diff --name-only $TRAVIS_COMMIT_RANGE | python3 scripts/pyfile_exists.py | xargs black --check || echo "Reformat required! Please run 'black <filename>' to reformat changes."
+        - black --version
+        - git diff --name-only $TRAVIS_COMMIT_RANGE | python3 scripts/pyfile_exists.py | xargs black --check || { echo "Reformat required! Please run 'black <filename>' to reformat changes." ; travis_terminate 1 ; }
+        - mypy --version
+        - mypy manticore || { echo "mypy type-checking error. Please read the error and fix." ; travis_terminate 1 ; }
     - stage: prepare
       env: TEST_TYPE=env
       script:
@@ -51,7 +54,7 @@ jobs:
       script:
         - true
       after_script:
-        - aws s3 sync "s3://manticore-testdata/coverage/$TRAVIS_COMMIT" coverage/ 
+        - aws s3 sync "s3://manticore-testdata/coverage/$TRAVIS_COMMIT" coverage/
         - ./cc-test-reporter sum-coverage --output - --parts $JOB_COUNT coverage/codeclimate.*.json | ./cc-test-reporter upload-coverage --input -
 
 install:

CONTRIBUTING.md

@@ -30,10 +30,20 @@ more documentation, look [here](https://guides.github.com/activities/forking/).
 
 Some pull request guidelines:
 
-- We use the [`black`](https://black.readthedocs.io/en/stable/index.html) auto-formatter
-  to enforce style conventions in Manticore. To ensure your code is properly 
-  formatted, run `black .` in the manticore directory before
-  committing.
+- We use the [`black`](https://black.readthedocs.io/en/stable/index.html)
+  auto-formatter to enforce style conventions in Manticore. To ensure your code
+  is properly formatted, run `black .` in the Manticore directory before
+  committing. Although unlikely, if you are still having trouble with getting
+  your code to pass formatting, check that you have the same version of `black`
+  installed as what is used in the CI.
+- We use the [`mypy`](https://github.com/python/mypy) static typing tool to
+  catch inconsistencies in the code base. At the time of this writing, we
+  only check the [manticore](./manticore) directory for inconsistencies and do
+  not yet enforce new contributions to include type hints. However, we greatly
+  appreciate if you do include/add them in any code that you touch in your PR!
+  Though, remember the next guideline if you are adding many type-hints, and
+  ask for input on how to organize the addition of a massive amount of type
+  hints. Check the CI configuration for the exact version of `mypy`.
 - Minimize irrelevant changes (formatting, whitespace, etc) to code that would
   otherwise not be touched by this patch. Save formatting or style corrections
   for a separate pull request that does not make any semantic changes.

manticore/binary/binary.py

@@ -1,10 +1,11 @@
 import io
+from typing import Dict, Type, Union
 
 from elftools.elf.elffile import ELFFile
 
 
 class Binary:
-    magics = {}
+    magics: Dict[bytes, Type["Binary"]] = {}
 
     def __new__(cls, path):
         if cls is Binary:

manticore/core/manticore.py

@@ -4,6 +4,7 @@
 import time
 import random
 import weakref
+from typing import Callable
 
 from contextlib import contextmanager
 
@@ -85,7 +86,7 @@ def __new__(cls, *args, **kwargs):
         return super().__new__(cls)
 
     # Decorators added first for convenience.
-    def sync(func):
+    def sync(func: Callable) -> Callable:  # type: ignore
         """Synchronization decorator"""
 
         @functools.wraps(func)
@@ -95,7 +96,7 @@ def newFunction(self, *args, **kw):
 
         return newFunction
 
-    def at_running(func):
+    def at_running(func: Callable) -> Callable:  # type: ignore
         """Allows the decorated method to run only when manticore is actively
            exploring states
         """
@@ -108,7 +109,7 @@ def newFunction(self, *args, **kw):
 
         return newFunction
 
-    def at_not_running(func):
+    def at_not_running(func: Callable) -> Callable:  # type: ignore
         """Allows the decorated method to run only when manticore is NOT
            exploring states
         """
@@ -574,7 +575,7 @@ def kill_state(self, state, delete=False):
             # add the state_id to the terminated list
             self._killed_states.append(state_id)
 
-    @property
+    @property  # type: ignore
     @sync
     def ready_states(self):
         """
@@ -600,7 +601,7 @@ def running_states(self):
         )
         return self.ready_states
 
-    @property
+    @property  # type: ignore
     @sync
     def terminated_states(self):
         """
@@ -614,7 +615,7 @@ def terminated_states(self):
             # Re-save the state in case the user changed its data
             self._save(state, state_id=state_id)
 
-    @property
+    @property  # type: ignore
     @sync
     @at_not_running
     def killed_states(self):
@@ -629,7 +630,7 @@ def killed_states(self):
             # Re-save the state in case the user changed its data
             self._save(state, state_id=state_id)
 
-    @property
+    @property  # type: ignore
     @sync
     @at_not_running
     def _all_states(self):
@@ -640,7 +641,7 @@ def _all_states(self):
         """
         return tuple(self._ready_states) + tuple(self._terminated_states)
 
-    @property
+    @property  # type: ignore
     @sync
     def all_states(self):
         """
@@ -777,7 +778,7 @@ def subscribe(self, name, callback):
             callback = MethodType(callback, self)
         super().subscribe(name, callback)
 
-    @property
+    @property  # type: ignore
     @at_not_running
     def context(self):
         """ Convenient access to shared context. We maintain a local copy of the

manticore/core/smtlib/expression.py

@@ -36,7 +36,7 @@ def taint(self):
         return self._taint
 
 
-def issymbolic(value):
+def issymbolic(value) -> bool:
     """
         Helper to determine whether an object is symbolic (e.g checking
         if data read from memory is symbolic)

manticore/core/smtlib/solver.py

@@ -18,6 +18,7 @@
 import collections
 import shlex
 import time
+from typing import Dict, Tuple
 from subprocess import PIPE, Popen
 import re
 from . import operators as Operators
@@ -49,7 +50,7 @@
 
 
 class SingletonMixin(object):
-    __singleton_instances = {}
+    __singleton_instances: Dict[Tuple[int, int], "SingletonMixin"] = {}
 
     @classmethod
     def instance(cls):
@@ -493,18 +494,24 @@ def optimize(self, constraints: ConstraintSet, x: BitVec, goal: str, M=10000):
                         maybe_sat = self._recv()
                         if maybe_sat == "sat":
                             m = RE_MIN_MAX_OBJECTIVE_EXPR_VALUE.match(_status)
-                            expr, value = m.group("expr"), m.group("value")
-                            assert expr == aux.name
-                            return int(value)
+                            if m:
+                                expr, value = m.group("expr"), m.group("value")
+                                assert expr == aux.name
+                                return int(value)
+                            else:
+                                raise SolverError("Could not match MinMax objective value regex")
                     elif _status == "sat":
                         ret = self._recv()
                         if not (ret.startswith("(") and ret.endswith(")")):
                             raise SolverError("bad output on max, z3 may have been killed")
 
                         m = RE_OBJECTIVES_EXPR_VALUE.match(ret)
-                        expr, value = m.group("expr"), m.group("value")
-                        assert expr == aux.name
-                        return int(value)
+                        if m:
+                            expr, value = m.group("expr"), m.group("value")
+                            assert expr == aux.name
+                            return int(value)
+                        else:
+                            raise SolverError("Could not match objective value regex")
                 finally:
                     self._pop()
                     self._reset(temp_cs)

manticore/core/workspace.py

@@ -9,10 +9,11 @@
 from contextlib import contextmanager
 
 try:
-    from contextlib import nullcontext
+    # nullcontext is not present before Python 3.7
+    from contextlib import nullcontext  # type: ignore
 except ImportError:
 
-    class nullcontext:
+    class nullcontext:  # type: ignore
         def __init__(self, enter_result=None):
             self.enter_result = enter_result
 

manticore/ethereum/abi.py

@@ -281,6 +281,8 @@ def _serialize_uint(value, size=32, padding=0):
         if not isinstance(value, (int, BitVec, EVMAccount)):
             raise ValueError
         if issymbolic(value):
+            # Help mypy out. Can remove this by teaching it how issymbolic works
+            assert isinstance(value, BitVec)
             # FIXME This temporary array variable should be obtained from a specific constraint store
             buffer = ArrayVariable(
                 index_bits=256, index_max=32, value_bits=8, name="temp{}".format(uuid.uuid1())
@@ -312,21 +314,21 @@ def _serialize_int(value: typing.Union[int, BitVec], size=32, padding=0):
         if not isinstance(value, (int, BitVec)):
             raise ValueError
         if issymbolic(value):
+            # Help mypy out. Can remove this by teaching it how issymbolic works
+            assert isinstance(value, BitVec)
             buf = ArrayVariable(
                 index_bits=256, index_max=32, value_bits=8, name="temp{}".format(uuid.uuid1())
             )
             value = Operators.SEXTEND(value, value.size, size * 8)
-            buf = ArrayProxy(buf.write_BE(padding, value, size))
+            return ArrayProxy(buf.write_BE(padding, value, size))
         else:
-            value = int(value)
-            buf = bytearray()
+            buf_arr = bytearray()
             for _ in range(padding):
-                buf.append(0)
+                buf_arr.append(0)
 
             for position in reversed(range(size)):
-                buf.append(Operators.EXTRACT(value, position * 8, 8))
-            buf = bytes(buf)
-        return buf
+                buf_arr.append(Operators.EXTRACT(value, position * 8, 8))
+            return bytes(buf_arr)
 
     @staticmethod
     def _readBE(data, nbytes, padding=False, offset=0):

manticore/ethereum/abitypes.py

@@ -223,7 +223,7 @@ def p_error(p):
 
 with warnings.catch_warnings():
     # yacc.yacc() doesn't close the debuglog file after generating the parser table.
-    warnings.simplefilter("ignore", category="ResourceWarning")
+    warnings.simplefilter("ignore", category=ResourceWarning)
     parser = yacc.yacc(debug=False)
 parse = parser.parse
 

manticore/ethereum/account.py

@@ -49,9 +49,6 @@ def __int__(self):
     def __str__(self):
         return str(self._address)
 
-    def __hash__(self):
-        return self._address
-
 
 class EVMContract(EVMAccount):
     """

manticore/ethereum/detectors.py

@@ -1,5 +1,7 @@
 from manticore.core.smtlib.visitors import simplify
 import hashlib
+from enum import Enum
+from typing import Optional
 import logging
 from contextlib import contextmanager
 
@@ -18,7 +20,7 @@
 logger = logging.getLogger(__name__)
 
 
-class DetectorClassification:
+class DetectorClassification(Enum):
     """
     Shall be consistent with
     https://github.com/trailofbits/slither/blob/563d5118298e4cae7f0ea5f2a531f0dcdcebd64d/slither/detectors/abstract_detector.py#L11-L15
@@ -31,10 +33,14 @@ class DetectorClassification:
 
 
 class Detector(Plugin):
-    ARGUMENT = None  # argument that needs to be passed to --detect to use given detector
-    HELP = None  # help string
-    IMPACT = None  # DetectorClassification value
-    CONFIDENCE = None  # DetectorClassification value
+    # argument that needs to be passed to --detect to use given detector
+    ARGUMENT: Optional[str] = None
+    # help string
+    HELP: Optional[str] = None
+    # DetectorClassification value
+    IMPACT: Optional[DetectorClassification] = None
+    # DetectorClassification value
+    CONFIDENCE: Optional[DetectorClassification] = None
 
     @property
     def name(self):

manticore/ethereum/manticore.py

@@ -406,11 +406,11 @@ def __init__(self, workspace_url: str = None, policy: str = "random"):
         else:
             raise NotImplemented
 
-        self._accounts = dict()
+        self._accounts: Dict[str, EVMContract] = dict()
         self._serializer = PickleSerializer()
 
         self.constraints = constraints
-        self.detectors = {}
+        self.detectors: Dict[str, Detector] = {}
         self.metadata: Dict[int, SolidityMetadata] = {}
 
     @property
@@ -419,7 +419,7 @@ def world(self):
         return self.get_world()
 
     # deprecate this 5 in favor of for state in m.all_states: do stuff?
-    @property
+    @property  # type: ignore
     @deprecated("You should iterate over `m.all_states` instead.")
     def completed_transactions(self):
         with self.locked_context("ethereum") as context:
@@ -942,7 +942,7 @@ def preconstraint_for_call_transaction(
         data: Array,
         value: Optional[Union[int, Expression]] = None,
         contract_metadata: Optional[SolidityMetadata] = None,
-    ) -> BoolOperation:
+    ):
         """ Returns a constraint that excludes combinations of value and data that would cause an exception in the EVM
             contract dispatcher.
 

manticore/ethereum/solidity.py

@@ -279,7 +279,7 @@ def function_signatures(self) -> Iterable[str]:
         """The signatures of all normal contract functions."""
         return self._function_signatures_by_selector.values()
 
-    @property
+    @property  # type: ignore
     @deprecated(
         "Use `.function_signatures` instead, which does not return the `'{fallback}()'` pseudo-signature"
     )
@@ -310,7 +310,7 @@ def function_selectors(self) -> Iterable[bytes]:
             return tuple(selectors)
         return (*selectors, self.fallback_function_selector)
 
-    @property
+    @property  # type: ignore
     @deprecated(
         "Use `.function_selectors` instead, which only returns a fallback"
         " function selector if the contract has a non-default fallback function."