Support Panic(uint256) calls for asserts in v0.8.0+ (#1514)

* Support panic() asserts

* Use typing extensions

mythril/analysis/module/base.py

@@ -4,7 +4,7 @@ This module includes an definition of the DetectionModule interface.
 DetectionModules implement different analysis rules to find weaknesses and vulnerabilities.
 """
 import logging
-from typing import List, Set, Optional
+from typing import List, Set, Optional, Tuple, Union
 
 from mythril.analysis.report import Issue
 from mythril.laser.ethereum.state.global_state import GlobalState
@@ -51,7 +51,7 @@ class DetectionModule(ABC):
 
     def __init__(self) -> None:
         self.issues = []  # type: List[Issue]
-        self.cache = set()  # type: Set[int]
+        self.cache = set()  # type: Set[Optional[Union[int, Tuple[int, str]]]]
 
     def reset_module(self):
         """ Resets the storage of this module """

mythril/analysis/module/modules/exceptions.py

@@ -1,15 +1,20 @@
 """This module contains the detection code for reachable exceptions."""
 import logging
 
+from typing import List
 from mythril.analysis import solver
 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 import util
 
 log = logging.getLogger(__name__)
 
+# The function signature of Panic(uint256)
+PANIC_SIGNATURE = [78, 72, 123, 113]
+
 
 class Exceptions(DetectionModule):
     """"""
@@ -18,7 +23,7 @@ class Exceptions(DetectionModule):
     swc_id = ASSERT_VIOLATION
     description = "Checks whether any exception states are reachable."
     entry_point = EntryPoint.CALLBACK
-    pre_hooks = ["ASSERT_FAIL"]
+    pre_hooks = ["ASSERT_FAIL", "REVERT"]
 
     def _execute(self, state: GlobalState) -> None:
         """
@@ -26,25 +31,33 @@ class Exceptions(DetectionModule):
         :param state:
         :return:
         """
-        if state.get_current_instruction()["address"] in self.cache:
+        if (
+            state.get_current_instruction()["address"],
+            state.environment.active_function_name,
+        ) in self.cache:
             return
         issues = self._analyze_state(state)
         for issue in issues:
-            self.cache.add(issue.address)
+            self.cache.add((issue.address, issue.function))
         self.issues.extend(issues)
 
     @staticmethod
-    def _analyze_state(state) -> list:
+    def _analyze_state(state) -> List[Issue]:
         """
 
         :param state:
         :return:
         """
-        log.debug("ASSERT_FAIL in function " + state.environment.active_function_name)
+        opcode = state.get_current_instruction()["opcode"]
+        if opcode == "REVERT" and not is_assertion_failure(state):
+            return []
+
+        log.debug(
+            "ASSERT_FAIL/REVERT in function " + state.environment.active_function_name
+        )
 
         try:
             address = state.get_current_instruction()["address"]
-
             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 "
@@ -76,4 +89,17 @@ class Exceptions(DetectionModule):
         return []
 
 
+def is_assertion_failure(global_state):
+    state = global_state.mstate
+    offset, length = state.stack.pop(), state.stack.pop()
+    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()

mythril/analysis/module/modules/unchecked_retval.py

@@ -1,7 +1,7 @@
 """This module contains detection code to find occurrences of calls whose
 return value remains unchecked."""
 from copy import copy
-from typing import cast, List, Union, Mapping
+from typing import cast, List
 
 from mythril.analysis import solver
 from mythril.analysis.report import Issue
@@ -14,13 +14,19 @@ from mythril.laser.ethereum.state.annotation import StateAnnotation
 from mythril.laser.ethereum.state.global_state import GlobalState
 
 import logging
+from typing_extensions import TypedDict
 
 log = logging.getLogger(__name__)
 
 
+class RetVal(TypedDict):
+    address: int
+    retval: BitVec
+
+
 class UncheckedRetvalAnnotation(StateAnnotation):
     def __init__(self) -> None:
-        self.retvals = []  # type: List[Mapping[str, Union[int, BitVec]]]
+        self.retvals: List[RetVal] = []
 
     def __copy__(self):
         result = UncheckedRetvalAnnotation()

mythril/analysis/report.py

@@ -23,12 +23,12 @@ class Issue:
 
     def __init__(
         self,
-        contract,
-        function_name,
-        address,
-        swc_id,
-        title,
-        bytecode,
+        contract: str,
+        function_name: str,
+        address: int,
+        swc_id: str,
+        title: str,
+        bytecode: str,
         gas_used=(None, None),
         severity=None,
         description_head="",
@@ -224,7 +224,11 @@ class Report:
         :param issue:
         """
         m = hashlib.md5()
-        m.update((issue.contract + str(issue.address) + issue.title).encode("utf-8"))
+        m.update(
+            (issue.contract + issue.function + str(issue.address) + issue.title).encode(
+                "utf-8"
+            )
+        )
         issue.resolve_function_names()
         self.issues[m.digest()] = issue
 

tests/integration_tests/analysis_tests.py

@@ -18,6 +18,17 @@ test_data = (
         },
         "0xab12585800000000000000000000000000000000000000000000000000000000000004d2",
     ),
+    (
+        "exceptions_0.8.0.sol.o",
+        {
+            "TX_COUNT": 1,
+            "TX_OUTPUT": 1,
+            "MODULE": "Exceptions",
+            "ISSUE_COUNT": 2,
+            "ISSUE_NUMBER": 0,
+        },
+        None,
+    ),
 )
 
 
@@ -28,5 +39,8 @@ def test_analysis(file_name, tx_data, calldata):
     output = json.loads(check_output(command, shell=True).decode("UTF-8"))
 
     assert len(output[0]["issues"]) == tx_data["ISSUE_COUNT"]
-    test_case = output[0]["issues"][tx_data["ISSUE_NUMBER"]]["extra"]["testCases"][0]
-    assert test_case["steps"][tx_data["TX_OUTPUT"]]["input"] == calldata
+    if calldata:
+        test_case = output[0]["issues"][tx_data["ISSUE_NUMBER"]]["extra"]["testCases"][
+            0
+        ]
+        assert test_case["steps"][tx_data["TX_OUTPUT"]]["input"] == calldata

tests/testdata/input_contracts/exceptions_0.8.0.sol

@@ -0,0 +1,21 @@
+pragma solidity ^0.8.0;
+
+
+contract Exceptions {
+
+    uint val;
+
+    function change_val() public {
+        val = 1;
+    }
+    function assert1() public pure {
+    	uint256 i = 1;
+        assert(i == 0);
+    }
+
+    function fail() public view {
+        assert(val==2);
+    }
+
+
+}

tests/testdata/inputs/exceptions_0.8.0.sol.o

@@ -0,0 +1 @@
+608060405234801561001057600080fd5b5060f18061001f6000396000f3fe6080604052348015600f57600080fd5b5060043610603c5760003560e01c8063a02f5b99146041578063a9cc4718146049578063b34c3610146051575b600080fd5b60476059565b005b604f6063565b005b60576075565b005b6001600081905550565b6002600054146073576072608c565b5b565b600060019050600081146089576088608c565b5b50565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052600160045260246000fdfea2646970667358221220cdbce6751f5dd32798edbe8c5cefae09753627f94e3f6e4a1f33afdb28a32e5464736f6c63430008060033