Avoid calling rename with level=L1

The method rename_level1 should be called directly
This will allow us to get rid of the L1 case in rename and make the
function return a type which reflects the level of renaming.

Author: romainbrenguier

src/goto-symex/goto_symex_state.cpp

@@ -174,7 +174,7 @@ void goto_symex_statet::assignment(
   bool allow_pointer_unsoundness)
 {
   // identifier should be l0 or l1, make sure it's l1
-  rename(lhs, ns, L1);
+  rename_level1(lhs, ns);
   irep_idt l1_identifier=lhs.get_identifier();
 
   // the type might need renaming
@@ -635,8 +635,10 @@ void goto_symex_statet::rename_address(
   auto rename_expr = [&](exprt &e) {
     if(level == L0)
       rename_level0(e, ns);
+    else if(level == L1)
+      rename_level1(e, ns);
     else
-      rename(e, ns, level);
+      rename(e, ns);
   };
 
   if(expr.id()==ID_symbol &&
@@ -737,8 +739,10 @@ void goto_symex_statet::rename(
   auto rename_expr = [&](exprt &e) {
     if(level == L0)
       rename_level0(e, ns);
+    else if(level == L1)
+      rename_level1(e, ns);
     else
-      rename(e, ns, level);
+      rename(e, ns);
   };
 
   // rename all the symbols with their last known value

src/goto-symex/symex_dead.cpp

@@ -27,7 +27,7 @@ void goto_symext::symex_dead(statet &state)
   // We also prevent propagation of old values.
 
   ssa_exprt ssa(code.symbol());
-  state.rename(ssa, ns, goto_symex_statet::L1);
+  state.rename_level1(ssa, ns);
 
   // in case of pointers, put something into the value set
   if(code.symbol().type().id() == ID_pointer)
@@ -38,7 +38,7 @@ void goto_symext::symex_dead(statet &state)
       return exprt(ID_invalid);
     }();
 
-    state.rename(rhs, ns, goto_symex_statet::L1);
+    state.rename_level1(rhs, ns);
     state.value_set.assign(ssa, rhs, ns, true, false);
   }
 

src/goto-symex/symex_decl.cpp

@@ -38,7 +38,7 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   // We also prevent propagation of old values.
 
   ssa_exprt ssa(expr);
-  state.rename(ssa, ns, goto_symex_statet::L1);
+  state.rename_level1(ssa, ns);
   const irep_idt &l1_identifier=ssa.get_identifier();
 
   // rename type to L2
@@ -54,7 +54,7 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
       return exprt(ID_invalid);
     }();
 
-    state.rename(rhs, ns, goto_symex_statet::L1);
+    state.rename_level1(rhs, ns);
     state.value_set.assign(ssa, rhs, ns, true, false);
   }
 

src/goto-symex/symex_dereference.cpp

@@ -381,12 +381,12 @@ void goto_symext::dereference(
   // from different frames. Would be enough to rename
   // symbols whose address is taken.
   PRECONDITION(!state.call_stack().empty());
-  state.rename(expr, ns, goto_symex_statet::L1);
+  state.rename_level1(expr, ns);
 
   // start the recursion!
   guardt guard{true_exprt{}};
   dereference_rec(expr, state, guard, write);
   // dereferencing may introduce new symbol_exprt
   // (like __CPROVER_memory)
-  state.rename(expr, ns, goto_symex_statet::L1);
+  state.rename_level1(expr, ns);
 }

src/goto-symex/symex_dereference_state.cpp

@@ -37,7 +37,7 @@ bool symex_dereference_statet::has_failed_symbol(
       symbolt sym=*symbol;
       symbolt *sym_ptr=nullptr;
       symbol_exprt sym_expr=sym.symbol_expr();
-      state.rename(sym_expr, ns, goto_symex_statet::L1);
+      state.rename_level1(sym_expr, ns);
       sym.name=to_ssa_expr(sym_expr).get_identifier();
       state.symbol_table.move(sym, sym_ptr);
       symbol=sym_ptr;
@@ -57,7 +57,7 @@ bool symex_dereference_statet::has_failed_symbol(
       symbolt sym=*symbol;
       symbolt *sym_ptr=nullptr;
       symbol_exprt sym_expr=sym.symbol_expr();
-      state.rename(sym_expr, ns, goto_symex_statet::L1);
+      state.rename_level1(sym_expr, ns);
       sym.name=to_ssa_expr(sym_expr).get_identifier();
       state.symbol_table.move(sym, sym_ptr);
       symbol=sym_ptr;

src/goto-symex/symex_function_call.cpp

@@ -422,7 +422,7 @@ void goto_symext::locality(
     // identifiers may be shared among functions
     // (e.g., due to inlining or other code restructuring)
 
-    state.rename(ssa, ns, goto_symex_statet::L1);
+    state.rename_level1(ssa, ns);
 
     irep_idt l1_name=ssa.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(guard_symbol_expr);
-      state.rename(new_lhs, ns, goto_symex_statet::L1);
+      state.rename_level1(new_lhs, ns);
       state.assignment(new_lhs, new_rhs, ns, true, false);
 
       guardt guard{true_exprt{}};

src/goto-symex/symex_start_thread.cpp

@@ -71,7 +71,7 @@ void goto_symext::symex_start_thread(statet &state)
     auto emplace_result = state.level1.current_names.emplace(
       lhs.get_l1_object_identifier(), std::make_pair(lhs, 0));
     CHECK_RETURN(emplace_result.second);
-    state.rename(lhs, ns, goto_symex_statet::L1);
+    state.rename_level1(lhs, ns);
     const irep_idt l1_name=lhs.get_l1_object_identifier();
     // store it
     state.l1_history.insert(l1_name);