Change the symex merge to use the full merge rather than ignoring comments#2258
Change the symex merge to use the full merge rather than ignoring comments#2258thk123 wants to merge 1 commit intodiffblue:developfrom
Conversation
…ments This ensures ireps that differ only by comments aren't inadvertently lost.
|
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? |
|
@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. |
|
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 |
|
The "other PR": #2261 Since this is a non-starter I'll just close out this PR. |
This ensures ireps that differ only by comments aren't inadvertently lost.
Not sure if this is a good idea - discussion welcome!