Check for length bin runtime

pull/355/head
Joran Honig 6 years ago
parent 621c8b95df
commit 44d25e48e7
  1. 60
      mythril/laser/ethereum/state.py
  2. 9
      mythril/laser/ethereum/svm.py

@ -1,12 +1,13 @@
from z3 import BitVec, BitVecVal from z3 import BitVec, BitVecVal
from copy import copy, deepcopy from copy import copy, deepcopy
from enum import Enum from enum import Enum
from random import random
class CalldataType(Enum): class CalldataType(Enum):
CONCRETE = 1 CONCRETE = 1
SYMBOLIC = 2 SYMBOLIC = 2
class Account: class Account:
""" """
Account class representing ethereum accounts Account class representing ethereum accounts
@ -31,6 +32,12 @@ class Account:
def __str__(self): def __str__(self):
return str(self.as_dict) return str(self.as_dict)
def set_balance(self, balance):
self.balance = balance
def add_balance(self, balance):
self.balance += balance
def get_storage(self, index): def get_storage(self, index):
return self.storage[index] if index in self.storage.keys() else BitVec("storage_" + str(index), 256) return self.storage[index] if index in self.storage.keys() else BitVec("storage_" + str(index), 256)
@ -149,3 +156,54 @@ class GlobalState:
""" Gets the current instruction for this GlobalState""" """ Gets the current instruction for this GlobalState"""
instructions = self.environment.code.instruction_list instructions = self.environment.code.instruction_list
return instructions[self.mstate.pc] return instructions[self.mstate.pc]
class WorldState:
"""
The WorldState class represents the world state as described in the yellowpaper
"""
def __init__(self):
"""
Constructor for the world state. Initializes the accounts record
"""
self.accounts = {}
def __getitem__(self, item):
"""
Gets an account from the worldstate using item as key
:param item: Address of the account to get
:return: Account associated with the address
"""
return self.accounts[item]
def create_account(self, balance=0):
"""
Create non-contract account
:param balance: Initial balance for the account
:return: The new account
"""
new_account = Account(self._generate_new_address(), balance=balance)
self._put_account(new_account)
return new_account
def create_initialized_contract_account(self, contract_code, storage):
"""
Creates a new contract account, based on the contract code and storage provided
The contract code only includes the runtime contract bytecode
:param contract_code: Runtime bytecode for the contract
:param storage: Initial storage for the contract
:return: The new account
"""
new_account = Account(self._generate_new_address(), code=contract_code, balance=0)
new_account.storage = storage
self._put_account(new_account)
def _generate_new_address(self):
""" Generates a new address for the global state"""
while True:
address = '0x' + ''.join([str(hex(random(0, 16)))[-1] for _ in range(20)])
if address not in self.accounts.keys():
return address
def _put_account(self, account):
self.accounts[account.address] = account

@ -1,6 +1,6 @@
from z3 import BitVec from z3 import BitVec
import logging import logging
from mythril.laser.ethereum.state import GlobalState, Environment, CalldataType, Account from mythril.laser.ethereum.state import GlobalState, Environment, CalldataType, Account, WorldState
from mythril.laser.ethereum.instructions import Instruction from mythril.laser.ethereum.instructions import Instruction
from mythril.laser.ethereum.cfg import NodeFlags, Node, Edge, JumpType from mythril.laser.ethereum.cfg import NodeFlags, Node, Edge, JumpType
from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy
@ -25,7 +25,8 @@ class LaserEVM:
""" """
def __init__(self, accounts, dynamic_loader=None, max_depth=22): def __init__(self, accounts, dynamic_loader=None, max_depth=22):
self.instructions_covered = [] self.instructions_covered = []
self.accounts = accounts self.world_state = WorldState()
self.world_state.accounts = accounts
self.nodes = {} self.nodes = {}
self.edges = [] self.edges = []
@ -47,7 +48,7 @@ class LaserEVM:
# Initialize the execution environment # Initialize the execution environment
environment = Environment( environment = Environment(
self.accounts[main_address], self.world_state[main_address],
BitVec("caller", 256), BitVec("caller", 256),
[], [],
BitVec("gasprice", 256), BitVec("gasprice", 256),
@ -61,7 +62,7 @@ class LaserEVM:
initial_node = Node(environment.active_account.contract_name) initial_node = Node(environment.active_account.contract_name)
self.nodes[initial_node.uid] = initial_node self.nodes[initial_node.uid] = initial_node
global_state = GlobalState(self.accounts, environment, initial_node) global_state = GlobalState(self.world_state, environment, initial_node)
initial_node.states.append(global_state) initial_node.states.append(global_state)
# Empty the work_list before starting an execution # Empty the work_list before starting an execution

Loading…
Cancel
Save