|
|
@ -73,10 +73,22 @@ class StateTransition(object): |
|
|
|
|
|
|
|
|
|
|
|
@staticmethod |
|
|
|
@staticmethod |
|
|
|
def call_on_state_copy(func: Callable, func_obj: "Instruction", state: GlobalState): |
|
|
|
def call_on_state_copy(func: Callable, func_obj: "Instruction", state: GlobalState): |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param func: |
|
|
|
|
|
|
|
:param func_obj: |
|
|
|
|
|
|
|
:param state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
global_state_copy = copy(state) |
|
|
|
global_state_copy = copy(state) |
|
|
|
return func(func_obj, global_state_copy) |
|
|
|
return func(func_obj, global_state_copy) |
|
|
|
|
|
|
|
|
|
|
|
def increment_states_pc(self, states: List[GlobalState]) -> List[GlobalState]: |
|
|
|
def increment_states_pc(self, states: List[GlobalState]) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param states: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
if self.increment_pc: |
|
|
|
if self.increment_pc: |
|
|
|
for state in states: |
|
|
|
for state in states: |
|
|
|
state.mstate.pc += 1 |
|
|
|
state.mstate.pc += 1 |
|
|
@ -84,6 +96,11 @@ class StateTransition(object): |
|
|
|
|
|
|
|
|
|
|
|
@staticmethod |
|
|
|
@staticmethod |
|
|
|
def check_gas_usage_limit(global_state: GlobalState): |
|
|
|
def check_gas_usage_limit(global_state: GlobalState): |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
global_state.mstate.check_gas() |
|
|
|
global_state.mstate.check_gas() |
|
|
|
if isinstance(global_state.current_transaction.gas_limit, BitVecRef): |
|
|
|
if isinstance(global_state.current_transaction.gas_limit, BitVecRef): |
|
|
|
try: |
|
|
|
try: |
|
|
@ -99,6 +116,11 @@ class StateTransition(object): |
|
|
|
raise OutOfGasException() |
|
|
|
raise OutOfGasException() |
|
|
|
|
|
|
|
|
|
|
|
def accumulate_gas(self, global_state: GlobalState): |
|
|
|
def accumulate_gas(self, global_state: GlobalState): |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
if not self.enable_gas: |
|
|
|
if not self.enable_gas: |
|
|
|
return global_state |
|
|
|
return global_state |
|
|
|
opcode = global_state.instruction["opcode"] |
|
|
|
opcode = global_state.instruction["opcode"] |
|
|
@ -111,6 +133,12 @@ class StateTransition(object): |
|
|
|
def wrapper( |
|
|
|
def wrapper( |
|
|
|
func_obj: "Instruction", global_state: GlobalState |
|
|
|
func_obj: "Instruction", global_state: GlobalState |
|
|
|
) -> List[GlobalState]: |
|
|
|
) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param func_obj: |
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
new_global_states = self.call_on_state_copy(func, func_obj, global_state) |
|
|
|
new_global_states = self.call_on_state_copy(func, func_obj, global_state) |
|
|
|
new_global_states = [ |
|
|
|
new_global_states = [ |
|
|
|
self.accumulate_gas(state) for state in new_global_states |
|
|
|
self.accumulate_gas(state) for state in new_global_states |
|
|
@ -156,10 +184,20 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def jumpdest_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def jumpdest_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def push_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def push_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
push_instruction = global_state.get_current_instruction() |
|
|
|
push_instruction = global_state.get_current_instruction() |
|
|
|
push_value = push_instruction["argument"][2:] |
|
|
|
push_value = push_instruction["argument"][2:] |
|
|
|
|
|
|
|
|
|
|
@ -174,12 +212,22 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def dup_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def dup_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
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] |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def swap_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def swap_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
depth = int(self.op_code[4:]) |
|
|
|
depth = int(self.op_code[4:]) |
|
|
|
stack = global_state.mstate.stack |
|
|
|
stack = global_state.mstate.stack |
|
|
|
stack[-depth - 1], stack[-1] = stack[-1], stack[-depth - 1] |
|
|
|
stack[-depth - 1], stack[-1] = stack[-1], stack[-depth - 1] |
|
|
@ -187,11 +235,21 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def pop_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def pop_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
global_state.mstate.stack.pop() |
|
|
|
global_state.mstate.stack.pop() |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def and_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def and_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
stack = global_state.mstate.stack |
|
|
|
stack = global_state.mstate.stack |
|
|
|
op1, op2 = stack.pop(), stack.pop() |
|
|
|
op1, op2 = stack.pop(), stack.pop() |
|
|
|
if type(op1) == BoolRef: |
|
|
|
if type(op1) == BoolRef: |
|
|
@ -204,6 +262,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def or_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def or_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
stack = global_state.mstate.stack |
|
|
|
stack = global_state.mstate.stack |
|
|
|
op1, op2 = stack.pop(), stack.pop() |
|
|
|
op1, op2 = stack.pop(), stack.pop() |
|
|
|
|
|
|
|
|
|
|
@ -219,18 +282,33 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def xor_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def xor_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
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] |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def not_(self, global_state: GlobalState): |
|
|
|
def not_(self, global_state: GlobalState): |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
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] |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def byte_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def byte_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
mstate = global_state.mstate |
|
|
|
mstate = global_state.mstate |
|
|
|
op0, op1 = mstate.stack.pop(), mstate.stack.pop() |
|
|
|
op0, op1 = mstate.stack.pop(), mstate.stack.pop() |
|
|
|
if not isinstance(op1, ExprRef): |
|
|
|
if not isinstance(op1, ExprRef): |
|
|
@ -256,6 +334,11 @@ class Instruction: |
|
|
|
# Arithmetic |
|
|
|
# Arithmetic |
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def add_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def add_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
global_state.mstate.stack.append( |
|
|
|
global_state.mstate.stack.append( |
|
|
|
( |
|
|
|
( |
|
|
|
helper.pop_bitvec(global_state.mstate) |
|
|
|
helper.pop_bitvec(global_state.mstate) |
|
|
@ -266,6 +349,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def sub_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def sub_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
global_state.mstate.stack.append( |
|
|
|
global_state.mstate.stack.append( |
|
|
|
( |
|
|
|
( |
|
|
|
helper.pop_bitvec(global_state.mstate) |
|
|
|
helper.pop_bitvec(global_state.mstate) |
|
|
@ -276,6 +364,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def mul_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def mul_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
global_state.mstate.stack.append( |
|
|
|
global_state.mstate.stack.append( |
|
|
|
( |
|
|
|
( |
|
|
|
helper.pop_bitvec(global_state.mstate) |
|
|
|
helper.pop_bitvec(global_state.mstate) |
|
|
@ -286,6 +379,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def div_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def div_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
op0, op1 = ( |
|
|
|
op0, op1 = ( |
|
|
|
util.pop_bitvec(global_state.mstate), |
|
|
|
util.pop_bitvec(global_state.mstate), |
|
|
|
util.pop_bitvec(global_state.mstate), |
|
|
|
util.pop_bitvec(global_state.mstate), |
|
|
@ -298,6 +396,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def sdiv_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def sdiv_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
s0, s1 = ( |
|
|
|
s0, s1 = ( |
|
|
|
util.pop_bitvec(global_state.mstate), |
|
|
|
util.pop_bitvec(global_state.mstate), |
|
|
|
util.pop_bitvec(global_state.mstate), |
|
|
|
util.pop_bitvec(global_state.mstate), |
|
|
@ -310,6 +413,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def mod_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def mod_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
s0, s1 = ( |
|
|
|
s0, s1 = ( |
|
|
|
util.pop_bitvec(global_state.mstate), |
|
|
|
util.pop_bitvec(global_state.mstate), |
|
|
|
util.pop_bitvec(global_state.mstate), |
|
|
|
util.pop_bitvec(global_state.mstate), |
|
|
@ -319,6 +427,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def smod_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def smod_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
s0, s1 = ( |
|
|
|
s0, s1 = ( |
|
|
|
util.pop_bitvec(global_state.mstate), |
|
|
|
util.pop_bitvec(global_state.mstate), |
|
|
|
util.pop_bitvec(global_state.mstate), |
|
|
|
util.pop_bitvec(global_state.mstate), |
|
|
@ -328,6 +441,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def addmod_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def addmod_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
s0, s1, s2 = ( |
|
|
|
s0, s1, s2 = ( |
|
|
|
util.pop_bitvec(global_state.mstate), |
|
|
|
util.pop_bitvec(global_state.mstate), |
|
|
|
util.pop_bitvec(global_state.mstate), |
|
|
|
util.pop_bitvec(global_state.mstate), |
|
|
@ -338,6 +456,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def mulmod_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def mulmod_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
s0, s1, s2 = ( |
|
|
|
s0, s1, s2 = ( |
|
|
|
util.pop_bitvec(global_state.mstate), |
|
|
|
util.pop_bitvec(global_state.mstate), |
|
|
|
util.pop_bitvec(global_state.mstate), |
|
|
|
util.pop_bitvec(global_state.mstate), |
|
|
@ -348,6 +471,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def exp_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def exp_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
base, exponent = util.pop_bitvec(state), util.pop_bitvec(state) |
|
|
|
base, exponent = util.pop_bitvec(state), util.pop_bitvec(state) |
|
|
|
|
|
|
|
|
|
|
@ -366,6 +494,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def signextend_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def signextend_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
s0, s1 = state.stack.pop(), state.stack.pop() |
|
|
|
s0, s1 = state.stack.pop(), state.stack.pop() |
|
|
|
|
|
|
|
|
|
|
@ -389,6 +522,11 @@ class Instruction: |
|
|
|
# Comparisons |
|
|
|
# Comparisons |
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def lt_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def lt_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
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) |
|
|
@ -396,6 +534,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def gt_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def gt_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
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) |
|
|
@ -403,6 +546,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def slt_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def slt_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
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) |
|
|
@ -410,6 +558,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def sgt_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def sgt_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
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) |
|
|
@ -418,6 +571,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def eq_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def eq_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
|
|
|
|
|
|
|
|
op1 = state.stack.pop() |
|
|
|
op1 = state.stack.pop() |
|
|
@ -436,6 +594,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def iszero_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def iszero_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
|
|
|
|
|
|
|
|
val = state.stack.pop() |
|
|
|
val = state.stack.pop() |
|
|
@ -447,6 +610,11 @@ class Instruction: |
|
|
|
# Call data |
|
|
|
# Call data |
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def callvalue_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def callvalue_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
environment = global_state.environment |
|
|
|
environment = global_state.environment |
|
|
|
state.stack.append(environment.callvalue) |
|
|
|
state.stack.append(environment.callvalue) |
|
|
@ -455,6 +623,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def calldataload_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def calldataload_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
environment = global_state.environment |
|
|
|
environment = global_state.environment |
|
|
|
op0 = state.stack.pop() |
|
|
|
op0 = state.stack.pop() |
|
|
@ -467,6 +640,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def calldatasize_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def calldatasize_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
environment = global_state.environment |
|
|
|
environment = global_state.environment |
|
|
|
state.stack.append(environment.calldata.calldatasize) |
|
|
|
state.stack.append(environment.calldata.calldatasize) |
|
|
@ -474,6 +652,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def calldatacopy_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def calldatacopy_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
environment = global_state.environment |
|
|
|
environment = global_state.environment |
|
|
|
op0, op1, op2 = state.stack.pop(), state.stack.pop(), state.stack.pop() |
|
|
|
op0, op1, op2 = state.stack.pop(), state.stack.pop(), state.stack.pop() |
|
|
@ -568,6 +751,11 @@ class Instruction: |
|
|
|
# Environment |
|
|
|
# Environment |
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def address_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def address_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
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) |
|
|
@ -575,6 +763,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def balance_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def balance_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
address = state.stack.pop() |
|
|
|
address = state.stack.pop() |
|
|
|
state.stack.append(global_state.new_bitvec("balance_at_" + str(address), 256)) |
|
|
|
state.stack.append(global_state.new_bitvec("balance_at_" + str(address), 256)) |
|
|
@ -582,6 +775,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def origin_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def origin_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
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) |
|
|
@ -589,6 +787,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def caller_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def caller_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
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) |
|
|
@ -596,6 +799,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def codesize_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def codesize_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
environment = global_state.environment |
|
|
|
environment = global_state.environment |
|
|
|
disassembly = environment.code |
|
|
|
disassembly = environment.code |
|
|
@ -604,6 +812,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition(enable_gas=False) |
|
|
|
@StateTransition(enable_gas=False) |
|
|
|
def sha3_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def sha3_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
global keccak_function_manager |
|
|
|
global keccak_function_manager |
|
|
|
|
|
|
|
|
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
@ -650,11 +863,21 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def gasprice_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def gasprice_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
global_state.mstate.stack.append(global_state.new_bitvec("gasprice", 256)) |
|
|
|
global_state.mstate.stack.append(global_state.new_bitvec("gasprice", 256)) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def codecopy_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def codecopy_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
memory_offset, code_offset, size = ( |
|
|
|
memory_offset, code_offset, size = ( |
|
|
|
global_state.mstate.stack.pop(), |
|
|
|
global_state.mstate.stack.pop(), |
|
|
|
global_state.mstate.stack.pop(), |
|
|
|
global_state.mstate.stack.pop(), |
|
|
@ -741,6 +964,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def extcodesize_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def extcodesize_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
addr = state.stack.pop() |
|
|
|
addr = state.stack.pop() |
|
|
|
environment = global_state.environment |
|
|
|
environment = global_state.environment |
|
|
@ -767,6 +995,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def extcodecopy_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def extcodecopy_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
# FIXME: not implemented |
|
|
|
# FIXME: not implemented |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
addr = state.stack.pop() |
|
|
|
addr = state.stack.pop() |
|
|
@ -776,6 +1009,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def returndatacopy_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def returndatacopy_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
# FIXME: not implemented |
|
|
|
# FIXME: not implemented |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
start, s2, size = state.stack.pop(), state.stack.pop(), state.stack.pop() |
|
|
|
start, s2, size = state.stack.pop(), state.stack.pop(), state.stack.pop() |
|
|
@ -784,11 +1022,21 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def returndatasize_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def returndatasize_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
global_state.mstate.stack.append(global_state.new_bitvec("returndatasize", 256)) |
|
|
|
global_state.mstate.stack.append(global_state.new_bitvec("returndatasize", 256)) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def blockhash_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def blockhash_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
blocknumber = state.stack.pop() |
|
|
|
blocknumber = state.stack.pop() |
|
|
|
state.stack.append( |
|
|
|
state.stack.append( |
|
|
@ -798,21 +1046,41 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def coinbase_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def coinbase_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
global_state.mstate.stack.append(global_state.new_bitvec("coinbase", 256)) |
|
|
|
global_state.mstate.stack.append(global_state.new_bitvec("coinbase", 256)) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def timestamp_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def timestamp_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
global_state.mstate.stack.append(global_state.new_bitvec("timestamp", 256)) |
|
|
|
global_state.mstate.stack.append(global_state.new_bitvec("timestamp", 256)) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def number_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def number_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
global_state.mstate.stack.append(global_state.new_bitvec("block_number", 256)) |
|
|
|
global_state.mstate.stack.append(global_state.new_bitvec("block_number", 256)) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def difficulty_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def difficulty_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
global_state.mstate.stack.append( |
|
|
|
global_state.mstate.stack.append( |
|
|
|
global_state.new_bitvec("block_difficulty", 256) |
|
|
|
global_state.new_bitvec("block_difficulty", 256) |
|
|
|
) |
|
|
|
) |
|
|
@ -820,12 +1088,22 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def gaslimit_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def gaslimit_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
global_state.mstate.stack.append(global_state.mstate.gas_limit) |
|
|
|
global_state.mstate.stack.append(global_state.mstate.gas_limit) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
# Memory operations |
|
|
|
# Memory operations |
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def mload_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def mload_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
op0 = state.stack.pop() |
|
|
|
op0 = state.stack.pop() |
|
|
|
|
|
|
|
|
|
|
@ -849,6 +1127,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def mstore_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def mstore_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
op0, value = state.stack.pop(), state.stack.pop() |
|
|
|
op0, value = state.stack.pop(), state.stack.pop() |
|
|
|
|
|
|
|
|
|
|
@ -873,6 +1156,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def mstore8_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def mstore8_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
op0, value = state.stack.pop(), state.stack.pop() |
|
|
|
op0, value = state.stack.pop(), state.stack.pop() |
|
|
|
|
|
|
|
|
|
|
@ -896,6 +1184,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def sload_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def sload_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
global keccak_function_manager |
|
|
|
global keccak_function_manager |
|
|
|
|
|
|
|
|
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
@ -965,6 +1258,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def sstore_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def sstore_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
global keccak_function_manager |
|
|
|
global keccak_function_manager |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
index, value = state.stack.pop(), state.stack.pop() |
|
|
|
index, value = state.stack.pop(), state.stack.pop() |
|
|
@ -1041,6 +1339,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition(increment_pc=False, enable_gas=False) |
|
|
|
@StateTransition(increment_pc=False, enable_gas=False) |
|
|
|
def jump_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def jump_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
disassembly = global_state.environment.code |
|
|
|
disassembly = global_state.environment.code |
|
|
|
try: |
|
|
|
try: |
|
|
@ -1075,6 +1378,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition(increment_pc=False, enable_gas=False) |
|
|
|
@StateTransition(increment_pc=False, enable_gas=False) |
|
|
|
def jumpi_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def jumpi_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
disassembly = global_state.environment.code |
|
|
|
disassembly = global_state.environment.code |
|
|
|
min_gas, max_gas = OPCODE_GAS["JUMPI"] |
|
|
|
min_gas, max_gas = OPCODE_GAS["JUMPI"] |
|
|
@ -1144,22 +1452,42 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def pc_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def pc_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
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] |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def msize_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def msize_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
global_state.mstate.stack.append(global_state.new_bitvec("msize", 256)) |
|
|
|
global_state.mstate.stack.append(global_state.new_bitvec("msize", 256)) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def gas_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def gas_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
# TODO: Push a Constrained variable which lies between min gas and max gas |
|
|
|
# TODO: Push a Constrained variable which lies between min gas and max gas |
|
|
|
global_state.mstate.stack.append(global_state.new_bitvec("gas", 256)) |
|
|
|
global_state.mstate.stack.append(global_state.new_bitvec("gas", 256)) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def log_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def log_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
# TODO: implement me |
|
|
|
# TODO: implement me |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
dpth = int(self.op_code[3:]) |
|
|
|
dpth = int(self.op_code[3:]) |
|
|
@ -1170,6 +1498,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def create_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def create_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
# TODO: implement me |
|
|
|
# TODO: implement me |
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
state.stack.pop(), state.stack.pop(), state.stack.pop() |
|
|
|
state.stack.pop(), state.stack.pop(), state.stack.pop() |
|
|
@ -1179,6 +1512,10 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def return_(self, global_state: GlobalState): |
|
|
|
def return_(self, global_state: GlobalState): |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param 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() |
|
|
|
return_data = [global_state.new_bitvec("return_data", 8)] |
|
|
|
return_data = [global_state.new_bitvec("return_data", 8)] |
|
|
@ -1192,6 +1529,10 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def suicide_(self, global_state: GlobalState): |
|
|
|
def suicide_(self, global_state: GlobalState): |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
""" |
|
|
|
target = global_state.mstate.stack.pop() |
|
|
|
target = global_state.mstate.stack.pop() |
|
|
|
account_created = False |
|
|
|
account_created = False |
|
|
|
# Often the target of the suicide instruction will be symbolic |
|
|
|
# Often the target of the suicide instruction will be symbolic |
|
|
@ -1223,6 +1564,10 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def revert_(self, global_state: GlobalState) -> None: |
|
|
|
def revert_(self, global_state: GlobalState) -> None: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param 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() |
|
|
|
return_data = [global_state.new_bitvec("return_data", 8)] |
|
|
|
return_data = [global_state.new_bitvec("return_data", 8)] |
|
|
@ -1238,20 +1583,36 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def assert_fail_(self, global_state: GlobalState): |
|
|
|
def assert_fail_(self, global_state: GlobalState): |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
""" |
|
|
|
# 0xfe: designated invalid opcode |
|
|
|
# 0xfe: designated invalid opcode |
|
|
|
raise InvalidInstruction |
|
|
|
raise InvalidInstruction |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def invalid_(self, global_state: GlobalState): |
|
|
|
def invalid_(self, global_state: GlobalState): |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
""" |
|
|
|
raise InvalidInstruction |
|
|
|
raise InvalidInstruction |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def stop_(self, global_state: GlobalState): |
|
|
|
def stop_(self, global_state: GlobalState): |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
""" |
|
|
|
global_state.current_transaction.end(global_state) |
|
|
|
global_state.current_transaction.end(global_state) |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def call_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def call_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
instr = global_state.get_current_instruction() |
|
|
|
instr = global_state.get_current_instruction() |
|
|
|
environment = global_state.environment |
|
|
|
environment = global_state.environment |
|
|
|
|
|
|
|
|
|
|
@ -1333,6 +1694,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def call_post(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def call_post(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
instr = global_state.get_current_instruction() |
|
|
|
instr = global_state.get_current_instruction() |
|
|
|
|
|
|
|
|
|
|
|
try: |
|
|
|
try: |
|
|
@ -1395,6 +1761,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def callcode_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def callcode_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
instr = global_state.get_current_instruction() |
|
|
|
instr = global_state.get_current_instruction() |
|
|
|
environment = global_state.environment |
|
|
|
environment = global_state.environment |
|
|
|
|
|
|
|
|
|
|
@ -1429,6 +1800,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def callcode_post(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def callcode_post(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
instr = global_state.get_current_instruction() |
|
|
|
instr = global_state.get_current_instruction() |
|
|
|
|
|
|
|
|
|
|
|
try: |
|
|
|
try: |
|
|
@ -1489,6 +1865,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def delegatecall_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def delegatecall_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
instr = global_state.get_current_instruction() |
|
|
|
instr = global_state.get_current_instruction() |
|
|
|
environment = global_state.environment |
|
|
|
environment = global_state.environment |
|
|
|
|
|
|
|
|
|
|
@ -1523,6 +1904,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def delegatecall_post(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def delegatecall_post(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
instr = global_state.get_current_instruction() |
|
|
|
instr = global_state.get_current_instruction() |
|
|
|
|
|
|
|
|
|
|
|
try: |
|
|
|
try: |
|
|
@ -1583,6 +1969,11 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@StateTransition() |
|
|
|
@StateTransition() |
|
|
|
def staticcall_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
def staticcall_(self, global_state: GlobalState) -> List[GlobalState]: |
|
|
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:param global_state: |
|
|
|
|
|
|
|
:return: |
|
|
|
|
|
|
|
""" |
|
|
|
# TODO: implement me |
|
|
|
# TODO: implement me |
|
|
|
instr = global_state.get_current_instruction() |
|
|
|
instr = global_state.get_current_instruction() |
|
|
|
global_state.mstate.stack.append( |
|
|
|
global_state.mstate.stack.append( |
|
|
|