|
|
|
@ -62,6 +62,10 @@ def _check_integer_overflow(statespace, state, node): |
|
|
|
|
|
|
|
|
|
# An integer overflow is possible if op0 + op1 or op0 * op1 > MAX_UINT |
|
|
|
|
|
|
|
|
|
allowed_types = [int, BitVecRef, BitVecNumRef] |
|
|
|
|
|
|
|
|
|
if type(op0) in allowed_types and type(op1) in allowed_types: |
|
|
|
|
|
|
|
|
|
if instruction['opcode'] == "ADD": |
|
|
|
|
expr = op0 + op1 |
|
|
|
|
else: |
|
|
|
@ -127,7 +131,6 @@ def _check_integer_underflow(statespace, state, node): |
|
|
|
|
|
|
|
|
|
logging.debug("[INTEGER_UNDERFLOW] Checking SUB {0}, {1} at address {2}".format(str(op0), str(op1), |
|
|
|
|
str(instruction['address']))) |
|
|
|
|
|
|
|
|
|
allowed_types = [int, BitVecRef, BitVecNumRef] |
|
|
|
|
|
|
|
|
|
if type(op0) in allowed_types and type(op1) in allowed_types: |
|
|
|
@ -175,14 +178,16 @@ def _check_usage(state, expression): |
|
|
|
|
|
|
|
|
|
def _check_jumpi(state, expression): |
|
|
|
|
""" Check if conditional jump is dependent on the result of expression""" |
|
|
|
|
assert state.get_current_instruction()['opcode'] is 'JUMPI' |
|
|
|
|
logging.info(state.get_current_instruction()['opcode']) |
|
|
|
|
assert state.get_current_instruction()['opcode'] == 'JUMPI' |
|
|
|
|
condition = state.mstate.stack[-2] |
|
|
|
|
return str(expression) in str(condition) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
def _check_sstore(state, expression): |
|
|
|
|
""" Check if store operation is dependent on the result of expression""" |
|
|
|
|
assert state.get_current_instruction()['opcode'] is 'SSTORE' |
|
|
|
|
logging.info(state.get_current_instruction()['opcode']) |
|
|
|
|
assert state.get_current_instruction()['opcode'] == 'SSTORE' |
|
|
|
|
value = state.mstate.stack[-2] |
|
|
|
|
return str(expression) in str(value) |
|
|
|
|
|
|
|
|
|