Refactor rename using iterators instead of recursion

[romainbrenguier]

According to my experiments this is less efficient than the recursive function (I think because of the use of mutate). @tautschnig still wanted this to be in a pull request to be able to discuss it.

• 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.
• 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).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[kroening]

I am thinking we want a function that takes a functor that can modify expressions, and does so using an explicit stack.

[tautschnig]

The problem with this implementation is that it calls mutate every time, even when this isn't necessary, because no renaming is to be done. This applies in particular to each of the calls to type renaming, which will hardly ever do anything (but still requires a writable reference). I've got an implementation (tautschnig@ee0b4a5) that does not require writable references, but it doesn't have the beauty of the depth iterator. If we could combine those, i.e., use the depth iterator, call the const-version of rename, and then mutate only if renaming was necessary, then we might have a nice result.

[romainbrenguier]

The problem with this implementation is that it calls mutate every time, even when this isn't necessary, because no renaming is to be done. This applies in particular to each of the calls to type renaming, which will hardly ever do anything (but still requires a writable reference). I've got an implementation (tautschnig@ee0b4a5) that does not require writable references, but it doesn't have the beauty of the depth iterator. If we could combine those, i.e., use the depth iterator, call the const-version of rename, and then mutate only if renaming was necessary, then we might have a nice result.

Making rename_address/type return optional to avoid exprt write will be good to have. Can you make a pull request with this change? Whether the version with depth iterator would be nicer than the recursive version is a matter of taste I guess. If there is no clear advantage in using iterators, I would leave rename as it is.

[tautschnig]

Making rename_address/type return optional to avoid exprt write will be good to have. Can you make a pull request with this change?

Done: #4286

[TGWDB]

Closing due to age (no further comment on PR content), please reopen with rebase on develop if you intent to continue this work.