Skip to content

Change the symex merge to use the full merge rather than ignoring comments #2258

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.

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

Conversation

thk123
Copy link
Contributor

@thk123 thk123 commented May 30, 2018

This ensures ireps that differ only by comments aren't inadvertently lost.

Not sure if this is a good idea - discussion welcome!

…ments

This ensures ireps that differ only by comments aren't inadvertently
lost.
@tautschnig
Copy link
Collaborator

No, please don't do this (hence marking do-not-merge), unless you have measurements that prove me wrong: there are a lot of expressions that are the same (think of type annotations, for example) except for the annotated source location, and not saving the memory space would be a waste.

I've lately been thinking going the opposite direction and completely removing comments. Those comments should not be relevant for the back-end, and thus removing them would open up some further optimisation avenues. Indeed part of the merge idea is that expressions that differ only by comments aren't actually to be distinguished.

So what is it that makes you want to retain them?

@thk123
Copy link
Contributor Author

thk123 commented May 30, 2018

@tautschnig This makes sense (and was to a large extend predicted) I have another PR imminently that moves a comment tree into the non-comment space which fixes the same problem. @peterschrammel suggested that we should probably just eliminate comments entirely, but I don't think either of us had thought about the case of source location.

@tautschnig
Copy link
Collaborator

If there is any information in comments that is required in the back-end then it must be moved out of the comments, yes. Looking forward to the next PR :-)

With regard to eliminating comments: we should be able to do this by introducing something I'd call decorated_exprt and decorated_typet that itself has the information that previously went into comments as regular named_sub members. This, however, requires changes across the code base to support.

@thk123
Copy link
Contributor Author

thk123 commented Jun 14, 2018

The "other PR": #2261

Since this is a non-starter I'll just close out this PR.

@thk123 thk123 closed this Jun 14, 2018
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants