Skip to content

Make the simplifier preserve syntactically equal types [blocks: #2064] #3652

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 2 commits into from
Jan 23, 2019
Merged

Make the simplifier preserve syntactically equal types [blocks: #2064] #3652

merged 2 commits into from
Jan 23, 2019

Conversation

tautschnig
Copy link
Collaborator

base_type_eq guarantees semantic equality, but the resulting expression should
always have exactly the same type.

  • 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 force-pushed the 2064-simplifier-preserve-types branch 2 times, most recently from 4fa4741 to 12b6724 Compare December 31, 2018 15:41
kroening
kroening reviewed Dec 31, 2018
View reviewed changes
src/util/simplify_expr_int.cpp Outdated
{
tmp.make_typecast(expr.type());
simplify_node(tmp);
}
Copy link
Member

Choose a reason for hiding this comment

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

This one is potentially problematic, as the typecast is semantic, and does not necessarily preserve the bit-pattern.
I would refuse to do the simplification if the type differs.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Ok, I’ll change this as suggested.

@kroening
Copy link
Member

Note that this may create further type-inconsistency in the expression tree; say a symbol expression might now have a type that is not syntactically identical to the type it has elsewhere or in the symbol table.

@tautschnig
Copy link
Collaborator Author

Note that this may create further type-inconsistency in the expression tree; say a symbol expression might now have a type that is not syntactically identical to the type it has elsewhere or in the symbol table.

I get that, but I was hoping to be doing some good as this should support the other PRs that try to maintain types. Wouldn’t those suffer from the same issue? I’d happily use base_type_eq in the POSTCONDITION. (This PR is factored out from #2064, where the simplifier ended up returning completely unrelated types. I’d be happy to enforce semantic equivalence only.)

@kroening
Copy link
Member

kroening commented Jan 2, 2019

@tautschnig I think the way to go is to get rid of base_type_eq and type_eq. This fixes the root cause of the issue.

@kroening
Copy link
Member

kroening commented Jan 2, 2019

I.e., in the code in the PR, I'd replace the call to base_type_eq by expr.type() == expr.op().type().

There are a few places left where struct_tags get expanded (say the Java object factory). These should be fixed first.

@tautschnig tautschnig self-assigned this Jan 4, 2019
@tautschnig tautschnig force-pushed the 2064-simplifier-preserve-types branch from 12b6724 to 3026a5d Compare January 9, 2019 21:19
@tautschnig
Copy link
Collaborator Author

I have added some commits that remove unnecessary expansion of types, but 1) the Java front-end still needs work, 2) this PR is getting too big so I've started factoring out individual commits, and 3) I've borrowed commits from other PRs.

@tautschnig tautschnig changed the title Make the simplifier preserve syntactically equal types [blocks: #2064] Make the simplifier preserve syntactically equal types [depends-on: #3647, #3738, #3739, blocks: #2064] Jan 10, 2019
kroening pushed a commit that referenced this pull request Jan 10, 2019
Merge pull request #3738 from tautschnig/no-follow-1
e1e2009 
Remove unnecessary ns.follow in symex_dereference [blocks: #3652]
tautschnig added a commit that referenced this pull request Jan 10, 2019
@tautschnig
Merge pull request #3647 from diffblue/symbol_factoryt_fix
dbc301f 
bugfix: symbol_factoryt must preserve struct_tag types [blocks: #3652]
@tautschnig tautschnig changed the title Make the simplifier preserve syntactically equal types [depends-on: #3647, #3738, #3739, blocks: #2064] Make the simplifier preserve syntactically equal types [depends-on: #3739, blocks: #2064] Jan 10, 2019
@tautschnig tautschnig changed the title Make the simplifier preserve syntactically equal types [depends-on: #3739, blocks: #2064] Make the simplifier preserve syntactically equal types [depends-on: #3633, #3739, blocks: #2064] Jan 10, 2019
kroening pushed a commit that referenced this pull request Jan 11, 2019
Merge pull request #3739 from tautschnig/no-follow-2
d21a6bc 
Remove unnecessary use of ns.follow in flattening [blocks: #3652]
@tautschnig tautschnig force-pushed the 2064-simplifier-preserve-types branch from 3026a5d to 620edc2 Compare January 14, 2019 21:48
tautschnig added a commit that referenced this pull request Jan 14, 2019
@tautschnig
Merge pull request #3806 from tautschnig/bits2expr
250f5af 
bits2expr must return an expression of the requested type [blocks: #3652]
@tautschnig tautschnig force-pushed the 2064-simplifier-preserve-types branch from 620edc2 to c8e0866 Compare January 15, 2019 09:35
@tautschnig tautschnig force-pushed the 2064-simplifier-preserve-types branch from c8e0866 to 9255f33 Compare January 23, 2019 16:32
@tautschnig tautschnig changed the title Make the simplifier preserve syntactically equal types [depends-on: #3633, #3739, blocks: #2064] Make the simplifier preserve syntactically equal types [blocks: #2064] Jan 23, 2019
@tautschnig
Copy link
Collaborator Author

I have cleared out all the dependencies, this PR is now really just adding extra checks in the simplifier while not going as far as what's going to happen in #2064 (more work in the string solver is required as it currently makes use of some elaborate expressions within types).

@tautschnig tautschnig force-pushed the 2064-simplifier-preserve-types branch from 9255f33 to 2b0800d Compare January 23, 2019 18:36
@tautschnig
Simplify concatenation only if types match
420cff3 
When simplifying the operands of a concatenation permits replacing the concat
expression by one of the (simplified) operands, only do so if that wouldn't
result in a type mismatch.
@tautschnig
Expression simplification must not alter the type
450e568 
Expression simplification should return an expression that is semantically
equivalent. The type may only differ in moving from a tag to an expanded type or
vice-versa, but the underlying types must always remain consistent.
@tautschnig tautschnig force-pushed the 2064-simplifier-preserve-types branch from 2b0800d to 450e568 Compare January 23, 2019 20:00
allredj
allredj reviewed Jan 23, 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: 450e568).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98386718

@tautschnig tautschnig merged commit 1f9d908 into diffblue:develop Jan 23, 2019
@tautschnig tautschnig deleted the 2064-simplifier-preserve-types branch January 23, 2019 22:24
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kroening kroening kroening left review comments

@allredj allredj allredj left review comments

@smowton smowton smowton approved these changes

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

@pkesseli pkesseli Awaiting requested review from pkesseli

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

@martin-cs martin-cs Awaiting requested review from martin-cs

@romainbrenguier romainbrenguier Awaiting requested review from romainbrenguier

Assignees

@tautschnig tautschnig

Labels
blocker
Projects
None yet
Milestone
No milestone
Development

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