{"action":"created","issue":{"url":"https://api.github.com/repos/diffblue/cbmc/issues/2572","repository_url":"https://api.github.com/repos/diffblue/cbmc","labels_url":"https://api.github.com/repos/diffblue/cbmc/issues/2572/labels{/name}","comments_url":"https://api.github.com/repos/diffblue/cbmc/issues/2572/comments","events_url":"https://api.github.com/repos/diffblue/cbmc/issues/2572/events","html_url":"https://github.com/diffblue/cbmc/pull/2572","id":339933462,"node_id":"MDExOlB1bGxSZXF1ZXN0MjAwNDY2NTc0","number":2572,"title":"Abstract interpretation framework: allow selective domain retention","user":{"login":"smowton","id":283483,"node_id":"MDQ6VXNlcjI4MzQ4Mw==","avatar_url":"https://avatars3.githubusercontent.com/u/283483?v=4","gravatar_id":"","url":"https://api.github.com/users/smowton","html_url":"https://github.com/smowton","followers_url":"https://api.github.com/users/smowton/followers","following_url":"https://api.github.com/users/smowton/following{/other_user}","gists_url":"https://api.github.com/users/smowton/gists{/gist_id}","starred_url":"https://api.github.com/users/smowton/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/smowton/subscriptions","organizations_url":"https://api.github.com/users/smowton/orgs","repos_url":"https://api.github.com/users/smowton/repos","events_url":"https://api.github.com/users/smowton/events{/privacy}","received_events_url":"https://api.github.com/users/smowton/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":7,"created_at":"2018-07-10T17:13:49Z","updated_at":"2018-07-11T08:37:42Z","closed_at":null,"author_association":"MEMBER","pull_request":{"url":"https://api.github.com/repos/diffblue/cbmc/pulls/2572","html_url":"https://github.com/diffblue/cbmc/pull/2572","diff_url":"https://github.com/diffblue/cbmc/pull/2572.diff","patch_url":"https://github.com/diffblue/cbmc/pull/2572.patch"},"body":"This allows users of the `ait` abstract interpretation framework to specify that only certain states are needed after\r\nits fixpoint computation is finished. For example, perhaps a particular analysis, or a particular user of that analysis,\r\nonly needs to know the results at END_FUNCTION instructions. In this case when a state does not need to be retained, and\r\nonly has a single successor, that state will be altered in place and passed to its successor instruction using std::move,\r\npermitting an analysis to optimise away much (potentially all) state copying.\r\n\r\nIn the best case (a long, straight-line function whose state grows with every instruction, such as a constant propagator\r\nreading \"int x = 1; int y = 2; int z = 3; ...\") this reduces analysis space and time complexity from quadratic to linear."},"comment":{"url":"https://api.github.com/repos/diffblue/cbmc/issues/comments/404090494","html_url":"https://github.com/diffblue/cbmc/pull/2572#issuecomment-404090494","issue_url":"https://api.github.com/repos/diffblue/cbmc/issues/2572","id":404090494,"node_id":"MDEyOklzc3VlQ29tbWVudDQwNDA5MDQ5NA==","user":{"login":"martin-cs","id":5333188,"node_id":"MDQ6VXNlcjUzMzMxODg=","avatar_url":"https://avatars0.githubusercontent.com/u/5333188?v=4","gravatar_id":"","url":"https://api.github.com/users/martin-cs","html_url":"https://github.com/martin-cs","followers_url":"https://api.github.com/users/martin-cs/followers","following_url":"https://api.github.com/users/martin-cs/following{/other_user}","gists_url":"https://api.github.com/users/martin-cs/gists{/gist_id}","starred_url":"https://api.github.com/users/martin-cs/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/martin-cs/subscriptions","organizations_url":"https://api.github.com/users/martin-cs/orgs","repos_url":"https://api.github.com/users/martin-cs/repos","events_url":"https://api.github.com/users/martin-cs/events{/privacy}","received_events_url":"https://api.github.com/users/martin-cs/received_events","type":"User","site_admin":false},"created_at":"2018-07-11T08:37:42Z","updated_at":"2018-07-11T08:37:42Z","author_association":"COLLABORATOR","body":"@smowton : working on it but running SC^2 today and presenting at SMT tomorrow so it might not be today.\r\n\r\n@tautschnig : as I see it, sharing maps are orthogonal to this optimisation.  They help reduce the amount of memory used to store domains; this reduces the number of domains stored.  As for publication ... if you know of a good source of published material on the actual practicalities of implementing an abstract interpreter I'd be interested to read it.  The thing I've been working on I am hoping to publish."}}
{"actor":{"display_login":"martin-cs"}}