Merge pull request #910 from JoranHonig/features/solver_stats

Solver statistics

mythril/laser/ethereum/state/constraints.py

@@ -1,7 +1,7 @@
 """This module contains the class used to represent state-change constraints in
 the call graph."""
 
-from mythril.laser.smt import Solver, Bool
+from mythril.laser.smt import Solver, Bool, symbol_factory
 
 from typing import Iterable, List, Optional, Union
 from z3 import unsat
@@ -40,6 +40,11 @@ class Constraints(list):
         solver = Solver()
         solver.set_timeout(self._default_timeout)
         for constraint in self[:]:
+            constraint = (
+                symbol_factory.Bool(constraint)
+                if isinstance(constraint, bool)
+                else constraint
+            )
             solver.add(constraint)
         self._is_possible = solver.check() != unsat
         return self._is_possible

mythril/laser/smt/__init__.py

@@ -17,7 +17,7 @@ from mythril.laser.smt.bitvec import (
 from mythril.laser.smt.expression import Expression, simplify
 from mythril.laser.smt.bool import Bool, is_true, is_false, Or, Not, And
 from mythril.laser.smt.array import K, Array, BaseArray
-from mythril.laser.smt.solver import Solver, Optimize
+from mythril.laser.smt.solver import Solver, Optimize, SolverStatistics
 from mythril.laser.smt.model import Model
 
 from typing import Union, Any, Optional, List, TypeVar, Generic

mythril/laser/smt/solver/__init__.py

@@ -0,0 +1,3 @@
+from mythril.laser.smt.solver.solver import Solver, Optimize, BaseSolver
+from mythril.laser.smt.solver.independence_solver import IndependenceSolver
+from mythril.laser.smt.solver.solver_statistics import SolverStatistics

mythril/laser/smt/solver/independence_solver.py

@@ -2,6 +2,8 @@ import z3
 
 from mythril.laser.smt.model import Model
 from mythril.laser.smt.bool import Bool
+from mythril.laser.smt.solver.solver_statistics import stat_smt_query
+
 from typing import Set, Tuple, Dict, List, cast
 
 
@@ -63,7 +65,7 @@ class DependenceMap:
             relevant_buckets.add(new_bucket)
             new_bucket = self._merge_buckets(relevant_buckets)
 
-        for variable in variables:
+        for variable in new_bucket.variables:
             self.variable_map[str(variable)] = new_bucket
 
     def _merge_buckets(self, bucket_list: Set[DependenceBucket]) -> DependenceBucket:
@@ -118,6 +120,7 @@ class IndependenceSolver:
         ]  # type: List[z3.BoolRef]
         self.constraints.extend(raw_constraints)
 
+    @stat_smt_query
     def check(self) -> z3.CheckSatResult:
         """Returns z3 smt check result. """
         dependence_map = DependenceMap()

mythril/laser/smt/solver/solver.py

@@ -7,7 +7,7 @@ from typing import Union, cast, TypeVar, Generic, List, Sequence
 from mythril.laser.smt.expression import Expression
 from mythril.laser.smt.model import Model
 from mythril.laser.smt.bool import Bool
-
+from mythril.laser.smt.solver.solver_statistics import stat_smt_query
 
 T = TypeVar("T", bound=Union[z3.Solver, z3.Optimize])
 
@@ -44,6 +44,7 @@ class BaseSolver(Generic[T]):
         """
         self.add(*constraints)
 
+    @stat_smt_query
     def check(self) -> z3.CheckSatResult:
         """Returns z3 smt check result.
         Also suppresses the stdout when running z3 library's check() to avoid unnecessary output

mythril/laser/smt/solver/solver_statistics.py

@@ -0,0 +1,43 @@
+from time import time
+
+from mythril.support.support_utils import Singleton
+
+from typing import Callable
+
+
+def stat_smt_query(func: Callable):
+    """Measures statistics for annotated smt query check function"""
+    stat_store = SolverStatistics()
+
+    def function_wrapper(*args, **kwargs):
+        if not stat_store.enabled:
+            return func(*args, **kwargs)
+
+        stat_store.query_count += 1
+        begin = time()
+
+        result = func(*args, **kwargs)
+
+        end = time()
+        stat_store.solver_time += end - begin
+
+        return result
+
+    return function_wrapper
+
+
+class SolverStatistics(object, metaclass=Singleton):
+    """ Solver Statistics Class
+
+    Keeps track of the important statistics around smt queries
+    """
+
+    def __init__(self):
+        self.enabled = False
+        self.query_count = 0
+        self.solver_time = 0
+
+    def __repr__(self):
+        return "Query count: {} \nSolver time: {}".format(
+            self.query_count, self.solver_time
+        )

mythril/mythril.py

@@ -35,6 +35,7 @@ from mythril.analysis.security import fire_lasers, retrieve_callback_issues
 from mythril.analysis.report import Report
 from mythril.support.truffle import analyze_truffle_project
 from mythril.ethereum.interface.leveldb.client import EthLevelDB
+from mythril.laser.smt import SolverStatistics
 
 log = logging.getLogger(__name__)
 
@@ -566,6 +567,7 @@ class Mythril(object):
         :return:
         """
         all_issues = []
+        SolverStatistics().enabled = True
         for contract in contracts or self.contracts:
             try:
                 sym = SymExecWrapper(
@@ -600,6 +602,7 @@ class Mythril(object):
                 issue.add_code_info(contract)
 
             all_issues += issues
+            log.info("Solver statistics: \n{}".format(str(SolverStatistics())))
 
         source_data = Source()
         source_data.get_source_from_contracts_list(self.contracts)

solidity_examples/BECToken.sol

@@ -1,4 +1,3 @@
-pragma solidity 0.5.0;
 
 /**
  * @title SafeMath
@@ -296,4 +295,4 @@ contract BecToken is PausableToken {
         //if ether is sent to this address, send it back.
         revert();
     }
-}
+}

tests/laser/smt/independece_solver_test.py

@@ -1,4 +1,4 @@
-from mythril.laser.smt.independence_solver import (
+from mythril.laser.smt.solver.independence_solver import (
     _get_expr_variables,
     DependenceBucket,
     DependenceMap,