Merge the two rename_ssa functions

We merge rename_level0_ssa and rename_level1_ssa in one template
rename_ssa<level> since the code is similar and their usage would be
similar.

Author: romainbrenguier

src/goto-symex/goto_symex_state.cpp

@@ -163,7 +163,7 @@ void goto_symex_statet::assignment(
   bool allow_pointer_unsoundness)
 {
   // identifier should be l0 or l1, make sure it's l1
-  lhs = rename_level1_ssa(std::move(lhs), ns);
+  lhs = rename_ssa<L1>(std::move(lhs), ns);
   irep_idt l1_identifier=lhs.get_identifier();
 
   // the type might need renaming
@@ -263,24 +263,29 @@ void goto_symex_statet::set_l2_indices(
   ssa_expr.set_level_2(level2.current_count(ssa_expr.get_identifier()));
 }
 
-ssa_exprt
-goto_symex_statet::rename_level0_ssa(ssa_exprt ssa, const namespacet &ns)
+template <goto_symex_statet::levelt level>
+ssa_exprt goto_symex_statet::rename_ssa(ssa_exprt ssa, const namespacet &ns)
 {
-  set_l0_indices(ssa, ns);
-  rename<L0>(ssa.type(), ssa.get_identifier(), ns);
-  ssa.update_type();
-  return ssa;
-}
+  static_assert(
+    level == L0 || level == L1,
+    "rename_ssa can only be used for levels L0 and L1");
+  if(level == L0)
+    set_l0_indices(ssa, ns);
+  else if(level == L1)
+    set_l1_indices(ssa, ns);
+  else
+    UNREACHABLE;
 
-ssa_exprt
-goto_symex_statet::rename_level1_ssa(ssa_exprt ssa, const namespacet &ns)
-{
-  set_l1_indices(ssa, ns);
-  rename<L1>(ssa.type(), ssa.get_identifier(), ns);
+  rename<level>(ssa.type(), ssa.get_identifier(), ns);
   ssa.update_type();
   return ssa;
 }
 
+/// Ensure `rename_ssa` gets compiled for L0
+template ssa_exprt goto_symex_statet::rename_ssa<goto_symex_statet::L0>(
+  ssa_exprt ssa,
+  const namespacet &ns);
+
 template <goto_symex_statet::levelt level>
 exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
 {
@@ -293,11 +298,11 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
 
     if(level == L0)
     {
-      ssa = rename_level0_ssa(std::move(ssa), ns);
+      ssa = rename_ssa<L0>(std::move(ssa), ns);
     }
     else if(level == L1)
     {
-      ssa = rename_level1_ssa(std::move(ssa), ns);
+      ssa = rename_ssa<L1>(std::move(ssa), ns);
     }
     else if(level==L2)
     {
@@ -331,8 +336,10 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
     // we never rename function symbols
     if(as_const(expr).type().id() == ID_code)
       rename<level>(expr.type(), to_symbol_expr(expr).get_identifier(), ns);
-    else
+    else if(level == L0 || level == L1)
       expr = rename<level>(ssa_exprt(expr), ns);
+    else // No SSA version for level2
+      expr = rename<level>((exprt)ssa_exprt(expr), ns);
   }
   else if(expr.id()==ID_address_of)
   {

src/goto-symex/goto_symex_state.h

@@ -182,9 +182,10 @@ class goto_symex_statet final : public goto_statet
   template <levelt level = L2>
   exprt rename(exprt expr, const namespacet &ns);
 
-  ssa_exprt rename_level0_ssa(ssa_exprt ssa, const namespacet &ns);
-
-  ssa_exprt rename_level1_ssa(ssa_exprt ssa, const namespacet &ns);
+  /// Version of rename which is specialized for SSA exprt.
+  /// Implementation only exists for level L0 and L1.
+  template <levelt level>
+  ssa_exprt rename_ssa(ssa_exprt ssa, const namespacet &ns);
 
   template <levelt level = L2>
   void rename(typet &type, const irep_idt &l1_identifier, const namespacet &ns);

src/goto-symex/symex_dead.cpp

@@ -26,7 +26,7 @@ void goto_symext::symex_dead(statet &state)
   // We increase the L2 renaming to make these non-deterministic.
   // We also prevent propagation of old values.
 
-  ssa_exprt ssa = state.rename_level1_ssa(ssa_exprt{code.symbol()}, ns);
+  ssa_exprt ssa = state.rename_ssa<statet::L1>(ssa_exprt{code.symbol()}, ns);
 
   // in case of pointers, put something into the value set
   if(code.symbol().type().id() == ID_pointer)

src/goto-symex/symex_decl.cpp

@@ -37,7 +37,7 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   // We increase the L2 renaming to make these non-deterministic.
   // We also prevent propagation of old values.
 
-  ssa_exprt ssa = state.rename_level1_ssa(ssa_exprt{expr}, ns);
+  ssa_exprt ssa = state.rename_ssa<statet::L1>(ssa_exprt{expr}, ns);
   const irep_idt &l1_identifier = ssa.get_identifier();
 
   // rename type to L2

src/goto-symex/symex_dereference_state.cpp

@@ -50,8 +50,8 @@ symex_dereference_statet::get_or_create_failed_symbol(const exprt &expr)
     {
       symbolt sym=*symbol;
       symbolt *sym_ptr=nullptr;
-      const ssa_exprt sym_expr =
-        state.rename_level1_ssa(ssa_exprt{sym.symbol_expr()}, ns);
+      const ssa_exprt sym_expr = state.rename_ssa<goto_symex_statet::L1>(
+        ssa_exprt{sym.symbol_expr()}, ns);
       sym.name = sym_expr.get_identifier();
       state.symbol_table.move(sym, sym_ptr);
       return sym_ptr;
@@ -70,8 +70,8 @@ symex_dereference_statet::get_or_create_failed_symbol(const exprt &expr)
     {
       symbolt sym=*symbol;
       symbolt *sym_ptr=nullptr;
-      const ssa_exprt sym_expr =
-        state.rename_level1_ssa(ssa_exprt{sym.symbol_expr()}, ns);
+      const ssa_exprt sym_expr = state.rename_ssa<goto_symex_statet::L1>(
+        ssa_exprt{sym.symbol_expr()}, ns);
       sym.name = sym_expr.get_identifier();
       state.symbol_table.move(sym, sym_ptr);
       return sym_ptr;

src/goto-symex/symex_function_call.cpp

@@ -395,8 +395,8 @@ static void locality(
       it++)
   {
     // get L0 name
-    ssa_exprt ssa =
-      state.rename_level0_ssa(ssa_exprt(ns.lookup(*it).symbol_expr()), ns);
+    ssa_exprt ssa = state.rename_ssa<goto_symex_statet::L0>(
+      ssa_exprt(ns.lookup(*it).symbol_expr()), ns);
     const irep_idt l0_name=ssa.get_identifier();
 
     // save old L1 name for popping the frame
@@ -418,7 +418,8 @@ static void locality(
     // identifiers may be shared among functions
     // (e.g., due to inlining or other code restructuring)
 
-    ssa_exprt ssa_l1 = state.rename_level1_ssa(std::move(ssa), ns);
+    ssa_exprt ssa_l1 =
+      state.rename_ssa<goto_symex_statet::L1>(std::move(ssa), ns);
 
     irep_idt l1_name = ssa_l1.get_identifier();
     unsigned offset=0;

src/goto-symex/symex_goto.cpp

@@ -248,7 +248,7 @@ void goto_symext::symex_goto(statet &state)
       exprt new_rhs = boolean_negate(new_guard);
 
       ssa_exprt new_lhs =
-        state.rename_level1_ssa(ssa_exprt{guard_symbol_expr}, ns);
+        state.rename_ssa<statet::L1>(ssa_exprt{guard_symbol_expr}, ns);
       state.assignment(new_lhs, new_rhs, ns, true, false);
 
       guardt guard{true_exprt{}};

src/goto-symex/symex_start_thread.cpp

@@ -73,7 +73,7 @@ void goto_symext::symex_start_thread(statet &state)
       std::forward_as_tuple(lhs.get_l1_object_identifier()),
       std::forward_as_tuple(lhs, 0));
     CHECK_RETURN(emplace_result.second);
-    const ssa_exprt lhs_l1 = state.rename_level1_ssa(std::move(lhs), ns);
+    const ssa_exprt lhs_l1 = state.rename_ssa<statet::L1>(std::move(lhs), ns);
     const irep_idt l1_name = lhs_l1.get_l1_object_identifier();
     // store it
     state.l1_history.insert(l1_name);