Basic solver stats (#2415)

* Implemented basic solver stats

* added assert

* improved stats

* added assert

* measure time in EVM

* removed redundant code

* linted

* fixed tests

* check if manticore executed

* fix

* fixes

manticore/core/manticore.py

@@ -14,7 +14,7 @@
 import shlex
 
 from ..core.plugin import Plugin, IntrospectionAPIPlugin, StateDescriptor
-from ..core.smtlib import Expression
+from ..core.smtlib import Expression, SOLVER_STATS
 from ..core.state import StateBase
 from ..core.workspace import ManticoreOutput
 from ..exceptions import ManticoreError
@@ -1106,6 +1106,10 @@ def run(self):
         """
         Runs analysis.
         """
+        # Start measuring the execution time
+        with self.locked_context() as context:
+            context["time_started"] = time.time()
+
         # Delete state cache
         # The cached version of a state may get out of sync if a worker in a
         # different process modifies the state
@@ -1219,7 +1223,28 @@ def save_run_data(self):
         with self._output.save_stream("manticore.yml") as f:
             config.save(f)
 
+        with self._output.save_stream("global.solver_stats") as f:
+            for s, n in sorted(SOLVER_STATS.items()):
+                f.write("%s: %d\n" % (s, n))
+
+        if SOLVER_STATS["timeout"] > 0 or SOLVER_STATS["unknown"] > 0:
+            logger.warning(
+                "The SMT solvers returned timeout or unknown for certain program paths. Results could not cover the entire set of possible paths"
+            )
+
         logger.info("Results in %s", self._output.store.uri)
+
+        time_ended = time.time()
+
+        with self.locked_context() as context:
+            if "time_started" in context:
+                time_elapsed = time_ended - context["time_started"]
+                logger.info("Total time: %s", time_elapsed)
+                context["time_ended"] = time_ended
+                context["time_elapsed"] = time_elapsed
+            else:
+                logger.warning("Manticore failed to run")
+
         self.wait_for_log_purge()
 
     def introspect(self) -> typing.Dict[int, StateDescriptor]:

manticore/core/smtlib/solver.py

@@ -78,6 +78,8 @@ class SolverType(config.ConfigEnum):
 )
 RE_MIN_MAX_OBJECTIVE_EXPR_VALUE = re.compile(r"(?P<expr>.*?)\s+\|->\s+(?P<value>.*)", re.DOTALL)
 
+SOLVER_STATS = {"unknown": 0, "timeout": 0}
+
 
 class SingletonMixin(object):
     __singleton_instances: Dict[Tuple[int, int], "SingletonMixin"] = {}
@@ -261,6 +263,8 @@ def is_started(self):
 
 
 class SMTLIBSolver(Solver):
+    sname: Optional[str] = None
+
     def __init__(
         self,
         command: str,
@@ -331,9 +335,18 @@ def _is_sat(self) -> bool:
         if consts.defaultunsat:
             if status == "unknown":
                 logger.info("Found an unknown core, probably a solver timeout")
+                SOLVER_STATS["timeout"] += 1
                 status = "unsat"
+                raise SolverUnknown(status)
+
         if status == "unknown":
+            SOLVER_STATS["unknown"] += 1
             raise SolverUnknown(status)
+        else:
+            assert self.sname is not None
+            SOLVER_STATS.setdefault(self.sname, 0)
+            SOLVER_STATS[self.sname] += 1
+
         return status == "sat"
 
     def _assert(self, expression: Bool):
@@ -464,6 +477,7 @@ def _optimize_generic(self, constraints: ConstraintSet, x: BitVec, goal: str, ma
                     M = L
 
                 if time.time() - start > consts.timeout:
+                    SOLVER_STATS["timeout"] += 1
                     raise SolverError("Timeout")
 
         # reset to before the dichotomic search
@@ -486,11 +500,15 @@ def _optimize_generic(self, constraints: ConstraintSet, x: BitVec, goal: str, ma
                 self._assert(X != last_value)
                 i = i + 1
                 if i > max_iter:
+                    SOLVER_STATS["unknown"] += 1
                     raise SolverError("Optimizing error, maximum number of iterations was reached")
                 if time.time() - start > consts.timeout:
+                    SOLVER_STATS["timeout"] += 1
                     raise SolverError("Timeout")
             if last_value is not None:
                 return last_value
+
+            SOLVER_STATS["unknown"] += 1
             raise SolverError("Optimizing error, unsat or unknown core")
 
     @lru_cache(maxsize=32)
@@ -547,6 +565,7 @@ def get_all_values(
                     else:
                         raise TooManySolutions(result)
                 if time.time() - start > consts.timeout:
+                    SOLVER_STATS["timeout"] += 1
                     if silent:
                         logger.info("Timeout searching for all solutions")
                         return list(result)
@@ -583,6 +602,11 @@ def _optimize_fancy(self, constraints: ConstraintSet, x: BitVec, goal: str, max_
             self._smtlib.send("(%s %s)" % (goal, aux.name))
             self._smtlib.send("(check-sat)")
             _status = self._smtlib.recv()
+
+            assert self.sname is not None
+            SOLVER_STATS.setdefault(self.sname, 0)
+            SOLVER_STATS[self.sname] += 1
+
             if _status == "sat":
                 return self._getvalue(aux)
             raise SolverError("Optimize failed")
@@ -621,6 +645,7 @@ def get_value(self, constraints: ConstraintSet, *expressions):
                         result.append(self.__getvalue_bv(var[i].name))
                     values.append(bytes(result))
                     if time.time() - start > consts.timeout:
+                        SOLVER_STATS["timeout"] += 1
                         raise SolverError("Timeout")
                     continue
 
@@ -638,6 +663,7 @@ def get_value(self, constraints: ConstraintSet, *expressions):
                 if isinstance(expression, BitVec):
                     values.append(self.__getvalue_bv(var.name))
             if time.time() - start > consts.timeout:
+                SOLVER_STATS["timeout"] += 1
                 raise SolverError("Timeout")
 
         if len(expressions) == 1:
@@ -647,6 +673,8 @@ def get_value(self, constraints: ConstraintSet, *expressions):
 
 
 class Z3Solver(SMTLIBSolver):
+    sname = "z3"
+
     def __init__(self):
         """
         Build a Z3 solver instance.
@@ -721,6 +749,8 @@ def _solver_version(self) -> Version:
 
 
 class YicesSolver(SMTLIBSolver):
+    sname = "yices"
+
     def __init__(self):
         init = ["(set-logic QF_AUFBV)"]
         command = f"{consts.yices_bin} --timeout={consts.timeout}  --incremental"
@@ -734,13 +764,17 @@ def __init__(self):
 
 
 class CVC4Solver(SMTLIBSolver):
+    sname = "cvc4"
+
     def __init__(self):
         init = ["(set-logic QF_AUFBV)", "(set-option :produce-models true)"]
         command = f"{consts.cvc4_bin} --tlimit={consts.timeout * 1000} --lang=smt2 --incremental"
         super().__init__(command=command, init=init)
 
 
 class BoolectorSolver(SMTLIBSolver):
+    sname = "boolector"
+
     def __init__(self):
         init = ["(set-logic QF_AUFBV)", "(set-option :produce-models true)"]
         command = f"{consts.boolector_bin} --time={consts.timeout} -i"

manticore/ethereum/manticore.py

@@ -1786,8 +1786,6 @@ def worker_finalize(q):
                     global_findings_stream.write("    ".join(source_code_snippet.splitlines(True)))
                     global_findings_stream.write("\n")
 
-        self.save_run_data()
-
         with self._output.save_stream("global.summary") as global_summary:
             # (accounts created by contract code are not in this list )
             global_summary.write("Global runtime coverage:\n")
@@ -1855,6 +1853,7 @@ def worker_finalize(q):
                 for o in sorted(visited):
                     f.write("0x%x\n" % o)
 
+        self.save_run_data()
         self.remove_all()
 
     def global_coverage(self, account):

manticore/native/manticore.py

@@ -402,8 +402,6 @@ def resolve(self, symbol):
             raise ValueError(f"The {self.binary_path} ELFfile does not contain symbol {symbol}")
 
     def run(self, timeout=None):
-        with self.locked_context() as context:
-            context["time_started"] = time.time()
         with self.kill_timeout(timeout):
             super().run()
 
@@ -414,16 +412,6 @@ def finalize(self):
     def save_run_data(self):
         super().save_run_data()
 
-        time_ended = time.time()
-
-        with self.locked_context() as context:
-            time_elapsed = time_ended - context["time_started"]
-
-            logger.info("Total time: %s", time_elapsed)
-
-            context["time_ended"] = time_ended
-            context["time_elapsed"] = time_elapsed
-
 
 def _make_initial_state(binary_path, **kwargs):
     with open(binary_path, "rb") as f:

manticore/wasm/manticore.py

@@ -46,9 +46,6 @@ def run(self, timeout=None):
 
         :param timeout: number of seconds after which to kill execution
         """
-        with self.locked_context() as context:
-            context["time_started"] = time.time()
-
         with self.kill_timeout(timeout):
             super().run()
 
@@ -63,16 +60,6 @@ def finalize(self):
     def save_run_data(self):
         super().save_run_data()
 
-        time_ended = time.time()
-
-        with self.locked_context() as context:
-            time_elapsed = time_ended - context["time_started"]
-
-            logger.info("Total time: %s", time_elapsed)
-
-            context["time_ended"] = time_ended
-            context["time_elapsed"] = time_elapsed
-
     def __getattr__(self, item):
         """
         Allows users to invoke & run functions in the same style as ethereum smart contracts. So: