Merge latest develop branch

mythril/analysis/modules/integer.py

@@ -75,10 +75,13 @@ class IntegerOverflowUnderflowModule(DetectionModule):
             op1 = BitVecVal(op1, 256)
 
         # Formulate expression
+        # FIXME: handle exponentiation
         if instruction["opcode"] == "ADD":
+            operator = "add"
             expr = op0 + op1
             # constraint = Not(BVAddNoOverflow(op0, op1, signed=False))
         else:
+            operator = "multiply"
             expr = op1 * op0
             # constraint = Not(BVMulNoOverflow(op0, op1, signed=False))
 
@@ -90,11 +93,6 @@ class IntegerOverflowUnderflowModule(DetectionModule):
             logging.debug("[INTEGER_OVERFLOW] no model found")
             return issues
 
-        if not self._verify_integer_overflow(
-            statespace, node, expr, state, model, constraint, op0, op1
-        ):
-            return issues
-
         # Build issue
         issue = Issue(
             contract=node.contract_name,
@@ -106,7 +104,9 @@ class IntegerOverflowUnderflowModule(DetectionModule):
             _type="Warning",
         )
 
-        issue.description = "The arithmetic operation can result in integer overflow.\n"
+        issue.description = "This binary {} operation can result in integer overflow.\n".format(
+            operator
+        )
         issue.debug = "Transaction Sequence: " + str(
             solver.get_transaction_sequence(state, node.constraints)
         )

tests/testdata/outputs_expected/ether_send.sol.o.json

@@ -1 +1 @@
-{"error": null, "issues": [{"address": 722, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "It seems that an attacker is able to execute an call instruction, this can mean that the attacker is able to extract funds out of the contract.", "function": "withdrawfunds()", "swc_id": "105", "title": "Ether send", "type": "Warning"}, {"address": 883, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The arithmetic operation can result in integer overflow.\n", "function": "invest()", "swc_id": "101", "title": "Integer Overflow", "type": "Warning"}], "success": true}
+{"error": null, "issues": [{"address": 722, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "It seems that an attacker is able to execute an call instruction, this can mean that the attacker is able to extract funds out of the contract.", "function": "withdrawfunds()", "swc_id": "105", "title": "Ether send", "type": "Warning"}, {"address": 883, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "This binary add operation can result in integer overflow.\n", "function": "invest()", "swc_id": "101", "title": "Integer Overflow", "type": "Warning"}], "success": true}

tests/testdata/outputs_expected/ether_send.sol.o.markdown

@@ -20,4 +20,4 @@ It seems that an attacker is able to execute an call instruction, this can mean
 
 ### Description
 
-The arithmetic operation can result in integer overflow.
+This binary add operation can result in integer overflow.

tests/testdata/outputs_expected/ether_send.sol.o.text

@@ -13,7 +13,7 @@ Type: Warning
 Contract: Unknown
 Function name: invest()
 PC address: 883
-The arithmetic operation can result in integer overflow.
+This binary add operation can result in integer overflow.
 
 --------------------
 

tests/testdata/outputs_expected/overflow.sol.o.json

@@ -1 +1 @@
-{"error": null, "issues": [{"address": 567, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The subtraction can result in an integer underflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Underflow", "type": "Warning"}, {"address": 649, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The subtraction can result in an integer underflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Underflow", "type": "Warning"}, {"address": 725, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The arithmetic operation can result in integer overflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Overflow", "type": "Warning"}], "success": true}
+{"error": null, "issues": [{"address": 567, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The subtraction can result in an integer underflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Underflow", "type": "Warning"}, {"address": 649, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The subtraction can result in an integer underflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Underflow", "type": "Warning"}, {"address": 725, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "This binary add operation can result in integer overflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Overflow", "type": "Warning"}], "success": true}

tests/testdata/outputs_expected/overflow.sol.o.markdown

@@ -31,4 +31,4 @@ The subtraction can result in an integer underflow.
 
 ### Description
 
-The arithmetic operation can result in integer overflow.
+This binary add operation can result in integer overflow.

tests/testdata/outputs_expected/overflow.sol.o.text

@@ -24,7 +24,7 @@ Type: Warning
 Contract: Unknown
 Function name: sendeth(address,uint256)
 PC address: 725
-The arithmetic operation can result in integer overflow.
+This binary add operation can result in integer overflow.
 
 --------------------
 

tests/testdata/outputs_expected/underflow.sol.o.json

@@ -1 +1 @@
-{"error": null, "issues": [{"address": 567, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The subtraction can result in an integer underflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Underflow", "type": "Warning"}, {"address": 649, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The subtraction can result in an integer underflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Underflow", "type": "Warning"}, {"address": 725, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The arithmetic operation can result in integer overflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Overflow", "type": "Warning"}], "success": true}
+{"error": null, "issues": [{"address": 567, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The subtraction can result in an integer underflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Underflow", "type": "Warning"}, {"address": 649, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The subtraction can result in an integer underflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Underflow", "type": "Warning"}, {"address": 725, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "This binary add operation can result in integer overflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Overflow", "type": "Warning"}], "success": true}

tests/testdata/outputs_expected/underflow.sol.o.markdown

@@ -31,4 +31,4 @@ The subtraction can result in an integer underflow.
 
 ### Description
 
-The arithmetic operation can result in integer overflow.
+This binary add operation can result in integer overflow.

tests/testdata/outputs_expected/underflow.sol.o.text

@@ -24,7 +24,7 @@ Type: Warning
 Contract: Unknown
 Function name: sendeth(address,uint256)
 PC address: 725
-The arithmetic operation can result in integer overflow.
+This binary add operation can result in integer overflow.
 
 --------------------