Add type hints to several parts of Manticore (#1667)

* Add type hints

* Add type hints in manticore/core/smtlib/solver.py

* Add type hints to the `unsigned_hexlify` helper function

* Add type hints & more robust error checking to a Solver internal method

* Add type hints in native memory code

* Add type hints to Linux platform test methods

* Add type hints for Linux `sys_access`

* Add type hints for AbstractCPU; rephrase a couple bits to appease mypy

* Add type hints to manticore/platforms/linux.py

* Add type hints for Workspace members

* Add type hints for `Operand`

* Add a return type hint per @ekilmer

Co-Authored-By: Eric Kilmer <eric.d.kilmer@gmail.com>

manticore/core/smtlib/constraints.py

@@ -56,19 +56,19 @@ def __reduce__(self):
             },
         )
 
-    def __enter__(self):
+    def __enter__(self) -> "ConstraintSet":
         assert self._child is None
         self._child = self.__class__()
         self._child._parent = self
         self._child._sid = self._sid
         self._child._declarations = dict(self._declarations)
         return self._child
 
-    def __exit__(self, ty, value, traceback):
+    def __exit__(self, ty, value, traceback) -> None:
         self._child._parent = None
         self._child = None
 
-    def __len__(self):
+    def __len__(self) -> int:
         if self._parent is not None:
             return len(self._constraints) + len(self._parent)
         return len(self._constraints)
@@ -107,7 +107,7 @@ def add(self, constraint, check=False):
             if not solver.check(self):
                 raise ValueError("Added an impossible constraint")
 
-    def _get_sid(self):
+    def _get_sid(self) -> int:
         """ Returns a unique id. """
         assert self._child is None
         self._sid += 1
@@ -263,7 +263,7 @@ def _make_unique_name(self, name="VAR"):
             name = f"{name}_{self._get_sid()}"
         return name
 
-    def is_declared(self, expression_var):
+    def is_declared(self, expression_var) -> bool:
         """ True if expression_var is declared in this constraint set """
         if not isinstance(expression_var, Variable):
             raise ValueError(f"Expression must be a Variable (not a {type(expression_var)})")

manticore/core/smtlib/solver.py

@@ -292,7 +292,7 @@ def _reset(self, constraints=None):
         if constraints is not None:
             self._send(constraints)
 
-    def _send(self, cmd: Union[str, ConstraintSet]):
+    def _send(self, cmd: str) -> None:
         """
         Send a string to the solver.
 
@@ -330,8 +330,13 @@ def _recv(self) -> str:
 
         return buf
 
-    def __readline_and_count(self):
-        buf = self._proc.stdout.readline()
+    def __readline_and_count(self) -> Tuple[str, int, int]:
+        stdout = self._proc.stdout
+        if stdout is None:
+            raise SolverError("Could not read from stdout: file descriptor is None")
+        buf = stdout.readline()
+        if buf is None:
+            raise SolverError("Could not read from stdout")
         return buf, buf.count("("), buf.count(")")
 
     # UTILS: check-sat get-value
@@ -411,7 +416,7 @@ def _pop(self):
         """Recall the last pushed constraint store and state."""
         self._send("(pop 1)")
 
-    def can_be_true(self, constraints: ConstraintSet, expression=True):
+    def can_be_true(self, constraints: ConstraintSet, expression: Union[bool, Bool] = True) -> bool:
         """Check if two potentially symbolic values can be equal"""
         if isinstance(expression, bool):
             if not expression:
@@ -592,7 +597,7 @@ def optimize(self, constraints: ConstraintSet, x: BitVec, goal: str, max_iter=10
                 return last_value
             raise SolverError("Optimizing error, unsat or unknown core")
 
-    def get_value(self, constraints, *expressions):
+    def get_value(self, constraints: ConstraintSet, *expressions):
         """
         Ask the solver for one possible result of given expressions using
         given set of constraints.

manticore/core/workspace.py

@@ -421,12 +421,12 @@ class Workspace:
 
     def __init__(self, store_or_desc=None):
         if isinstance(store_or_desc, Store):
-            self._store = store_or_desc
+            self._store: Store = store_or_desc
         else:
             self._store = Store.fromdescriptor(store_or_desc)
-        self._serializer = PickleSerializer()
-        self._prefix = "state_"
-        self._suffix = ".pkl"
+        self._serializer: StateSerializer = PickleSerializer()
+        self._prefix: str = "state_"
+        self._suffix: str = ".pkl"
 
     @property
     def uri(self):

manticore/native/cpu/abstractcpu.py

@@ -10,7 +10,7 @@
 
 from .disasm import init_disassembler
 from ..memory import ConcretizeMemory, InvalidMemoryAccess, FileMap, AnonMap
-from ..memory import LazySMemory
+from ..memory import LazySMemory, Memory
 from ...core.smtlib import Operators, Constant, issymbolic
 from ...core.smtlib import visitors
 from ...core.smtlib.solver import Z3Solver
@@ -264,9 +264,9 @@ class Abi:
     Used for function call and system call models.
     """
 
-    def __init__(self, cpu):
+    def __init__(self, cpu: "Cpu"):
         """
-        :param manticore.core.cpu.Cpu cpu: CPU to initialize with
+        :param CPU to initialize with
         """
         self._cpu = cpu
 
@@ -392,7 +392,7 @@ def invoke(self, model, prefix_args=None):
 platform_logger = logging.getLogger("manticore.platforms.platform")
 
 
-def unsigned_hexlify(i):
+def unsigned_hexlify(i: Any) -> Any:
     if type(i) is int:
         if i < 0:
             return hex((1 << 64) + i)
@@ -497,7 +497,7 @@ class Cpu(Eventful):
         "execute_syscall",
     }
 
-    def __init__(self, regfile: RegisterFile, memory, **kwargs):
+    def __init__(self, regfile: RegisterFile, memory: Memory, **kwargs):
         assert isinstance(regfile, RegisterFile)
         self._disasm = kwargs.pop("disasm", "capstone")
         super().__init__(**kwargs)
@@ -645,7 +645,7 @@ def emulate_until(self, target: int):
     #############################
     # Memory access
     @property
-    def memory(self):
+    def memory(self) -> Memory:
         return self._memory
 
     def write_int(self, where, expression, size=None, force=False):
@@ -680,8 +680,7 @@ def _raw_read(self, where: int, size=1) -> bytes:
         """
         map = self.memory.map_containing(where)
         start = map._get_offset(where)
-        mapType = type(map)
-        if mapType is FileMap:
+        if isinstance(map, FileMap):
             end = map._get_offset(where + size)
 
             if end > map._mapped_size:
@@ -699,7 +698,7 @@ def _raw_read(self, where: int, size=1) -> bytes:
                 data += map._overlay[offset]
             data += raw_data[len(data) :]
 
-        elif mapType is AnonMap:
+        elif isinstance(map, AnonMap):
             data = bytes(map._data[start : start + size])
         else:
             data = b"".join(self.memory[where : where + size])
@@ -743,15 +742,13 @@ def write_bytes(self, where: int, data, force: bool = False) -> None:
         # At the very least, using it in non-concrete mode will break the symbolic strcmp/strlen models. The 1024 byte
         # minimum is intended to minimize the potential effects of this by ensuring that if there _are_ any other
         # issues, they'll only crop up when we're doing very large writes, which are fairly uncommon.
-        can_write_raw = (
-            type(mp) is AnonMap
+        if (
+            isinstance(mp, AnonMap)
             and isinstance(data, (str, bytes))
             and (mp.end - mp.start + 1) >= len(data) >= 1024
             and not issymbolic(data)
             and self._concrete
-        )
-
-        if can_write_raw:
+        ):
             logger.debug("Using fast write")
             offset = mp._get_offset(where)
             if isinstance(data, str):