Make level argument of rename a template argument

The level argument is always known from the call site (except for
rename recursive calls), and there are only 3 possible values, so it
makes sense to have it as a template argument.
This will be useful in particular, when we want the return type to
depend on the level.

Author: romainbrenguier

src/goto-instrument/accelerate/scratch_program.cpp

@@ -71,7 +71,7 @@ exprt scratch_programt::eval(const exprt &e)
 {
   exprt ssa=e;
 
-  symex_state->rename(ssa, ns);
+  symex_state->rename<goto_symex_statet::L2>(ssa, ns);
 
   return checker->get(ssa);
 }

src/goto-symex/goto_symex_state.cpp

@@ -162,11 +162,11 @@ 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<L1>(lhs, ns);
   irep_idt l1_identifier=lhs.get_identifier();
 
   // the type might need renaming
-  rename(lhs.type(), l1_identifier, ns);
+  rename<L2>(lhs.type(), l1_identifier, ns);
   lhs.update_type();
   if(run_validation_checks)
   {
@@ -266,15 +266,13 @@ ssa_exprt
 goto_symex_statet::rename_level0_ssa(ssa_exprt ssa, const namespacet &ns)
 {
   set_l0_indices(ssa, ns);
-  rename(ssa.type(), ssa.get_identifier(), ns, L0);
+  rename<L0>(ssa.type(), ssa.get_identifier(), ns);
   ssa.update_type();
   return ssa;
 }
 
-void goto_symex_statet::rename(
-  exprt &expr,
-  const namespacet &ns,
-  levelt level)
+template <goto_symex_statet::levelt level>
+void goto_symex_statet::rename(exprt &expr, const namespacet &ns)
 {
   // rename all the symbols with their last known value
 
@@ -290,13 +288,13 @@ void goto_symex_statet::rename(
     else if(level == L1)
     {
       set_l1_indices(ssa, ns);
-      rename(expr.type(), ssa.get_identifier(), ns, level);
+      rename<level>(expr.type(), ssa.get_identifier(), ns);
       ssa.update_type();
     }
     else if(level==L2)
     {
       set_l1_indices(ssa, ns);
-      rename(expr.type(), ssa.get_identifier(), ns, level);
+      rename<level>(expr.type(), ssa.get_identifier(), ns);
       ssa.update_type();
 
       if(l2_thread_read_encoding(ssa, ns))
@@ -325,32 +323,27 @@ void goto_symex_statet::rename(
     // we never rename function symbols
     if(as_const(expr).type().id() == ID_code)
     {
-      rename(
-        expr.type(),
-        to_symbol_expr(expr).get_identifier(),
-        ns,
-        level);
-
+      rename<level>(expr.type(), to_symbol_expr(expr).get_identifier(), ns);
       return;
     }
 
     expr=ssa_exprt(expr);
-    rename(expr, ns, level);
+    rename<level>(expr, ns);
   }
   else if(expr.id()==ID_address_of)
   {
     auto &address_of_expr = to_address_of_expr(expr);
-    rename_address(address_of_expr.object(), ns, level);
+    rename_address<level>(address_of_expr.object(), ns);
     to_pointer_type(expr.type()).subtype() =
       as_const(address_of_expr).object().type();
   }
   else
   {
-    rename(expr.type(), irep_idt(), ns, level);
+    rename<level>(expr.type(), irep_idt(), ns);
 
     // do this recursively
     Forall_operands(it, expr)
-      rename(*it, ns, level);
+      rename<level>(*it, ns);
 
     const exprt &c_expr = as_const(expr);
     INVARIANT(
@@ -541,10 +534,8 @@ bool goto_symex_statet::l2_thread_write_encoding(
   return threads.size()>1;
 }
 
-void goto_symex_statet::rename_address(
-  exprt &expr,
-  const namespacet &ns,
-  levelt level)
+template <goto_symex_statet::levelt level>
+void goto_symex_statet::rename_address(exprt &expr, const namespacet &ns)
 {
   if(expr.id()==ID_symbol &&
      expr.get_bool(ID_C_SSA_symbol))
@@ -554,42 +545,42 @@ void goto_symex_statet::rename_address(
     // only do L1!
     set_l1_indices(ssa, ns);
 
-    rename(expr.type(), ssa.get_identifier(), ns, level);
+    rename<level>(expr.type(), ssa.get_identifier(), ns);
     ssa.update_type();
   }
   else if(expr.id()==ID_symbol)
   {
     expr=ssa_exprt(expr);
-    rename_address(expr, ns, level);
+    rename_address<level>(expr, ns);
   }
   else
   {
     if(expr.id()==ID_index)
     {
       index_exprt &index_expr=to_index_expr(expr);
 
-      rename_address(index_expr.array(), ns, level);
+      rename_address<level>(index_expr.array(), ns);
       PRECONDITION(index_expr.array().type().id() == ID_array);
       expr.type() = to_array_type(index_expr.array().type()).subtype();
 
       // the index is not an address
-      rename(index_expr.index(), ns, level);
+      rename<level>(index_expr.index(), ns);
     }
     else if(expr.id()==ID_if)
     {
       // the condition is not an address
       if_exprt &if_expr=to_if_expr(expr);
-      rename(if_expr.cond(), ns, level);
-      rename_address(if_expr.true_case(), ns, level);
-      rename_address(if_expr.false_case(), ns, level);
+      rename<level>(if_expr.cond(), ns);
+      rename_address<level>(if_expr.true_case(), ns);
+      rename_address<level>(if_expr.false_case(), ns);
 
       if_expr.type()=if_expr.true_case().type();
     }
     else if(expr.id()==ID_member)
     {
       member_exprt &member_expr=to_member_expr(expr);
 
-      rename_address(member_expr.struct_op(), ns, level);
+      rename_address<level>(member_expr.struct_op(), ns);
 
       // type might not have been renamed in case of nesting of
       // structs and pointers/arrays
@@ -606,17 +597,17 @@ void goto_symex_statet::rename_address(
         expr.type()=comp.type();
       }
       else
-        rename(expr.type(), irep_idt(), ns, level);
+        rename<level>(expr.type(), irep_idt(), ns);
     }
     else
     {
       // this could go wrong, but we would have to re-typecheck ...
-      rename(expr.type(), irep_idt(), ns, level);
+      rename<level>(expr.type(), irep_idt(), ns);
 
       // do this recursively; we assume here
       // that all the operands are addresses
       Forall_operands(it, expr)
-        rename_address(*it, ns, level);
+        rename_address<level>(*it, ns);
     }
   }
 }
@@ -674,11 +665,11 @@ static bool requires_renaming(const typet &type, const namespacet &ns)
   return false;
 }
 
+template <goto_symex_statet::levelt level>
 void goto_symex_statet::rename(
   typet &type,
   const irep_idt &l1_identifier,
-  const namespacet &ns,
-  levelt level)
+  const namespacet &ns)
 {
   // check whether there are symbol expressions in the type; if not, there
   // is no need to expand the struct/union tags in the type
@@ -717,8 +708,8 @@ void goto_symex_statet::rename(
   if(type.id()==ID_array)
   {
     auto &array_type = to_array_type(type);
-    rename(array_type.subtype(), irep_idt(), ns, level);
-    rename(array_type.size(), ns, level);
+    rename<level>(array_type.subtype(), irep_idt(), ns);
+    rename<level>(array_type.size(), ns);
   }
   else if(type.id() == ID_struct || type.id() == ID_union)
   {
@@ -729,14 +720,14 @@ void goto_symex_statet::rename(
     {
       // be careful, or it might get cyclic
       if(component.type().id() == ID_array)
-        rename(to_array_type(component.type()).size(), ns, level);
+        rename<level>(to_array_type(component.type()).size(), ns);
       else if(component.type().id() != ID_pointer)
-        rename(component.type(), irep_idt(), ns, level);
+        rename<level>(component.type(), irep_idt(), ns);
     }
   }
   else if(type.id()==ID_pointer)
   {
-    rename(to_pointer_type(type).subtype(), irep_idt(), ns, level);
+    rename<level>(to_pointer_type(type).subtype(), irep_idt(), ns);
   }
 
   if(level==L2 &&

src/goto-symex/goto_symex_state.h

@@ -179,15 +179,13 @@ class goto_symex_statet final : public goto_statet
   ///
   /// A full explanation of SSA (which is why we do this renaming) is in
   /// the SSA section of background-concepts.md.
-  void rename(exprt &expr, const namespacet &ns, levelt level=L2);
+  template <levelt level = L2>
+  void rename(exprt &expr, const namespacet &ns);
 
   ssa_exprt rename_level0_ssa(ssa_exprt ssa, const namespacet &ns);
 
-  void rename(
-    typet &type,
-    const irep_idt &l1_identifier,
-    const namespacet &ns,
-    levelt level=L2);
+  template <levelt level = L2>
+  void rename(typet &type, const irep_idt &l1_identifier, const namespacet &ns);
 
   void assignment(
     ssa_exprt &lhs, // L0/L1
@@ -198,7 +196,8 @@ class goto_symex_statet final : public goto_statet
     bool allow_pointer_unsoundness=false);
 
 protected:
-  void rename_address(exprt &expr, const namespacet &ns, levelt level);
+  template <levelt>
+  void rename_address(exprt &expr, const namespacet &ns);
 
   /// Update level 0 values.
   void set_l0_indices(ssa_exprt &expr, const namespacet &ns);

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<goto_symex_statet::L1>(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)
     else
       rhs=exprt(ID_invalid);
 
-    state.rename(rhs, ns, goto_symex_statet::L1);
+    state.rename<goto_symex_statet::L1>(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<goto_symex_statet::L1>(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)
     else
       rhs=exprt(ID_invalid);
 
-    state.rename(rhs, ns, goto_symex_statet::L1);
+    state.rename<goto_symex_statet::L1>(rhs, ns);
     state.value_set.assign(ssa, rhs, ns, true, false);
   }
 

src/goto-symex/symex_dereference.cpp

@@ -357,11 +357,11 @@ void goto_symext::dereference(exprt &expr, statet &state)
   // 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<goto_symex_statet::L1>(expr, ns);
 
   // start the recursion!
   dereference_rec(expr, state);
   // dereferencing may introduce new symbol_exprt
   // (like __CPROVER_memory)
-  state.rename(expr, ns, goto_symex_statet::L1);
+  state.rename<goto_symex_statet::L1>(expr, ns);
 }

src/goto-symex/symex_dereference_state.cpp

@@ -51,7 +51,7 @@ symex_dereference_statet::get_or_create_failed_symbol(const exprt &expr)
       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<goto_symex_statet::L1>(sym_expr, ns);
       sym.name=to_ssa_expr(sym_expr).get_identifier();
       state.symbol_table.move(sym, sym_ptr);
       return sym_ptr;
@@ -71,7 +71,7 @@ symex_dereference_statet::get_or_create_failed_symbol(const exprt &expr)
       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<goto_symex_statet::L1>(sym_expr, ns);
       sym.name=to_ssa_expr(sym_expr).get_identifier();
       state.symbol_table.move(sym, sym_ptr);
       return sym_ptr;

src/goto-symex/symex_function_call.cpp

@@ -418,7 +418,7 @@ static void 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<goto_symex_statet::L1>(ssa, ns);
 
     irep_idt l1_name=ssa.get_identifier();
     unsigned offset=0;

src/goto-symex/symex_goto.cpp

@@ -249,7 +249,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<goto_symex_statet::L1>(new_lhs, 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);
-    state.rename(lhs, ns, goto_symex_statet::L1);
+    state.rename<goto_symex_statet::L1>(lhs, ns);
     const irep_idt l1_name=lhs.get_l1_object_identifier();
     // store it
     state.l1_history.insert(l1_name);