Repository: ConsenSys/mythril-classic
Pull request #910 (2019-02-06 08:44:25)

Solver statistics
This pr implements the logic to measure query count and solving time.

Additionally two minor bugs were fixed


Patch:
diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py
index ba488ac2..15e9c43f 100644
--- a/mythril/laser/ethereum/state/constraints.py
+++ b/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
diff --git a/mythril/laser/smt/__init__.py b/mythril/laser/smt/__init__.py
index 98f52d7e..28f0c42b 100644
--- a/mythril/laser/smt/__init__.py
+++ b/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
diff --git a/mythril/laser/smt/solver/__init__.py b/mythril/laser/smt/solver/__init__.py
new file mode 100644
index 00000000..f2839b9a
--- /dev/null
+++ b/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
diff --git a/mythril/laser/smt/independence_solver.py b/mythril/laser/smt/solver/independence_solver.py
similarity index 97%
rename from mythril/laser/smt/independence_solver.py
rename to mythril/laser/smt/solver/independence_solver.py
index 781a26fd..8f64de46 100644
--- a/mythril/laser/smt/independence_solver.py
+++ b/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()
diff --git a/mythril/laser/smt/solver.py b/mythril/laser/smt/solver/solver.py
similarity index 96%
rename from mythril/laser/smt/solver.py
rename to mythril/laser/smt/solver/solver.py
index 55d6d4ef..2f3d4ac1 100644
--- a/mythril/laser/smt/solver.py
+++ b/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
diff --git a/mythril/laser/smt/solver/solver_statistics.py b/mythril/laser/smt/solver/solver_statistics.py
new file mode 100644
index 00000000..603caf69
--- /dev/null
+++ b/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
+        )
diff --git a/mythril/mythril.py b/mythril/mythril.py
index 5c08ab8a..2f082ba0 100644
--- a/mythril/mythril.py
+++ b/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)
diff --git a/solidity_examples/BECToken.sol b/solidity_examples/BECToken.sol
index 3a14fd12..98bd5a09 100644
--- a/solidity_examples/BECToken.sol
+++ b/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();
     }
-}
\ No newline at end of file
+}


Test patch:
diff --git a/tests/laser/smt/independece_solver_test.py b/tests/laser/smt/independece_solver_test.py
index 829b4707..27288752 100644
--- a/tests/laser/smt/independece_solver_test.py
+++ b/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,