save

mythril/analysis/modules/exceptions.py

@@ -24,9 +24,7 @@ def execute(statespace):
         for state in node.states:
 
             instruction = state.get_current_instruction()
-
             if(instruction['opcode'] == "ASSERT_FAIL"):
-
                 try:
                     model = solver.get_model(node.constraints)
                     address = state.get_current_instruction()['address']

mythril/analysis/modules/integer.py

@@ -30,6 +30,7 @@ def execute(statespace):
         node = statespace.nodes[k]
 
         for state in node.states:
+            # pass
             issues += _check_integer_underflow(statespace, state, node)
             issues += _check_integer_overflow(statespace, state, node)
 
@@ -50,6 +51,8 @@ def _check_integer_overflow(statespace, state, node):
     instruction = state.get_current_instruction()
     if instruction['opcode'] not in ("ADD", "MUL"):
         return issues
+    if instruction['address'] != 755:
+        return issues
 
     # Formulate overflow constraints
     stack = state.mstate.stack
@@ -108,7 +111,6 @@ def _verify_integer_overflow(statespace, node, expr, state, model, constraint, o
 
     return _try_constraints(node.constraints, [Not(constraint)]) is not None
 
-
 def _try_constraints(constraints, new_constraints):
     """
     Tries new constraints

mythril/analysis/solver.py

@@ -4,7 +4,7 @@ import logging
 
 def get_model(constraints):
     s = Solver()
-    s.set("timeout", 10000)
+    s.set("timeout", 100000)
 
     for constraint in constraints:
         s.add(constraint)
@@ -12,7 +12,7 @@ def get_model(constraints):
     if result == sat:
         return s.model()
     elif result == unknown:
-        logging.info("Timeout encountered while solving expression using z3")
+        logging.error("Timeout encountered while solving expression using z3")
     raise UnsatError
 
 

mythril/laser/ethereum/instructions.py

@@ -778,7 +778,7 @@ class Instruction:
                 new_state = copy(global_state)
                 new_state.mstate.pc = index
                 new_state.mstate.depth += 1
-                new_state.mstate.constraints.append(condi)
+                new_state.mstate.constraints.append(simplify(condi))
 
                 states.append(new_state)
             else:
@@ -786,12 +786,11 @@ class Instruction:
 
         # False case
         negated = Not(condition) if type(condition) == BoolRef else condition == 0
-        sat = not is_false(simplify(negated)) if type(condi) == BoolRef else not negated
 
-        if sat:
+        if (type(negated) == bool and negated) or (type(negated) == BoolRef and not is_false(simplify(negated))):
             new_state = copy(global_state)
             new_state.mstate.depth += 1
-            new_state.mstate.constraints.append(negated)
+            new_state.mstate.constraints.append(simplify(negated))
             states.append(new_state)
         else:
             logging.debug("Pruned unreachable states.")

mythril/laser/ethereum/state.py

@@ -39,7 +39,12 @@ class Account:
         self.balance += balance
 
     def get_storage(self, index):
-        return self.storage[index] if index in self.storage.keys() else BitVec("storage_" + str(index), 256)
+        if index in self.storage.keys():
+            return self.storage[index]
+        else:
+            symbol = BitVec("storage_" + str(index), 256)
+            self.storage[index] = symbol
+            return symbol
 
     @property
     def as_dict(self):

mythril/laser/ethereum/svm.py

@@ -70,7 +70,7 @@ class LaserEVM:
             try:
                 new_states, op_code = self.execute_state(global_state)
             except NotImplementedError:
-                logging.debug("Encountered unimplemented instruction")
+                logging.error("Encountered unimplemented instruction: {}".format(op_code))
                 continue
 
             if len(new_states) == 0: