Do not unnecessarily break sharing during renaming

[tautschnig]

Not all subexpressions (or types) change during renaming. Only actually write to
the result when there was a change. This preserves sharing. On SV-COMP's
ReachSafety-ECA benchmarks the time spent in goto_symex_state::rename(exprt &,
...) is now 1944 seconds, when previously it was 2326 seconds. On the other
hand, the time spent in merge_ireps did not improve, the number of recursive
operator== calls in fact was higher (6930718243 rising to from 5710509892).

The time spent in goto_symex_statet::rename(typet &, ...) increases from 530
seconds to 568 seconds, which suggests there is room for improvement.

I will keep this PR in Draft status to make sure #3996 won't need a rebase.

• 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/
• n/a 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).
• 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.

[romainbrenguier]

I think for review it would be nice to split the PR in three commits: on that makes rename_address return an optional, one for rename_type and one for rename_expr.

[tautschnig]

Split into three commits done and rebased onto current develop - releasing for review.

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: 7cf4875).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102536309

[allredj]

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 5ef434d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102537067
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]

Looks good -- my comments about redundant quality tests may in fact be subsumed by later commits.

Question: does this render the rename-required pre-pass redundant? Should we combine the two methods into one walk at this point?

Pattern question: mild preference for something that takes an exprt & as at present, carefully turns that into a const exprt &, uses that to determine if anything needs doing, and then writes to it if appropriate, rather than having the if(ret) val = *ret; pattern at every callsite

[tautschnig]

I'm taking the liberty to mark this dependent-on-#4264.

[romainbrenguier]

@tautschnig #4286 has been merged, and this needs rebasing

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: 71aec16).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103873701

[tautschnig]

I'm currently running benchmarks of develop vs. this branch to back up these changes by performance data. If those do not yield any negative results I'm inclined to merge this as-is and do the cleanup proposed by @romainbrenguier and @smowton in follow-up work.

[tautschnig]

Here are my profiling results (on ReachSafety-ECA from SV-COMP):
develop performs 2959.21 symex steps per second, applying this PR we achieve 2844.20 steps per second (approximately 4% slowdown). The number of calls to detach reduces from 25,442,953,846 to 18,862,575,940. The amount of time spent in rename<L2>(exprt, ...) seems to increase from 434 seconds to 464 seconds, but it's not entirely clear what that time is spent on other than just doing recursive calls - it seems the recursive calls got a bit more expensive, which would seem fair given that we now have a return value to manipulate and some branching to do.

In my opinion this is no clear indication either way. I think the approach of not breaking sharing is cleaner, but it's certainly no performance win by itself.

@kroening @peterschrammel @romainbrenguier @smowton Can you please voice your opinions on whether we should do this or not?

[romainbrenguier]

Since it doesn't have a positive impact on performances and makes the code more complicated, I would be in favor of not merging it.

[romainbrenguier]

I'm "requesting changes" so that this doesn't get merged by mistake.

[smowton]

Agreed that the sharing breaking is a great thing, and it seems like it shouldn't be too difficult to get that without incurring a lot of extra cost tracking that. Could you find out if it reduces the lost time to return exprt rather than optionalt<exprt> and use &old_expr.read() == &new_expr.read() to determine if there has been a change? In particular this will enable return elision as we'll be directly returning an exprt.

[tautschnig]

Closing as all this code has been substantially rewritten already and uses move semantics today.