{"action":"created","issue":{"url":"https://api.github.com/repos/nunoplopes/alive/issues/29","repository_url":"https://api.github.com/repos/nunoplopes/alive","labels_url":"https://api.github.com/repos/nunoplopes/alive/issues/29/labels{/name}","comments_url":"https://api.github.com/repos/nunoplopes/alive/issues/29/comments","events_url":"https://api.github.com/repos/nunoplopes/alive/issues/29/events","html_url":"https://github.com/nunoplopes/alive/issues/29","id":104238169,"number":29,"title":"Precondition doesn't type check","user":{"login":"nunoplopes","id":2998477,"avatar_url":"https://avatars.githubusercontent.com/u/2998477?v=3","gravatar_id":"","url":"https://api.github.com/users/nunoplopes","html_url":"https://github.com/nunoplopes","followers_url":"https://api.github.com/users/nunoplopes/followers","following_url":"https://api.github.com/users/nunoplopes/following{/other_user}","gists_url":"https://api.github.com/users/nunoplopes/gists{/gist_id}","starred_url":"https://api.github.com/users/nunoplopes/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nunoplopes/subscriptions","organizations_url":"https://api.github.com/users/nunoplopes/orgs","repos_url":"https://api.github.com/users/nunoplopes/repos","events_url":"https://api.github.com/users/nunoplopes/events{/privacy}","received_events_url":"https://api.github.com/users/nunoplopes/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2015-09-01T10:41:49Z","updated_at":"2016-02-03T20:20:05Z","closed_at":null,"body":"We should either reconsider adding +1 bit for positive numbers, have a way to downcast it or different syntax or...?\r\n(test case from John Regehr)\r\n```\r\nPrecondition: (computeKnownZeroBits(%in) == 4294443007)\r\n   %1 = icmp eq i32 %in, 0\r\n   %out = select i1 %1, 1, 2\r\n=>\r\n   %3 = lshr i32 %in, 20\r\n   %out = add %3, 1\r\n\r\nPrecondition does not type check\r\n```"},"comment":{"url":"https://api.github.com/repos/nunoplopes/alive/issues/comments/179440752","html_url":"https://github.com/nunoplopes/alive/issues/29#issuecomment-179440752","issue_url":"https://api.github.com/repos/nunoplopes/alive/issues/29","id":179440752,"user":{"login":"davemenendez","id":8042785,"avatar_url":"https://avatars.githubusercontent.com/u/8042785?v=3","gravatar_id":"","url":"https://api.github.com/users/davemenendez","html_url":"https://github.com/davemenendez","followers_url":"https://api.github.com/users/davemenendez/followers","following_url":"https://api.github.com/users/davemenendez/following{/other_user}","gists_url":"https://api.github.com/users/davemenendez/gists{/gist_id}","starred_url":"https://api.github.com/users/davemenendez/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/davemenendez/subscriptions","organizations_url":"https://api.github.com/users/davemenendez/orgs","repos_url":"https://api.github.com/users/davemenendez/repos","events_url":"https://api.github.com/users/davemenendez/events{/privacy}","received_events_url":"https://api.github.com/users/davemenendez/received_events","type":"User","site_admin":false},"created_at":"2016-02-03T20:20:05Z","updated_at":"2016-02-03T20:20:05Z","body":"The way we calculate minimum bit-widths for integer literals seems to be broken for negatives, as well.\r\n\r\n```\r\n>>> c = ConstantVal(-3, IntType())\r\n>>> c.getTypeConstraints()\r\nAnd(And(t_-3_0 == 0,\r\n        Or(size_-3_0 == 8,\r\n           size_-3_0 == 4,\r\n           And(size_-3_0 > 0, size_-3_0 <= 64))),\r\n    size_-3_0 >= 2)\r\n```\r\n\r\nUnfortunately, you can't represent -3 in two bits. I think't Python's `bit_length()` assumes an extra sign bit."}}