Make set_l2_indices return a copy

This is in preparation to making it return a renamedt object.

Author: romainbrenguier

src/goto-symex/goto_symex_state.cpp

@@ -188,7 +188,7 @@ void goto_symex_statet::assignment(
   const auto level2_it =
     level2.current_names.emplace(l1_identifier, std::make_pair(lhs, 0)).first;
   symex_renaming_levelt::increase_counter(level2_it);
-  set_l2_indices(lhs, ns);
+  lhs = set_l2_indices(lhs, ns);
 
   // in case we happen to be multi-threaded, record the memory access
   bool is_shared=l2_thread_write_encoding(lhs, ns);
@@ -247,15 +247,14 @@ goto_symex_statet::set_l1_indices(ssa_exprt ssa_expr, const namespacet &ns)
   return level1(level0(std::move(ssa_expr), ns, source.thread_nr));
 }
 
-void goto_symex_statet::set_l2_indices(
-  ssa_exprt &ssa_expr,
-  const namespacet &ns)
+ssa_exprt
+goto_symex_statet::set_l2_indices(ssa_exprt ssa_expr, const namespacet &ns)
 {
   if(!ssa_expr.get_level_2().empty())
-    return;
+    return ssa_expr;
   renamedt<ssa_exprt, L2> l2 =
     level2(level1(level0(std::move(ssa_expr), ns, source.thread_nr)));
-  ssa_expr = l2.get();
+  return l2.get();
 }
 
 template <levelt level>
@@ -330,7 +329,7 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
         if(p_it != propagation.end())
           expr=p_it->second; // already L2
         else
-          set_l2_indices(ssa, ns);
+          ssa = set_l2_indices(ssa, ns);
       }
     }
   }
@@ -445,7 +444,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
       cond |= guardt{no_write.op()};
 
     if_exprt tmp(cond.as_expr(), ssa_l1, ssa_l1);
-    set_l2_indices(to_ssa_expr(tmp.true_case()), ns);
+    tmp.true_case() = set_l2_indices(to_ssa_expr(tmp.true_case()), ns);
 
     if(a_s_read.second.empty())
     {
@@ -478,8 +477,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
       source,
       symex_targett::assignment_typet::PHI);
 
-    set_l2_indices(ssa_l1, ns);
-    expr=ssa_l1;
+    expr = set_l2_indices(ssa_l1, ns);
 
     a_s_read.second.push_back(guard);
     if(!no_write.op().is_false())
@@ -495,15 +493,13 @@ bool goto_symex_statet::l2_thread_read_encoding(
   // No event and no fresh index, but avoid constant propagation
   if(!record_events)
   {
-    set_l2_indices(ssa_l1, ns);
-    expr=ssa_l1;
+    expr = set_l2_indices(ssa_l1, ns);
     return true;
   }
 
   // produce a fresh L2 name
   symex_renaming_levelt::increase_counter(level2_it);
-  set_l2_indices(ssa_l1, ns);
-  expr=ssa_l1;
+  expr = set_l2_indices(ssa_l1, ns);
 
   // and record that
   INVARIANT_STRUCTURED(

src/goto-symex/goto_symex_state.h

@@ -120,7 +120,7 @@ class goto_symex_statet final : public goto_statet
   renamedt<ssa_exprt, L1> set_l1_indices(ssa_exprt expr, const namespacet &ns);
 
   /// Update level 0, 1 and 2 values.
-  void set_l2_indices(ssa_exprt &expr, const namespacet &ns);
+  ssa_exprt set_l2_indices(ssa_exprt expr, const namespacet &ns);
 
   // this maps L1 names to (L2) types
   typedef std::unordered_map<irep_idt, typet> l1_typest;