|
|
@ -27,8 +27,13 @@ class StopSignal(Exception): |
|
|
|
pass |
|
|
|
pass |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
class PCMutator(object): |
|
|
|
class StateTransition(object): |
|
|
|
""" Wrapper that handles copy and original return """ |
|
|
|
"""Decorator that handles global state copy and original return. |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This decorator calls the decorated instruction mutator function on a copy of the state that |
|
|
|
|
|
|
|
is passed to it. After the call, the resulting new states' program counter is automatically |
|
|
|
|
|
|
|
incremented if `increment_pc=True`. |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
def __init__(self, increment_pc=True): |
|
|
|
def __init__(self, increment_pc=True): |
|
|
|
self.increment_pc = increment_pc |
|
|
|
self.increment_pc = increment_pc |
|
|
@ -85,23 +90,23 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
return instruction_mutator(global_state) |
|
|
|
return instruction_mutator(global_state) |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def jumpdest_(self, global_state): |
|
|
|
def jumpdest_(self, global_state): |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def push_(self, global_state): |
|
|
|
def push_(self, global_state): |
|
|
|
value = BitVecVal(int(global_state.get_current_instruction()['argument'][2:], 16), 256) |
|
|
|
value = BitVecVal(int(global_state.get_current_instruction()['argument'][2:], 16), 256) |
|
|
|
global_state.mstate.stack.append(value) |
|
|
|
global_state.mstate.stack.append(value) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def dup_(self, global_state): |
|
|
|
def dup_(self, global_state): |
|
|
|
value = int(global_state.get_current_instruction()['opcode'][3:], 10) |
|
|
|
value = int(global_state.get_current_instruction()['opcode'][3:], 10) |
|
|
|
global_state.mstate.stack.append(global_state.mstate.stack[-value]) |
|
|
|
global_state.mstate.stack.append(global_state.mstate.stack[-value]) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def swap_(self, global_state): |
|
|
|
def swap_(self, global_state): |
|
|
|
depth = int(self.op_code[4:]) |
|
|
|
depth = int(self.op_code[4:]) |
|
|
|
try: |
|
|
|
try: |
|
|
@ -111,7 +116,7 @@ class Instruction: |
|
|
|
raise StackUnderflowException() |
|
|
|
raise StackUnderflowException() |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def pop_(self, global_state): |
|
|
|
def pop_(self, global_state): |
|
|
|
try: |
|
|
|
try: |
|
|
|
global_state.mstate.stack.pop() |
|
|
|
global_state.mstate.stack.pop() |
|
|
@ -119,7 +124,7 @@ class Instruction: |
|
|
|
raise StackUnderflowException() |
|
|
|
raise StackUnderflowException() |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def and_(self, global_state): |
|
|
|
def and_(self, global_state): |
|
|
|
try: |
|
|
|
try: |
|
|
|
stack = global_state.mstate.stack |
|
|
|
stack = global_state.mstate.stack |
|
|
@ -134,7 +139,7 @@ class Instruction: |
|
|
|
raise StackUnderflowException() |
|
|
|
raise StackUnderflowException() |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def or_(self, global_state): |
|
|
|
def or_(self, global_state): |
|
|
|
stack = global_state.mstate.stack |
|
|
|
stack = global_state.mstate.stack |
|
|
|
try: |
|
|
|
try: |
|
|
@ -151,19 +156,19 @@ class Instruction: |
|
|
|
raise StackUnderflowException() |
|
|
|
raise StackUnderflowException() |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def xor_(self, global_state): |
|
|
|
def xor_(self, global_state): |
|
|
|
mstate = global_state.mstate |
|
|
|
mstate = global_state.mstate |
|
|
|
mstate.stack.append(mstate.stack.pop() ^ mstate.stack.pop()) |
|
|
|
mstate.stack.append(mstate.stack.pop() ^ mstate.stack.pop()) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def not_(self, global_state: GlobalState): |
|
|
|
def not_(self, global_state: GlobalState): |
|
|
|
mstate = global_state.mstate |
|
|
|
mstate = global_state.mstate |
|
|
|
mstate.stack.append(TT256M1 - mstate.stack.pop()) |
|
|
|
mstate.stack.append(TT256M1 - mstate.stack.pop()) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def byte_(self, global_state): |
|
|
|
def byte_(self, global_state): |
|
|
|
mstate = global_state.mstate |
|
|
|
mstate = global_state.mstate |
|
|
|
op0, op1 = mstate.stack.pop(), mstate.stack.pop() |
|
|
|
op0, op1 = mstate.stack.pop(), mstate.stack.pop() |
|
|
@ -184,25 +189,25 @@ class Instruction: |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
# Arithmetic |
|
|
|
# Arithmetic |
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def add_(self, global_state): |
|
|
|
def add_(self, global_state): |
|
|
|
global_state.mstate.stack.append( |
|
|
|
global_state.mstate.stack.append( |
|
|
|
(helper.pop_bitvec(global_state.mstate) + helper.pop_bitvec(global_state.mstate))) |
|
|
|
(helper.pop_bitvec(global_state.mstate) + helper.pop_bitvec(global_state.mstate))) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def sub_(self, global_state): |
|
|
|
def sub_(self, global_state): |
|
|
|
global_state.mstate.stack.append( |
|
|
|
global_state.mstate.stack.append( |
|
|
|
(helper.pop_bitvec(global_state.mstate) - helper.pop_bitvec(global_state.mstate))) |
|
|
|
(helper.pop_bitvec(global_state.mstate) - helper.pop_bitvec(global_state.mstate))) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def mul_(self, global_state): |
|
|
|
def mul_(self, global_state): |
|
|
|
global_state.mstate.stack.append( |
|
|
|
global_state.mstate.stack.append( |
|
|
|
(helper.pop_bitvec(global_state.mstate) * helper.pop_bitvec(global_state.mstate))) |
|
|
|
(helper.pop_bitvec(global_state.mstate) * helper.pop_bitvec(global_state.mstate))) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def div_(self, global_state): |
|
|
|
def div_(self, global_state): |
|
|
|
op0, op1 = util.pop_bitvec(global_state.mstate), util.pop_bitvec(global_state.mstate) |
|
|
|
op0, op1 = util.pop_bitvec(global_state.mstate), util.pop_bitvec(global_state.mstate) |
|
|
|
if op1 == 0: |
|
|
|
if op1 == 0: |
|
|
@ -211,7 +216,7 @@ class Instruction: |
|
|
|
global_state.mstate.stack.append(UDiv(op0, op1)) |
|
|
|
global_state.mstate.stack.append(UDiv(op0, op1)) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def sdiv_(self, global_state): |
|
|
|
def sdiv_(self, global_state): |
|
|
|
s0, s1 = util.pop_bitvec(global_state.mstate), util.pop_bitvec(global_state.mstate) |
|
|
|
s0, s1 = util.pop_bitvec(global_state.mstate), util.pop_bitvec(global_state.mstate) |
|
|
|
if s1 == 0: |
|
|
|
if s1 == 0: |
|
|
@ -220,33 +225,33 @@ class Instruction: |
|
|
|
global_state.mstate.stack.append(s0 / s1) |
|
|
|
global_state.mstate.stack.append(s0 / s1) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def mod_(self, global_state): |
|
|
|
def mod_(self, global_state): |
|
|
|
s0, s1 = util.pop_bitvec(global_state.mstate), util.pop_bitvec(global_state.mstate) |
|
|
|
s0, s1 = util.pop_bitvec(global_state.mstate), util.pop_bitvec(global_state.mstate) |
|
|
|
global_state.mstate.stack.append(0 if s1 == 0 else URem(s0, s1)) |
|
|
|
global_state.mstate.stack.append(0 if s1 == 0 else URem(s0, s1)) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def smod_(self, global_state): |
|
|
|
def smod_(self, global_state): |
|
|
|
s0, s1 = util.pop_bitvec(global_state.mstate), util.pop_bitvec(global_state.mstate) |
|
|
|
s0, s1 = util.pop_bitvec(global_state.mstate), util.pop_bitvec(global_state.mstate) |
|
|
|
global_state.mstate.stack.append(0 if s1 == 0 else SRem(s0, s1)) |
|
|
|
global_state.mstate.stack.append(0 if s1 == 0 else SRem(s0, s1)) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def addmod_(self, global_state): |
|
|
|
def addmod_(self, global_state): |
|
|
|
s0, s1, s2 = util.pop_bitvec(global_state.mstate), util.pop_bitvec(global_state.mstate), util.pop_bitvec( |
|
|
|
s0, s1, s2 = util.pop_bitvec(global_state.mstate), util.pop_bitvec(global_state.mstate), util.pop_bitvec( |
|
|
|
global_state.mstate) |
|
|
|
global_state.mstate) |
|
|
|
global_state.mstate.stack.append(URem(URem(s0, s2) + URem(s1, s2), s2)) |
|
|
|
global_state.mstate.stack.append(URem(URem(s0, s2) + URem(s1, s2), s2)) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def mulmod_(self, global_state): |
|
|
|
def mulmod_(self, global_state): |
|
|
|
s0, s1, s2 = util.pop_bitvec(global_state.mstate), util.pop_bitvec(global_state.mstate), util.pop_bitvec( |
|
|
|
s0, s1, s2 = util.pop_bitvec(global_state.mstate), util.pop_bitvec(global_state.mstate), util.pop_bitvec( |
|
|
|
global_state.mstate) |
|
|
|
global_state.mstate) |
|
|
|
global_state.mstate.stack.append(URem(URem(s0, s2) * URem(s1, s2), s2)) |
|
|
|
global_state.mstate.stack.append(URem(URem(s0, s2) * URem(s1, s2), s2)) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def exp_(self, global_state): |
|
|
|
def exp_(self, global_state): |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
|
|
|
|
|
|
|
@ -258,7 +263,7 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def signextend_(self, global_state): |
|
|
|
def signextend_(self, global_state): |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
s0, s1 = state.stack.pop(), state.stack.pop() |
|
|
|
s0, s1 = state.stack.pop(), state.stack.pop() |
|
|
@ -282,28 +287,28 @@ class Instruction: |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
# Comparisons |
|
|
|
# Comparisons |
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def lt_(self, global_state): |
|
|
|
def lt_(self, global_state): |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
exp = ULT(util.pop_bitvec(state), util.pop_bitvec(state)) |
|
|
|
exp = ULT(util.pop_bitvec(state), util.pop_bitvec(state)) |
|
|
|
state.stack.append(exp) |
|
|
|
state.stack.append(exp) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def gt_(self, global_state): |
|
|
|
def gt_(self, global_state): |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
exp = UGT(util.pop_bitvec(state), util.pop_bitvec(state)) |
|
|
|
exp = UGT(util.pop_bitvec(state), util.pop_bitvec(state)) |
|
|
|
state.stack.append(exp) |
|
|
|
state.stack.append(exp) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def slt_(self, global_state): |
|
|
|
def slt_(self, global_state): |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
exp = util.pop_bitvec(state) < util.pop_bitvec(state) |
|
|
|
exp = util.pop_bitvec(state) < util.pop_bitvec(state) |
|
|
|
state.stack.append(exp) |
|
|
|
state.stack.append(exp) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def sgt_(self, global_state): |
|
|
|
def sgt_(self, global_state): |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
|
|
|
|
|
|
|
@ -311,7 +316,7 @@ class Instruction: |
|
|
|
state.stack.append(exp) |
|
|
|
state.stack.append(exp) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def eq_(self, global_state): |
|
|
|
def eq_(self, global_state): |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
|
|
|
|
|
|
|
@ -329,7 +334,7 @@ class Instruction: |
|
|
|
state.stack.append(exp) |
|
|
|
state.stack.append(exp) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def iszero_(self, global_state): |
|
|
|
def iszero_(self, global_state): |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
|
|
|
|
|
|
|
@ -340,7 +345,7 @@ class Instruction: |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
# Call data |
|
|
|
# Call data |
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def callvalue_(self, global_state): |
|
|
|
def callvalue_(self, global_state): |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
environment = global_state.environment |
|
|
|
environment = global_state.environment |
|
|
@ -348,7 +353,7 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def calldataload_(self, global_state): |
|
|
|
def calldataload_(self, global_state): |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
environment = global_state.environment |
|
|
|
environment = global_state.environment |
|
|
@ -388,7 +393,7 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def calldatasize_(self, global_state): |
|
|
|
def calldatasize_(self, global_state): |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
environment = global_state.environment |
|
|
|
environment = global_state.environment |
|
|
@ -398,7 +403,7 @@ class Instruction: |
|
|
|
state.stack.append(BitVecVal(len(environment.calldata), 256)) |
|
|
|
state.stack.append(BitVecVal(len(environment.calldata), 256)) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def calldatacopy_(self, global_state): |
|
|
|
def calldatacopy_(self, global_state): |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
environment = global_state.environment |
|
|
|
environment = global_state.environment |
|
|
@ -463,35 +468,35 @@ class Instruction: |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
# Environment |
|
|
|
# Environment |
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def address_(self, global_state): |
|
|
|
def address_(self, global_state): |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
environment = global_state.environment |
|
|
|
environment = global_state.environment |
|
|
|
state.stack.append(environment.address) |
|
|
|
state.stack.append(environment.address) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def balance_(self, global_state): |
|
|
|
def balance_(self, global_state): |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
address = state.stack.pop() |
|
|
|
address = state.stack.pop() |
|
|
|
state.stack.append(BitVec("balance_at_" + str(address), 256)) |
|
|
|
state.stack.append(BitVec("balance_at_" + str(address), 256)) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def origin_(self, global_state): |
|
|
|
def origin_(self, global_state): |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
environment = global_state.environment |
|
|
|
environment = global_state.environment |
|
|
|
state.stack.append(environment.origin) |
|
|
|
state.stack.append(environment.origin) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def caller_(self, global_state): |
|
|
|
def caller_(self, global_state): |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
environment = global_state.environment |
|
|
|
environment = global_state.environment |
|
|
|
state.stack.append(environment.sender) |
|
|
|
state.stack.append(environment.sender) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def codesize_(self, global_state): |
|
|
|
def codesize_(self, global_state): |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
environment = global_state.environment |
|
|
|
environment = global_state.environment |
|
|
@ -499,7 +504,7 @@ class Instruction: |
|
|
|
state.stack.append(len(disassembly.bytecode) // 2) |
|
|
|
state.stack.append(len(disassembly.bytecode) // 2) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def sha3_(self, global_state): |
|
|
|
def sha3_(self, global_state): |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
environment = global_state.environment |
|
|
|
environment = global_state.environment |
|
|
@ -537,12 +542,12 @@ class Instruction: |
|
|
|
state.stack.append(BitVecVal(util.concrete_int_from_bytes(keccac, 0), 256)) |
|
|
|
state.stack.append(BitVecVal(util.concrete_int_from_bytes(keccac, 0), 256)) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def gasprice_(self, global_state): |
|
|
|
def gasprice_(self, global_state): |
|
|
|
global_state.mstate.stack.append(BitVec("gasprice", 256)) |
|
|
|
global_state.mstate.stack.append(BitVec("gasprice", 256)) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def codecopy_(self, global_state): |
|
|
|
def codecopy_(self, global_state): |
|
|
|
memory_offset, code_offset, size = global_state.mstate.stack.pop(), global_state.mstate.stack.pop(), global_state.mstate.stack.pop() |
|
|
|
memory_offset, code_offset, size = global_state.mstate.stack.pop(), global_state.mstate.stack.pop(), global_state.mstate.stack.pop() |
|
|
|
|
|
|
|
|
|
|
@ -591,7 +596,7 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def extcodesize_(self, global_state): |
|
|
|
def extcodesize_(self, global_state): |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
addr = state.stack.pop() |
|
|
|
addr = state.stack.pop() |
|
|
@ -617,7 +622,7 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def extcodecopy_(self, global_state): |
|
|
|
def extcodecopy_(self, global_state): |
|
|
|
# FIXME: not implemented |
|
|
|
# FIXME: not implemented |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
@ -625,45 +630,45 @@ class Instruction: |
|
|
|
start, s2, size = state.stack.pop(), state.stack.pop(), state.stack.pop() |
|
|
|
start, s2, size = state.stack.pop(), state.stack.pop(), state.stack.pop() |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def returndatasize_(self, global_state): |
|
|
|
def returndatasize_(self, global_state): |
|
|
|
global_state.mstate.stack.append(BitVec("returndatasize", 256)) |
|
|
|
global_state.mstate.stack.append(BitVec("returndatasize", 256)) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def blockhash_(self, global_state): |
|
|
|
def blockhash_(self, global_state): |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
blocknumber = state.stack.pop() |
|
|
|
blocknumber = state.stack.pop() |
|
|
|
state.stack.append(BitVec("blockhash_block_" + str(blocknumber), 256)) |
|
|
|
state.stack.append(BitVec("blockhash_block_" + str(blocknumber), 256)) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def coinbase_(self, global_state): |
|
|
|
def coinbase_(self, global_state): |
|
|
|
global_state.mstate.stack.append(BitVec("coinbase", 256)) |
|
|
|
global_state.mstate.stack.append(BitVec("coinbase", 256)) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def timestamp_(self, global_state): |
|
|
|
def timestamp_(self, global_state): |
|
|
|
global_state.mstate.stack.append(BitVec("timestamp", 256)) |
|
|
|
global_state.mstate.stack.append(BitVec("timestamp", 256)) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def number_(self, global_state): |
|
|
|
def number_(self, global_state): |
|
|
|
global_state.mstate.stack.append(BitVec("block_number", 256)) |
|
|
|
global_state.mstate.stack.append(BitVec("block_number", 256)) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def difficulty_(self, global_state): |
|
|
|
def difficulty_(self, global_state): |
|
|
|
global_state.mstate.stack.append(BitVec("block_difficulty", 256)) |
|
|
|
global_state.mstate.stack.append(BitVec("block_difficulty", 256)) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def gaslimit_(self, global_state): |
|
|
|
def gaslimit_(self, global_state): |
|
|
|
global_state.mstate.stack.append(BitVec("block_gaslimit", 256)) |
|
|
|
global_state.mstate.stack.append(BitVec("block_gaslimit", 256)) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
# Memory operations |
|
|
|
# Memory operations |
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def mload_(self, global_state): |
|
|
|
def mload_(self, global_state): |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
op0 = state.stack.pop() |
|
|
|
op0 = state.stack.pop() |
|
|
@ -690,7 +695,7 @@ class Instruction: |
|
|
|
state.stack.append(data) |
|
|
|
state.stack.append(data) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def mstore_(self, global_state): |
|
|
|
def mstore_(self, global_state): |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
try: |
|
|
|
try: |
|
|
@ -728,7 +733,7 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def mstore8_(self, global_state): |
|
|
|
def mstore8_(self, global_state): |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
op0, value = state.stack.pop(), state.stack.pop() |
|
|
|
op0, value = state.stack.pop(), state.stack.pop() |
|
|
@ -744,7 +749,7 @@ class Instruction: |
|
|
|
state.memory[offset] = value % 256 |
|
|
|
state.memory[offset] = value % 256 |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def sload_(self, global_state): |
|
|
|
def sload_(self, global_state): |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
index = state.stack.pop() |
|
|
|
index = state.stack.pop() |
|
|
@ -764,7 +769,7 @@ class Instruction: |
|
|
|
state.stack.append(data) |
|
|
|
state.stack.append(data) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def sstore_(self, global_state): |
|
|
|
def sstore_(self, global_state): |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
index, value = state.stack.pop(), state.stack.pop() |
|
|
|
index, value = state.stack.pop(), state.stack.pop() |
|
|
@ -786,7 +791,7 @@ class Instruction: |
|
|
|
logging.debug("Error writing to storage: Invalid index") |
|
|
|
logging.debug("Error writing to storage: Invalid index") |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator(increment_pc=False) |
|
|
|
@StateTransition(increment_pc=False) |
|
|
|
def jump_(self, global_state): |
|
|
|
def jump_(self, global_state): |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
disassembly = global_state.environment.code |
|
|
|
disassembly = global_state.environment.code |
|
|
@ -815,7 +820,7 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
return [new_state] |
|
|
|
return [new_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator(increment_pc=False) |
|
|
|
@StateTransition(increment_pc=False) |
|
|
|
def jumpi_(self, global_state): |
|
|
|
def jumpi_(self, global_state): |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
disassembly = global_state.environment.code |
|
|
|
disassembly = global_state.environment.code |
|
|
@ -865,22 +870,22 @@ class Instruction: |
|
|
|
logging.debug("Pruned unreachable states.") |
|
|
|
logging.debug("Pruned unreachable states.") |
|
|
|
return states |
|
|
|
return states |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def pc_(self, global_state): |
|
|
|
def pc_(self, global_state): |
|
|
|
global_state.mstate.stack.append(global_state.mstate.pc - 1) |
|
|
|
global_state.mstate.stack.append(global_state.mstate.pc - 1) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def msize_(self, global_state): |
|
|
|
def msize_(self, global_state): |
|
|
|
global_state.mstate.stack.append(BitVec("msize", 256)) |
|
|
|
global_state.mstate.stack.append(BitVec("msize", 256)) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def gas_(self, global_state): |
|
|
|
def gas_(self, global_state): |
|
|
|
global_state.mstate.stack.append(BitVec("gas", 256)) |
|
|
|
global_state.mstate.stack.append(BitVec("gas", 256)) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def log_(self, global_state): |
|
|
|
def log_(self, global_state): |
|
|
|
# TODO: implement me |
|
|
|
# TODO: implement me |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
@ -890,7 +895,7 @@ class Instruction: |
|
|
|
# Not supported |
|
|
|
# Not supported |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def create_(self, global_state): |
|
|
|
def create_(self, global_state): |
|
|
|
# TODO: implement me |
|
|
|
# TODO: implement me |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
@ -899,7 +904,7 @@ class Instruction: |
|
|
|
state.stack.append(0) |
|
|
|
state.stack.append(0) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def return_(self, global_state): |
|
|
|
def return_(self, global_state): |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
offset, length = state.stack.pop(), state.stack.pop() |
|
|
|
offset, length = state.stack.pop(), state.stack.pop() |
|
|
@ -910,27 +915,27 @@ class Instruction: |
|
|
|
logging.debug("Return with symbolic length or offset. Not supported") |
|
|
|
logging.debug("Return with symbolic length or offset. Not supported") |
|
|
|
global_state.current_transaction.end(global_state, return_data) |
|
|
|
global_state.current_transaction.end(global_state, return_data) |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def suicide_(self, global_state): |
|
|
|
def suicide_(self, global_state): |
|
|
|
return [] |
|
|
|
return [] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def revert_(self, global_state): |
|
|
|
def revert_(self, global_state): |
|
|
|
return [] |
|
|
|
return [] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def assert_fail_(self, global_state): |
|
|
|
def assert_fail_(self, global_state): |
|
|
|
return [] |
|
|
|
return [] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def invalid_(self, global_state): |
|
|
|
def invalid_(self, global_state): |
|
|
|
return [] |
|
|
|
return [] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def stop_(self, global_state): |
|
|
|
def stop_(self, global_state): |
|
|
|
global_state.current_transaction.end(global_state) |
|
|
|
global_state.current_transaction.end(global_state) |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def call_(self, global_state): |
|
|
|
def call_(self, global_state): |
|
|
|
instr = global_state.get_current_instruction() |
|
|
|
instr = global_state.get_current_instruction() |
|
|
|
environment = global_state.environment |
|
|
|
environment = global_state.environment |
|
|
@ -988,7 +993,7 @@ class Instruction: |
|
|
|
call_data_type) |
|
|
|
call_data_type) |
|
|
|
raise TransactionStartSignal(transaction, self.op_code) |
|
|
|
raise TransactionStartSignal(transaction, self.op_code) |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def call_post(self, global_state): |
|
|
|
def call_post(self, global_state): |
|
|
|
instr = global_state.get_current_instruction() |
|
|
|
instr = global_state.get_current_instruction() |
|
|
|
|
|
|
|
|
|
|
@ -1029,7 +1034,7 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def callcode_(self, global_state): |
|
|
|
def callcode_(self, global_state): |
|
|
|
instr = global_state.get_current_instruction() |
|
|
|
instr = global_state.get_current_instruction() |
|
|
|
environment = global_state.environment |
|
|
|
environment = global_state.environment |
|
|
@ -1056,7 +1061,7 @@ class Instruction: |
|
|
|
) |
|
|
|
) |
|
|
|
raise TransactionStartSignal(transaction, self.op_code) |
|
|
|
raise TransactionStartSignal(transaction, self.op_code) |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def callcode_post(self, global_state): |
|
|
|
def callcode_post(self, global_state): |
|
|
|
instr = global_state.get_current_instruction() |
|
|
|
instr = global_state.get_current_instruction() |
|
|
|
|
|
|
|
|
|
|
@ -1098,7 +1103,7 @@ class Instruction: |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def delegatecall_(self, global_state): |
|
|
|
def delegatecall_(self, global_state): |
|
|
|
instr = global_state.get_current_instruction() |
|
|
|
instr = global_state.get_current_instruction() |
|
|
|
environment = global_state.environment |
|
|
|
environment = global_state.environment |
|
|
@ -1126,7 +1131,7 @@ class Instruction: |
|
|
|
raise TransactionStartSignal(transaction, self.op_code) |
|
|
|
raise TransactionStartSignal(transaction, self.op_code) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def delegatecall_post(self, global_state): |
|
|
|
def delegatecall_post(self, global_state): |
|
|
|
instr = global_state.get_current_instruction() |
|
|
|
instr = global_state.get_current_instruction() |
|
|
|
|
|
|
|
|
|
|
@ -1170,7 +1175,7 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@PCMutator() |
|
|
|
@StateTransition() |
|
|
|
def staticcall_(self, global_state): |
|
|
|
def staticcall_(self, global_state): |
|
|
|
# TODO: implement me |
|
|
|
# TODO: implement me |
|
|
|
instr = global_state.get_current_instruction() |
|
|
|
instr = global_state.get_current_instruction() |
|
|
|