Handle issues with simplify (#1674)

* Add exit code * Update docs with tutorial * Fix docs * Reformat * Fix the issue with loop-bound and solver-timeout * Add test changes * Restrict hexbytes * Use solver over simplify
Consensys · Sep 3, 2022 · 427d40e · 427d40e
1 parent 8d863fb
commit 427d40e
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 5 deletions.
diff --git a/mythril/analysis/module/modules/integer.py b/mythril/analysis/module/modules/integer.py
@@ -207,7 +207,6 @@ def _handle_sstore(state: GlobalState) -> None:
             return
 
         state_annotation = _get_overflowunderflow_state_annotation(state)
-
         for annotation in value.annotations:
             if isinstance(annotation, OverUnderflowAnnotation):
                 state_annotation.overflowing_state_annotations.add(annotation)

diff --git a/mythril/interfaces/cli.py b/mythril/interfaces/cli.py
@@ -514,7 +514,7 @@ def add_analysis_args(options):
         "--pruning-factor",
         type=float,
         default=1,
-        help="Checks for reachability at the rate of <pruning-factor>. Where 1 means checks every execution",
+        help="Checks for reachability at the rate of <pruning-factor> (range 0-1.0). Where 1.0 would mean checking for every execution",
     )
     options.add_argument(
         "--unconstrained-storage",

diff --git a/mythril/laser/ethereum/state/calldata.py b/mythril/laser/ethereum/state/calldata.py
@@ -4,10 +4,11 @@
 
 from typing import Any, Union
 
-from z3 import Model
+from z3 import Model, unsat, unknown
 from z3.z3types import Z3Exception
 
 from mythril.laser.ethereum.util import get_concrete_int
+
 from mythril.laser.smt import (
     Array,
     BitVec,
@@ -18,6 +19,7 @@
     K,
     simplify,
     symbol_factory,
+    Solver,
 )
 
 
@@ -73,16 +75,22 @@ def __getitem__(self, item: Union[int, slice, BitVec]) -> Any:
                     else symbol_factory.BitVecVal(start, 256)
                 )
                 parts = []
-                while simplify(current_index != stop):
+                while True:
+                    s = Solver()
+                    s.set_timeout(1000)
+                    s.add(current_index != stop)
+                    result = s.check()
+                    if result in (unsat, unknown):
+                        break
                     element = self._load(current_index)
                     if not isinstance(element, Expression):
                         element = symbol_factory.BitVecVal(element, 8)
 
                     parts.append(element)
                     current_index = simplify(current_index + step)
+
             except Z3Exception:
                 raise IndexError("Invalid Calldata Slice")
-
             return parts
 
         raise ValueError