Skip to content

Json output through languaget interface#2098

Closed
peterschrammel wants to merge 5 commits intodiffblue:developfrom
peterschrammel:json-expr-languaget
Closed

Json output through languaget interface#2098
peterschrammel wants to merge 5 commits intodiffblue:developfrom
peterschrammel:json-expr-languaget

Conversation

@peterschrammel
Copy link
Member

@peterschrammel peterschrammel commented Apr 21, 2018 •
edited
Loading

This removes the dependency of util on langapi.

Depends on #2111 merged

Depends on #2115 merged

@kroening
Copy link
Collaborator

kroening commented Apr 21, 2018

Does source_locationt really need language-specific conversion?

@peterschrammel
Copy link
Member Author

peterschrammel commented Apr 21, 2018 •
edited
Loading

It has the bytecode index as an attribute, which will eventually be moved to a java_source_locationt, derived from source_locationt.

@peterschrammel peterschrammel force-pushed the json-expr-languaget branch 4 times, most recently from b8d311f to 4d3cca3 Compare April 22, 2018 13:00
peterschrammel
peterschrammel commented Apr 22, 2018
View reviewed changes
src/goto-programs/loop_ids.cpp
forall_goto_functions(it, goto_functions)
show_loop_ids_json(ui, it->second.body, loops);

// TODO: this needs clean up
Copy link
Member Author

@peterschrammel peterschrammel Apr 22, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Needs separate fixing (#1757 (comment))

src/analyses/dependence_graph.cpp
const namespacet &ns) const
{
json_arrayt graph;
json_exprt json;
Copy link
Member Author

@peterschrammel peterschrammel Apr 22, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Might need separate fixing if language-specific output is desired (#1757 (comment))

src/goto-programs/loop_ids.cpp
json_objectt &loop=loops.push_back().make_object();
loop["name"]=json_stringt(id);
loop["sourceLocation"]=json(it->source_location);
loop["sourceLocation"] = json_exprt()(it->source_location);
Copy link
Member Author

@peterschrammel peterschrammel Apr 22, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Needs separate fixing (#1757 (comment))

@tautschnig
Copy link
Collaborator

tautschnig commented Apr 23, 2018

May I suggest that the work done here is used as a basis for multiple PRs? It looks like a series of independent bug-fixes are happening here.

@peterschrammel
Copy link
Member Author

peterschrammel commented Apr 23, 2018 •
edited
Loading

@tautschnig, I can split up the first 7 commits into a few independent PRs. The last 3 commits that contain the big chunk of work, however, depend on everything before.

@tautschnig
Copy link
Collaborator

tautschnig commented Apr 23, 2018

Maybe it's just me, but I found it really hard to make sense of the changes when looking at the combined diff. It may be easier when doing commit-by-commit, but meaningful PRs might help get this merged very quickly.

@peterschrammel peterschrammel mentioned this pull request Apr 25, 2018
Merged
@peterschrammel peterschrammel force-pushed the json-expr-languaget branch 3 times, most recently from 5a576b5 to f60e5be Compare April 26, 2018 09:16
@peterschrammel
Copy link
Member Author

peterschrammel commented Apr 26, 2018

@tautschnig, this is now rebased on develop (two previous PRs have been merged). I've split the remaining commits to make them more digestible, ensuring that all commits build. Please re-review.

tautschnig
tautschnig approved these changes Apr 26, 2018
View reviewed changes
Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks ok to me.

src/goto-programs/json_goto_trace.h
#include <util/json_expr.h>
#include <util/invariant.h>

#include <langapi/mode.h>
Copy link
Collaborator

@tautschnig tautschnig Apr 26, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why is this file required here?

@peterschrammel
Copy link
Member Author

peterschrammel commented Apr 27, 2018

Labelling "do not merge" because TG bump is not passing yet.

@smowton
Copy link
Contributor

smowton commented Apr 27, 2018

Similar to the other PR, I suggest distinguishing languaget, which is a pretty heavy-weight parser / converter class, from a lighter (probably singleton) language_infot used to do stateless conversions like this. Constructing and then destroying the whole Java parsing machinery every time I want to format an expression seems like it would be costly.

@thk123
Copy link
Contributor

thk123 commented May 1, 2018

Due to above comment will hold of reviewing this - please let me know if you'd like it reviewed as is

@peterschrammel peterschrammel mentioned this pull request May 5, 2018
Closed
@TGWDB
Copy link
Contributor

TGWDB commented Feb 22, 2021

Closing this as it appears there is no progress on this at the moment. Also this appears to relate to #2157 that may be required to progress well here.

If you believe this is erroneous, please reopen this PR.

@TGWDB TGWDB closed this Feb 22, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@tautschnig tautschnig tautschnig approved these changes

@cesaro cesaro Awaiting requested review from cesaro

@chrisr-diffblue chrisr-diffblue Awaiting requested review from chrisr-diffblue

@kroening kroening Awaiting requested review from kroening kroening is a code owner

@martin-cs martin-cs Awaiting requested review from martin-cs martin-cs is a code owner

@mgudemann mgudemann Awaiting requested review from mgudemann

@smowton smowton Awaiting requested review from smowton

@thk123 thk123 Awaiting requested review from thk123

Assignees

@cesaro cesaro

@smowton smowton

@thk123 thk123

@mgudemann mgudemann

@martin-cs martin-cs

@chrisr-diffblue chrisr-diffblue

Labels

do not merge Java Front End

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

10 participants

@peterschrammel @kroening @tautschnig @smowton @thk123 @TGWDB @cesaro @mgudemann @martin-cs @chrisr-diffblue