diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index e0c2c785..5b327189 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1384,12 +1384,12 @@ class Instruction: key_argument = keccak_function_manager.get_argument(keccak_key) index_argument = keccak_function_manager.get_argument(index) condition = index_argument == key_argument - condition = ( + condition_z3 = ( condition if isinstance(condition, Bool) else symbol_factory.Bool(condition) ) - constraints.append((keccak_key, condition)) + constraints.append((keccak_key, condition_z3)) for (keccak_key, constraint) in constraints: if constraint in state.constraints: diff --git a/tests/laser/evm_testsuite/evm_test.py b/tests/laser/evm_testsuite/evm_test.py index 6227b3ce..54d16b22 100644 --- a/tests/laser/evm_testsuite/evm_test.py +++ b/tests/laser/evm_testsuite/evm_test.py @@ -136,10 +136,10 @@ def test_vmtest( assert account.nonce == int(details["nonce"], 16) assert account.code.bytecode == details["code"][2:] - + print(account.storage._storage, details["storage"]) for index, value in details["storage"].items(): expected = int(value, 16) - actual = account.storage[int(index, 16)] + actual = account.storage[str(int(index, 16))] if isinstance(actual, Expression): actual = actual.value actual = 1 if actual is True else 0 if actual is False else actual diff --git a/tests/testdata/outputs_expected/overflow.sol.o.graph.html b/tests/testdata/outputs_expected/overflow.sol.o.graph.html index 70210177..a245f3a4 100644 --- a/tests/testdata/outputs_expected/overflow.sol.o.graph.html +++ b/tests/testdata/outputs_expected/overflow.sol.o.graph.html @@ -24,8 +24,8 @@ @@ -59,4 +59,4 @@ }); - + \ No newline at end of file diff --git a/tests/testdata/outputs_expected/overflow.sol.o.json b/tests/testdata/outputs_expected/overflow.sol.o.json index 89fdb839..c8d029f7 100644 --- a/tests/testdata/outputs_expected/overflow.sol.o.json +++ b/tests/testdata/outputs_expected/overflow.sol.o.json @@ -26,6 +26,19 @@ "sourceMap": null, "swc-id": "101", "title": "Integer Underflow" + }, + { + "address": 725, + "contract": "Unknown", + "debug": "", + "description": "The binary addition can overflow.\nThe operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.", + "function": "sendeth(address,uint256)", + "max_gas_used": 78155, + "min_gas_used": 17019, + "severity": "High", + "sourceMap": null, + "swc-id": "101", + "title": "Integer Overflow" } ], "success": true diff --git a/tests/testdata/outputs_expected/overflow.sol.o.jsonv2 b/tests/testdata/outputs_expected/overflow.sol.o.jsonv2 index dfcc29d5..570fdeba 100644 --- a/tests/testdata/outputs_expected/overflow.sol.o.jsonv2 +++ b/tests/testdata/outputs_expected/overflow.sol.o.jsonv2 @@ -34,6 +34,23 @@ "severity": "High", "swcID": "SWC-101", "swcTitle": "Integer Overflow and Underflow" + }, + { + "description": { + "head": "The binary addition can overflow.", + "tail": "The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion." + }, + "extra": { + "discoveryTime": "" + }, + "locations": [ + { + "sourceMap": "725:1:0" + } + ], + "severity": "High", + "swcID": "SWC-101", + "swcTitle": "Integer Overflow and Underflow" } ], "meta": {}, diff --git a/tests/testdata/outputs_expected/overflow.sol.o.markdown b/tests/testdata/outputs_expected/overflow.sol.o.markdown index 8774d894..82642a1e 100644 --- a/tests/testdata/outputs_expected/overflow.sol.o.markdown +++ b/tests/testdata/outputs_expected/overflow.sol.o.markdown @@ -25,3 +25,16 @@ The operands of the subtraction operation are not sufficiently constrained. The The binary subtraction can underflow. The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion. + +## Integer Overflow +- SWC ID: 101 +- Severity: High +- Contract: Unknown +- Function name: `sendeth(address,uint256)` +- PC address: 725 +- Estimated Gas Usage: 17019 - 78155 + +### Description + +The binary addition can overflow. +The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion. diff --git a/tests/testdata/outputs_expected/overflow.sol.o.text b/tests/testdata/outputs_expected/overflow.sol.o.text index 698665d8..e70dda5b 100644 --- a/tests/testdata/outputs_expected/overflow.sol.o.text +++ b/tests/testdata/outputs_expected/overflow.sol.o.text @@ -20,3 +20,14 @@ The binary subtraction can underflow. The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion. -------------------- +==== Integer Overflow ==== +SWC ID: 101 +Severity: High +Contract: Unknown +Function name: sendeth(address,uint256) +PC address: 725 +Estimated Gas Usage: 17019 - 78155 +The binary addition can overflow. +The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion. +-------------------- + diff --git a/tests/testdata/outputs_expected/underflow.sol.o.graph.html b/tests/testdata/outputs_expected/underflow.sol.o.graph.html index 62381211..64d31932 100644 --- a/tests/testdata/outputs_expected/underflow.sol.o.graph.html +++ b/tests/testdata/outputs_expected/underflow.sol.o.graph.html @@ -24,8 +24,8 @@ diff --git a/tests/testdata/outputs_expected/underflow.sol.o.json b/tests/testdata/outputs_expected/underflow.sol.o.json index 6a2464d5..a0042598 100644 --- a/tests/testdata/outputs_expected/underflow.sol.o.json +++ b/tests/testdata/outputs_expected/underflow.sol.o.json @@ -26,6 +26,19 @@ "sourceMap": null, "swc-id": "101", "title": "Integer Underflow" + }, + { + "address": 725, + "contract": "Unknown", + "debug": "", + "description": "The binary addition can overflow.\nThe operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.", + "function": "sendeth(address,uint256)", + "max_gas_used": 52861, + "min_gas_used": 11915, + "severity": "High", + "sourceMap": null, + "swc-id": "101", + "title": "Integer Overflow" } ], "success": true diff --git a/tests/testdata/outputs_expected/underflow.sol.o.jsonv2 b/tests/testdata/outputs_expected/underflow.sol.o.jsonv2 index 94854e04..b6611bdd 100644 --- a/tests/testdata/outputs_expected/underflow.sol.o.jsonv2 +++ b/tests/testdata/outputs_expected/underflow.sol.o.jsonv2 @@ -34,6 +34,23 @@ "severity": "High", "swcID": "SWC-101", "swcTitle": "Integer Overflow and Underflow" + }, + { + "description": { + "head": "The binary addition can overflow.", + "tail": "The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion." + }, + "extra": { + "discoveryTime": "" + }, + "locations": [ + { + "sourceMap": "725:1:0" + } + ], + "severity": "High", + "swcID": "SWC-101", + "swcTitle": "Integer Overflow and Underflow" } ], "meta": {}, diff --git a/tests/testdata/outputs_expected/underflow.sol.o.markdown b/tests/testdata/outputs_expected/underflow.sol.o.markdown index 48399072..acc444d4 100644 --- a/tests/testdata/outputs_expected/underflow.sol.o.markdown +++ b/tests/testdata/outputs_expected/underflow.sol.o.markdown @@ -25,3 +25,16 @@ The operands of the subtraction operation are not sufficiently constrained. The The binary subtraction can underflow. The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion. + +## Integer Overflow +- SWC ID: 101 +- Severity: High +- Contract: Unknown +- Function name: `sendeth(address,uint256)` +- PC address: 725 +- Estimated Gas Usage: 11915 - 52861 + +### Description + +The binary addition can overflow. +The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion. diff --git a/tests/testdata/outputs_expected/underflow.sol.o.text b/tests/testdata/outputs_expected/underflow.sol.o.text index 16701a04..498ff588 100644 --- a/tests/testdata/outputs_expected/underflow.sol.o.text +++ b/tests/testdata/outputs_expected/underflow.sol.o.text @@ -20,3 +20,14 @@ The binary subtraction can underflow. The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion. -------------------- +==== Integer Overflow ==== +SWC ID: 101 +Severity: High +Contract: Unknown +Function name: sendeth(address,uint256) +PC address: 725 +Estimated Gas Usage: 11915 - 52861 +The binary addition can overflow. +The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion. +-------------------- +