Misc bug fixes (#1764)

mythril/laser/ethereum/instructions.py

@@ -5,6 +5,7 @@ import logging
 from copy import copy, deepcopy
 from typing import cast, Callable, List, Union, Tuple
 
+from mythril.exceptions import UnsatError
 from mythril.laser.smt import (
     Extract,
     Expression,
@@ -1742,7 +1743,10 @@ class Instruction:
                 size = size.value
         code_raw = []
         constraints = global_state.world_state.constraints
-        model = get_model(constraints)
+        try:
+            model = get_model(constraints)
+        except UnsatError:
+            model = None
         if isinstance(call_data, ConcreteCalldata):
             for element in call_data.concrete(model):
                 if isinstance(element, BitVec) and element.symbolic:

mythril/laser/ethereum/state/calldata.py

@@ -202,7 +202,12 @@ class BasicConcreteCalldata(BaseCalldata):
         """
         concrete_calldata = []
         for data in self._calldata:
-            concrete_calldata.append(model.eval(data, model_completion=True))
+            if isinstance(data, BitVec) and data.symbolic and model is not None:
+                concrete_calldata.append(model.eval(data, model_completion=True))
+            elif isinstance(data, BitVec) and data.symbolic is False:
+                concrete_calldata.append(data)
+            else:
+                break
         return concrete_calldata
 
     @property

mythril/solidity/soliditycontract.py

@@ -309,9 +309,9 @@ class SolidityContract(EVMContract):
         mappings = self.constructor_mappings if constructor else self.mappings
         index = helper.get_instruction_index(disassembly.instruction_list, address)
 
-        if index >= len(mappings):
-            # TODO: Find why this scenario happens.
-            mappings = self.constructor_mappings if not constructor else self.mappings
+        if index is None or index >= len(mappings):
+            # TODO: Find why this scenario happens. Possibly an external call
+            return None
 
         file_index = mappings[index].solidity_file_idx