"""This module contains a representation of a smart contract's memory."""
from copy import copy
from typing import cast, Dict, List, Union, overload
from z3 import Z3Exception
from mythril.laser.ethereum import util
from mythril.laser.smt import (
BitVec,
Bool,
Concat,
Extract,
If,
simplify,
symbol_factory,
)
[docs]def convert_bv(val: Union[int, BitVec]) -> BitVec:
if isinstance(val, BitVec):
return val
return symbol_factory.BitVecVal(val, 256)
# No of iterations to perform when iteration size is symbolic
APPROX_ITR = 100
[docs]class Memory:
"""A class representing contract memory with random access."""
def __init__(self):
""""""
self._msize = 0
self._memory = {} # type: Dict[BitVec, Union[int, BitVec]]
def __len__(self):
"""
:return:
"""
return self._msize
def __copy__(self):
new_memory = Memory()
new_memory._memory = copy(self._memory)
new_memory._msize = self._msize
return new_memory
[docs] def extend(self, size: int):
"""
:param size:
"""
self._msize += size
[docs] def get_word_at(self, index: int) -> Union[int, BitVec]:
"""Access a word from a specified memory index.
:param index: integer representing the index to access
:return: 32 byte word at the specified index
"""
try:
return symbol_factory.BitVecVal(
util.concrete_int_from_bytes(
bytes([util.get_concrete_int(b) for b in self[index : index + 32]]),
0,
),
256,
)
except TypeError:
result = simplify(
Concat(
[
b if isinstance(b, BitVec) else symbol_factory.BitVecVal(b, 8)
for b in cast(
List[Union[int, BitVec]], self[index : index + 32]
)
]
)
)
assert result.size() == 256
return result
[docs] def write_word_at(self, index: int, value: Union[int, BitVec, bool, Bool]) -> None:
"""Writes a 32 byte word to memory at the specified index`
:param index: index to write to
:param value: the value to write to memory
"""
try:
# Attempt to concretize value
if isinstance(value, bool):
_bytes = (
int(1).to_bytes(32, byteorder="big")
if value
else int(0).to_bytes(32, byteorder="big")
)
else:
_bytes = util.concrete_int_to_bytes(value)
assert len(_bytes) == 32
self[index : index + 32] = list(bytearray(_bytes))
except (Z3Exception, AttributeError): # BitVector or BoolRef
value = cast(Union[BitVec, Bool], value)
if isinstance(value, Bool):
value_to_write = If(
value,
symbol_factory.BitVecVal(1, 256),
symbol_factory.BitVecVal(0, 256),
)
else:
value_to_write = value
assert value_to_write.size() == 256
for i in range(0, value_to_write.size(), 8):
self[index + 31 - (i // 8)] = Extract(i + 7, i, value_to_write)
@overload
def __getitem__(self, item: BitVec) -> Union[int, BitVec]:
...
@overload
def __getitem__(self, item: slice) -> List[Union[int, BitVec]]:
...
def __getitem__(
self, item: Union[BitVec, slice]
) -> Union[BitVec, int, List[Union[int, BitVec]]]:
"""
:param item:
:return:
"""
if isinstance(item, slice):
start, step, stop = item.start, item.step, item.stop
if start is None:
start = 0
if stop is None: # 2**256 is just a bit too big
raise IndexError("Invalid Memory Slice")
if step is None:
step = 1
bvstart, bvstop, bvstep = (
convert_bv(start),
convert_bv(stop),
convert_bv(step),
)
ret_lis = []
symbolic_len = False
itr = symbol_factory.BitVecVal(0, 256)
if (bvstop - bvstart).symbolic:
symbolic_len = True
while simplify(bvstep * itr != simplify(bvstop - bvstart)) and (
not symbolic_len or itr <= APPROX_ITR
):
ret_lis.append(self[bvstart + bvstep * itr])
itr += 1
return ret_lis
item = simplify(convert_bv(item))
return self._memory.get(item, 0)
def __setitem__(
self,
key: Union[int, BitVec, slice],
value: Union[BitVec, int, List[Union[int, BitVec]]],
):
"""
:param key:
:param value:
"""
if isinstance(key, slice):
start, step, stop = key.start, key.step, key.stop
if start is None:
start = 0
if stop is None:
raise IndexError("Invalid Memory Slice")
if step is None:
step = 1
else:
assert False, "Currently mentioning step size is not supported"
assert type(value) == list
bvstart, bvstop, bvstep = (
convert_bv(start),
convert_bv(stop),
convert_bv(step),
)
symbolic_len = False
itr = symbol_factory.BitVecVal(0, 256)
if (bvstop - bvstart).symbolic:
symbolic_len = True
while simplify(bvstep * itr != simplify(bvstop - bvstart)) and (
not symbolic_len or itr <= APPROX_ITR
):
self[bvstart + itr * bvstep] = cast(List[Union[int, BitVec]], value)[
itr.value
]
itr += 1
else:
bv_key = simplify(convert_bv(key))
if bv_key >= len(self):
return
if isinstance(value, int):
assert 0 <= value <= 0xFF
if isinstance(value, BitVec):
assert value.size() == 8
self._memory[bv_key] = cast(Union[int, BitVec], value)