Merge with master

.github/ISSUE_TEMPLATE/analysis-module.md

@@ -4,34 +4,34 @@ about: Create an analysis module feature request
 
 ---
 
-Please remove any of the optional sections if they are not applicable.
+<!-- Please remove any of the optional sections if they are not applicable. -->
 
 ## Description
 
-Replace this text with a description of an vulnerability that should be
+<!-- Replace this text with a description of an vulnerability that should be
-detected by a Mythril analysis module.
+detected by a Mythril analysis module. -->
 
 ## Tests
 
-_This section is optional._
+<!-- This section is optional.
 
 Replace this text with suggestions on how to test the feature,
 if it is not obvious. This might require certain Solidity source,
 bytecode, or a Truffle project. You can also provide
-links to existing code.
+links to existing code. -->
 
 ## Implementation details
 
-_This section is optional._
+<!-- This section is optional.
 
 If you have thoughts about how to implement the analysis, feel free
-replace this text with that.
+replace this text with that. -->
 
 ## Links
 
-_This section is optional._
+<!-- This section is optional.
 
 Replace this text with any links describing the issue or pointing to resources
 that can help in implementing the analysis
 
-Thanks for helping!
+Thanks for helping! -->

.github/ISSUE_TEMPLATE/bug-report.md

@@ -4,25 +4,20 @@ about: Tell us about Mythril bugs to help us improve
 
 ---
 
-_Note: did you notice that there is now a template for requesting new features?_
+<!-- Note: did you notice that there is now a template for requesting new features?
 
-Please remove any of the optional sections if they are not applicable.
+Please remove any of the optional sections if they are not applicable. -->
 
 ## Description
 
-Replace this text with a clear and concise description of the bug.
+<!-- Replace this text with a clear and concise description of the bug. -->
 
 ## How to Reproduce
 
-Please show both the input you gave and the
+<!-- Please show both the input you gave and the
-output you got in describing how to reproduce the bug:
+output you got in describing how to reproduce the bug.
 
-1. Go to '...'
+For example:
-2. Click on '....'
-3. Scroll down to '....'
-4. See error
-
-or give a complete console log with input and output
 
 ```console
 $ myth <command-line-options>
@@ -34,22 +29,34 @@ Function name: ...
 $
 ```
 
+or perhaps:
+
+1. Go to '...'
+2. Click on '....'
+3. Scroll down to '....'
+4. See error
+
+
 If there is a Solidity source code, a truffle project, or bytecode
 that is involved, please provide that or links to it.
 
+-->
+
 ## Expected behavior
 
-A clear and concise description of what you expected to happen.
+<!-- A clear and concise description of what you expected to happen. -->
 
 ## Screenshots
 
-_This section is optional._
+<!-- This section is optional.
 
 If applicable, add screenshots to help explain your problem.
 
+-->
+
 ## Environment
 
-_This section sometimes is optional but helpful to us._
+<!-- This section sometimes is optional but helpful to us.
 
 Please modify for your setup
 
@@ -58,10 +65,14 @@ Please modify for your setup
 - Python version: `python -V`
 - OS and Version: [e.g. Mac OS High Sierra]
 
+-->
+
 ## Additional Environment or Context
 
-_This section is optional._
+<!-- This section is optional.
 
 Add any other context about the problem here or special environment setup
 
 Thanks for helping!
+
+-->

.github/ISSUE_TEMPLATE/feature-request.md

@@ -6,15 +6,16 @@ about: Tell us about a new feature that would make Mythril better
 
 ## Description
 
-Replace this text with a short description of the feature.
+<!-- Replace this text with a short description of the feature. -->
 
 ## Background
 
-Replace this text with any additional background for the
+<! -- Replace this text with any additional background for the
-feature, for example: user scenarios, or the value of the feature.
+feature, for example: user scenarios, or the value of the feature. -->
 
 ## Tests
-_This section is optional._
+
+<!-- This section is optional.
 
 Replace this text with suggestions on how to test the feature,
 if it is not obvious. This might require certain Solidity source,
@@ -22,3 +23,5 @@ bytecode, or a Truffle project. You can also provide
 links to existing code.
 
 Thanks for helping!
+
+-->

README.md

@@ -7,9 +7,11 @@
 
 <img height="120px" align="right" src="https://github.com/ConsenSys/mythril/raw/master/static/mythril.png" alt="mythril" />
 
-Mythril OSS is the classic open-source version of [Mythril](https://mythril.ai), a security analysis tool for Ethereum smart contracts. It uses concolic analysis, taint analysis and control flow checking to detect a variety of security vulnerabilities.
+Mythril OSS is the classic security analysis tool for Ethereum smart contracts. It uses concolic analysis, taint analysis and control flow checking to detect a variety of security vulnerabilities. 
 
-**Special Announcement**: The Mythril community is moving to [Discord](https://discord.gg/dFHQGrE). Our Gitter channels and Telegram groups will be closed shortly. Whether you want to contribute, need support, or want to learn what we have cooking for the future, out [Discord server](https://discord.gg/dFHQGrE) will serve your needs!
+Whether you want to contribute, need support, or want to learn what we have cooking for the future, our [Discord server](https://discord.gg/dFHQGrE) will serve your needs!
+
+Oh and by the way, we're now building a whole security tools ecosystem with [Mythril Platform API](https://mythril.ai). You should definitely check that out as well.
 
 ## Installation and setup
 

coverage_report.sh

@@ -12,4 +12,5 @@ rm -rf coverage_html_report
 py.test \
     --cov=mythril \
     --cov-config=tox.ini \
-    --cov-report=html:coverage_html_report \
+    --cov-report=html:coverage_reports/coverage_html_report \
+    --cov-report=xml:coverage_reports/coverage_xml_report.xml

mythril/analysis/modules/suicide.py

@@ -1,9 +1,7 @@
-from z3 import *
 from mythril.analysis import solver
 from mythril.analysis.ops import *
 from mythril.analysis.report import Issue
 from mythril.exceptions import UnsatError
-import re
 import logging
 
 
@@ -15,86 +13,59 @@ Check for SUICIDE instructions that either can be reached by anyone, or where ms
 '''
 
 
-def execute(statespace):
+def execute(state_space):
 
     logging.debug("Executing module: UNCHECKED_SUICIDE")
 
     issues = []
 
-    for k in statespace.nodes:
+    for k in state_space.nodes:
-        node = statespace.nodes[k]
+        node = state_space.nodes[k]
 
         for state in node.states:
+            issues += _analyze_state(state, node)
 
-            instruction = state.get_current_instruction()
+    return issues
-
-            if(instruction['opcode'] == "SUICIDE"):
-
-                logging.debug("[UNCHECKED_SUICIDE] suicide in function " + node.function_name)
-
-                description = "The function `" + node.function_name + "` executes the SUICIDE instruction. "
-
-                stack = copy.deepcopy(state.mstate.stack)
-                to = stack.pop()
-
-                if ("caller" in str(to)):
-                    description += "The remaining Ether is sent to the caller's address.\n"
-                elif ("storage" in str(to)):
-                    description += "The remaining Ether is sent to a stored address.\n"
-                elif ("calldata" in str(to)):
-                    description += "The remaining Ether is sent to an address provided as a function argument.\n"
-                elif (type(to) == BitVecNumRef):
-                    description += "The remaining Ether is sent to: " + hex(to.as_long()) + "\n"
-                else:
-                    description += "The remaining Ether is sent to: " + str(to) + "\n"
-
-                constrained = False
-                can_solve = True
-
-                index = 0
-
-                while(can_solve and index < len(node.constraints)):
-
-                    constraint = node.constraints[index]
-                    index += 1
-
-                    m = re.search(r'storage_([a-z0-9_&^]+)', str(constraint))
-
-                    if (m):
-                        constrained = True
-                        idx = m.group(1)
-
-                        logging.debug("STORAGE CONSTRAINT FOUND: " + idx)
-
-                        func = statespace.find_storage_write(state.environment.active_account.address, idx)
-
-                        if func:
-                            description += "\nThere is a check on storage index " + str(idx) + ". This storage index can be written to by calling the function `" + func + "`."
-                            break
-                        else:
-                            logging.debug("[UNCHECKED_SUICIDE] No storage writes to index " + str(idx))
-                            can_solve = False
-                            break
-
-                    elif (re.search(r"caller", str(constraint)) and re.search(r'[0-9]{20}', str(constraint))):
-                        can_solve = False
-                        break
-
-                if not constrained:
-                    description += "\nIt seems that this function can be called without restrictions."
-
-                if can_solve:
-
-                    try:
-
-                        model = solver.get_model(node.constraints)
-
-                        debug = "SOLVER OUTPUT:\n" + solver.pretty_print_model(model)
 
-                        issue = Issue(node.contract_name, node.function_name, instruction['address'], "Unchecked SUICIDE", "Warning", description, debug)
-                        issues.append(issue)
 
-                    except UnsatError:
+def _analyze_state(state, node):
-                            logging.debug("[UNCHECKED_SUICIDE] no model found")
+    issues = []
+    instruction = state.get_current_instruction()
+
+    if instruction['opcode'] != "SUICIDE":
+        return []
+
+    to = state.mstate.stack[-1]
+
+    logging.debug("[UNCHECKED_SUICIDE] suicide in function " + node.function_name)
+    description = "The function `" + node.function_name + "` executes the SUICIDE instruction. "
+
+    if "caller" in str(to):
+        description += "The remaining Ether is sent to the caller's address.\n"
+    elif "storage" in str(to):
+        description += "The remaining Ether is sent to a stored address.\n"
+    elif "calldata" in str(to):
+        description += "The remaining Ether is sent to an address provided as a function argument.\n"
+    elif type(to) == BitVecNumRef:
+        description += "The remaining Ether is sent to: " + hex(to.as_long()) + "\n"
+    else:
+        description += "The remaining Ether is sent to: " + str(to) + "\n"
+
+    not_creator_constraints = []
+    if len(state.world_state.transaction_sequence) > 1:
+        creator = state.world_state.transaction_sequence[0].caller
+        for transaction in state.world_state.transaction_sequence[1:]:
+            not_creator_constraints.append(Not(Extract(159, 0, transaction.caller) == Extract(159, 0, creator)))
+            not_creator_constraints.append(Not(Extract(159, 0, transaction.caller) == 0))
+
+    try:
+        model = solver.get_model(node.constraints + not_creator_constraints)
+
+        debug = "SOLVER OUTPUT:\n" + solver.pretty_print_model(model)
+
+        issue = Issue(node.contract_name, node.function_name, instruction['address'], "Unchecked SUICIDE", "Warning", description, debug)
+        issues.append(issue)
+    except UnsatError:
+            logging.debug("[UNCHECKED_SUICIDE] no model found")
 
     return issues

mythril/analysis/report.py

@@ -35,7 +35,7 @@ class Issue:
 
     def add_code_info(self, contract):
         if self.address:
-            codeinfo = contract.get_source_info(self.address)
+            codeinfo = contract.get_source_info(self.address, constructor=(self.function == 'constructor'))
             self.filename = codeinfo.filename
             self.code = codeinfo.code
             self.lineno = codeinfo.lineno

mythril/analysis/templates/callgraph.html

@@ -8,6 +8,7 @@
     {% if not phrackify %}
     <style type="text/css">
         #mynetwork {
+          height: 100%;
             background-color: #232625;
         }
         body {
@@ -15,10 +16,14 @@
             color: #ffffff;
             font-size: 10px;
         }
+        html, body {
+          height: 95%;
+        }
     </style>
     {% else %}
     <style type="text/css">
         #mynetwork {
+            height: 100%;
             background-color: #ffffff;
         }
         body {
@@ -27,6 +32,9 @@
             font-size: 10px;
             font-family: "courier new";
         }
+        html, body {
+          height: 95%;
+        }
     </style>
     {% endif %}
 
@@ -38,7 +46,7 @@
 </head>
 <body>
 <p>{{ title }}</p>
-<p><div id="mynetwork"></div><br/></p>
+<div id="mynetwork"></div>
 <script type="text/javascript">
     var container = document.getElementById('mynetwork');
 

mythril/ether/ethcontract.py

@@ -17,7 +17,8 @@ class ETHContract(persistent.Persistent):
         code = re.sub(r'(_+.*_+)', 'aa' * 20, code)
 
         self.code = code
-        self.disassembly = Disassembly(self.code, enable_online_lookup=enable_online_lookup)
+        self.disassembly = Disassembly(code, enable_online_lookup=enable_online_lookup)
+        self.creation_disassembly = Disassembly(creation_code, enable_online_lookup=enable_online_lookup)
 
     def as_dict(self):
 

mythril/ether/soliditycontract.py

@@ -52,7 +52,8 @@ class SolidityContract(ETHContract):
         has_contract = False
 
         # If a contract name has been specified, find the bytecode of that specific contract
-
+        srcmap_constructor = []
+        srcmap = []
         if name:
             for key, contract in sorted(data['contracts'].items()):
                 filename, _name = key.split(":")
@@ -61,6 +62,7 @@ class SolidityContract(ETHContract):
                     code = contract['bin-runtime']
                     creation_code = contract['bin']
                     srcmap = contract['srcmap-runtime'].split(";")
+                    srcmap_constructor = contract['srcmap'].split(";")
                     has_contract = True
                     break
 
@@ -74,6 +76,7 @@ class SolidityContract(ETHContract):
                     code = contract['bin-runtime']
                     creation_code = contract['bin']
                     srcmap = contract['srcmap-runtime'].split(";")
+                    srcmap_constructor = contract['srcmap'].split(";")
                     has_contract = True
 
         if not has_contract:
@@ -81,6 +84,31 @@ class SolidityContract(ETHContract):
 
         self.mappings = []
 
+        self.constructor_mappings = []
+
+        self._get_solc_mappings(srcmap)
+        self._get_solc_mappings(srcmap_constructor, constructor=True)
+
+        super().__init__(code, creation_code, name=name)
+
+    def get_source_info(self, address, constructor=False):
+        disassembly = self.creation_disassembly if constructor else self.disassembly
+        mappings = self.constructor_mappings if constructor else self.mappings
+        index = helper.get_instruction_index(disassembly.instruction_list, address)
+        solidity_file = self.solidity_files[mappings[index].solidity_file_idx]
+
+        filename = solidity_file.filename
+
+        offset = mappings[index].offset
+        length = mappings[index].length
+
+        code = solidity_file.data.encode('utf-8')[offset:offset + length].decode('utf-8', errors="ignore")
+        lineno = mappings[index].lineno
+
+        return SourceCodeInfo(filename, lineno, code)
+
+    def _get_solc_mappings(self, srcmap, constructor=False):
+        mappings = self.constructor_mappings if constructor else self.mappings
         for item in srcmap:
             mapping = item.split(":")
 
@@ -94,22 +122,4 @@ class SolidityContract(ETHContract):
                 idx = int(mapping[2])
             lineno = self.solidity_files[idx].data.encode('utf-8')[0:offset].count('\n'.encode('utf-8')) + 1
 
-            self.mappings.append(SourceMapping(idx, offset, length, lineno))
+            mappings.append(SourceMapping(idx, offset, length, lineno))
-
-        super().__init__(code, creation_code, name=name)
-
-    def get_source_info(self, address):
-
-        index = helper.get_instruction_index(self.disassembly.instruction_list, address)
-
-        solidity_file = self.solidity_files[self.mappings[index].solidity_file_idx]
-
-        filename = solidity_file.filename
-
-        offset = self.mappings[index].offset
-        length = self.mappings[index].length
-
-        code = solidity_file.data.encode('utf-8')[offset:offset + length].decode('utf-8')
-        lineno = self.mappings[index].lineno
-
-        return SourceCodeInfo(filename, lineno, code)

mythril/ether/util.py

@@ -18,7 +18,7 @@ def safe_decode(hex_encoded_string):
 
 def get_solc_json(file, solc_binary="solc", solc_args=None):
 
-    cmd = [solc_binary, "--combined-json", "bin,bin-runtime,srcmap-runtime", '--allow-paths', "."]
+    cmd = [solc_binary, "--combined-json", "bin,bin-runtime,srcmap,srcmap-runtime", '--allow-paths', "."]
 
     if solc_args:
         cmd.extend(solc_args.split(" "))

mythril/laser/ethereum/instructions.py

@@ -3,9 +3,8 @@ import logging
 from copy import copy, deepcopy
 
 from ethereum import utils
-from z3 import BitVec, Extract, UDiv, simplify, Concat, ULT, UGT, BitVecNumRef, Not, \
+from z3 import Extract, UDiv, simplify, Concat, ULT, UGT, BitVecNumRef, Not, \
-    is_false, is_expr, ExprRef, URem, SRem
+    is_false, is_expr, ExprRef, URem, SRem, BitVec, Solver, is_true, BitVecVal, If, BoolRef, Or
-from z3 import BitVecVal, If, BoolRef
 
 import mythril.laser.ethereum.util as helper
 from mythril.laser.ethereum import util
@@ -15,10 +14,13 @@ import mythril.laser.ethereum.natives as natives
 from mythril.laser.ethereum.transaction import MessageCallTransaction, TransactionStartSignal, \
     ContractCreationTransaction
 from mythril.laser.ethereum.exceptions import VmException, StackUnderflowException
+from mythril.laser.ethereum.keccak import KeccakFunctionManager
 
 TT256 = 2 ** 256
 TT256M1 = 2 ** 256 - 1
 
+keccak_function_manager = KeccakFunctionManager()
+
 
 def instruction(func):
     """ Wrapper that handles copy and original return """
@@ -166,7 +168,7 @@ class Instruction:
                 result = 0
         except AttributeError:
             logging.debug("BYTE: Unsupported symbolic byte offset")
-            result = BitVec(str(simplify(op1)) + "[" + str(simplify(op0)) + "]", 256)
+            result = global_state.new_bitvec(str(simplify(op1)) + "[" + str(simplify(op0)) + "]", 256)
 
         mstate.stack.append(result)
         return [global_state]
@@ -240,7 +242,7 @@ class Instruction:
 
         base, exponent = util.pop_bitvec(state), util.pop_bitvec(state)
         if (type(base) != BitVecNumRef) or (type(exponent) != BitVecNumRef):
-            state.stack.append(BitVec("(" + str(simplify(base)) + ")**(" + str(simplify(exponent)) + ")", 256))
+            state.stack.append(global_state.new_bitvec("(" + str(simplify(base)) + ")**(" + str(simplify(exponent)) + ")", 256))
         else:
             state.stack.append(pow(base.as_long(), exponent.as_long(), 2**256))
 
@@ -347,12 +349,12 @@ class Instruction:
             b = environment.calldata[offset]
         except AttributeError:
             logging.debug("CALLDATALOAD: Unsupported symbolic index")
-            state.stack.append(BitVec(
+            state.stack.append(global_state.new_bitvec(
                 "calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256))
             return [global_state]
         except IndexError:
             logging.debug("Calldata not set, using symbolic variable instead")
-            state.stack.append(BitVec(
+            state.stack.append(global_state.new_bitvec(
                 "calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256))
             return [global_state]
 
@@ -367,11 +369,11 @@ class Instruction:
                 state.stack.append(BitVecVal(int.from_bytes(val, byteorder='big'), 256))
             # FIXME: broad exception catch
             except:
-                state.stack.append(BitVec(
+                state.stack.append(global_state.new_bitvec(
                     "calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256))
         else:
             # symbolic variable
-            state.stack.append(BitVec(
+            state.stack.append(global_state.new_bitvec(
                 "calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256))
 
         return [global_state]
@@ -381,7 +383,7 @@ class Instruction:
         state = global_state.mstate
         environment = global_state.environment
         if environment.calldata_type == CalldataType.SYMBOLIC:
-            state.stack.append(BitVec("calldatasize_" + environment.active_account.contract_name, 256))
+            state.stack.append(global_state.new_bitvec("calldatasize_" + environment.active_account.contract_name, 256))
         else:
             state.stack.append(BitVecVal(len(environment.calldata), 256))
         return [global_state]
@@ -419,7 +421,7 @@ class Instruction:
 
         if dstart_sym or size_sym:
             state.mem_extend(mstart, 1)
-            state.memory[mstart] = BitVec(
+            state.memory[mstart] = global_state.new_bitvec(
                 "calldata_" + str(environment.active_account.contract_name) + "[" + str(dstart) + ": + " + str(
                     size) + "]", 256)
             return [global_state]
@@ -431,7 +433,7 @@ class Instruction:
             except:
                 logging.debug("Memory allocation error: mstart = " + str(mstart) + ", size = " + str(size))
                 state.mem_extend(mstart, 1)
-                state.memory[mstart] = BitVec(
+                state.memory[mstart] = global_state.new_bitvec(
                     "calldata_" + str(environment.active_account.contract_name) + "[" + str(dstart) + ": + " + str(
                         size) + "]", 256)
                 return [global_state]
@@ -445,7 +447,7 @@ class Instruction:
             except:
                 logging.debug("Exception copying calldata to memory")
 
-                state.memory[mstart] = BitVec(
+                state.memory[mstart] = global_state.new_bitvec(
                     "calldata_" + str(environment.active_account.contract_name) + "[" + str(dstart) + ": + " + str(
                         size) + "]", 256)
         return [global_state]
@@ -462,7 +464,7 @@ class Instruction:
     def balance_(self, global_state):
         state = global_state.mstate
         address = state.stack.pop()
-        state.stack.append(BitVec("balance_at_" + str(address), 256))
+        state.stack.append(global_state.new_bitvec("balance_at_" + str(address), 256))
         return [global_state]
 
     @instruction
@@ -489,6 +491,8 @@ class Instruction:
 
     @instruction
     def sha3_(self, global_state):
+        global keccak_function_manager
+
         state = global_state.mstate
         environment = global_state.environment
         op0, op1 = state.stack.pop(), state.stack.pop()
@@ -509,23 +513,22 @@ class Instruction:
                              for i in state.memory[index: index + length]])
 
         except AttributeError:
+            argument = str(state.memory[index]).replace(" ", "_")
 
-            svar = str(state.memory[index])
+            result = BitVec("KECCAC[{}]".format(argument), 256)
-
+            keccak_function_manager.add_keccak(result, state.memory[index])
-            svar = svar.replace(" ", "_")
+            state.stack.append(result)
-
-            state.stack.append(BitVec("keccac_" + svar, 256))
             return [global_state]
 
-        keccac = utils.sha3(utils.bytearray_to_bytestr(data))
+        keccak = utils.sha3(utils.bytearray_to_bytestr(data))
-        logging.debug("Computed SHA3 Hash: " + str(binascii.hexlify(keccac)))
+        logging.debug("Computed SHA3 Hash: " + str(binascii.hexlify(keccak)))
 
-        state.stack.append(BitVecVal(util.concrete_int_from_bytes(keccac, 0), 256))
+        state.stack.append(BitVecVal(util.concrete_int_from_bytes(keccak, 0), 256))
         return [global_state]
 
     @instruction
     def gasprice_(self, global_state):
-        global_state.mstate.stack.append(BitVec("gasprice", 256))
+        global_state.mstate.stack.append(global_state.new_bitvec("gasprice", 256))
         return [global_state]
 
     @instruction
@@ -545,7 +548,7 @@ class Instruction:
             # except both attribute error and Exception
             global_state.mstate.mem_extend(concrete_memory_offset, 1)
             global_state.mstate.memory[concrete_memory_offset] = \
-                BitVec("code({})".format(global_state.environment.active_account.contract_name), 256)
+                global_state.new_bitvec("code({})".format(global_state.environment.active_account.contract_name), 256)
             return [global_state]
 
         try:
@@ -555,7 +558,7 @@ class Instruction:
             global_state.mstate.mem_extend(concrete_memory_offset, concrete_size)
             for i in range(concrete_size):
                 global_state.mstate.memory[concrete_memory_offset + i] = \
-                    BitVec("code({})".format(global_state.environment.active_account.contract_name), 256)
+                    global_state.new_bitvec("code({})".format(global_state.environment.active_account.contract_name), 256)
             return [global_state]
 
         bytecode = global_state.environment.code.bytecode
@@ -564,7 +567,7 @@ class Instruction:
             if concrete_code_offset >= len(global_state.environment.code.bytecode) // 2:
                 global_state.mstate.mem_extend(concrete_memory_offset, 1)
                 global_state.mstate.memory[concrete_memory_offset] = \
-                    BitVec("code({})".format(global_state.environment.active_account.contract_name), 256)
+                    global_state.new_bitvec("code({})".format(global_state.environment.active_account.contract_name), 256)
                 return [global_state]
 
         for i in range(concrete_size):
@@ -573,7 +576,7 @@ class Instruction:
                     int(bytecode[2*(concrete_code_offset + i): 2*(concrete_code_offset + i + 1)], 16)
             else:
                 global_state.mstate.memory[concrete_memory_offset + i] = \
-                    BitVec("code({})".format(global_state.environment.active_account.contract_name), 256)
+                    global_state.new_bitvec("code({})".format(global_state.environment.active_account.contract_name), 256)
 
         return [global_state]
 
@@ -586,14 +589,14 @@ class Instruction:
             addr = hex(helper.get_concrete_int(addr))
         except AttributeError:
             logging.info("unsupported symbolic address for EXTCODESIZE")
-            state.stack.append(BitVec("extcodesize_" + str(addr), 256))
+            state.stack.append(global_state.new_bitvec("extcodesize_" + str(addr), 256))
             return [global_state]
 
         try:
             code = self.dynamic_loader.dynld(environment.active_account.address, addr)
         except Exception as e:
             logging.info("error accessing contract storage due to: " + str(e))
-            state.stack.append(BitVec("extcodesize_" + str(addr), 256))
+            state.stack.append(global_state.new_bitvec("extcodesize_" + str(addr), 256))
             return [global_state]
 
         if code is None:
@@ -613,39 +616,39 @@ class Instruction:
 
     @instruction
     def returndatasize_(self, global_state):
-        global_state.mstate.stack.append(BitVec("returndatasize", 256))
+        global_state.mstate.stack.append(global_state.new_bitvec("returndatasize", 256))
         return [global_state]
 
     @instruction
     def blockhash_(self, global_state):
         state = global_state.mstate
         blocknumber = state.stack.pop()
-        state.stack.append(BitVec("blockhash_block_" + str(blocknumber), 256))
+        state.stack.append(global_state.new_bitvec("blockhash_block_" + str(blocknumber), 256))
         return [global_state]
 
     @instruction
     def coinbase_(self, global_state):
-        global_state.mstate.stack.append(BitVec("coinbase", 256))
+        global_state.mstate.stack.append(global_state.new_bitvec("coinbase", 256))
         return [global_state]
 
     @instruction
     def timestamp_(self, global_state):
-        global_state.mstate.stack.append(BitVec("timestamp", 256))
+        global_state.mstate.stack.append(global_state.new_bitvec("timestamp", 256))
         return [global_state]
 
     @instruction
     def number_(self, global_state):
-        global_state.mstate.stack.append(BitVec("block_number", 256))
+        global_state.mstate.stack.append(global_state.new_bitvec("block_number", 256))
         return [global_state]
 
     @instruction
     def difficulty_(self, global_state):
-        global_state.mstate.stack.append(BitVec("block_difficulty", 256))
+        global_state.mstate.stack.append(global_state.new_bitvec("block_difficulty", 256))
         return [global_state]
 
     @instruction
     def gaslimit_(self, global_state):
-        global_state.mstate.stack.append(BitVec("block_gaslimit", 256))
+        global_state.mstate.stack.append(global_state.new_bitvec("block_gaslimit", 256))
         return [global_state]
 
     # Memory operations
@@ -660,14 +663,14 @@ class Instruction:
             offset = util.get_concrete_int(op0)
         except AttributeError:
             logging.debug("Can't MLOAD from symbolic index")
-            data = BitVec("mem[" + str(simplify(op0)) + "]", 256)
+            data = global_state.new_bitvec("mem[" + str(simplify(op0)) + "]", 256)
             state.stack.append(data)
             return [global_state]
 
         try:
             data = util.concrete_int_from_bytes(state.memory, offset)
         except IndexError:  # Memory slot not allocated
-            data = BitVec("mem[" + str(offset) + "]", 256)
+            data = global_state.new_bitvec("mem[" + str(offset) + "]", 256)
         except TypeError:  # Symbolic memory
             data = state.memory[offset]
 
@@ -732,26 +735,68 @@ class Instruction:
 
     @instruction
     def sload_(self, global_state):
+        global keccak_function_manager
+        
         state = global_state.mstate
         index = state.stack.pop()
         logging.debug("Storage access at index " + str(index))
 
         try:
             index = util.get_concrete_int(index)
-        except AttributeError:
+            return self._sload_helper(global_state, index)
-            index = str(index)
 
+        except AttributeError:
+            if not keccak_function_manager.is_keccak(index):
+                return self._sload_helper(global_state, str(index))
+
+            storage_keys = global_state.environment.active_account.storage.keys()
+            keccak_keys = list(filter(keccak_function_manager.is_keccak, storage_keys))
+
+            results = []
+            constraints = []
+
+            for keccak_key in keccak_keys:
+                key_argument = keccak_function_manager.get_argument(keccak_key)
+                index_argument = keccak_function_manager.get_argument(index)
+                constraints.append((keccak_key, key_argument == index_argument))
+
+            for (keccak_key, constraint) in constraints:
+                if constraint in state.constraints:
+                    results += self._sload_helper(global_state, keccak_key, [constraint])
+            if len(results) > 0:
+                return results
+
+            for (keccak_key, constraint) in constraints:
+                results += self._sload_helper(copy(global_state), keccak_key, [constraint])
+            if len(results) > 0:
+                return results
+            
+            return self._sload_helper(global_state, str(index))
+
+    def _sload_helper(self, global_state, index, constraints=None):
         try:
             data = global_state.environment.active_account.storage[index]
         except KeyError:
-            data = BitVec("storage_" + str(index), 256)
+            data = global_state.new_bitvec("storage_" + str(index), 256)
             global_state.environment.active_account.storage[index] = data
 
-        state.stack.append(data)
+        if constraints is not None:
+            global_state.mstate.constraints += constraints
+
+        global_state.mstate.stack.append(data)
         return [global_state]
 
+    def _get_constraints(self, keccak_keys, this_key, argument):
+        global keccak_function_manager
+        for keccak_key in keccak_keys:
+            if keccak_key == this_key:
+                continue
+            keccak_argument = keccak_function_manager.get_argument(keccak_key)
+            yield keccak_argument != argument
+
     @instruction
     def sstore_(self, global_state):
+        global keccak_function_manager
         state = global_state.mstate
         index, value = state.stack.pop(), state.stack.pop()
 
@@ -759,17 +804,52 @@ class Instruction:
 
         try:
             index = util.get_concrete_int(index)
+            return self._sstore_helper(global_state, index, value)
         except AttributeError:
-            index = str(index)
+            is_keccak = keccak_function_manager.is_keccak(index)
+            if not is_keccak:
+                return self._sstore_helper(global_state, str(index), value)
+
+            storage_keys = global_state.environment.active_account.storage.keys()
+            keccak_keys = filter(keccak_function_manager.is_keccak, storage_keys)
+
+            solver = Solver()
+            solver.set(timeout=1000)
+
+            results = []
+            new = False
 
+            for keccak_key in keccak_keys:
+                key_argument = keccak_function_manager.get_argument(keccak_key)
+                index_argument = keccak_function_manager.get_argument(index)
+
+                if is_true(key_argument == index_argument):
+                    return self._sstore_helper(copy(global_state), keccak_key, value, key_argument == index_argument)
+
+                results += self._sstore_helper(copy(global_state), keccak_key, value, key_argument == index_argument)
+
+                new = Or(new, key_argument != index_argument)
+
+            if len(results) > 0:
+                results += self._sstore_helper(copy(global_state), str(index), value, new)
+                return results
+
+            return self._sstore_helper(global_state, str(index), value)
+
+    def _sstore_helper(self, global_state, index, value, constraint=None):
         try:
             global_state.environment.active_account = deepcopy(global_state.environment.active_account)
             global_state.accounts[
                 global_state.environment.active_account.address] = global_state.environment.active_account
 
-            global_state.environment.active_account.storage[index] = value
+            global_state.environment.active_account.storage[index] =\
+                value if not isinstance(value, ExprRef) else simplify(value)
         except KeyError:
             logging.debug("Error writing to storage: Invalid index")
+
+        if constraint is not None:
+            global_state.mstate.constraints.append(constraint)
+
         return [global_state]
 
     @instruction
@@ -858,12 +938,12 @@ class Instruction:
 
     @instruction
     def msize_(self, global_state):
-        global_state.mstate.stack.append(BitVec("msize", 256))
+        global_state.mstate.stack.append(global_state.new_bitvec("msize", 256))
         return [global_state]
 
     @instruction
     def gas_(self, global_state):
-        global_state.mstate.stack.append(BitVec("gas", 256))
+        global_state.mstate.stack.append(global_state.new_bitvec("gas", 256))
         return [global_state]
 
     @instruction
@@ -889,7 +969,7 @@ class Instruction:
     def return_(self, global_state):
         state = global_state.mstate
         offset, length = state.stack.pop(), state.stack.pop()
-        return_data = [BitVec("return_data", 256)]
+        return_data = [global_state.new_bitvec("return_data", 256)]
         try:
             return_data = state.memory[util.get_concrete_int(offset):util.get_concrete_int(offset + length)]
         except AttributeError:
@@ -930,9 +1010,9 @@ class Instruction:
                 "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e)
             )
             # TODO: decide what to do in this case
-            global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
+            global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
             return [global_state]
-        global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
+        global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
 
         if 0 < int(callee_address, 16) < 5:
             logging.info("Native contract called: " + callee_address)
@@ -954,7 +1034,7 @@ class Instruction:
             except natives.NativeContractException:
                 contract_list = ['ecerecover', 'sha256', 'ripemd160', 'identity']
                 for i in range(mem_out_sz):
-                    global_state.mstate.memory[mem_out_start + i] = BitVec(contract_list[call_address_int - 1] +
+                    global_state.mstate.memory[mem_out_start + i] = global_state.new_bitvec(contract_list[call_address_int - 1] +
                                                                            "(" + str(call_data) + ")", 256)
 
                 return [global_state]
@@ -968,11 +1048,11 @@ class Instruction:
         transaction = MessageCallTransaction(global_state.world_state,
                                              callee_account,
                                              BitVecVal(int(environment.active_account.address, 16), 256),
-                                             call_data,
+                                             call_data=call_data,
-                                             environment.gasprice,
+                                             gas_price=environment.gasprice,
-                                             value,
+                                             call_value=value,
-                                             environment.origin,
+                                             origin=environment.origin,
-                                             call_data_type)
+                                             call_data_type=call_data_type)
         raise TransactionStartSignal(transaction, self.op_code)
 
     @instruction
@@ -986,12 +1066,12 @@ class Instruction:
             logging.info(
                 "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e)
             )
-            global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
+            global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
             return [global_state]
 
         if global_state.last_return_data is None:
             # Put return value on stack
-            return_value = BitVec("retval_" + str(instr['address']), 256)
+            return_value = global_state.new_bitvec("retval_" + str(instr['address']), 256)
             global_state.mstate.stack.append(return_value)
             global_state.mstate.constraints.append(return_value == 0)
 
@@ -1001,7 +1081,7 @@ class Instruction:
             memory_out_offset = util.get_concrete_int(memory_out_offset) if isinstance(memory_out_offset, ExprRef) else memory_out_offset
             memory_out_size = util.get_concrete_int(memory_out_size) if isinstance(memory_out_size, ExprRef) else memory_out_size
         except AttributeError:
-            global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
+            global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
             return [global_state]
 
         # Copy memory
@@ -1010,7 +1090,7 @@ class Instruction:
             global_state.mstate.memory[i + memory_out_offset] = global_state.last_return_data[i]
 
         # Put return value on stack
-        return_value = BitVec("retval_" + str(instr['address']), 256)
+        return_value = global_state.new_bitvec("retval_" + str(instr['address']), 256)
         global_state.mstate.stack.append(return_value)
         global_state.mstate.constraints.append(return_value == 1)
 
@@ -1028,18 +1108,18 @@ class Instruction:
             logging.info(
                 "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e)
             )
-            global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
+            global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
             return [global_state]
 
         transaction = MessageCallTransaction(global_state.world_state,
                                              environment.active_account,
                                              environment.address,
-                                             call_data,
+                                             call_data=call_data,
-                                             environment.gasprice,
+                                             gas_price=environment.gasprice,
-                                             value,
+                                             call_value=value,
-                                             environment.origin,
+                                             origin=environment.origin,
-                                             call_data_type,
+                                             call_data_type=call_data_type,
-                                             callee_account.code
+                                             code=callee_account.code
                                              )
         raise TransactionStartSignal(transaction, self.op_code)
 
@@ -1054,12 +1134,12 @@ class Instruction:
             logging.info(
                 "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e)
             )
-            global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
+            global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
             return [global_state]
 
         if global_state.last_return_data is None:
             # Put return value on stack
-            return_value = BitVec("retval_" + str(instr['address']), 256)
+            return_value = global_state.new_bitvec("retval_" + str(instr['address']), 256)
             global_state.mstate.stack.append(return_value)
             global_state.mstate.constraints.append(return_value == 0)
 
@@ -1069,7 +1149,7 @@ class Instruction:
             memory_out_offset = util.get_concrete_int(memory_out_offset) if isinstance(memory_out_offset, ExprRef) else memory_out_offset
             memory_out_size = util.get_concrete_int(memory_out_size) if isinstance(memory_out_size, ExprRef) else memory_out_size
         except AttributeError:
-            global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
+            global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
             return [global_state]
 
         # Copy memory
@@ -1078,7 +1158,7 @@ class Instruction:
             global_state.mstate.memory[i + memory_out_offset] = global_state.last_return_data[i]
 
         # Put return value on stack
-        return_value = BitVec("retval_" + str(instr['address']), 256)
+        return_value = global_state.new_bitvec("retval_" + str(instr['address']), 256)
         global_state.mstate.stack.append(return_value)
         global_state.mstate.constraints.append(return_value == 1)
 
@@ -1097,18 +1177,18 @@ class Instruction:
             logging.info(
                 "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e)
             )
-            global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
+            global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
             return [global_state]
 
         transaction = MessageCallTransaction(global_state.world_state,
                                              environment.active_account,
                                              environment.sender,
                                              call_data,
-                                             environment.gasprice,
+                                             gas_price=environment.gasprice,
-                                             environment.callvalue,
+                                             call_value=environment.callvalue,
-                                             environment.origin,
+                                             origin=environment.origin,
-                                             call_data_type,
+                                             call_data_type=call_data_type,
-                                             callee_account.code
+                                             code=callee_account.code
                                              )
         raise TransactionStartSignal(transaction, self.op_code)
 
@@ -1124,12 +1204,12 @@ class Instruction:
             logging.info(
                 "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e)
             )
-            global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
+            global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
             return [global_state]
 
         if global_state.last_return_data is None:
             # Put return value on stack
-            return_value = BitVec("retval_" + str(instr['address']), 256)
+            return_value = global_state.new_bitvec("retval_" + str(instr['address']), 256)
             global_state.mstate.stack.append(return_value)
             global_state.mstate.constraints.append(return_value == 0)
 
@@ -1141,7 +1221,7 @@ class Instruction:
             memory_out_size = util.get_concrete_int(memory_out_size) if isinstance(memory_out_size,
                                                                                    ExprRef) else memory_out_size
         except AttributeError:
-            global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
+            global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
             return [global_state]
 
             # Copy memory
@@ -1151,7 +1231,7 @@ class Instruction:
             global_state.mstate.memory[i + memory_out_offset] = global_state.last_return_data[i]
 
         # Put return value on stack
-        return_value = BitVec("retval_" + str(instr['address']), 256)
+        return_value = global_state.new_bitvec("retval_" + str(instr['address']), 256)
         global_state.mstate.stack.append(return_value)
         global_state.mstate.constraints.append(return_value == 1)
 
@@ -1161,5 +1241,6 @@ class Instruction:
     def staticcall_(self, global_state):
         # TODO: implement me
         instr = global_state.get_current_instruction()
-        global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
+        global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
         return [global_state]
+

mythril/laser/ethereum/keccak.py

@@ -0,0 +1,17 @@
+from z3 import ExprRef
+
+class KeccakFunctionManager:
+    def __init__(self):
+        self.keccak_expression_mapping = {}
+
+    def is_keccak(self, expression) -> bool:
+        return str(expression) in self.keccak_expression_mapping.keys()
+
+    def get_argument(self, expression) -> ExprRef:
+        if not self.is_keccak(expression):
+            raise ValueError("Expression is not a recognized keccac result")
+        return self.keccak_expression_mapping[str(expression)][1]
+
+    def add_keccak(self, expression: ExprRef, argument: ExprRef):
+        index = str(expression)
+        self.keccak_expression_mapping[index] = (expression, argument)

mythril/laser/ethereum/state.py

@@ -1,4 +1,4 @@
-from z3 import BitVec, BitVecVal
+from z3 import BitVec, BitVecVal, Solver, ExprRef, sat
 from copy import copy, deepcopy
 from enum import Enum
 from random import randint
@@ -41,6 +41,8 @@ class Storage:
     def __setitem__(self, key, value):
         self._storage[key] = value
 
+    def keys(self):
+        return self._storage.keys()
 
 class Account:
     """
@@ -217,17 +219,23 @@ class GlobalState:
     def instruction(self):
         return self.get_current_instruction()
 
+    def new_bitvec(self, name, size=256):
+        transaction_id = self.current_transaction.id
+        node_id = self.node.uid
+
+        return BitVec("{}_{}".format(transaction_id, name), size)
 
 class WorldState:
     """
     The WorldState class represents the world state as described in the yellow paper
     """
-    def __init__(self):
+    def __init__(self, transaction_sequence=None):
         """
         Constructor for the world state. Initializes the accounts record
         """
         self.accounts = {}
         self.node = None
+        self.transaction_sequence = transaction_sequence or []
 
     def __getitem__(self, item):
         """
@@ -238,7 +246,7 @@ class WorldState:
         return self.accounts[item]
 
     def __copy__(self):
-        new_world_state = WorldState()
+        new_world_state = WorldState(transaction_sequence=self.transaction_sequence[:])
         new_world_state.accounts = copy(self.accounts)
         new_world_state.node = self.node
         return new_world_state

mythril/laser/ethereum/svm.py

@@ -181,6 +181,10 @@ class LaserEVM:
         elif opcode == "JUMPI":
             for state in new_states:
                 self._new_node_state(state, JumpType.CONDITIONAL, state.mstate.constraints[-1])
+        elif opcode in ("SLOAD", "SSTORE") and len(new_states) > 1:
+            for state in new_states:
+                self._new_node_state(state, JumpType.CONDITIONAL, state.mstate.constraints[-1])
+
         elif opcode in ("CALL", 'CALLCODE', 'DELEGATECALL', 'STATICCALL'):
             assert len(new_states) <= 1
             for state in new_states:

mythril/laser/ethereum/transaction/concolic.py

@@ -1,4 +1,4 @@
-from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction, ContractCreationTransaction
+from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction, ContractCreationTransaction, get_next_transaction_id
 from z3 import BitVec
 from mythril.laser.ethereum.state import GlobalState, Environment, CalldataType, Account, WorldState
 from mythril.disassembler.disassembly import Disassembly
@@ -12,6 +12,7 @@ def execute_message_call(laser_evm, callee_address, caller_address, origin_addre
 
     for open_world_state in open_states:
         transaction = MessageCallTransaction(
+            identifier=get_next_transaction_id(),
             world_state=open_world_state,
             callee_account=open_world_state[callee_address],
             caller=caller_address,

mythril/laser/ethereum/transaction/symbolic.py

@@ -1,8 +1,10 @@
-from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction, ContractCreationTransaction
+from z3 import BitVec, Extract, Not
-from z3 import BitVec
+
-from mythril.laser.ethereum.state import CalldataType
 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.ethereum.cfg import Node, Edge, JumpType
+from mythril.laser.ethereum.state import CalldataType
+from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction, ContractCreationTransaction,\
+    get_next_transaction_id
 
 
 def execute_message_call(laser_evm, callee_address):
@@ -11,15 +13,17 @@ def execute_message_call(laser_evm, callee_address):
     del laser_evm.open_states[:]
 
     for open_world_state in open_states:
+        next_transaction_id = get_next_transaction_id()
         transaction = MessageCallTransaction(
-            open_world_state,
+            world_state=open_world_state,
-            open_world_state[callee_address],
+            callee_account=open_world_state[callee_address],
-            BitVec("caller", 256),
+            caller=BitVec("caller{}".format(next_transaction_id), 256),
-            [],
+            identifier=next_transaction_id,
-            BitVec("gas_price", 256),
+            call_data=[],
-            BitVec("call_value", 256),
+            gas_price=BitVec("gas_price{}".format(next_transaction_id), 256),
-            BitVec("origin", 256),
+            call_value=BitVec("call_value{}".format(next_transaction_id), 256),
-            CalldataType.SYMBOLIC,
+            origin=BitVec("origin{}".format(next_transaction_id), 256),
+            call_data_type=CalldataType.SYMBOLIC,
         )
         _setup_global_state_for_execution(laser_evm, transaction)
 
@@ -36,18 +40,19 @@ def execute_contract_creation(laser_evm, contract_initialization_code, contract_
         new_account.contract_name = contract_name
 
     for open_world_state in open_states:
+        next_transaction_id = get_next_transaction_id()
         transaction = ContractCreationTransaction(
             open_world_state,
-            BitVec("caller", 256),
+            BitVec("creator{}".format(next_transaction_id), 256),
+            next_transaction_id,
             new_account,
             Disassembly(contract_initialization_code),
             [],
-            BitVec("gas_price", 256),
+            BitVec("gas_price{}".format(next_transaction_id), 256),
-            BitVec("call_value", 256),
+            BitVec("call_value{}".format(next_transaction_id), 256),
-            BitVec("origin", 256),
+            BitVec("origin{}".format(next_transaction_id), 256),
             CalldataType.SYMBOLIC
         )
-
         _setup_global_state_for_execution(laser_evm, transaction)
     laser_evm.exec(True)
 
@@ -69,6 +74,7 @@ def _setup_global_state_for_execution(laser_evm, transaction):
         global_state.mstate.constraints = transaction.world_state.node.constraints
         new_node.constraints = global_state.mstate.constraints
 
+    global_state.world_state.transaction_sequence.append(transaction)
     global_state.node = new_node
     new_node.states.append(global_state)
     laser_evm.work_list.append(global_state)

mythril/laser/ethereum/transaction/transaction_models.py

@@ -4,6 +4,13 @@ from mythril.laser.ethereum.state import GlobalState, Environment, WorldState
 from z3 import BitVec
 import array
 
+_next_transaction_id = 0
+
+
+def get_next_transaction_id():
+    global _next_transaction_id
+    _next_transaction_id += 1
+    return _next_transaction_id
 
 class TransactionEndSignal(Exception):
     """ Exception raised when a transaction is finalized"""
@@ -25,21 +32,23 @@ class MessageCallTransaction:
                  callee_account,
                  caller,
                  call_data=(),
-                 gas_price=BitVec("gasprice", 256),
+                 identifier=None,
-                 call_value=BitVec("callvalue", 256),
+                 gas_price=None,
-                 origin=BitVec("origin", 256),
+                 call_value=None,
-                 call_data_type=BitVec("call_data_type", 256),
+                 origin=None,
+                 call_data_type=None,
                  code=None
                  ):
         assert isinstance(world_state, WorldState)
+        self.id = identifier or get_next_transaction_id()
         self.world_state = world_state
         self.callee_account = callee_account
         self.caller = caller
         self.call_data = call_data
-        self.gas_price = gas_price
+        self.gas_price = BitVec("gasprice{}".format(identifier), 256) if gas_price is None else gas_price
-        self.call_value = call_value
+        self.call_value = BitVec("callvalue{}".format(identifier), 256) if call_value is None else call_value
-        self.origin = origin
+        self.origin = BitVec("origin{}".format(identifier), 256) if origin is None else origin
-        self.call_data_type = call_data_type
+        self.call_data_type = BitVec("call_data_type{}".format(identifier), 256) if call_data_type is None else call_data_type
         self.code = code
         self.return_data = None
 
@@ -71,27 +80,30 @@ class ContractCreationTransaction:
     def __init__(self,
                  world_state,
                  caller,
+                 identifier=None,
                  callee_account=None,
                  code=None,
                  call_data=(),
-                 gas_price=BitVec("gasprice", 256),
+                 gas_price=None,
-                 call_value=BitVec("callvalue", 256),
+                 call_value=None,
-                 origin=BitVec("origin", 256),
+                 origin=None,
-                 call_data_type=BitVec("call_data_type", 256),
+                 call_data_type=None,
                  ):
         assert isinstance(world_state, WorldState)
-
+        self.id = identifier or get_next_transaction_id()
         self.world_state = world_state
         # TODO: set correct balance for new account
         self.callee_account = callee_account if callee_account else world_state.create_account(0, concrete_storage=True)
 
         self.caller = caller
-        self.call_data = call_data
-        self.gas_price = gas_price
-        self.call_value = call_value
 
+        self.gas_price = BitVec("gasprice{}".format(identifier), 256) if gas_price is None else gas_price
+        self.call_value = BitVec("callvalue{}".format(identifier), 256) if call_value is None else call_value
+        self.origin = BitVec("origin{}".format(identifier), 256) if origin is None else origin
+        self.call_data_type = BitVec("call_data_type{}".format(identifier), 256) if call_data_type is None else call_data_type
+
+        self.call_data = call_data
         self.origin = origin
-        self.call_data_type = call_data_type
         self.code = code
         self.return_data = None
 

mythril/mythril.py

@@ -220,7 +220,7 @@ class Mythril(object):
 
     def set_api_rpc(self, rpc=None, rpctls=False):
         if rpc == 'ganache':
-            rpcconfig = ('localhost', 7545, False)
+            rpcconfig = ('localhost', 8545, False)
         else:
             m = re.match(r'infura-(.*)', rpc)
             if m and m.group(1) in ['mainnet', 'rinkeby', 'kovan', 'ropsten']:

mythril/version.py

@@ -1,3 +1,3 @@
 # This file is suitable for sourcing inside POSIX shell, e.g. bash as
 # well as for importing into Python
-VERSION="v0.18.11"  # NOQA
+VERSION="v0.18.12"  # NOQA

solidity_examples/rubixi.sol

@@ -45,7 +45,7 @@ contract Rubixi {
                 addPayout(_fee);
         }
 
-        //Function called for valid tx to the contract 
+        //Function called for valid tx to the contract
         function addPayout(uint _fee) private {
                 //Adds new address to participant array
                 participants.push(Participant(msg.sender, (msg.value * pyramidMultiplier) / 100));
@@ -149,4 +149,4 @@ contract Rubixi {
                         Payout = participants[orderInPyramid].payout / 1 ether;
                 }
         }
-}
+}

tests/report_test.py

@@ -24,7 +24,7 @@ def _fix_debug_data(json_str):
 
 def _generate_report(input_file):
     contract = ETHContract(input_file.read_text())
-    sym = SymExecWrapper(contract, address=(util.get_indexed_address(0)), strategy="dfs")
+    sym = SymExecWrapper(contract, address=(util.get_indexed_address(0)), strategy="dfs", execution_timeout=30)
     issues = fire_lasers(sym)
 
     report = Report()

tests/solidity_contract_test.py

@@ -26,3 +26,14 @@ class SolidityContractTest(BaseTestCase):
         self.assertEqual(code_info.filename, str(input_file))
         self.assertEqual(code_info.lineno, 6)
         self.assertEqual(code_info.code, "msg.sender.transfer(1 ether)")
+
+    def test_get_source_info_with_contract_name_specified_constructor(self):
+        input_file = TEST_FILES / "constructor_assert.sol"
+        contract = SolidityContract(str(input_file), name="AssertFail")
+
+        code_info = contract.get_source_info(62, constructor=True)
+
+        self.assertEqual(code_info.filename, str(input_file))
+        self.assertEqual(code_info.lineno, 6)
+        self.assertEqual(code_info.code, "assert(var1>0)")
+

tests/testdata/input_contracts/constructor_assert.sol

@@ -0,0 +1,8 @@
+pragma solidity ^0.4.24;
+
+contract AssertFail {
+
+	constructor(uint8 var1){
+		assert(var1>0);
+	}
+}

tests/testdata/input_contracts/metacoin.sol

@@ -1,8 +1,8 @@
 pragma solidity ^0.4.17;
 
-contract metaCoin {
+contract MetaCoin {
 	mapping (address => uint) public balances;
-	function metaCoin() public {
+	function MetaCoin() public {
 		balances[msg.sender] = 10000;
 	}
 	

tests/testdata/outputs_expected/metacoin.sol.o.json

@@ -1 +1 @@
-{"error": null, "issues": [{"address": 498, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "A possible integer overflow exists in the function `sendToken(address,uint256)`.\nThe addition or multiplication may result in a value higher than the maximum representable integer.", "function": "sendToken(address,uint256)", "title": "Integer Overflow", "type": "Warning"}], "success": true}
+{"error": null, "issues": [], "success": true}

tests/testdata/outputs_expected/metacoin.sol.o.markdown

@@ -1,13 +1,3 @@
-# Analysis results for test-filename.sol
+# Analysis results for None
 
-## Integer Overflow
+The analysis was completed successfully. No issues were detected.
-
-- Type: Warning
-- Contract: Unknown
-- Function name: `sendToken(address,uint256)`
-- PC address: 498
-
-### Description
-
-A possible integer overflow exists in the function `sendToken(address,uint256)`.
-The addition or multiplication may result in a value higher than the maximum representable integer.

tests/testdata/outputs_expected/metacoin.sol.o.text

@@ -1,9 +1 @@
-==== Integer Overflow ====
+The analysis was completed successfully. No issues were detected.
-Type: Warning
-Contract: Unknown
-Function name: sendToken(address,uint256)
-PC address: 498
-A possible integer overflow exists in the function `sendToken(address,uint256)`.
-The addition or multiplication may result in a value higher than the maximum representable integer.
---------------------
-

tests/testdata/outputs_expected/suicide.sol.o.json

@@ -1 +1 @@
-{"error": null, "issues": [{"address": 146, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The function `_function_0xcbf0b0c0` executes the SUICIDE instruction. The remaining Ether is sent to an address provided as a function argument.\n\nIt seems that this function can be called without restrictions.", "function": "_function_0xcbf0b0c0", "title": "Unchecked SUICIDE", "type": "Warning"}], "success": true}
+{"error": null, "issues": [{"address": 146, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The function `_function_0xcbf0b0c0` executes the SUICIDE instruction. The remaining Ether is sent to an address provided as a function argument.\n", "function": "_function_0xcbf0b0c0", "title": "Unchecked SUICIDE", "type": "Warning"}], "success": true}

tests/testdata/outputs_expected/suicide.sol.o.markdown

@@ -10,5 +10,3 @@
 ### Description
 
 The function `_function_0xcbf0b0c0` executes the SUICIDE instruction. The remaining Ether is sent to an address provided as a function argument.
-
-It seems that this function can be called without restrictions.

tests/testdata/outputs_expected/suicide.sol.o.text

@@ -5,6 +5,5 @@ Function name: _function_0xcbf0b0c0
 PC address: 146
 The function `_function_0xcbf0b0c0` executes the SUICIDE instruction. The remaining Ether is sent to an address provided as a function argument.
 
-It seems that this function can be called without restrictions.
 --------------------
 

tests/testdata/outputs_expected_laser_result/constructor_assert.sol.json

@@ -0,0 +1,472 @@
+{
+    "accounts": {
+        "0x0000000000000000000000000000000000000000": {
+            "storage": "<mythril.laser.ethereum.state.Storage object at 0x7f18fbbcab70>",
+            "nonce": 0,
+            "balance": "balance",
+            "code": [
+                {
+                    "address": 0,
+                    "argument": "0x80",
+                    "opcode": "PUSH1"
+                },
+                {
+                    "address": 2,
+                    "argument": "0x40",
+                    "opcode": "PUSH1"
+                },
+                {
+                    "address": 4,
+                    "opcode": "MSTORE"
+                },
+                {
+                    "address": 5,
+                    "argument": "0x00",
+                    "opcode": "PUSH1"
+                },
+                {
+                    "address": 7,
+                    "opcode": "DUP1"
+                },
+                {
+                    "address": 8,
+                    "opcode": "REVERT"
+                },
+                {
+                    "address": 9,
+                    "opcode": "STOP"
+                }
+            ]
+        }
+    },
+    "total_states": 5,
+    "nodes": {
+        "933": {
+            "contract_name": "unknown",
+            "flags": "NodeFlags()",
+            "constraints": [],
+            "function_name": "unknown",
+            "start_addr": 0,
+            "uid": 933,
+            "states": [
+                {
+                    "accounts": "dict_keys(['0x0000000000000000000000000000000000000000'])",
+                    "mstate": {
+                        "gas": 10000000,
+                        "memory": [],
+                        "pc": 0,
+                        "memsize": 0,
+                        "stack": []
+                    },
+                    "environment": {
+                        "sender": "caller",
+                        "callvalue": "call_value",
+                        "origin": "origin",
+                        "active_account": "0x0000000000000000000000000000000000000000",
+                        "gasprice": "gas_price",
+                        "calldata": [],
+                        "calldata_type": "CalldataType.SYMBOLIC"
+                    }
+                },
+                {
+                    "accounts": "dict_keys(['0x0000000000000000000000000000000000000000'])",
+                    "mstate": {
+                        "gas": 10000000,
+                        "memory": [],
+                        "pc": 1,
+                        "memsize": 0,
+                        "stack": [
+                            "128"
+                        ]
+                    },
+                    "environment": {
+                        "sender": "caller",
+                        "callvalue": "call_value",
+                        "origin": "origin",
+                        "active_account": "0x0000000000000000000000000000000000000000",
+                        "gasprice": "gas_price",
+                        "calldata": [],
+                        "calldata_type": "CalldataType.SYMBOLIC"
+                    }
+                },
+                {
+                    "accounts": "dict_keys(['0x0000000000000000000000000000000000000000'])",
+                    "mstate": {
+                        "gas": 10000000,
+                        "memory": [],
+                        "pc": 2,
+                        "memsize": 0,
+                        "stack": [
+                            "128",
+                            "64"
+                        ]
+                    },
+                    "environment": {
+                        "sender": "caller",
+                        "callvalue": "call_value",
+                        "origin": "origin",
+                        "active_account": "0x0000000000000000000000000000000000000000",
+                        "gasprice": "gas_price",
+                        "calldata": [],
+                        "calldata_type": "CalldataType.SYMBOLIC"
+                    }
+                },
+                {
+                    "accounts": "dict_keys(['0x0000000000000000000000000000000000000000'])",
+                    "mstate": {
+                        "gas": 10000000,
+                        "memory": [
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            128
+                        ],
+                        "pc": 3,
+                        "memsize": 96,
+                        "stack": []
+                    },
+                    "environment": {
+                        "sender": "caller",
+                        "callvalue": "call_value",
+                        "origin": "origin",
+                        "active_account": "0x0000000000000000000000000000000000000000",
+                        "gasprice": "gas_price",
+                        "calldata": [],
+                        "calldata_type": "CalldataType.SYMBOLIC"
+                    }
+                },
+                {
+                    "accounts": "dict_keys(['0x0000000000000000000000000000000000000000'])",
+                    "mstate": {
+                        "gas": 10000000,
+                        "memory": [
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            128
+                        ],
+                        "pc": 4,
+                        "memsize": 96,
+                        "stack": [
+                            "0"
+                        ]
+                    },
+                    "environment": {
+                        "sender": "caller",
+                        "callvalue": "call_value",
+                        "origin": "origin",
+                        "active_account": "0x0000000000000000000000000000000000000000",
+                        "gasprice": "gas_price",
+                        "calldata": [],
+                        "calldata_type": "CalldataType.SYMBOLIC"
+                    }
+                },
+                {
+                    "accounts": "dict_keys(['0x0000000000000000000000000000000000000000'])",
+                    "mstate": {
+                        "gas": 10000000,
+                        "memory": [
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            0,
+                            128
+                        ],
+                        "pc": 5,
+                        "memsize": 96,
+                        "stack": [
+                            "0",
+                            "0"
+                        ]
+                    },
+                    "environment": {
+                        "sender": "caller",
+                        "callvalue": "call_value",
+                        "origin": "origin",
+                        "active_account": "0x0000000000000000000000000000000000000000",
+                        "gasprice": "gas_price",
+                        "calldata": [],
+                        "calldata_type": "CalldataType.SYMBOLIC"
+                    }
+                }
+            ]
+        }
+    },
+    "max_depth": 22,
+    "edges": []
+}