Skip to content

Do not use base_type_eq with non-code types [blocks: #4056] #4314

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 6 commits into from
Mar 7, 2019
Merged

Do not use base_type_eq with non-code types [blocks: #4056] #4314

merged 6 commits into from
Mar 7, 2019

Conversation

tautschnig
Copy link
Collaborator

We consistently use tag types, and two expressions are now base_type_eq if, and
only if, they have types that compare equal.

This PR should unblock various PRs building on #4056 by skipping the breaking changes that relate to linking.

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a 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.

@tautschnig tautschnig self-assigned this Mar 2, 2019
@tautschnig tautschnig force-pushed the base_type-object-types branch from 9586664 to 9ff73d9 Compare March 2, 2019 23:39
@tautschnig tautschnig assigned smowton and kroening and unassigned tautschnig Mar 3, 2019
@kroening kroening removed their assignment Mar 3, 2019
@tautschnig tautschnig self-assigned this Mar 3, 2019
@tautschnig tautschnig force-pushed the base_type-object-types branch from 9ff73d9 to b133eb3 Compare March 3, 2019 21:15
@tautschnig tautschnig removed their assignment Mar 3, 2019
@tautschnig tautschnig force-pushed the base_type-object-types branch from b133eb3 to 91ce314 Compare March 3, 2019 22:02
allredj
allredj reviewed Mar 4, 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: 91ce314).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102973206
Status will be re-evaluated on next push.
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 compatibility was already broken by an earlier merge.

smowton
smowton approved these changes Mar 4, 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.

Note however that in order not to have terrible performance consequences for Java we must first merge simplify-after-deref or equivalent code, because this exposes the difference between e.g. List, List<T> and List<Integer>, which value-set-deref will express using a byte-extract op, and which the simplifier can remove.

@tautschnig
Copy link
Collaborator Author

@smowton Would you be able to contribute some performance comparison data that shows how important simplify-after-deref is?

@tautschnig tautschnig mentioned this pull request Mar 4, 2019
Merged
4 tasks
@tautschnig tautschnig force-pushed the base_type-object-types branch from 91ce314 to 1f3d104 Compare March 4, 2019 14:14
allredj
allredj reviewed Mar 4, 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: 1f3d104).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103074413
Status will be re-evaluated on next push.
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 compatibility was already broken by an earlier merge.

@smowton
Copy link
Contributor

smowton commented Mar 6, 2019

Benchmarks posted at #3725

smowton and others added 6 commits March 6, 2019 22:57
@smowton @tautschnig
Symex-dereference: simplify after deref
73fadb3 
This is generally useful because it turns member-of-if into if-of-member, which
avoids repeatedly quoting large complex if expressions in a with_exprt, but it
is especially good for field sensitivity as it puts member expressions directly
on top of symbol expressions, which field sensitivity knows how to deal with.
@tautschnig
Test to make sure generics do not result in constant propagation failure
0b09ffa 
This was fine with develop with and without simplification after dereferencing,
but would break if removing base_type_eq without adding the simplification step.
@tautschnig
Do not use base_type_eq with non-code types
97a82a1 
We consistently use tag types, and two expressions are now base_type_eq if, and
only if, they have types that compare equal.
@smowton @tautschnig
Value-set: compare against real type, not followed type
4063203
@smowton @tautschnig
Fix terminology now that base_type_eq is no longer used
37b43c7 
No functional changes
@smowton @tautschnig
Remove comment that no longer applies
cb67b9b 
The check is probably ok to go too, but we should make type preservation of `simplify` an invariant first.
@tautschnig tautschnig force-pushed the base_type-object-types branch from 1f3d104 to cb67b9b Compare March 6, 2019 23:11
allredj
allredj reviewed Mar 7, 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: cb67b9b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103460609

@tautschnig tautschnig merged commit 1e3f64d into diffblue:develop Mar 7, 2019
@tautschnig tautschnig deleted the base_type-object-types branch March 7, 2019 06:54
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 peterschrammel approved these changes

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

@danpoe danpoe Awaiting requested review from danpoe

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue Awaiting requested review from hannes-steffenhagen-diffblue

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

@owen-mc-diffblue owen-mc-diffblue Awaiting requested review from owen-mc-diffblue

@pkesseli pkesseli Awaiting requested review from pkesseli

@romainbrenguier romainbrenguier Awaiting requested review from romainbrenguier

@thk123 thk123 Awaiting requested review from thk123

Assignees

@smowton smowton

@peterschrammel peterschrammel

@romainbrenguier romainbrenguier

Labels
blocker cleanup
Projects
None yet
Milestone
No milestone
Development

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