Introduce a renamedt type for renamed expressions in symex #4305
Conversation
romainbrenguier
requested review from
chrisr-diffblue,
danpoe,
hannes-steffenhagen-diffblue,
kroening,
martin-cs,
peterschrammel and
tautschnig
as code owners
romainbrenguier
force-pushed
the
refactor/renamedt
branch
3 times, most recently
from
a11b0d4 to
43ed0d3
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 43ed0d3).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102817834
| /// Wrapper for expressions or types which have been renamed up to a given | ||
| /// \p level | ||
| template <typename underlyingt, levelt level> | ||
| class renamedt |
There was a problem hiding this comment.
underlyingt appears to be ssa_exprt everywhere -- simply hardwire that?
There was a problem hiding this comment.
For now it is, but my plan is to next use it with exprt (draft PR here: #3986 though it needs to be rebased on this one), we could also think of using it with typet
There was a problem hiding this comment.
Some more comments and a +1 on @kroening's comment that underlyingt should be hardwired to ssa_exprt.
src/goto-symex/goto_symex_state.cpp
Outdated
| level0(ssa_expr, ns, source.thread_nr); | ||
| level1(ssa_expr); | ||
| ssa_exprt l0 = level0(std::move(ssa_expr), ns, source.thread_nr); | ||
| ssa_expr = level1(std::move(l0)); |
There was a problem hiding this comment.
Could we just do ssa_expr = level1(level0(std::move(ssa_expr), ns, source.thread_nr)); please?
src/goto-symex/goto_symex_state.cpp
Outdated
| level2(ssa_expr); | ||
| ssa_exprt l0 = level0(std::move(ssa_expr), ns, source.thread_nr); | ||
| ssa_exprt l1 = level1(std::move(l0)); | ||
| ssa_expr = level2(std::move(l1)); |
There was a problem hiding this comment.
ssa_expr = level2(level1(level0(std::move(ssa_expr), ns, source.thread_nr)));
src/goto-symex/renaming_level.cpp
Outdated
| { | ||
| // already renamed? | ||
| if(!ssa_expr.get_level_0().empty()) | ||
| return; | ||
| return std::move(ssa_expr); |
There was a problem hiding this comment.
@kroening @NathanJPhillips @smowton is the std::move actually necessary/desirable here (and in all the other cases where the argument is returned)? But maybe it doesn't matter much, because subsequent commits modify these lines.
There was a problem hiding this comment.
@tautschnig @romainbrenguier The std::move is not necessary; C++11 guarantees that the move constructor will be used without it, i.e., it's noise.
There was a problem hiding this comment.
There are three scenarios where std::move is needed:
- The parameter is an rvalue reference
- You want to move something whose lifetime isn't ending yet (but you are sure that you won't use it anymore)
- You want to return something that's derived from the return type.
These aren't super intuitive.
This is to be uniform with the other levels.
This is so that the returned type can eventually reflect the renaming.
This seems a more appropriate to find it, and we could use the levelt type for templates we will define in this file.
This is a wrapper that will be used to signal that an expression or type has been renamed to a given level. It makes it possible to define functions which only accept expression which have been through renaming.
This makes it explicit that the expresssion has been renamed.
This makes it explicit in the type that the expression has been renamed.
This makes it in the type the result has been renamed and a level 1 expression is expected as argument.
romainbrenguier
force-pushed
the
refactor/renamedt
branch
from
43ed0d3 to
b5ae64b
Compare
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: b5ae64b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102966820
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.
This is a wrapper that will be used to signal that an expression or type
has been renamed to a given level.
It makes it possible to define functions which only accept expression
which have been through renaming.
This is preliminary to #3986 but some of its part becomes redundant, and it needs to be reworked on afterwards.
Eventually expressions of this type will be propagated everywhere renamed expressions are used and
.get()should only be used when constructing the target equations.