"""This module contains the detection code for reachable exceptions."""
import logging
from typing import cast, List, Optional
from mythril.analysis import solver
from mythril.analysis.issue_annotation import IssueAnnotation
from mythril.analysis.module.base import DetectionModule, EntryPoint
from mythril.analysis.report import Issue
from mythril.analysis.swc_data import ASSERT_VIOLATION
from mythril.exceptions import UnsatError
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.ethereum.state.annotation import StateAnnotation
from mythril.laser.ethereum import util
from mythril.laser.smt import And
from mythril.support.support_utils import get_code_hash
log = logging.getLogger(__name__)
# The function signature of Panic(uint256)
PANIC_SIGNATURE = [78, 72, 123, 113]
[docs]class LastJumpAnnotation(StateAnnotation):
"""State Annotation used if an overflow is both possible and used in the annotated path"""
def __init__(self, last_jump: Optional[int] = None) -> None:
self.last_jump: int = last_jump
def __copy__(self):
new_annotation = LastJumpAnnotation(self.last_jump)
return new_annotation
[docs]class Exceptions(DetectionModule):
""""""
name = "Assertion violation"
swc_id = ASSERT_VIOLATION
description = "Checks whether any exception states are reachable."
entry_point = EntryPoint.CALLBACK
pre_hooks = ["INVALID", "JUMP", "REVERT"]
def __init__(self):
super().__init__()
self.auto_cache = False
def _execute(self, state: GlobalState) -> List[Issue]:
"""
:param state:
:return:
"""
issues = self._analyze_state(state)
for issue in issues:
self.cache.add((issue.source_location, issue.bytecode_hash))
return issues
def _analyze_state(self, state) -> List[Issue]:
"""
:param state:
:return:
"""
opcode = state.get_current_instruction()["opcode"]
address = state.get_current_instruction()["address"]
annotations = cast(
List[LastJumpAnnotation],
[a for a in state.get_annotations(LastJumpAnnotation)],
)
if len(annotations) == 0:
state.annotate(LastJumpAnnotation())
annotations = cast(
List[LastJumpAnnotation],
[a for a in state.get_annotations(LastJumpAnnotation)],
)
if opcode == "JUMP":
annotations[0].last_jump = address
return []
if opcode == "REVERT" and not is_assertion_failure(state):
return []
cache_address = annotations[0].last_jump
if (
cache_address,
get_code_hash(state.environment.code.bytecode),
) in self.cache:
return []
log.debug(
"ASSERT_FAIL/REVERT in function " + state.environment.active_function_name
)
try:
description_tail = (
"It is possible to trigger an assertion violation. Note that Solidity assert() statements should "
"only be used to check invariants. Review the transaction trace generated for this issue and "
"either make sure your program logic is correct, or use require() instead of assert() if your goal "
"is to constrain user inputs or enforce preconditions. Remember to validate inputs from both callers "
"(for instance, via passed arguments) and callees (for instance, via return values)."
)
transaction_sequence = solver.get_transaction_sequence(
state, state.world_state.constraints
)
issue = Issue(
contract=state.environment.active_account.contract_name,
function_name=state.environment.active_function_name,
address=address,
swc_id=ASSERT_VIOLATION,
title="Exception State",
severity="Medium",
description_head="An assertion violation was triggered.",
description_tail=description_tail,
bytecode=state.environment.code.bytecode,
transaction_sequence=transaction_sequence,
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
source_location=cache_address,
)
state.annotate(
IssueAnnotation(
conditions=[And(*state.world_state.constraints)],
issue=issue,
detector=self,
)
)
return [issue]
except UnsatError:
log.debug("no model found")
return []
[docs]def is_assertion_failure(global_state):
state = global_state.mstate
offset, length = state.stack[-1], state.stack[-2]
try:
return_data = state.memory[
util.get_concrete_int(offset) : util.get_concrete_int(offset + length)
]
except TypeError:
return False
return return_data[:4] == PANIC_SIGNATURE and return_data[-1] == 1
detector = Exceptions()