Make symex_level::rename functions return a value

This is so that the returned type can eventually reflect the renaming.

Author: romainbrenguier

src/goto-symex/goto_symex_state.cpp

@@ -237,7 +237,7 @@ void goto_symex_statet::set_l0_indices(
   ssa_exprt &ssa_expr,
   const namespacet &ns)
 {
-  level0(ssa_expr, ns, source.thread_nr);
+  ssa_expr = level0(std::move(ssa_expr), ns, source.thread_nr);
 }
 
 void goto_symex_statet::set_l1_indices(
@@ -248,8 +248,8 @@ void goto_symex_statet::set_l1_indices(
     return;
   if(!ssa_expr.get_level_1().empty())
     return;
-  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));
 }
 
 void goto_symex_statet::set_l2_indices(
@@ -258,9 +258,9 @@ void goto_symex_statet::set_l2_indices(
 {
   if(!ssa_expr.get_level_2().empty())
     return;
-  level0(ssa_expr, ns, source.thread_nr);
-  level1(ssa_expr);
-  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));
 }
 
 template <goto_symex_statet::levelt level>

src/goto-symex/renaming_level.cpp

@@ -17,50 +17,53 @@ Author: Romain Brenguier, [email protected]
 
 #include "goto_symex_state.h"
 
-void symex_level0t::
-operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr) const
+ssa_exprt symex_level0t::
+operator()(ssa_exprt ssa_expr, const namespacet &ns, unsigned thread_nr) const
 {
   // already renamed?
   if(!ssa_expr.get_level_0().empty())
-    return;
+    return ssa_expr;
 
   const irep_idt &obj_identifier = ssa_expr.get_object_name();
 
   // guards are not L0-renamed
   if(obj_identifier == goto_symex_statet::guard_identifier())
-    return;
+    return ssa_expr;
 
   const symbolt *s;
   const bool found_l0 = !ns.lookup(obj_identifier, s);
   INVARIANT(found_l0, "level0: failed to find " + id2string(obj_identifier));
 
   // don't rename shared variables or functions
   if(s->type.id() == ID_code || s->is_shared())
-    return;
+    return ssa_expr;
 
   // rename!
   ssa_expr.set_level_0(thread_nr);
+  return ssa_expr;
 }
 
-void symex_level1t::operator()(ssa_exprt &ssa_expr) const
+ssa_exprt symex_level1t::operator()(ssa_exprt ssa_expr) const
 {
   // already renamed?
   if(!ssa_expr.get_level_1().empty())
-    return;
+    return ssa_expr;
 
   const irep_idt l0_name = ssa_expr.get_l1_object_identifier();
 
   const auto it = current_names.find(l0_name);
   if(it == current_names.end())
-    return;
+    return ssa_expr;
 
   // rename!
   ssa_expr.set_level_1(it->second.second);
+  return ssa_expr;
 }
 
-void symex_level2t::operator()(ssa_exprt &ssa_expr) const
+ssa_exprt symex_level2t::operator()(ssa_exprt ssa_expr) const
 {
   ssa_expr.set_level_2(current_count(ssa_expr.get_identifier()));
+  return ssa_expr;
 }
 
 void symex_level1t::restore_from(

src/goto-symex/renaming_level.h

@@ -56,8 +56,10 @@ struct symex_renaming_levelt
 /// The renaming is built for one particular interleaving.
 struct symex_level0t : public symex_renaming_levelt
 {
-  void operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr)
-    const;
+  ssa_exprt operator()(
+    ssa_exprt ssa_expr,
+    const namespacet &ns,
+    unsigned thread_nr) const;
 
   symex_level0t() = default;
   ~symex_level0t() override = default;
@@ -68,7 +70,7 @@ struct symex_level0t : public symex_renaming_levelt
 /// This is to preserve locality in case of recursion
 struct symex_level1t : public symex_renaming_levelt
 {
-  void operator()(ssa_exprt &ssa_expr) const;
+  ssa_exprt operator()(ssa_exprt ssa_expr) const;
 
   /// Insert the content of \p other into this renaming
   void restore_from(const current_namest &other);
@@ -82,7 +84,7 @@ struct symex_level1t : public symex_renaming_levelt
 /// This is to ensure each variable is only assigned once.
 struct symex_level2t : public symex_renaming_levelt
 {
-  void operator()(ssa_exprt &ssa_expr) const;
+  ssa_exprt operator()(ssa_exprt ssa_expr) const;
 
   symex_level2t() = default;
   ~symex_level2t() override = default;