Exception (0xfe) detection and examples

mythril/analysis/modules/dependence_on_predictable_vars.py

@@ -9,7 +9,7 @@ import logging
 '''
 MODULE DESCRIPTION:
 
-Check for CALLs that send >0 Ether as a result of computation based on predictable state variables such as
+Check for CALLs that send >0 Ether as a result of computation based on predictable variables such as
 block.coinbase, block.gaslimit, block.timestamp, block.number
 
 TODO:
@@ -56,7 +56,7 @@ def execute(statespace):
             for item in found:
                 description += "- block.{}\n".format(item)
             if solve(call):
-                issue = Issue(call.node.contract_name, call.node.function_name, address, "Dependence on predictable variable", "Warning",
+                issue = Issue(call.node.contract_name, call.node.function_name, address, "Dependence on predictable environment variable", "Warning",
                               description)
                 issues.append(issue)
 

mythril/analysis/modules/exceptions.py

@@ -14,7 +14,7 @@ Check for constraints on tx.origin (i.e., access to some functionality is restri
 
 def execute(statespace):
 
-    logging.debug("Executing module: ASSERT_VIOLATION")
+    logging.debug("Executing module: EXCEPTIONS")
 
     issues = []
 
@@ -31,12 +31,13 @@ def execute(statespace):
 
                 try:
                     model = solver.get_model(node.constraints)
-                    logging.debug("[ASSERT_VIOLATION] MODEL: " + str(model))
+                    logging.debug("[EXCEPTIONS] MODEL: " + str(model))
 
                     address = state.get_current_instruction()['address']
 
-                    description = "A reachable exception has been detected (opcode 0xfe). This can be caused by a type error, division by zero, out-of-bounds array access, or assert violation.\n\n"
-                    description += "The exception is triggered under the following conditions:\n\n"
+                    description = "A reachable exception (opcode 0xfe) has been detected. This can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. "
+                    description += "Note that assert() should only be used to check invariants. Use require() for regular input checking\n"
+                    description += "This code path is executed under the following conditions:\n\n"
 
                     for d in model.decls():
 
@@ -47,7 +48,7 @@ def execute(statespace):
 
                         description += ("%s: %s\n" % (d.name(), condition))
 
-                    description += "\nNote that assert() should only be used to check invariants. Use require() for regular input checking.\n"
+                    description += "\n"
 
                     issues.append(Issue(node.contract_name, node.function_name, address, "Assertion violation", "Informational", description))
 

solidity_examples/exceptions.sol

@@ -0,0 +1,39 @@
+contract Exceptions {
+
+    uint256[8] myarray;
+
+    function assert1() {
+    	uint256 i = 1;
+        assert(i == 0);
+    }
+
+    function assert2() {
+    	uint256 i = 1;
+        assert(i > 0);
+    }
+
+    function assert3(uint256 input) {
+        assert(input != 23);
+    }
+
+    function divisionby0(uint256 input) {
+        uint256 i = 1/input;
+    }
+
+    function thisisfine(uint256 input) {
+        if (input > 0) {
+            uint256 i = 1/input;
+        }
+    }    
+
+    function arrayaccess(uint256 index) {
+        uint256 i = myarray[index];
+    }
+
+    function thisisalsofind(uint256 index) {
+        if (index < 8) {
+            uint256 i = myarray[index];
+        }
+    }
+
+}

solidity_examples/invalid_opcodes.sol

@@ -1,16 +0,0 @@
-contract InvalidOpcodes {
-    
-    function assert1() {
-    	uint256 i = 1;
-        assert(i == 0);
-    }
-
-    function assert2() {
-    	uint256 i = 1;
-        assert(i > 0);
-    }
-
-    function assert3(uint input) {
-        assert(input != 23);
-    }
-}