{"action":"created","issue":{"url":"https://api.github.com/repos/boogie-org/boogie/issues/5","labels_url":"https://api.github.com/repos/boogie-org/boogie/issues/5/labels{/name}","comments_url":"https://api.github.com/repos/boogie-org/boogie/issues/5/comments","events_url":"https://api.github.com/repos/boogie-org/boogie/issues/5/events","html_url":"https://github.com/boogie-org/boogie/issues/5","id":65769209,"number":5,"title":"Language improvements to help represent debug info and MORE!","user":{"login":"delcypher","id":511795,"avatar_url":"https://avatars.githubusercontent.com/u/511795?v=3","gravatar_id":"","url":"https://api.github.com/users/delcypher","html_url":"https://github.com/delcypher","followers_url":"https://api.github.com/users/delcypher/followers","following_url":"https://api.github.com/users/delcypher/following{/other_user}","gists_url":"https://api.github.com/users/delcypher/gists{/gist_id}","starred_url":"https://api.github.com/users/delcypher/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/delcypher/subscriptions","organizations_url":"https://api.github.com/users/delcypher/orgs","repos_url":"https://api.github.com/users/delcypher/repos","events_url":"https://api.github.com/users/delcypher/events{/privacy}","received_events_url":"https://api.github.com/users/delcypher/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/boogie-org/boogie/labels/enhancement","name":"enhancement","color":"84b6eb"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":6,"created_at":"2015-04-01T20:09:49Z","updated_at":"2015-04-23T04:11:16Z","closed_at":null,"body":"Boogie currently doesn't allow attributes on all commands (e.g. assignment, goto). There doesn't seem to be a good reason for this. Allowing this would allow debug information to represented in a sane way (currently people just add ``assume true`` which is ugly)."},"comment":{"url":"https://api.github.com/repos/boogie-org/boogie/issues/comments/95422492","html_url":"https://github.com/boogie-org/boogie/issues/5#issuecomment-95422492","issue_url":"https://api.github.com/repos/boogie-org/boogie/issues/5","id":95422492,"user":{"login":"akashlal","id":1886307,"avatar_url":"https://avatars.githubusercontent.com/u/1886307?v=3","gravatar_id":"","url":"https://api.github.com/users/akashlal","html_url":"https://github.com/akashlal","followers_url":"https://api.github.com/users/akashlal/followers","following_url":"https://api.github.com/users/akashlal/following{/other_user}","gists_url":"https://api.github.com/users/akashlal/gists{/gist_id}","starred_url":"https://api.github.com/users/akashlal/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/akashlal/subscriptions","organizations_url":"https://api.github.com/users/akashlal/orgs","repos_url":"https://api.github.com/users/akashlal/repos","events_url":"https://api.github.com/users/akashlal/events{/privacy}","received_events_url":"https://api.github.com/users/akashlal/received_events","type":"User","site_admin":false},"created_at":"2015-04-23T04:11:16Z","updated_at":"2015-04-23T04:11:16Z","body":"Hi Dan,\nLet me add my 2c.\n\n1. Attributes everywhere: seems reasonable to me.\n\n2. Using attributes on basic blocks to represent debugging information: I\ndon't think this is such a good idea. I actually don't see anything wrong\nor ugly about the way debugging information is represented today. I treat\nbasic blocks and transfer commands as just control artifacts. Program\ntransformations like removing empty basic blocks and coalescing basic\nblocks (done for efficiency and readability) would not be possible if\nblocks or transfer commands carry attributes. Similarly for static\nprocedure inlining, if return commands have attributes. Attributes on an\nassume command survives all these transformations, which I like. I think of\na trace of a sequence of commands (with no control constructs), which is\nwhy I prefer embedding source information inside a command.\n\nMore importantly, I think the job of the compiler would become even harder\nif it has to match source information to Boogie control constructs. For\nexample, in the internal IR that I generate for C, the source information\nis already embedded as an IR command. It is more convenient to spit it out\nas a Boogie command rather than to start a new basic block.\n\nOf course, none of these are fundamental restrictions, just inertia.\n\n3. Attribute references. I like the fact that collecting repeated\nattributes together in a single reference reduces the memory footprint. Are\nyou proposing to hide the attribute references from the user? That is, when\nthe Boogie program is parsed in, the references \"@1\" will get expanded to\nthe actual attribute? If so, we only save space on disk, not ram. If not,\nthen we need extra logic to read attributes. Further, what happens when you\nEmit a program? Does it emit with attribute references or without?\n\nAkash\n\n\n\n\n\n\nOn Thu, Apr 23, 2015 at 3:52 AM, Dan Liew <notifications@github.com> wrote:\n\n> @pdeligia <https://github.com/pdeligia> I'm also sceptical of where I've\n> placed the attributes for the assign command which is why I'm raising this\n> issue early so we can discuss it. I guess our options are\n>\n> {:attribute \"foo\"} x, y := y, x;\n>\n> x, y {:attribute \"foo\"} := y, x;\n>\n> x, y := {:attribute \"foo\"} y, x;\n>\n> x,y := y, x {:attribute \"foo\"};\n>\n> Something we might want to bear in mind is... *what if in the future we\n> want to add attributes to expressions too*. In that case only the first\n> two options are usable.\n>\n> —\n> Reply to this email directly or view it on GitHub\n> <https://github.com/boogie-org/boogie/issues/5#issuecomment-95355401>.\n>\n"}}