{"action":"closed","issue":{"url":"https://api.github.com/repos/smackers/smack/issues/165","repository_url":"https://api.github.com/repos/smackers/smack","labels_url":"https://api.github.com/repos/smackers/smack/issues/165/labels{/name}","comments_url":"https://api.github.com/repos/smackers/smack/issues/165/comments","events_url":"https://api.github.com/repos/smackers/smack/issues/165/events","html_url":"https://github.com/smackers/smack/issues/165","id":146145171,"node_id":"MDU6SXNzdWUxNDYxNDUxNzE=","number":165,"title":"Model LLVM arithmetic with overflow intrinsics","user":{"login":"shaobo-he","id":5892703,"node_id":"MDQ6VXNlcjU4OTI3MDM=","avatar_url":"https://avatars1.githubusercontent.com/u/5892703?v=4","gravatar_id":"","url":"https://api.github.com/users/shaobo-he","html_url":"https://github.com/shaobo-he","followers_url":"https://api.github.com/users/shaobo-he/followers","following_url":"https://api.github.com/users/shaobo-he/following{/other_user}","gists_url":"https://api.github.com/users/shaobo-he/gists{/gist_id}","starred_url":"https://api.github.com/users/shaobo-he/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/shaobo-he/subscriptions","organizations_url":"https://api.github.com/users/shaobo-he/orgs","repos_url":"https://api.github.com/users/shaobo-he/repos","events_url":"https://api.github.com/users/shaobo-he/events{/privacy}","received_events_url":"https://api.github.com/users/shaobo-he/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":5,"created_at":"2016-04-06T00:07:00Z","updated_at":"2018-06-04T17:43:35Z","closed_at":"2018-06-04T17:43:35Z","author_association":"CONTRIBUTOR","body":"Rust compiler will compile arithmetic operations into LLVM arithmetic with overflow intrinsics. Take the following rust program as an example,\n\n``` rust\nfn main() {\n    let mut v = 2 ;\n    v = v * v;\n    assert!(v == 4);\n}\n```\n\nThe corresponding bytecode is,\n\n``` llvm\n%0 = load i32* %v, align 4, !dbg !817\n%1 = load i32* %v, align 4, !dbg !817\n%2 = call { i32, i1 } @llvm.smul.with.overflow.i32(i32 %0, i32 %1), !dbg !817\n%3 = extractvalue { i32, i1 } %2, 0, !dbg !817\n%4 = extractvalue { i32, i1 } %2, 1, !dbg !817\n```\n\nRustc also uses similar [intrinsics](http://llvm.org/docs/LangRef.html#arithmetic-with-overflow-intrinsics) for other arithmetic operations.\n\nWe have identified an issue #162 that these intrinsics are dropped due to transformation pass used by SMACK. In this issue, we would like to implement proper translation of these intrinsics. \n\nOne solution is to add a pass to change calls to these intrinsics to other functions with bodies that implement corresponding arithmetics. We can hand code the functions in a file and link it to the original bc file.\n"}}
{"actor":{"display_login":"zvonimir"}}