Skip to content

Make JSON symbol table input and output consistent #3726

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 3 commits into from
Jan 9, 2019
Merged

Make JSON symbol table input and output consistent #3726

merged 3 commits into from
Jan 9, 2019

Conversation

danpoe
Copy link
Contributor

@danpoe danpoe commented Jan 8, 2019 •
edited
Loading

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@danpoe danpoe force-pushed the fixes/json-symbol-table branch 2 times, most recently from 5135862 to f88d91f Compare January 8, 2019 17:27
allredj
allredj reviewed Jan 8, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

✔️
Passed Diffblue compatibility checks (cbmc commit: f88d91f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/96648090

tautschnig
tautschnig approved these changes Jan 8, 2019
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 good to me, but should likely receive a review from someone who depends on the JSON symbol table.

unit/json_symbol_table.cpp Outdated
optionst options;
cbmc_parse_optionst::set_default_options(options);

null_message_handlert null_message_handler;
Copy link
Collaborator

Choose a reason for hiding this comment

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

You might want to use the one from unit/testing-utils/message.h.

smowton
smowton reviewed Jan 9, 2019
View reviewed changes
src/util/json_irep.cpp Outdated
}

{
const auto it = json_object.find("comment");
Copy link
Contributor

Choose a reason for hiding this comment

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

Not any more

src/util/symbol.cpp Outdated

bool symbolt::operator==(const symbolt &other) const
{
return type == other.type && value == other.value &&
Copy link
Contributor

Choose a reason for hiding this comment

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

Suggest for readability do // clang-format off and list one condition per line

src/util/symbol_table.cpp Outdated
std::vector<std::pair<irep_idt, irep_idt>> v1;
std::vector<std::pair<irep_idt, irep_idt>> v2;

for(const auto &pair : internal_symbol_base_map)
Copy link
Contributor

Choose a reason for hiding this comment

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

v1(internal_symbol_base_map.begin(), internal_symbol_base_map.end()), similarly v2.

chrisr-diffblue
chrisr-diffblue approved these changes Jan 9, 2019
View reviewed changes
Copy link
Contributor

@chrisr-diffblue chrisr-diffblue left a comment

Choose a reason for hiding this comment

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

We'll need to update gnat2goto, but we can do that when we next bump its cbmc submodule.

@danpoe danpoe force-pushed the fixes/json-symbol-table branch 2 times, most recently from 5996247 to 8d4ca27 Compare January 9, 2019 11:17
allredj
allredj reviewed Jan 9, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 5996247).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/96741193
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

  • the cbmc commit has disappeared in the mean time (e.g. in a force-push)
  • the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

@danpoe danpoe force-pushed the fixes/json-symbol-table branch from 8d4ca27 to a3f38e7 Compare January 9, 2019 12:20
danpoe added 3 commits January 9, 2019 12:20
@danpoe
Make symbol table JSON output and input consistent
3614bdc 
This adapts the JSON symbol table output function show_symbol_table_json_ui()
and the JSON symbol table input function symbol_table_from_json() to use a
consistent format.
@danpoe
Add equality operators to symbolt and symbol_tablet
13dac86 
This adds equality member operators to symbolt and symbol_tablet. They will be
useful in unit tests to check that when outputting a symbol table in JSON and
reading it back in again the same symbol table is obtained.
@danpoe
Add unit test to check symbol table JSON input and output format cons…
a3f38e7 
…istency

The unit test first outputs a symbol table to JSON via show_symbol_table() and
then reads it back in again via symbol_table_from_json(). Then, it checks that
the initial symbol table and the symbol table read back in again are equal.
allredj
allredj reviewed Jan 9, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

✔️
Passed Diffblue compatibility checks (cbmc commit: 8d4ca27).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/96741962

@danpoe danpoe merged commit 30e5339 into diffblue:develop Jan 9, 2019
allredj
allredj reviewed Jan 9, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

🚫
This PR failed Diffblue compatibility checks (cbmc commit: a3f38e7).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/96747712
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

  • the cbmc commit has disappeared in the mean time (e.g. in a force-push)
  • the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

@chrisr-diffblue chrisr-diffblue mentioned this pull request Jan 31, 2019
Merged
@danpoe danpoe deleted the fixes/json-symbol-table branch June 2, 2020 17:13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@allredj allredj allredj left review comments

@smowton smowton smowton approved these changes

@tautschnig tautschnig tautschnig approved these changes

@peterschrammel peterschrammel peterschrammel approved these changes

@chrisr-diffblue chrisr-diffblue chrisr-diffblue approved these changes

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

@pkesseli pkesseli Awaiting requested review from pkesseli

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@danpoe @smowton @tautschnig @peterschrammel @allredj @chrisr-diffblue