Extract a rename_level2_ssa function

This is useful for the cases when the solver knows the expression to be
an SSA exprt.

Author: romainbrenguier

src/goto-symex/goto_symex_state.cpp

@@ -371,35 +371,40 @@ exprt goto_symex_statet::rename_level1(exprt expr, const namespacet &ns)
   return expr;
 }
 
+exprt goto_symex_statet::rename_level2_ssa(ssa_exprt ssa, const namespacet &ns)
+{
+  set_l1_indices(ssa, ns);
+  rename(ssa.type(), ssa.get_identifier(), ns);
+  ssa.update_type();
+
+  if(l2_thread_read_encoding(ssa, ns))
+  {
+    // renaming taken care of by l2_thread_encoding
+  }
+  else if(!ssa.get_level_2().empty())
+  {
+    // already at L2
+  }
+  else
+  {
+    // We also consider propagation if we go up to L2.
+    // L1 identifiers are used for propagation!
+    auto p_it = propagation.find(ssa.get_identifier());
+
+    if(p_it != propagation.end())
+      return p_it->second; // already L2
+
+    set_l2_indices(ssa, ns);
+  }
+  return ssa;
+}
+
 void goto_symex_statet::rename_level2(exprt &expr, const namespacet &ns)
 {
   // rename all the symbols with their last known value
   renaming_strategyt strategy;
   strategy.rename_ssa = [this](ssa_exprt ssa, const namespacet &ns) -> exprt {
-    set_l1_indices(ssa, ns);
-    rename(ssa.type(), ssa.get_identifier(), ns, L2);
-    ssa.update_type();
-
-    if(l2_thread_read_encoding(ssa, ns))
-    {
-      // renaming taken care of by l2_thread_encoding
-    }
-    else if(!ssa.get_level_2().empty())
-    {
-      // already at L2
-    }
-    else
-    {
-      // We also consider propagation if we go up to L2.
-      // L1 identifiers are used for propagation!
-      auto p_it = propagation.find(ssa.get_identifier());
-
-      if(p_it != propagation.end())
-        return p_it->second; // already L2
-
-      set_l2_indices(ssa, ns);
-    }
-    return ssa;
+    return rename_level2_ssa(ssa, ns);
   };
   strategy.rename_address =
     [&](address_of_exprt &address_of_expr, const namespacet &ns) {

src/goto-symex/goto_symex_state.h

@@ -182,6 +182,7 @@ class goto_symex_statet final : public goto_statet
   ssa_exprt rename_level0_ssa(ssa_exprt ssa, const namespacet &ns);
   ssa_exprt rename_level1_ssa(ssa_exprt expr, const namespacet &ns);
   exprt rename_level1(exprt expr, const namespacet &ns);
+  exprt rename_level2_ssa(ssa_exprt expr, const namespacet &ns);
   void rename_level2(exprt &expr, const namespacet &ns);
   void rename(
     typet &type,