{"action":"created","issue":{"url":"https://api.github.com/repos/ConsenSys/mythril/issues/266","repository_url":"https://api.github.com/repos/ConsenSys/mythril","labels_url":"https://api.github.com/repos/ConsenSys/mythril/issues/266/labels{/name}","comments_url":"https://api.github.com/repos/ConsenSys/mythril/issues/266/comments","events_url":"https://api.github.com/repos/ConsenSys/mythril/issues/266/events","html_url":"https://github.com/ConsenSys/mythril/issues/266","id":331391823,"node_id":"MDU6SXNzdWUzMzEzOTE4MjM=","number":266,"title":"Simple function is not flagged as containing an int overflow","user":{"login":"fernand","id":706462,"node_id":"MDQ6VXNlcjcwNjQ2Mg==","avatar_url":"https://avatars3.githubusercontent.com/u/706462?v=4","gravatar_id":"","url":"https://api.github.com/users/fernand","html_url":"https://github.com/fernand","followers_url":"https://api.github.com/users/fernand/followers","following_url":"https://api.github.com/users/fernand/following{/other_user}","gists_url":"https://api.github.com/users/fernand/gists{/gist_id}","starred_url":"https://api.github.com/users/fernand/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/fernand/subscriptions","organizations_url":"https://api.github.com/users/fernand/orgs","repos_url":"https://api.github.com/users/fernand/repos","events_url":"https://api.github.com/users/fernand/events{/privacy}","received_events_url":"https://api.github.com/users/fernand/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":{"login":"JoranHonig","id":8710366,"node_id":"MDQ6VXNlcjg3MTAzNjY=","avatar_url":"https://avatars0.githubusercontent.com/u/8710366?v=4","gravatar_id":"","url":"https://api.github.com/users/JoranHonig","html_url":"https://github.com/JoranHonig","followers_url":"https://api.github.com/users/JoranHonig/followers","following_url":"https://api.github.com/users/JoranHonig/following{/other_user}","gists_url":"https://api.github.com/users/JoranHonig/gists{/gist_id}","starred_url":"https://api.github.com/users/JoranHonig/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/JoranHonig/subscriptions","organizations_url":"https://api.github.com/users/JoranHonig/orgs","repos_url":"https://api.github.com/users/JoranHonig/repos","events_url":"https://api.github.com/users/JoranHonig/events{/privacy}","received_events_url":"https://api.github.com/users/JoranHonig/received_events","type":"User","site_admin":false},"assignees":[{"login":"JoranHonig","id":8710366,"node_id":"MDQ6VXNlcjg3MTAzNjY=","avatar_url":"https://avatars0.githubusercontent.com/u/8710366?v=4","gravatar_id":"","url":"https://api.github.com/users/JoranHonig","html_url":"https://github.com/JoranHonig","followers_url":"https://api.github.com/users/JoranHonig/followers","following_url":"https://api.github.com/users/JoranHonig/following{/other_user}","gists_url":"https://api.github.com/users/JoranHonig/gists{/gist_id}","starred_url":"https://api.github.com/users/JoranHonig/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/JoranHonig/subscriptions","organizations_url":"https://api.github.com/users/JoranHonig/orgs","repos_url":"https://api.github.com/users/JoranHonig/repos","events_url":"https://api.github.com/users/JoranHonig/events{/privacy}","received_events_url":"https://api.github.com/users/JoranHonig/received_events","type":"User","site_admin":false}],"milestone":null,"comments":0,"created_at":"2018-06-12T00:04:45Z","updated_at":"2018-06-12T04:45:14Z","closed_at":null,"author_association":"NONE","body":"I'm trying to understand why the following contract isn't flagged as containing a potential integer overflow:\r\n```\r\ncontract Test {\r\n    function test(uint256 input1, uint256 input2) returns(uint256) {\r\n        uint256 res = input1 * input2;\r\n        return res;\r\n    }\r\n}\r\n```\r\nI used `--solc-args=--optimize` to get simpler EVM instructions.\r\nIt looks like Z3 is trying to solve the following constraints and returns `unsat` for the relevant `MUL` operation in the `integer` module `_check_integer_overflow` function:\r\n```\r\n[Not(ULT(calldatasize_Test, 4)), UDiv(calldata_Test_0,\r\n      26959946667150639794667015087019630673637144422540572481103610249216) &\r\n 4294967295 ==\r\n 3951741217, callvalue == 0, Or(And(ULT(calldata_Test_4*calldata_Test_36,\r\n            calldata_Test_36),\r\n        calldata_Test_4 != 0),\r\n    And(ULT(calldata_Test_4*calldata_Test_36,\r\n            calldata_Test_4),\r\n        calldata_Test_36 != 0))]\r\n```\r\nHowever if I try to initialize these constraints myself by setting all the calldata/value vars to `BitVec(256)` the solver *does* find a solution (as it should).\r\nWhat am I missing?"},"comment":{"url":"https://api.github.com/repos/ConsenSys/mythril/issues/comments/396464232","html_url":"https://github.com/ConsenSys/mythril/issues/266#issuecomment-396464232","issue_url":"https://api.github.com/repos/ConsenSys/mythril/issues/266","id":396464232,"node_id":"MDEyOklzc3VlQ29tbWVudDM5NjQ2NDIzMg==","user":{"login":"b-mueller","id":5194767,"node_id":"MDQ6VXNlcjUxOTQ3Njc=","avatar_url":"https://avatars1.githubusercontent.com/u/5194767?v=4","gravatar_id":"","url":"https://api.github.com/users/b-mueller","html_url":"https://github.com/b-mueller","followers_url":"https://api.github.com/users/b-mueller/followers","following_url":"https://api.github.com/users/b-mueller/following{/other_user}","gists_url":"https://api.github.com/users/b-mueller/gists{/gist_id}","starred_url":"https://api.github.com/users/b-mueller/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/b-mueller/subscriptions","organizations_url":"https://api.github.com/users/b-mueller/orgs","repos_url":"https://api.github.com/users/b-mueller/repos","events_url":"https://api.github.com/users/b-mueller/events{/privacy}","received_events_url":"https://api.github.com/users/b-mueller/received_events","type":"User","site_admin":false},"created_at":"2018-06-12T04:45:14Z","updated_at":"2018-06-12T04:45:14Z","author_association":"MEMBER","body":"I think it has to do with the way we qualify integer overflows as false positives. Overflows are not reported unless they change the account state or impact program flow.\r\n\r\nIf let's say you would also *use* your vulnerable function in an if-statement, the integer overflow would be reported:\r\n\r\n```\r\ncontract Test {\r\n\r\n    function test(uint256 input1, uint256 input2) returns(uint256) {\r\n        uint256 res = input1 * input2;\r\n        return res;\r\n    }\r\n\r\n    function useTest(uint256 input1, uint256 input2) returns(bool) {\r\n    \tif(test(input1, input2) < 1000) {\r\n    \t\treturn true;\r\n    \t}\r\n\r\n    \treturn false;\r\n    }\r\n}\r\n```\r\n\r\nOr, say you'd save the result in a state variable:\r\n\r\n```\r\ncontract Test {\r\n\r\n    uint256 res;\r\n\r\n    function test(uint256 input1, uint256 input2) returns(uint256) {\r\n        res = input1 * input2;\r\n    }\r\n}\r\n```\r\n\r\nDoes that make sense?"}}
{"actor":{"display_login":"b-mueller"}}