Skip to content

Check all struct members for possible need for renaming #3918

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 4 commits into from
Jan 24, 2019
Merged

Check all struct members for possible need for renaming #3918

merged 4 commits into from
Jan 24, 2019

Conversation

tautschnig
Copy link
Collaborator

Follow-up to #3633. I'm not labelling this "bugfix" as I wasn't actually able to trigger a bug, even though there are changes that make it seem more correct.

  • 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.

smowton
smowton approved these changes Jan 24, 2019
View reviewed changes
Copy link
Contributor

@smowton smowton left a comment

Choose a reason for hiding this comment

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

I think that sort of VL-struct might be a GNU extension, so wouldn't be surprised if MSVC starts cursing like a sailor

@tautschnig tautschnig mentioned this pull request Jan 24, 2019
Merged
2 tasks
@tautschnig
Copy link
Collaborator Author

Clang does refuse to compile this, GCC is ok - I haven't actually tried MSVC.

@kroening
Copy link
Member

You might try:

  • Make first member of a pointer.
  • Make second member of struct a flexible _Bool array, to avoid multiplication problem.

To make the lack of renaming actually a problem, this needs to happen in a loop, and the size needs to differ between iterations.

@kroening
Copy link
Member

BTW, my plan is to add a goto-program transformation pass that compiles these away. They add a lot of grief for a feature that has very few users.

@tautschnig
Copy link
Collaborator Author

To make the lack of renaming actually a problem, this needs to happen in a loop, and the size needs to differ between iterations.

Thanks, I have built a test that seems to fail, but actually it fails even without the recent optimisation. I'll work on it.

@tautschnig
Check all struct members for possible need for renaming
480f19e 
Don't stop after the first non-pointer element. But really it worked either way,
because struct tags are in place everywhere and we don't actually need to
rename.
@tautschnig
Use get_fresh_aux_symbol to create $array_size and fix its type
0e01c89 
An array_size symbol should be of type size_type(), and we can safely rely on
common logic to find fresh symbols.
@tautschnig
Extend the previous test with an access to the array
3a50362 
The test currently fails an invariant in the array decision procedure.
@tautschnig tautschnig force-pushed the fix-requires-renaming branch from 51c44e6 to 4381f04 Compare January 24, 2019 17:09
allredj
allredj reviewed Jan 24, 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: 51c44e6).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98498677
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.

@tautschnig
Copy link
Collaborator Author

I have added failing tests, but might actually deal with them in separate PRs.

@tautschnig
Failing test to demonstrate renaming inconsistencies
e98554b 
The mapping from L1 names to types is not in line with the different types used
across loop iterations.
@tautschnig tautschnig force-pushed the fix-requires-renaming branch from 4381f04 to e98554b Compare January 24, 2019 17:21
allredj
allredj reviewed Jan 24, 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: e98554b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98516182
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.

@tautschnig tautschnig merged commit dca1a9f into diffblue:develop Jan 24, 2019
@tautschnig tautschnig deleted the fix-requires-renaming branch January 24, 2019 21:17
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

@kroening kroening kroening approved these changes

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

Assignees

@kroening kroening

@romainbrenguier romainbrenguier

Labels
cleanup
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@tautschnig @kroening @smowton @allredj @romainbrenguier