Merge pull request #141 from JoranHonig/bugfix/maxuint

Assertion change in integer.py and fix flaky tests

mythril/analysis/modules/integer.py

@@ -15,9 +15,6 @@ For every SUB instruction, check if there's a possible state where op1 > op0.
 For every ADD, MUL instruction, check if there's a possible state where op1 + op0 > 2^32 - 1
 '''
 
-MAX_UINT = 2 ** 256 - 1
-
-
 def execute(statespace):
     """
     Executes analysis module for integer underflow and integer overflow
@@ -72,7 +69,7 @@ def _check_integer_overflow(statespace, state, node):
         expr = op0 * op1
 
     # Check satisfiable
-    constraint = UGT(expr, MAX_UINT)
+    constraint = Or(ULT(expr, op0), ULT(expr, op1))
     model = _try_constraints(node.constraints, [constraint])
 
     if model is None:

mythril/analysis/solver.py

@@ -4,7 +4,7 @@ from mythril.exceptions import UnsatError
 
 def get_model(constraints):
     s = Solver()
-    s.set("timeout", 2000)
+    s.set("timeout", 10000)
 
     for constraint in constraints:
         s.add(constraint)

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

@@ -9,6 +9,14 @@
             "type": "Warning",
             "address": 816,
             "debug": "<DEBUG-DATA>"
+        },
+        {
+            "title": "Integer Overflow ",
+            "description": "A possible integer overflow exists in the function `invest()`.\nThe addition or multiplication may result in a value higher than the maximum representable integer.",
+            "function": "invest()",
+            "type": "Warning",
+            "address": 483,
+            "debug": "<DEBUG-DATA>"
         }
     ]
 }

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

@@ -11,4 +11,16 @@
 
 In the function `withdrawfunds()` a non-zero amount of Ether is sent to msg.sender.
 
-There is a check on storage index 1. This storage slot can be written to by calling the function `crowdfunding()`.
+There is a check on storage index 1. This storage slot can be written to by calling the function `crowdfunding()`.
+
+## Integer Overflow 
+
+- Type: Warning
+- Contract: Unknown
+- Function name: `invest()`
+- PC address: 483
+
+### Description
+
+A possible integer overflow exists in the function `invest()`.
+The addition or multiplication may result in a value higher than the maximum representable integer.

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

@@ -8,3 +8,12 @@ In the function `withdrawfunds()` a non-zero amount of Ether is sent to msg.send
 There is a check on storage index 1. This storage slot can be written to by calling the function `crowdfunding()`.
 --------------------
 
+==== Integer Overflow  ====
+Type: Warning
+Contract: Unknown
+Function name: invest()
+PC address: 483
+A possible integer overflow exists in the function `invest()`.
+The addition or multiplication may result in a value higher than the maximum representable integer.
+--------------------
+

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

@@ -1,5 +1,14 @@
 {
     "success": true,
     "error": null,
-    "issues": []
+    "issues": [
+        {
+            "title": "Integer Overflow ",
+            "description": "A possible integer overflow exists in the function `sendToken(address,uint256)`.\nThe addition or multiplication may result in a value higher than the maximum representable integer.",
+            "function": "sendToken(address,uint256)",
+            "type": "Warning",
+            "address": 498,
+            "debug": "<DEBUG-DATA>"
+        }
+    ]
 }

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

@@ -0,0 +1,13 @@
+# Analysis results for test-filename.sol
+
+## Integer Overflow 
+
+- Type: Warning
+- Contract: Unknown
+- Function name: `sendToken(address,uint256)`
+- PC address: 498
+
+### Description
+
+A possible integer overflow exists in the function `sendToken(address,uint256)`.
+The addition or multiplication may result in a value higher than the maximum representable integer.

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

@@ -0,0 +1,9 @@
+==== Integer Overflow  ====
+Type: Warning
+Contract: Unknown
+Function name: sendToken(address,uint256)
+PC address: 498
+A possible integer overflow exists in the function `sendToken(address,uint256)`.
+The addition or multiplication may result in a value higher than the maximum representable integer.
+--------------------
+

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

@@ -10,6 +10,14 @@
             "address": 649,
             "debug": "<DEBUG-DATA>"
         },
+        {
+            "title": "Integer Overflow ",
+            "description": "A possible integer overflow exists in the function `sendeth(address,uint256)`.\nThe addition or multiplication may result in a value higher than the maximum representable integer.",
+            "function": "sendeth(address,uint256)",
+            "type": "Warning",
+            "address": 725,
+            "debug": "<DEBUG-DATA>"
+        },
         {
             "title": "Integer Underflow",
             "description": "A possible integer underflow exists in the function `sendeth(address,uint256)`.\nThe subtraction may result in a value < 0.",

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

@@ -12,6 +12,18 @@
 A possible integer underflow exists in the function `sendeth(address,uint256)`.
 The subtraction may result in a value < 0.
 
+## Integer Overflow 
+
+- Type: Warning
+- Contract: Unknown
+- Function name: `sendeth(address,uint256)`
+- PC address: 725
+
+### Description
+
+A possible integer overflow exists in the function `sendeth(address,uint256)`.
+The addition or multiplication may result in a value higher than the maximum representable integer.
+
 ## Integer Underflow
 
 - Type: Warning

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

@@ -7,6 +7,15 @@ A possible integer underflow exists in the function `sendeth(address,uint256)`.
 The subtraction may result in a value < 0.
 --------------------
 
+==== Integer Overflow  ====
+Type: Warning
+Contract: Unknown
+Function name: sendeth(address,uint256)
+PC address: 725
+A possible integer overflow exists in the function `sendeth(address,uint256)`.
+The addition or multiplication may result in a value higher than the maximum representable integer.
+--------------------
+
 ==== Integer Underflow ====
 Type: Warning
 Contract: Unknown

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

@@ -12,12 +12,20 @@
         },
         {
             "title": "Ether send",
-            "description": "In the function `_function_0x686f2c90` a non-zero amount of Ether is sent to an address taken from storage slot 5.\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\n\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.",
-            "function": "_function_0x686f2c90",
+            "description": "In the function `_function_0xb4022950` a non-zero amount of Ether is sent to an address taken from storage slot 5.\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\n\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.",
+            "function": "_function_0xb4022950",
             "type": "Warning",
             "address": 1940,
             "debug": "<DEBUG-DATA>"
         },
+        {
+            "title": "Ether send",
+            "description": "In the function `_function_0xb4022950` a non-zero amount of Ether is sent to an address taken from storage slot 5.\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\n\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.",
+            "function": "_function_0xb4022950",
+            "type": "Warning",
+            "address": 2582,
+            "debug": "<DEBUG-DATA>"
+        },
         {
             "title": "Exception state",
             "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. This is acceptable in most situations. Note however that `assert()` should only be used to check invariants. Use `require()` for regular input checking. ",

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

@@ -19,16 +19,36 @@ There is a check on storage index 1. This storage slot can be written to by call
 
 - Type: Warning
 - Contract: Unknown
-- Function name: `_function_0x686f2c90`
+- Function name: `_function_0xb4022950`
 - PC address: 1940
 
 ### Description
 
-In the function `_function_0x686f2c90` a non-zero amount of Ether is sent to an address taken from storage slot 5.
+In the function `_function_0xb4022950` a non-zero amount of Ether is sent to an address taken from storage slot 5.
+There is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.
+
+There is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.
+There is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.
+There is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.
+There is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.
+
+## Ether send
+
+- Type: Warning
+- Contract: Unknown
+- Function name: `_function_0xb4022950`
+- PC address: 2582
+
+### Description
+
+In the function `_function_0xb4022950` a non-zero amount of Ether is sent to an address taken from storage slot 5.
 There is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.
 
 There is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.
 There is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.
+There is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.
+There is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.
+There is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.
 
 ## Exception state
 

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

@@ -13,13 +13,30 @@ There is a check on storage index 1. This storage slot can be written to by call
 ==== Ether send ====
 Type: Warning
 Contract: Unknown
-Function name: _function_0x686f2c90
+Function name: _function_0xb4022950
 PC address: 1940
-In the function `_function_0x686f2c90` a non-zero amount of Ether is sent to an address taken from storage slot 5.
+In the function `_function_0xb4022950` a non-zero amount of Ether is sent to an address taken from storage slot 5.
 There is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.
 
 There is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.
 There is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.
+There is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.
+There is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.
+--------------------
+
+==== Ether send ====
+Type: Warning
+Contract: Unknown
+Function name: _function_0xb4022950
+PC address: 2582
+In the function `_function_0xb4022950` a non-zero amount of Ether is sent to an address taken from storage slot 5.
+There is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.
+
+There is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.
+There is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.
+There is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.
+There is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.
+There is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.
 --------------------
 
 ==== Exception state ====

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

@@ -10,6 +10,14 @@
             "address": 649,
             "debug": "<DEBUG-DATA>"
         },
+        {
+            "title": "Integer Overflow ",
+            "description": "A possible integer overflow exists in the function `sendeth(address,uint256)`.\nThe addition or multiplication may result in a value higher than the maximum representable integer.",
+            "function": "sendeth(address,uint256)",
+            "type": "Warning",
+            "address": 725,
+            "debug": "<DEBUG-DATA>"
+        },
         {
             "title": "Integer Underflow",
             "description": "A possible integer underflow exists in the function `sendeth(address,uint256)`.\nThe subtraction may result in a value < 0.",

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

@@ -12,6 +12,18 @@
 A possible integer underflow exists in the function `sendeth(address,uint256)`.
 The subtraction may result in a value < 0.
 
+## Integer Overflow 
+
+- Type: Warning
+- Contract: Unknown
+- Function name: `sendeth(address,uint256)`
+- PC address: 725
+
+### Description
+
+A possible integer overflow exists in the function `sendeth(address,uint256)`.
+The addition or multiplication may result in a value higher than the maximum representable integer.
+
 ## Integer Underflow
 
 - Type: Warning

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

@@ -7,6 +7,15 @@ A possible integer underflow exists in the function `sendeth(address,uint256)`.
 The subtraction may result in a value < 0.
 --------------------
 
+==== Integer Overflow  ====
+Type: Warning
+Contract: Unknown
+Function name: sendeth(address,uint256)
+PC address: 725
+A possible integer overflow exists in the function `sendeth(address,uint256)`.
+The addition or multiplication may result in a value higher than the maximum representable integer.
+--------------------
+
 ==== Integer Underflow ====
 Type: Warning
 Contract: Unknown