Work on "Model is not Available" errors in tests (#1659)

* Check disk/memory usage if we get unsat results

* Expand "Model unavailable" message

* Ignore missing psutil imports

* Add resource checks to CLI application

manticore/__main__.py

@@ -11,7 +11,7 @@ from crytic_compile import is_supported, cryticparser
 from .core.manticore import ManticoreBase, set_verbosity
 from .ethereum.cli import ethereum_main
 from .wasm.cli import wasm_main
-from .utils import config, log, install_helper
+from .utils import config, log, install_helper, resources
 
 consts = config.get_group("main")
 consts.add("recursionlimit", default=10000, description="Value to set for Python recursion limit")
@@ -38,6 +38,9 @@ def main():
 
     set_verbosity(args.v)
 
+    resources.check_disk_usage()
+    resources.check_memory_usage()
+
     if args.argv[0].endswith(".sol") or is_supported(args.argv[0]):
         ethereum_main(args, logger)
     elif args.argv[0].endswith(".wasm") or args.argv[0].endswith(".wat"):

manticore/core/smtlib/solver.py

@@ -26,6 +26,7 @@ from .constraints import *
 from .visitors import *
 from ...exceptions import Z3NotFoundError, SolverError, SolverUnknown, TooManySolutions, SmtlibError
 from ...utils import config
+from ...utils.resources import check_memory_usage, check_disk_usage
 from . import issymbolic
 
 logger = logging.getLogger(__name__)
@@ -355,7 +356,11 @@ class Z3Solver(Solver):
         if status == "unknown":
             raise SolverUnknown(status)
 
-        return status == "sat"
+        is_sat = status == "sat"
+        if not is_sat:
+            check_memory_usage()
+            check_disk_usage()
+        return is_sat
 
     def _assert(self, expression: Bool):
         """Auxiliary method to send an assert"""
@@ -614,7 +619,9 @@ class Z3Solver(Solver):
 
                     self._reset(temp_cs)
                     if not self._is_sat():
-                        raise SolverError("Model is not available")
+                        raise SolverError(
+                            "Solver could not find a value for expression under current constraint set"
+                        )
 
                     for i in range(expression.index_max):
                         self._send("(get-value (%s))" % var[i].name)
@@ -634,7 +641,9 @@ class Z3Solver(Solver):
                 self._reset(temp_cs)
 
                 if not self._is_sat():
-                    raise SolverError("Model is not available")
+                    raise SolverError(
+                        "Solver could not find a value for expression under current constraint set"
+                    )
 
                 self._send("(get-value (%s))" % var.name)
                 ret = self._recv()

manticore/utils/resources.py

@@ -0,0 +1,33 @@
+import logging
+from psutil import disk_usage, virtual_memory
+
+logger = logging.getLogger(__name__)
+logger.setLevel(logging.INFO)
+
+#: Percentage of _used_ memory to warn above
+memory_warn_percent = 95.0
+#: Number of free bytes to warn below
+memory_warn_absolute = (1024 ** 3) // 2
+#: Number of free bytes to warn below
+disk_warn = 1024 ** 3
+
+
+def check_memory_usage():
+    """
+    Print a warning message if the available memory space is below memory_warn
+    """
+    usage = virtual_memory()
+    if usage.percent >= 95.0 or usage.available < memory_warn_absolute:
+        logger.warning(
+            "System only has %d kib of virtual memory available", usage.available // 1024
+        )
+
+
+def check_disk_usage(path="."):
+    """
+    Print a warning message if the available disk space is below disk_warn
+    :param path: System path to check. Defaults to the current directory.
+    """
+    usage = disk_usage(path)
+    if usage.free < (disk_warn):
+        logger.warning("Only %d kib of disk space remaining", usage.free // 1024)

mypy.ini

@@ -42,3 +42,6 @@ ignore_missing_imports = True
 
 [mypy-wasm.*]
 ignore_missing_imports = True
+
+[mypy-psutil.*]
+ignore_missing_imports = True

setup.py

@@ -60,6 +60,7 @@ setup(
         "crytic-compile>=0.1.1",
         "wasm",
         "dataclasses; python_version < '3.7'",
+        "psutil",
     ]
     + rtd_dependent_deps(),
     extras_require=extra_require,