Rename rename_level2 and remove optional argument

The rename function is now only used with level2, so the optional
argument becomes useless.
We rename it to a more explicit name, which is also uniform with the other levels.

Author: romainbrenguier

src/goto-instrument/accelerate/scratch_program.cpp

@@ -64,7 +64,7 @@ exprt scratch_programt::eval(const exprt &e)
 {
   exprt ssa=e;
 
-  symex_state.rename(ssa, ns);
+  symex_state.rename_level2(ssa, ns);
 
   return checker->get(ssa);
 }

src/goto-symex/goto_symex_state.cpp

@@ -359,14 +359,9 @@ void goto_symex_statet::rename_level1(exprt &expr, const namespacet &ns)
   }
 }
 
-void goto_symex_statet::rename(
-  exprt &expr,
-  const namespacet &ns,
-  levelt level)
+void goto_symex_statet::rename_level2(exprt &expr, const namespacet &ns)
 {
   // rename all the symbols with their last known value
-  PRECONDITION(level == L2);
-
   if(expr.id()==ID_symbol &&
      expr.get_bool(ID_C_SSA_symbol))
   {
@@ -406,7 +401,7 @@ void goto_symex_statet::rename(
     }
 
     expr=ssa_exprt(expr);
-    rename(expr, ns);
+    rename_level2(expr, ns);
   }
   else if(expr.id()==ID_address_of)
   {
@@ -421,7 +416,7 @@ void goto_symex_statet::rename(
 
     // do this recursively
     Forall_operands(it, expr)
-      rename(*it, ns);
+      rename_level2(*it, ns);
 
     // some fixes
     if(expr.id()==ID_with)
@@ -623,7 +618,7 @@ void goto_symex_statet::rename_address(
     else if(level == L1)
       rename_level1(e, ns);
     else
-      rename(e, ns);
+      rename_level2(e, ns);
   };
 
   if(expr.id()==ID_symbol &&
@@ -727,7 +722,7 @@ void goto_symex_statet::rename(
     else if(level == L1)
       rename_level1(e, ns);
     else
-      rename(e, ns);
+      rename_level2(e, ns);
   };
 
   // rename all the symbols with their last known value

src/goto-symex/goto_symex_state.h

@@ -71,9 +71,9 @@ class goto_symex_statet final
   enum levelt { L0=0, L1=1, L2=2 };
 
   // performs renaming _up to_ the given level
-  void rename(exprt &expr, const namespacet &ns, levelt level=L2);
   void rename_level0(exprt &expr, const namespacet &ns);
   void rename_level1(exprt &expr, const namespacet &ns);
+  void rename_level2(exprt &expr, const namespacet &ns);
   void rename(
     typet &type,
     const irep_idt &l1_identifier,

src/goto-symex/symex_assign.cpp

@@ -212,7 +212,7 @@ void goto_symext::symex_assign_symbol(
     tmp_ssa_rhs.swap(ssa_rhs);
   }
 
-  state.rename(ssa_rhs, ns);
+  state.rename_level2(ssa_rhs, ns);
   do_simplify(ssa_rhs);
 
   ssa_exprt ssa_lhs=lhs;
@@ -228,7 +228,7 @@ void goto_symext::symex_assign_symbol(
   ssa_full_lhs=add_to_lhs(ssa_full_lhs, ssa_lhs);
   const bool record_events=state.record_events;
   state.record_events=false;
-  state.rename(ssa_full_lhs, ns);
+  state.rename_level2(ssa_full_lhs, ns);
   state.record_events=record_events;
 
   guardt tmp_guard(state.guard);
@@ -408,7 +408,7 @@ void goto_symext::symex_assign_if(
   guardt old_guard=guard;
 
   exprt renamed_guard=lhs.cond();
-  state.rename(renamed_guard, ns);
+  state.rename_level2(renamed_guard, ns);
   do_simplify(renamed_guard);
 
   if(!renamed_guard.is_false())

src/goto-symex/symex_builtin_functions.cpp

@@ -70,7 +70,7 @@ void goto_symext::symex_allocate(
   else
   {
     exprt tmp_size=size;
-    state.rename(tmp_size, ns); // to allow constant propagation
+    state.rename_level2(tmp_size, ns); // to allow constant propagation
     simplify(tmp_size, ns);
 
     // special treatment for sizeof(T)*x
@@ -162,7 +162,7 @@ void goto_symext::symex_allocate(
   state.symbol_table.add(value_symbol);
 
   exprt zero_init=code.op1();
-  state.rename(zero_init, ns); // to allow constant propagation
+  state.rename_level2(zero_init, ns); // to allow constant propagation
   simplify(zero_init, ns);
 
   INVARIANT(
@@ -232,7 +232,7 @@ void goto_symext::symex_gcc_builtin_va_arg_next(
     return; // ignore
 
   exprt tmp=code.op0();
-  state.rename(tmp, ns); // to allow constant propagation
+  state.rename_level2(tmp, ns); // to allow constant propagation
   do_simplify(tmp);
   irep_idt id=get_symbol(tmp);
 
@@ -310,7 +310,7 @@ void goto_symext::symex_printf(
   PRECONDITION(!rhs.operands().empty());
 
   exprt tmp_rhs=rhs;
-  state.rename(tmp_rhs, ns);
+  state.rename_level2(tmp_rhs, ns);
   do_simplify(tmp_rhs);
 
   const exprt::operandst &operands=tmp_rhs.operands();
@@ -336,14 +336,14 @@ void goto_symext::symex_input(
 
   exprt id_arg=code.op0();
 
-  state.rename(id_arg, ns);
+  state.rename_level2(id_arg, ns);
 
   std::list<exprt> args;
 
   for(std::size_t i=1; i<code.operands().size(); i++)
   {
     args.push_back(code.operands()[i]);
-    state.rename(args.back(), ns);
+    state.rename_level2(args.back(), ns);
     do_simplify(args.back());
   }
 
@@ -360,14 +360,14 @@ void goto_symext::symex_output(
 
   exprt id_arg=code.op0();
 
-  state.rename(id_arg, ns);
+  state.rename_level2(id_arg, ns);
 
   std::list<exprt> args;
 
   for(std::size_t i=1; i<code.operands().size(); i++)
   {
     args.push_back(code.operands()[i]);
-    state.rename(args.back(), ns);
+    state.rename_level2(args.back(), ns);
     do_simplify(args.back());
   }
 
@@ -481,7 +481,7 @@ void goto_symext::symex_trace(
     for(std::size_t j=2; j<code.arguments().size(); j++)
     {
       exprt var(code.arguments()[j]);
-      state.rename(var, ns);
+      state.rename_level2(var, ns);
       vars.push_back(var);
     }
 

src/goto-symex/symex_decl.cpp

@@ -70,7 +70,7 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   symex_renaming_levelt::increase_counter(level2_it);
   const bool record_events=state.record_events;
   state.record_events=false;
-  state.rename(ssa, ns);
+  state.rename_level2(ssa, ns);
   state.record_events=record_events;
 
   // we hide the declaration of auxiliary variables

src/goto-symex/symex_function_call.cpp

@@ -267,7 +267,7 @@ void goto_symext::symex_function_call_code(
   // read the arguments -- before the locality renaming
   exprt::operandst arguments = call.arguments();
   for(auto &a : arguments)
-    state.rename(a, ns);
+    state.rename_level2(a, ns);
 
   // we hide the call if the caller and callee are both hidden
   const bool hidden = state.top().hidden_function && goto_function.is_hidden();

src/goto-symex/symex_goto.cpp

@@ -38,7 +38,7 @@ void goto_symext::symex_goto(statet &state)
   clean_expr(old_guard, state, false);
 
   exprt new_guard=old_guard;
-  state.rename(new_guard, ns);
+  state.rename_level2(new_guard, ns);
   do_simplify(new_guard);
 
   if(new_guard.is_false())
@@ -269,7 +269,7 @@ void goto_symext::symex_goto(statet &state)
         symex_targett::assignment_typet::GUARD);
 
       guard_expr = boolean_negate(guard_symbol_expr);
-      state.rename(guard_expr, ns);
+      state.rename_level2(guard_expr, ns);
     }
 
     if(state.has_saved_jump_target)

src/goto-symex/symex_main.cpp

@@ -95,7 +95,7 @@ void goto_symext::vcc(
   }
 
   // now rename, enables propagation
-  state.rename(expr, ns);
+  state.rename_level2(expr, ns);
 
   // now try simplifier on it
   do_simplify(expr);
@@ -410,7 +410,7 @@ void goto_symext::symex_step(
     {
       exprt tmp=instruction.guard;
       clean_expr(tmp, state, false);
-      state.rename(tmp, ns);
+      state.rename_level2(tmp, ns);
       symex_assume(state, tmp);
     }