{"action":"created","issue":{"url":"https://api.github.com/repos/diffblue/cbmc/issues/2192","repository_url":"https://api.github.com/repos/diffblue/cbmc","labels_url":"https://api.github.com/repos/diffblue/cbmc/issues/2192/labels{/name}","comments_url":"https://api.github.com/repos/diffblue/cbmc/issues/2192/comments","events_url":"https://api.github.com/repos/diffblue/cbmc/issues/2192/events","html_url":"https://github.com/diffblue/cbmc/pull/2192","id":323974351,"number":2192,"title":"Introduce expression/type formatting functor","user":{"login":"kroening","id":1830565,"avatar_url":"https://avatars0.githubusercontent.com/u/1830565?v=4","gravatar_id":"","url":"https://api.github.com/users/kroening","html_url":"https://github.com/kroening","followers_url":"https://api.github.com/users/kroening/followers","following_url":"https://api.github.com/users/kroening/following{/other_user}","gists_url":"https://api.github.com/users/kroening/gists{/gist_id}","starred_url":"https://api.github.com/users/kroening/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/kroening/subscriptions","organizations_url":"https://api.github.com/users/kroening/orgs","repos_url":"https://api.github.com/users/kroening/repos","events_url":"https://api.github.com/users/kroening/events{/privacy}","received_events_url":"https://api.github.com/users/kroening/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":{"login":"kroening","id":1830565,"avatar_url":"https://avatars0.githubusercontent.com/u/1830565?v=4","gravatar_id":"","url":"https://api.github.com/users/kroening","html_url":"https://github.com/kroening","followers_url":"https://api.github.com/users/kroening/followers","following_url":"https://api.github.com/users/kroening/following{/other_user}","gists_url":"https://api.github.com/users/kroening/gists{/gist_id}","starred_url":"https://api.github.com/users/kroening/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/kroening/subscriptions","organizations_url":"https://api.github.com/users/kroening/orgs","repos_url":"https://api.github.com/users/kroening/repos","events_url":"https://api.github.com/users/kroening/events{/privacy}","received_events_url":"https://api.github.com/users/kroening/received_events","type":"User","site_admin":false},"assignees":[{"login":"kroening","id":1830565,"avatar_url":"https://avatars0.githubusercontent.com/u/1830565?v=4","gravatar_id":"","url":"https://api.github.com/users/kroening","html_url":"https://github.com/kroening","followers_url":"https://api.github.com/users/kroening/followers","following_url":"https://api.github.com/users/kroening/following{/other_user}","gists_url":"https://api.github.com/users/kroening/gists{/gist_id}","starred_url":"https://api.github.com/users/kroening/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/kroening/subscriptions","organizations_url":"https://api.github.com/users/kroening/orgs","repos_url":"https://api.github.com/users/kroening/repos","events_url":"https://api.github.com/users/kroening/events{/privacy}","received_events_url":"https://api.github.com/users/kroening/received_events","type":"User","site_admin":false}],"milestone":null,"comments":14,"created_at":"2018-05-17T11:02:12Z","updated_at":"2018-05-21T09:54:04Z","closed_at":null,"author_association":"MEMBER","pull_request":{"url":"https://api.github.com/repos/diffblue/cbmc/pulls/2192","html_url":"https://github.com/diffblue/cbmc/pull/2192","diff_url":"https://github.com/diffblue/cbmc/pull/2192.diff","patch_url":"https://github.com/diffblue/cbmc/pull/2192.patch"},"body":"The interface comes with an exemplar of an application (show_symbol_table).\r\nNote that this can replace util/format_expr.h and util/format_type.h.\r\n\r\nThis is extensible, i.e., it is possible to make the debug_formatter treat particular cases differently; it is possible to pass further data along with the formatter, say a symbol table, a wide space policy, etc., if needed. The formatter can be stateful (say for indents, parentheses, etc.)."},"comment":{"url":"https://api.github.com/repos/diffblue/cbmc/issues/comments/390608510","html_url":"https://github.com/diffblue/cbmc/pull/2192#issuecomment-390608510","issue_url":"https://api.github.com/repos/diffblue/cbmc/issues/2192","id":390608510,"user":{"login":"tautschnig","id":1144736,"avatar_url":"https://avatars3.githubusercontent.com/u/1144736?v=4","gravatar_id":"","url":"https://api.github.com/users/tautschnig","html_url":"https://github.com/tautschnig","followers_url":"https://api.github.com/users/tautschnig/followers","following_url":"https://api.github.com/users/tautschnig/following{/other_user}","gists_url":"https://api.github.com/users/tautschnig/gists{/gist_id}","starred_url":"https://api.github.com/users/tautschnig/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/tautschnig/subscriptions","organizations_url":"https://api.github.com/users/tautschnig/orgs","repos_url":"https://api.github.com/users/tautschnig/repos","events_url":"https://api.github.com/users/tautschnig/events{/privacy}","received_events_url":"https://api.github.com/users/tautschnig/received_events","type":"User","site_admin":false},"created_at":"2018-05-21T09:54:04Z","updated_at":"2018-05-21T09:54:04Z","author_association":"COLLABORATOR","body":"A couple of thoughts as the overall design goals and plans aren't very clear to me. Just my opinion, I would very much welcome comments/feedback/push-back:\r\n1. We should have an implementation that prints goto-program expressions in a what we designate as goto-program-expression syntax. First, what is a \"goto-program expression?\"  That's any expression appearing in a goto-program, with its semantics defined by our back-ends. In many cases the semantics will be the same as those of similarly-named expressions in C or Java, but this needn't be the case. Also there are some expressions that only exist in goto-program world, and not necessarily in any of the front-end languages (one of those is \"byte extract\"). We may choose the use a syntax that is very similar to that of C or Java to represent goto-program expressions, and implicitly we have been doing so all along. Let's clean this up and make clear that there is a syntax for goto-program expressions. I would argue that `format_expr` is taking care of this, once completely done. Completeness should be defined by \"for every expression supported by our back-end, there must be a well-defined syntax.\" Notably, any use of `pretty()` ought to be replaced by `UNREACHABLE`. Running `--show-goto-functions` (while making `--show-goto-functions` use `format`) on all regression tests might be a decent starting point to test this.\r\n2. If the above is acceptable, then there is no need for a `debug_formatter` or the likes as we would use `format_expr` as the one and only acceptable form of output for all back-end parts.\r\n3. Places where front-end-language specific output is to be used should be limited to a) output of front-end expressions (such as warnings or errors during parsing, type-checking or conversion), b) output of results that are to be translated back to the input language, such as counterexample traces or test suites, c) expressions in the symbol table that have not been converted (for example, the `value` has not necessarily been converted, and should thus be printed using language-specific syntax), and d) dump-c or any other means that very explicitly translates goto-program expressions back to the input-language world.\r\n4. `expr2ct` (and others deriving from it) should be changed to create valid C (Java, etc.) expressions in all cases. One example that comes to mind `convert_constant_bool` which still prints the non-C constants `TRUE` and `FALSE`. This would be perfectly fine in goto-program world, but should not exist in the input-language front-end. Support for printing, e.g., \"byte_extract\" would no longer be provided.\r\n5. The functors introduced here may be a good idea, but they lack the one bit of configurability that we actually need when producing output: awareness of the target context language, i.e., is it plain text, JSON, XML, or something else? We might want to have a distinct syntax for goto-programs (and goto-program expressions) in plain text/JSON/XML, in which case the point of creating the output needs to be aware. We may also choose _not_ to have this, in which case all we need to watch out for is doing proper escaping before embedding strings in JSON/XML output. Note that for C/Java, there is (AFAIK) no JSON/XML syntax, and thus such a distinction is not necessary - only the escaping part needs taking care of in case we embed such output in JSON/XML."}}
{"actor":{"display_login":"tautschnig"}}